В.Н. Пильщиков - Язык Плэнер, страница 38

Функция САХ010АТЕЯ уже рассматривалась (см. 1 4.4): она применяется для поиска утворждений-кандидатов. Эту же функцию можно использовать и для нахождения теорем-кандидатов. В таком случае цри обращенин к ней: (САХ010АТЕЯ раз зуде], РЯПВН в качестве аргумента уаг должен быль задал Т-образец илп;переменная, значением которой является Т-образец, а значением второго аргумента обязан быть один из следующих атомов: СОХЯЕ1), АХТЕС или ЕВАЯ1ХС.

Зтот атом указывает, теоремы какого типа (целевые, записывающие или вычеркивающие) следует просматривать данной функции. Как уже было сказано в 1 5.3, теорема является кандидатом на вызов по образцу рад если ее обрааец соответствует образцу рог в предположении, что переменным обоих образцов соовветотвуют любые элементы з другом образце и что списковым элементам (с верхнего уровня) соответствуют любые списки той же длины. Значением функции САХ010АТЕЯ является 1 список, составленный иа имен теорем-кандидатов требуемого типа и списков свойств этих теорем. Значение функции может быть, например, таким: (ТН2 (С1 ЛЯЯ 5) ТН7 ( ) ТН1 (01РР1С()ЬТУ ЕАЯУСЬЛЯЯ 2)) С помощью следующей встроенной функции можно вызывать теоремы по имени: (ЛРРЬУ рог гд-лате], РЯСВВ Первый аргумент этой функции должен быть Т-образцом или .-переменной, значением которой является Т-образец, а значением второго аргумента обязан быть идентификатор — имя одной из теорем.

Функция осуществляет вызов атой теоремы по обраацу рах Если вызов теоремы неуапешен илн если указанной теоремы вообще нет, тогда вычисление функции АРРА неуспешно (она не ставит Р-точку). Если же образец теоремы соответствует образцу рос и ее тело успешно, то вычисление функции успешно и ее значением объявляется значение, выработанное теоремой. Функции САХ010ЛТЕЯ и АРРЬТ предоставляют пользователзо возможность по-своему организовать вызов теорем, если его не удовлетворяет тот, что встроен в язык. Редактирование рекомендаций.

Рекомендации, которые польаователь дает функциям, вызывающим теоремы по образцу, могут 180 быть определены как заранее (при написании пРогРаммы), так и непосредственно перед вызовом теорем (с помощью РНТЕВ-реноме»«дац«п«). Но после того кик рекомендации определены, юнн не меняются. В то же время в некоторых случаях возникает потребность в изменении рекомендаций, после тх»го иак вызов теорем уже начался. Например, может потребоваться изменить тип рекомендации (скажек, с ОЯЕ на УЯЕ1) или порядок просмотра теорем, запретить вызов ранее рекомендованной теоремы или, наоборот, рекомендовать новую теорему. Так, теорема, описывающая действие «поднять предмет правой рукой» и не сумевшая достичь поставленной цели, может исключать из числа рекомендованных теорему, описывающую действие «поднять предмет левой ру«сей».

Для редактирования уже действующих рекомендаций в язык встроены следугощие функции: ОЕТРОББ, которая позволяет узнать, какие теоремы еще не вызывалис»«но могут быть вызваны; СЕТВЕС, с помощью которой можно определить, канне злементы рекомендации предстоит еще рассмотреть; РСТВЕС, которая дает возможность заменить прежнюю рекомендацию на новую. Все зги функции работают с рекомендацией ближайшей объемлющей функции, вызывающей теоремы по образцу. Функция 6ЕТРОЯБ: [ОЕТРОЯБ). Данная фукция находит ближайшую объемлющую функцию, которая осуществляет вызов теорем, и в качестве своего значения выдает ее текущий'список возможностей, т.

