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

Аргумент р1 задает список свойств для данной теоремые); этот аргумент не вычисляется и должен иметь вид (1141А Р1 1121)з Уз. 11111,Л ), в~( где 1И0г — название (идентификатор), а Уг — значение (любое «) Этот список свойств не имеет никакого отношения к списку свойств идентификатора гв; зто разные списки свойств. $62 выражение) С-го свойства. Если аргумент р1 не задан, то с теоремой связьгвается пустой список свойогв. Аргумент»(е называется апределню»цим еырамением теоремы и должен иметь вид (суре [е» из,'.

е ) рас е» е» ... ее)» и» > О, й ъ 1. Список (и» ие ° .. и ) — это описание ленальных переменных теоремы, а последовательность простых форм е» вЂ” гела теоремы. Описание локальных переменных и тело теоремы — точно такие же, как и у функции РКОО (см. 1 1.9). Любая теорема вычисляется так н»е, как функцпя РВОО, но вывывается не по имени, а по образцу.

Элемент р໠— Это образец теоремы. Он обязательно должен быть 1 списком, не содержащим обращений к функциям и сопоставнтелим, а также никаких со»эюнтных образцов. Таким образом, элементами втого спнскового образца могут быть только атомы, простые обращения к переменным и константам и 1 списки с теми же ограничениями. Подобные образцы мы будем называть Т- образцами, Элемент суре определяет тип описываемой теоремы и может быть одним из следу»ощих атомов: СО1»ЯЕ»С (от слова сопзециепС), Ар)ТЕС (от апзесебепС) или ЕВАЯ1НО. При СОРСЯЕ() определяется целевая теорема, при АХТЕС вЂ” записывающая теорема, при ЕКАЯ11)Π— вычеркивающая теорема.

