В.Н. Пильщиков - Язык Плэнер (1156455), страница 33
Текст из файла (страница 33)
Если среди попользуемых операций есть такие, применение которых приводит к одному и тому же результату, то они описываются теоремами' с одииаковыми образцами. Эти теоремы предлагают разные способы достижения одной и той же цели. Нри таком использовании теорем цель решаемой задачи может быть описана в виде выаывающего образца, и тогда решение задачи будет найдоно автоматически.
В самом деле, при вызове теорем по этому обравцу-цели транслятор языка подыскивает теорему, которая своим образцом «обещаетз получить нужный результат. Тело такой теоремы описывает алгоритм достижения цели, поэтому, выполняя его, транслятор и находит решение аадачи. Может, правда, оказаться, что в текущей обстановке предложенный теоремой путь достижения цели не приводит к успеху, тогда транслятор отказывается от этой теоремы н отыскивает другую подходящую теорему. Так, опираясь иа имеющиеся теоремы и сочетая вызов по обраацу с режимом возвратов, транслятор языка и осуществляет поиск решения задачи, описанной пользователем. Не следует, однако, думать, что поиск решения аадачи заключается лишь в выборе одной подходящей теоремы. Как правило, теоремы з свою очередь ставят цели, поэтому прн достп- 158 женин одной цели обычно возникает целая иерархия подцелей, для достижения каждой из которых транслятор подыскивает свою подходящую теорему.
Такой механизм достижения цели путем сведения ее к подцелям принято называть дедуктивным лез«ни«мол. Пронллюстрируем скааанное на простом примере. Предположим, что на столе построена башня из кубиков. Если факт «х находится на у» представляется утверждением (06( х у), то ситуация,.изображенная на рмс.
б, описывается базой данных из трех утверждений (ОН А В), (Ог1 В С) и (ОМ С ТАВЬЕ). Предположим также, что понятие «выше» определяется через понятие «находнться ле» . следующим образом: оа (х, з) ш а Ьаа«(х, з) Рнс. И. оа(х, у) /~аЬозе(у, з) =» адоае(х, з) Первое из этих предложений может быть описано в виде плэнерской теоремы (назовем ее ТН1) с образцом: (АВОЧЕ «Х «Е) и телом из одного оператора: [ЗЕАКСН (ОН,Х .2)) Образец втой теоремы указывает, что с ее помощью можно по.
казать, что некоторый кубик Х расположен вылив некоторого кубика 2, а ее тело говорит, что для этого достаточно найти в базе данных утверждение о том, что Х находится на Е. Второе предложение можно описать в виде теоремы (обозна'чим ее ТН2), которая имеет аналогичный обравец: (АВОЧЕ «Х «Е) но другое тело: [ЗЕАКСН (ОМ .Х «УЦ [АСН1ЕЧЕ (АВОЧЕ Ч .ЕЦ Это тело предлагает иной способ доказательства того, что Х вы. ше Ул сначала надо найти тот кубик У, на котором находится Х, а затем надо доказать; что Ч выше Е.
АСН1ЕЧŠ— это встроенная функция пленера, которая осуществляет вывоз теорем по образцу, являющемуся ее аргументом. Таким образом, для доказательства аого, что х выше. Е, предлагается вызвать любую теорему, которая своим образцом «обещает» это сделать (такой теоремой может быть и сама теорема ТН2). Фбй Теперь предположим, что мы хотим доказать, что кубик А расположен выше кубика С. Такая цель задается выражением (АСН1ЕУЕ (АВОУЕ А С)) На этом описание нашей задачи заканчивается.
Решение же ее будет найдено автоматически в результате вычисления укааанного обращения к функции АСН!ЕЧЕ, которое осуществляется следующим образом. Функция АСН1ЕУЕ вызывает любую иэ теорем, образцы которых соответствуют образцу (АВОЧЕ А С). Таких теорем две: ТН1 и ТН2. Предположим, что первой вызвана теорема ТН1. При сопоставлении ее образца с вьюывающям обраацом переменная Х получает значение А, а переменная 2 — значение С. Далее вычисляется тело теоремы, т. е. обращение к функции ЯЕАВСН, »юторая пытаотся найти в базе данных утверждение (ОМ А С). Такого утверждения там вет, поэтому вычисление атой функции н, следовательно, тела теоремы неуспыпно. Это означает, что хотя теорема ТН1 и аобещала» доказать, что А выше С, но сделать ато она не смогла.
Поэтому функция АСН1ЕУЕ отказывается от теоремы ТН1 я теперь вызывает теорему ТН2. Здесь также при сопоставлении обраацов переменная Х получает значение А, а переменная 2 — значение С. Далее вычисляется тело теоремы ТН2. Сначала функция ЯЕАНСН находит в'базе данных утверждение (01» А В), соответствующее ее обраацу (ОЯ .Х «Ч), и при этом переменной Ч присваивается аначение В. Затем функция АСН1ЕЧЕ ставит цель: доказать, что В выше С. Для этого вывывается теорема, образец которой соответствует образцу (АВОУЕ В С). Предположим, что вызвана теорема ТН1.
Тогда ее переменные Х и 2 получают соответсззеняо значения В и С. На зтст раз вычисление тела теоремы ТН1 успению, так кзк в базе данных естЬ утверждение (ОМ В 'С). Поэтому усполша и функция АСН1ЕЧЕ, выававшая ее. Поскольку обращение к функции АСН1ЕУŠ— последний оператор в теле теоремы ТН2, то на этом успешно завершается вычисление теоремы ТН2 н вычисление исходного выражения (АСН1ЕУЕ (АВОУЕ А С)). То, что вычисление атого выражения закончилось успехом, и означает, что поставленная цель — доказать, что А выше ф— достигнута. Если бы вычисление этого выражения было неуспешным, то зто значило бы, что высказывание «А выше С» ложно или, если говорить болев осторожно, недокаауемо при имеющихся фактах (баае данных) и имеющихся правилах вывода (теоремах ТН1 и ТН2).
Рассмотренный пример показывает, что программировать на планере можно ие только описывая алгоритм решения задачи, но и описывая лишь постановку 'задачи, В последнем случае . ответственность за поиск ее решения возлагается на транслятор азыка. И если эта задача может быть решена, то транслятор в конце концов найдет решение.
В атом смысле пленер можно рассматривать не только как язык программирования, но и как систему искусственного интеллекта. Однако не следует увлекаться автоматическим поиском решения вадач, поскольку он осуществляется методом полного перебора ' и потому поиск решения сложных задач занимает очень много времени. Более рааумиым является способ программирования, при котором пользователь управляет работой дедуктивного механизма.
Пользователь обычно знает, какие теоремы являются наиболее подходящими для достижения определенных целей, а какие теоремы, напротив, в данных конкретных условиях не подойдут. Для того чтобы он мог передавать такие внания дедуктивному мехапизму, язык предоставляет пользователю возможность давать рввемвпдации относительно того, какие теоремы следует вызывать, а какие иет, в каком порядке следует их выаывать. Например, при следующем вызове теорем по образцу (АСН(ЕУЕ (БОВБЕТ А В) (ОБЕ ТН5 (МОЯ ТН7))] указала рекомендация (список, начинающийся с ОБЕ), которая требует, чтобы в первую очередь была вызвана теорема ТН5, а если она не подойдет, тогда могут быть вывваны любые.
другие теоремы, образцы которых соответотвуют выэывазощему образцу (БСВБЕТ А В), по только ие теорема.ТН7. Иногда рекомендации, которые пользователь может дать дедуктивному механизму, зависят от того, какая конкретная обстаповка складывается при достииеении цели, поэтому в планере предусмотрена возможность определения рекомендаций в процеосе ~вычисления программы, разрешено и изменение ранее данных реномендаций. В языне также предусмотрены способы борьбы с зацикливаниями при достижении целей. С помощью всех этих средств пользователь может направлять работу'дедуктивного механизма в нужное русло, повышать его эффективность. Кроме рассмотренных выше теорем, которые применяются при достижении целей и потому называются целевыми, в пленере имеются также записывающие и вычврвивающив теоремы.
Этн теоремы определяются, вызываются и вычисляются так же, как и целевые теоремы; различаются лишь ситуации, в которых опи выаываются. Записывающие теоремы выаываются тогда, когда в базу данных записываются утверждения, соответствующие их образцам, а вычеркивающие теоремы — при вычеркивании из базы данных утверясдений, соответствующих их образцам. Назначение этих теорем — контролировать изменения базы данных. Онн зз В. Н. Пклыцваоз могут проверять езаконностьз (с точки зрения условий решаемой задачи) производимых записей и вычеркиваний или выполнять сопутствующие им изменения базы данных. Например, записывающая теорема с образцом' (еХ ПРОДАЛ «Ъ') и телом (ЕВАЯЕ (.Х ИМЕЕТ Х)) вызывается' тогда, когда в базу данных записывается утверждение о том, что некий Х продал нечто г.
Действие теоремы заключается в том, что она попутно с этой записью вычеркивает из базы данных ставшее теперь ложным утверждение о том; что этот Х имеет г. Как и другие процедуры языка, теоремы имеют имена, и любую теорему можно вызвать по имени (при этом вызывающий образец играет роль фактического параметра). Однако в таких случаях более уместным будет испольаование функций, а не теорем. Кроме того, теоремы, как и утверждения, могут иметь спиоки свойств, где указываются дополнительные сведения о теоремах.
Имена и списки свойств теорем нужны в основном для того, чтобы в рекомендациях можно было ссыпаться на конкретные тео. ромы и указывать характеристики, которые доюкны иметь вызываемые теоремы. 5.2. Определение теорем В языке нет встроенных теорем. Любая теорема, которая будет использоваться в программе, должна быть определена. Для ° того нужно, как и при определении функций к сопоставителей, обратиться и вотроенвой функции ПЕР)ХЕ, которая н наивом случае может иметь три аргумента: (ПЕР)ХЕ ГЬ де р)2), Здесь гй обозначает идентификатор, указывающий имя определяемой теоремы.