е. список имен теорем-нандидатов, которые иока еще ие вызывались (в етом списке нет имени теоремы, вычисляющейси в даялый момент). Если такой ближайшей функцией является функция АРРЬ«', то выдается пустой список (). Если среди объемлющих функций нет ии одной, что вызывает теоремы, то вырабатывается неуспех с сообщением СЕТРОЯЯ. Функция 6ЕП1ЕС: [СЕТВЕС) . Эта функция также находит ближайшую объемлющую функцию, вызывающую теоремы, и выдает в качестве своего значения ее текущую рекомендацию (в ней иет тех злементов исходной рекомендации, которые уже были рассмотрены, но есть элемент, рассматриваемый в настоящий момент).

Если такой ближажпей функцией является функция АРР1'«', то ОЕТВЕС в качестве своего значения выдает идентификатор — имя выаванной теоремы. Если среди объемлющих функций нет таких, которые вызывают теоремы, то вырабатывается неуспех с сообщением ОЕТВЕС. Функция РУТВЕС: [РУТКЕС «1, БОЕВ. 181 Яначением 1, аргумента этой функции должен быть список, представляющий собой рекомендацию, начинающуюся с СЯЕ, СЯЕ1 ели ТК'г'. Функция Р()ТВЕС находит ближайшую объемлющую функцию, вызывающую теоремьь и заменяет ее текущую рекомендацию пе новую — на 1.. Как только закончится вычисление теоремы, в которой произошло обращение к РОТКЕС, так оразу ;ке вступит в силу эта навал рекомендация.

Обратный опеРатор функции Р()ТВЕС не запоминает. Ее значение — список 1, Если блржайшей функцией, вызывающей теоремы, является функция АРРЬг' или если среди объемлющих функций нет таких, которые вызывают теоремы; тогда функция РНТВЕС вырабатывает неуспех, связывая с пим сообщение РОТВЕС. Операции пад списками свойств теорем. В заключение рассмотрим встрооппьге функции, с.помощью которых можно анализировать и изменять списки свойств теорем. Функция ОЕТН: [СЕТН гй-пате 1па?), ЯНВВ. Эта функция действует аналогично функции ОЕТ (см.

$1.17), по по отношению к списку свойств теоремы, имя которой вадается аргументом зй-пате, Таким образом, функция СЕТН выдает в качестве своего значения весЬ список свойств этой теоремы, если аргумент 1пл не задан, либо значение только одного свойства — того, название которого определяет аргумент 1пА Если нужной теоремы пет, вырабатывается неуспех с сообщением СЕТН. Функция РЮТН: [Р()ТН зй-пате 1пд и), Я()ВК. Данная функция, аналогичная функции РОТ (см.

$ 1Л7), заменяет в списке свойств теоремы, имя которой указано аргументом 1й-пате, прежнее значение свойства с названием ай на новое значение У. Одновременно запоминается обратный оператор, назначение которого — восстановить при неуспехе прежнее значение этого свойства. Если указанной теоремы иет, вырабатываетсй неуспех с сообщением Р()ТН. Функция РРЮТН: [РР()ТН зй-пате 1пб с], ЯСВВ. Эта функции действует аналогично функции РСТН, но обратный оператор не запоминает.

5.6. Примеры использования целевых теорем Пленер, как и любой другой язык программирования, предназначен для записи разработанных человеком алгоритмов решения задач. В то же время ла пленере можно программировать 182 путем описания того, что имеется и что надо получить, беа явного указания того, как это можно получить. Ответствеяность за поиск решения описанной задачи возлагается при этом на дедуктивный моханизм яаыка. В предыдущих параграфах уже встречались отдельные примеры работы этого мехэниама и использования целевых теорем при описании задач.

В данном параграфе эти же.аспекты будут рассмотрены более детально. Как уже было сказано, основное назначение целевых теорем'— описывать элементарные средства достижения целей, из которых (средств) и должно быть составлено решение задачи. Образец каждой такай теоремы обычно описывает ту цель, которой можно достичь с помощью теоремы, а ее тело — действия, которые следует предпринять, для того чтобы можно было считать агу цель достигнутои. Действия могут быть самыми разиообразнычп, но обычно они следующие: либо показывается, что цель является следствием из фактов, описанных в текущей базе данных, либо осуществляется (допустимым образом) такое изменение базы данных, чтобы в новой базе данных цель оказалась достигнутой.

