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

Например, пр»«,вычнслешги [АСН1ЕЧЕ (ЬЕЯБ»Р 53)] зта теорема может присвоить переменной Р значение В, т. е. на запрос «найти объект, меньший 53» она даст ответ В: [АСН1ЕЧЕ (ЬЕЯЯ «Р 53)] теорема ТВАХЯ: Х связывается с Р, Х: = 53 («) [ЯЕАВСН (ЬЕББ .Х «7)] — успех, Х:= С (Р:= С), У:= 53 [СОА1 (ЬЕББ 53 53Ц [БЕАВСН (1,ЕББ 53 53)] — неуспех [АСН1ЕЧЕ (1,ЕЯЯ 53 53Ц теорема ТВА(«)Б: Х: = 53, 22 = 53 [ЯЕАВСН (ЬЕЯЯ 53 «УЦ вЂ” неуспех возврат по иеусиеху к («) [ЯЕАВСН (ЬЕЯЯ .Х «7Ц вЂ” успех, Х;=В (Р;=В), У:=С [ООАЬ (1ЕББ С 53Ц [БЕАВСН (1ЕЯЯ С 53Ц вЂ” успех выход из ТВАМБ успех (Здесь ме»кду пунктирными линиями показана неуспешная ветвь вычисления.) Теорема ТВА)«)Я вЂ” пример описания «чисто» логического высказывания.

Но в плзнерских теоремах можно применять и велогические действия и проверки, можно использовать не только приказы типа «найти что-то» или «доказать что=то», но и любые другие процедуры языка. Например, для доказательства «х меньше з» можно воспользоваться и арифметическими функциями, если з и « — числа: [ОЕР!5)Е ЬЕЯБ (СОг)ЯЕ(] (Х Е) (ЬЕЯЯ «Х «2) [ОНРАЬБЕ [АМВ [)ЧОМ .Х] [)«)ОМ .Е] [1 Т .Х .Е]]]Ц Каждан из теорем ТВАНЯ и ЬЕБЯ предлагает свой способ достижения одной и той же цели и применима при свонх условиях. Так, 'теорема ЬЕЯБ не сможет доказать (20 меньше С», но легко докааывает «20 меньша 53», тогда как теорема ТКАНАЯ не сумеет доказать последнее высказывание при имеющейся базе данных.

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

Именно эта трактом«а и лен«ит в основе представления операций в виде плзнерских теорем: результат В выносится в обрааец теоремы, а приказы «удовлетворить предпосылки А» и «зыполнить действие О» оформляются как тело теоремы. Но что здесь понимается под словами «выполнить действие»2 Дейсввие — ато неиоторое изменение реальной обстановки. Поскольку в плэнерских программах обстановка описывается в виде базы данных, то изменение обстановки имитируется изменением бааы данных.

Тем' самым под «вьиюлненнеы действия» подразумевается соответствующее иаменение базы данных, а именно: вычеркивание утверждений, описывающих факты, которые после выполнения действия стали ложными, и запись новых утверждений, которые описывают факты, ставшие истинными. Рассмотрим, например, действия робота «перенести некого.

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

результат: в этой же точке окажется и робот). Данное действие имеет две предпосылки. Первую из них— ТН. должен быть пшиком — проверяет функция БЕАКСН, с обра щения к которой начинается тело теоремы. Вторая предпосылка— робот должен окаааться в той же. точке, что и ящик (только тогда робот может начать перенос). Теорема определяет, в какой точке Х сейчас находится лщик, и ставит цель сделать так, чтобы стало истинным утвср»кдение о том, что робот находится в точке Х «). Достичь этой цели можно с помощью какой-либо теоремы, описывающей передвижение робота.

Какая именно из них будет испольаована, мы не знаем, да это и не надо нам знать. Однако нам известно заранее, что достаточно найти лишь один способ подхода работа к ящику и что в случае последующего неуспеха функция СОА1 не должна возобновлять свою работу. Именно это мы и указали с помощью СБЕ1-рекс»«ендации.

Если удалось удовлетворить обе предпось»лки, то далее теорема «выполняст» само действие переноса ящика: оиа вычеркивает Ф из базы данных утверждении о том, что ящик и робот находятся в точке Х, и записывает утверждения о том, что они теперь расположены в точке У. В конце теоремы ааписано обращение к функции РСАМН1Р)С, которая будет 'рассмотрена чуть позже.

Пока же можно считать, что она действует как пустой оператор. *) Отметим, что в теоремах рассматриваемого типа следует не столько проверять, выполнены лк предпосылки, сколько требов«ть, чтобы онн стали выполненными, Если, например, в теореме НЕСТИ заменить обращение к функции 6ОАЕ на обращение к функции БЕАКСН, т. е.

на проверку, находится ли робот в точке Х, н если ока»кется, что робота нет в этой точке, то теорема никогда нс сможет достичь своей цели. 1Я7 Действие «перемещение робота иа точки Х в точку Уз аписывается следующей теоремой: [ПЕР)МЕ ИДТИ (СОХБЕО (Х У) (АТК «У) [60АЬ (АТК «Х) (СБЕ1 [ЫОВ ИДТИ]Ц [ЕКАБЕ (АТК .ХЦ [АББЕКТ (АТК .У)] [РЬАММ1Х6 (ИДТИ ИЗ .Х В УЦЦ Образец теоремы указывает, что в результате выполнения теоремы робот окажется в точке У.

Предпосылкой описываемого действия является то, что робот находится в какой-либо точке Х на иолу. Если он не на полу (а, например, на ящике), тогда функция СОИ требует сделать так, чтобы он оказался на полу; при атом может быть применена любая подходящая теорема, но не сама теорема ИДТИ. Собственно же действие перехода имитируется вычеркиванием утверждения о том, что робот в Х, и записью утверждения о том, что робот в У.

Рассмотрим, как будут использоваться обе зти теоремы в задаче, в которой требуется поместить ящики ВОХ1 и ВОХ2 в какую-нибудь одну точку, если в исходной ситуации робот находился на полу в точке Р, ящик ВОХ1 — в точке (), а ящик ВОХ2 — в точке В. База данных, описывающая исходную ситуацию, задается так: [ПАТА (АТК Р) (ВОХ ВОХ1) (АТ ВОХ1 О) (ВОХ ВОХ2) (АТ В(]~2 КЦ а цель задачи задается выражением [РК06 (Н) [60А1 (АТ ВОХ1 '«Н)] [СОИ (АТ ВОХ2 .НЦ] Вычисление этого выражения осуществляется следующим образом: [60А1 (АТ ВОХ1 «НЦ [БЕАКСН (АТ ВОХ1 «НЦ вЂ” успех, Н: успех [60А1 (АТ ВОХ2 ()Ц [БЕАКСН (АТ ВОХ2 О)] — неуспех [АСН1ЕУЕ (АТ ВОХ2 ОЦ теорема НЕСТИ: = ТН: = ВОХ2, У: = О [БЕАКСН (ВОХ ВОХ2)] — успех [БЕАКСН1 (АТ ВОХ2»ХЦ вЂ” успех, Х: =К [60А1 (АТК КЦ [БЕАКСН (АТК К)] — неуспех [АСН1ЕУЕ (АТК К)] теорема ИДТИ: У: = К 188 [ООА1 (АТК еХ)] [БЕАКСН (АТК»Х)] — успех, Х: = Р [ЕВАБЕ (АТК РЦ [Аяяевт (Атв к)] [' 'р"" выход иа ИДТИ [ЕВАЯЕ (АТ ВОХ2 В)] [ЕВАБЕ (АТК К)] [АБЯЕВТ (Ат ВОХ2 О)] аперенести ВОХ2 из К в Оз [Аяяевт (Атк а)] выход из НЕСТИ успех Таким образом, была выбрана точка О, где уже находился лщик ВОХ1, после чего робот подошел к ящику ВОХ2 и перенес его в точку О.