Рассмотрнм несколько примеров: [ПЕР)ХЕ ТН5 (СОНЯЕСС (Х) (А»11МАЬ»Х) [ЯЕАКСН (МОРСКЕУ .ХЦ) (В1РР1СПЬТУ ЕАЯ»'Ц Здесь определена целевая теорема с именем ТН5, которая имеет одну локальную переменную Х и образец (АН)МАЬ еХ). Тело этой теоремы состоит из одного оператора — обращения к функции ЯЕАВСН. С теоремой связывается свойство с названием 01РР1СПЬТ т' и значением ЕАЯТ'.

Содержательно эту теорему можно трактовать так: если надо доказать, что Х вЂ” животное, то для этого достаточно показаттн что Х вЂ” обезьяна. Свойство же теоремы может означать, что сделать это несложно. [ВЕР1НЕ ПОЕЗДКА (АЕТЕС (Х Т З) (»Х УЕХАЛ В «Т) [ЯЕАВСН1 (.Х НАХОДИТСЯ В еЗ)) [ЕКАЯЕ (.Х НАХОДИТСЯ В .2)) [АЯЯЕВТ (.Х НАХОДИТСЯ В УЦЦ 163 1се У этой ааписывающей теоремы с именем ПОЕЗДКА три локальных переменных Х, Ч и 3. Ее образец — («Х УЕХАЛ Б «Ч), а тело ее состоит из трех операторов. С теоремой связывается пустой список свойств.

Как уязе было сказано, ааписывающие теоремы вызываются в тех случаях, когда в базу данных записываются утверждения, соответствующие их обраацам. Теорема ПОЕЗДКА вызывается при занесении в базу данных ин4юрмации о том, что некий Х уехал в некоторое место Ч. Теорема требует, чтобы попутно иэ базы данных было вычеркнуто утверждение о прежнем местонахождении этого Х и было записано утверждение о том, что Х находится теперь в Ч.

[ОЕР1НЕ БАНКРОТ (ЕВАЗ1НО (Х) (БОГАТ «Х) [АЗЗЕВТ (БЕДЕН .Х)])] Данная вычеркивающая теорема предназначена для вывоза в тех случаях, когда иа базы данных вычеркивается утверждение о том, что некто Х богат. Теорема требует, чтобы одновременно с этим в баау данных было записано утверждение о том, что этот Х беден. 5.3. Вызов теорем Теоремы вызываются при вычислении встроенных функций АСН1ЕЧЕ, РВАЧ«' и СНАНСЕ. Обращения к этим функциям и их действия аналогичны, но каждая иа них вызывает теоремы только асвоегоз типа: функция АСН1ЕЧЕ вызывает целевые теоремы, функция ПВА% — ааписывающие теоремы, а функция СНАКСЕ— вычеркивающие теоремы.

Поэтому механизм вызова теорем мы рассмотрим на примере функции АСН1ЕЧЕ. Фушщия АСН1ЕЧЕ: [АСН!ЕЧЕ раз гес7], РЗПБВ. Эта функция вызывает целевые теоремы по обраацу раз согласно рекомендации тес. Аргумент раз должен быть Т-образцом или .-переменной, значением которой является Т-обрааец. Рекомендация же гес должна быть одной иа следующих (й~ О): (ПЗЕ г~ гг ... г«) (ПЗЕ1 г~ гг ...

г«) (ТВ1...,... „) (Р1ЬТЕВ 1) Элементы рекомендации — 'г, — должны быть простыми образцамн, а 1 — простой формой. Отсутствие рекомендации эквивалентно заданию рекомендации (БЗЕ); рекомендации (БЗЕ), (ПЗЕ1) и (ТВЧ) рассматриваются как сокрашения от (ЮЗЕ []),(ПЗЕ1 []) и (ТВЧ []) соответственно. 1б4 Для краткости рекомендацвю, начипающутося с БЯЕ, будем называть УЯЕ-рекомендацией, рекомендацию, начинающуюся с НЯЕ1, — УЯЕ1-рекомендацией и т. п.

Если прн обращении к функции АСН1ЕУЕ указана РПТЕВ- рекомендация, то функция начинает свою работу с того, что вычисляет форму 1 из этой рекомендации. Значением данкой формы должна быть рекомендация, начинающаяся с СЯЕ, ВЯЕ1 плк ТКУ, либо пустой список (). Последний вариант означает, что теоремы ке должны вызываться, поэтому фуакцня сразу заканчивает свою работу со значением (). Другие значения этой формы определяют рекомендацаи, согласно которым н будут выэыватьоя теоремы. Р1ЬТЕВ-рекомендация предоставляет возможность строить рекомендации в процессе выполнения программы, если они пе были известны заранее, при каписаннн программы.

Просмотр теорем. После вычисления Р1ЬТЕВ-рекомендации, а если ее нет, то сразу, функция АСН1ЕУЕ ставит Р-точку к затем соотавляет таис называемый сансов вовк«ясностей, в который (в порядке, определяемом реалнзацией языка) заносят имена всех целевых теорем, являющкхся кандидатами па вызов по образцу э«к Теорема являетсн кандидатом, если ее образец соответствует вызывающему образцу в предположении, что любым переменным яз обоих этих образцов воегда есть соответствие и что подспискам с верхнего уровня образцов соответствуют любые подсписки той же длины; прк таком частичном сопоставлении никакие присваивания переменным пе осуществляются.

В атом смысле образец (АТ .Х (»У 1)) соответствует образцу (АТ ВОХ «2) или образцу (.Р «Ъ7 (2 4)), но не соответствует образцам (ОХ ВОХ «2) и (АТ «% ВЦ. Список воэможностей определяет, какие теоремы в принципе могут быть вызваны по образцу рал Но яот какие из кнх действительно будут вызываться и в каком порядке, определяет рекомендация тес. Для этого элементы рекомендации (образцы г,) просматриваются последовательно слева направо, п для каждого кз них выполняются следующие действия.

Образец г» по очереди сопоставляется с именами иэ списка возможностей. Подчеркнем, что сопоставление производится именно с идентификаторами-именами. Единственное, нсключепне— встроенный соноставнтель ТЕЯТ: (ТЕЯТ Гвй~ рей ... 1пйэ р«Ц, РЯСВВ, й ~~ 1, который действует аналогично сопоставителю НАЯ (см.

1 2.8), но проверяет не список свойств идентификатора-имени, а список свойств теоремы с втнм именем. 185 Если нашлось нмя, соответствующее образцу ге то оло удаляется из списка возможностей, а теорема с этим именем вызывается. Если она ие подошла (при полном сопоставлении ее образец не соответствует вызывающему образцу или оказалось неуспешным вычисление ее тела), тогда побочные эффекты сопоставления ее имени с образцом гг уничтожаются, теорема отвергается и в списке воэможностей отыскивается другое имп, соответствующее образцу г;.

Когда зтат список будет просмотрен полностью, элемент гг удаляется из рекомендации тес и теперь все описанные действия повторяются по отношению к следующему элементу рекомендации. Если в рекомендации больше нет элементов, вызов теорем прекращается. Поскольку имя вызванной теоремы удаляется из списка возможностей, повторно зта теорема уже не будет вызываться, Одна. ко зто не всегда удобно, поэтому из описанного выше правила сделано исключение: если г~ — идентификатор, т. е. ои явно указывает имя теоремы, которую рекомендуется вызвать, то зта теорема (при условии, коночпо, что она целевая) вызываетса в любом случае, есть ее имя в списке возможностей или нет. Проиллюстрируем правило просмотра теорем на примере: (УЯЕ ТН6 (ЕТ (МОК ТН1) (ТЕЯТ С1АЯЯ А) «Х1 ТН9).

Пусть исходный список возможностей имеет вид (ТН1 ТН2 ТН5 ТН6 ТН9). Выбирается первый элемент рекомендации — ТН6. Этот атом удаляется из списка возможностей, и вызывается теорема с именем ТН6. Предположим, что она не подошла. Тогда рассматривается следующий элемент рекомендации — обращение к сопоставителю ЕТ.

Он по очереди сопоставляется с оставшимися идентификаторами из списка ваемо>кностой. Ему соответствует имя любой, кроме ТН1, теоремы, у которой свойство с названием С1АЯЯ имеет значение А; кроме того, при сопоставлении имя теоремы присваивается переменной Х, чем можно будет воспольвоваться в дальнейшем.

Пусть первым из таких имен был идентификатор ТН2. Тогда этот идентификатор удаляется из списка возможностей, и затем вызывается теорема ТН2. Если она не подошла, то определяется другое имя, соответствующее сопоставителю ЕТ. Если это, например, ТН9, то вызывается теорема с этим именем, а само имн удаляется из списка возможностей, который теперь принимает вид (ТН1 ТН5). Предположим, что и теорема ТН9 не подошла. Поскольку для данного элемента рекомендации список возможностей просмотрен полностью, далее рассматрнвается последний элемент рекомендации — ТН9.

Это — явно указанное нмя теоремы, поэтому, хотя такого ямекн уже нет в списке возможностей, теорема ТН9 все равно вызывается. Если она вновь не подошла, вызов теорем ааввршается. Теоремы же ТН1 и ТН5 так и не будут вызваны. Отметим важный случай вывоза теорем. Если при обращении к функции АСН1ЕЧЕ ке была указана рекомендация или если была дана рекомендация без элементов, типа (УЯЕ), то вызываться будут- все теоремы-кандидаты в том порядке, в котором расположены их имена'в списке возможностей, т.

е. в порядке, определяемом транслятором языка. Вызов теоремы. Рассмотрим теперь, как осуществляется вывоз выбранной теоремы. Презкде всего вводятся локальные переменные этой теоремы. Некоторые из ннх, согласно описанию, получают начальные значенля, а другие остаются беа значения. Далее осуществляется сопоставление вызьзвающего образца с образцом теоремы.

Детали этого сопоставления будут рассмотрены в 4 5.4, а пока лишь отметим, что в вызывающем образце используются переменные, существовавшие до появления локальных переменных теоремы, а в образце теоремы используются ее локальные переменные (допусиает, ся также и применение внешних по отношению к теореме переменных). Если данное сопоставление неудачно, то на этом вызов теоремы завершается — теорема не подошла; ее локальные кеременные уничтожаются. Но если сопоставление удачно, тогда вычисляется тело теоремы.

Зто вычисление начянаетсй при тен значениях и ограничениях на значения .(см. $ 5.4) переменных, которые они получили при сопоставлении. В данном случаа успех/неуспех вызова теоремы зависит от того, успешно или нет вычисление ее тела. Если оно неуспешно, то при распространении неуспеха будут отменены побочные эффекты как операторов тела теоремы, так и сопоставления ее обрааца с вызывающим образцом. При любом исходе по окончании вычисления тела теоремы ее локальные переменные уничтожаются. Рассмотрим следующий пример. Пусть при вычислении [РКОО ((У 5) Е) [АСН1ЕЧЕ (БЛИЗКО Ч 4.95 еЕ)Ц для вызова выбрана теорема с таким определяющим выражением: (СОМЯЕО (Х У (ЕРЯ 0.1)) (БЛИЗКО»Х еУ .ЕРЯ) [УКРАЬЯЕ [БТ [АВЯ [ — .Х .У)] .ЕРЯ))) При вызове этой теоремы прежде всего будут введены ее локальные переменные: Х и У без значений, а ЕРЯ вЂ” со значением ОД, (Отметим, что переменная х из теоремы не имеет никакого от- ношения к переменной Ч из функции РВО6.) Затем выполняется сопоставление образцов, причем переменные У и Е вызывающего образца берутся из функции РВ()6, а под переменными Х, У и ЕРБ образца теоремы понимаются ее локальные переменные.