В первом случае теоремы отвечают на вопросы типа «верно лэ, что данный предмет находится в данном месте», а во втором случае теоремы удовлетворяют требования типа «сделать так, чтобы данный предмет оказался в данном месте». Первые теоремы примеияютсн для описания логических аакономерностей (правил вывода, свойств используемых понятий, связей между ними н т.

п.) той задачи, решение которой должна найти плэнерская программа, а вторые теоремы используются для описания операций и правил преобразования (например, элементарных действий робота), которые разрешено применять в этой аадаче. Рассмотрим примеры определения и испольаования целевых теорем обоих указанных типов. Логические правила обычно записываются в виде «если А, то Вм Это можно интерпретировать следующим образом: если надо показать истинность В, то следует .показать истинность А. Подобная императивная трактовка правил и лежит в основе описания пх в виде плэнерских теорем: сзедствне В выносится в образец теоремы, а предпосылка (или предпосылки) А оформляются как тело теоремы. Например, свойство транзитивпости отношения «меиыпе» з логической нотации ааписывается так: 1«««(х, у) Д 1е««(у, з) ~ (е««(л, з). Нужная для нас интерпретация: если надо доказать, что л меньше з, то для этого следует найти камой.

нибудь у, о котором известно, что х меньше его, и затем следует доказать, что у меньше г. 183 Этой интерпретации соответствует следующая целевая теорема: [РЕР(НЕ ТВАНЯ (СО(»)ЯЕ(] (Х У Е) (ЬЕБЯ «Х «Е) [БЕАВСН (1ЕЯБ .Х «УЦ [60АЬ (1 ЕЯЯ .»' .ЕЦЦ Эту теорему можно использовать для доказательства фактов об оглашении «меньше», которые янно не указаны в базе данных, ио которые логически следуют иэ записанных там фактов. Пусть к примеру, база данных была заполнена в результате вычисления [РАТА (ЬЕЯЯ А В) (ЬЕЯЯ А 20) (1ЕБЯ В С) (ЬЕЯБ С 53Ц Если мы хотим проверить, «верно ли, что А меньше 53>, тогда достаточно вычислить выражение [60А1 (1ЕЯЯ А 53)] Ответ на поставленный вопрос будет найден автоматически («да», если вычисление этого выражения успешно, и «нет», если оно неуспешно).

В нашем случае поиск ответа осуществляется следующим образом (напомним, что .функция 60АЬ вЂ” это комбинация функций ЯЕАВСН и АСН1ЕЧЕ): [60АЬ (ЬЕЯБ А 53Ц [БЕАВСН (1ЕЯЯ А 53Ц вЂ” неуспех [АСН1ЕЧЕ (ЬЕЯЯ А 53Ц теорема ТВА)»)Б: Х: = А, Ул = 53 [ЯЕАВСН (1ЕЯБ А «УЦ вЂ” успех, У: = В [60АЬ (ЬЕЯБ В 53)! [ЯЕАВСН (ЬЕБЯ В 53Ц вЂ” неуспех [АСН!ЕЧЕ (ЬЕЯЯ В 53)] теорема ТВОЯ: Х:= В, Х:= 53' [ЯЕАВСН (ЬЕЯЯ В «УЦ вЂ” успех, »'= С [60А1 (1ЕЯБ С 53Ц [ЯЕАВСН (ЬЕЯБ С 53)] — успех выход из ТВАМБ выход иэ ТВЛНЯ успех Здесь для доказательства «А меныпе 53» было найдено В, которое больше А, а затем была поставлена цель дока»ать, что В меньше 53.

Для этого же было найдено С, которое больше В, а затем была поставлена цель доказать, что»С меньше 53». Последнее высказывание доказывается непосредственно — нахож дением соответствующего утверждения в базе данных. Таким обрааом, была найдена цепочка А ( В ( С ( 53, которая н доказывает исходное высказывание. Теорему ТВАКЯ можно использовать также и для поиска объектов, связанных отношением «меньше», причем таких объектов, о которых в базе данных не оказано явно, что один меньше другого.