Intel_Nils (526801), страница 44
Текст из файла (страница 44)
Как следствие этих определений мы получаем, что сопз (саг (х), сдг (х)) = х. ') Хорошее описание языка Е!$Р содержатся а книге Вайссмана (1967). 7Х !гример автоматического написании программм 221 Нетрудно видеть целесообразность использования этих функций как компонент более сложных операций над списками, таких, как программа сортировки, которую мы хотим построить. Еше одна элементарная функция, гпегпе, выбранная нами, сушественно более сложна по сравнению с первыми тремя. У функции гпегпе (сливаться, соединяться) два аргумента: первый является элементом, а второй — отсортированным списком. Значением гпегде(х,у) служит новый список, аодержаший элемент х и все элементы списка у, причем этот новый список уже подвергнут сортировке.
Таким образом, тетке (х,у) находит соответствующее место в отсортированном списке у для такого размещения там элемента х, чтобы результируюший список не нуждался в сортировке. Теперь сформулируем «аксиомы», формализуюшие наши определения и нужное нам отношение вход — выход )г(х, у). Прежде всего мы определим отношение сортировки Я(х,у) и терминах двух других отношений: 1. ()ухну)((й(х, у)Ф(5(у) Л 1(х, у)3 Л ((5(у) Л 1(х, у))=Р ~Я(х, у))).
Интуитивный смысл отношения 5(у) состоит в том, что «список у уже подвергнут сортировке», Смысл отношения 1(х, у)— «два списка х и у содержат одни и те же элементы (но не обязательно в одинаковом порядке)». Теперь мы предлагаем (рекуррентные) определения для 5 и 1 через элементарные функции: 2. (зйхзауЫи) (1 (х, у) =р1(сопз(и, х), гпегде (и, у))). 3. 1(п11, и!1) (п11 обозначает пустой список). 4. (вгх)1у)(5(у)~5(гпегйе(х, у))). 5. 5(п11). На самом деле определения 2 — 5 несколько слабее того интуитивного определения, которое мы дали выше, но они достаточны для построения доказательства ').
Множество предложений, соответствуюшнх приведенным выше правильно построенным формулам 1 — 5, таково: 1а. — 11(х, у) ~l 5 (у). 1Ь. Я (х„ у) ~/ 1(х, у). 1с. -5 (у) т/ -1 (х, у) ~/ 11(х, у). 2. ° 1(х, у) Ч 1(сопз (и, х), тетке(и, у)). ') Представленная здесь аксиоматизапия в сущности совпадает с аксноматизанией, предложенной ранее Робертом йейтсом нз Станфордского исследовательского янститута. 222 Гл. 7; Применения исчисления прединитое к решению лидин 3. 1(п)1, пВ). 4. 8(у) 1/ Я(шегйе(х, у)). 5.
8(ш!). Нашей стратегией будет попытка доказать (всяЗу)сг(я,у) по индукции. Мы будем доказывать это предположение для списка длины нуль, затем предположим, что оно верно для списков длины и ) О, и докажем его справедливость для списков длины и+ 1. Результатом будет рекурсивная функция, сортирующая список произвольной длины. , -я1ян,у! 1х,у) ч я1х.р! 317! ч !1пн.р! .
51пн! »Цпй,п11! пц! пц р я с. 7.10. дерево опровержения для (Зу) Л(пн, у). Доказывая таким способом, мы существенно помогаем написанию программы, «встраивая» проверку условного ветвления для я = п11. Если этот тест удовлетворяется, мы переходим к программе, образованной доказательством для входных списков длины л = О. В противном случае мы переходим к программе, образованной доказательством, использующим предположение индукции.
Такая схема упрощает наш пример, поскольку освобождает от формализации условных функций и введении необходимых отношений равенства. В случае списков длины п = 0 предположение можно сформулировать и виде (Бу)1т(п)1, у). Отрицанием его будет сг(п11, у). Дерево опровержения изображена на рис. 7.10. После извлечения ответа из этого дерева мы получаем ответное утверждение )с(ш1, п1!). уд Лример автоматического написания программы 223 Таким образом, здесь мы имеем до некоторой степени тривиальный рейультат: «Если длина списка х равна О, то у = и!1». [х]]у) тт Я[х,у) '-М(сапе[сот(а],саг(ауау) [[(х.у) и а[у) я ](му) ] (сепо(саг(а),еаг(а]),у) чг -З(у) е(иу]) о -Леуу цсаг[а),у) Чт З(юпвгуе(саг(а],у)) ((х,у] ч Л(х,у] З[хегав(сот[а)],у] чт .
я(саг(а),у) 8([пвп]в (х,у)) чт 5(у] -л(саг(а),у] чт з1у] з(у) чт -я(х,у) -а[сит(а],у]ч я[ду) и [сигя, ео*(о[с[к]]) пц Р и е 7.11. Дерево опровержеиия дяя (ЧхЗу) [т (к, у). Сформулируем теперь предположение индукции: «Для каждого непустого списка х значение с([г(х) можно отсортировать». Представим себе, что у нас есть функция зог1, которая может произвести сортировку списка меньшего размера.
Предположение индукции в форме предложения имеет вид 6. )с (сдг (х), аог1 (с[[г (х))). 224 Гл. 7. Применения исчислении яредикатое к решеншо задач Разумеется, мы сейчас предполагаем, что х Ф п!1, и обращение к программе, образованной этой частью доказательства, происходит в случае, когда не выполняется тест х = п11. Для доказательства (УхВ у) 1с (х, у) нам яонадобится следующее соотношение между саг, сопз и сбг: чг х(сопя (саг (х), сг!г (х)) = х). Опять-таки, чтобы избежать трудностей, связанных с предикатами равенства, введем это соотношение в виде предложения 7. й(сопз(саг(х), сбг(х)), у) Ч й(х, у). (Заметим, что это предложение становится тавтологией после подстановки х = сопз (саг(х),спг(х)), справедливость которой вытекает из определения функций саг, сопз и сбг.) Отрицанием предположения служит 8.
!'1 (в, у). Здесь а — сколемова функция, появляющаяся, когда в предположении содержатся переменные, относящиеся к квантору всеобщности. Граф опровержения изображен на рис. 7.11. Исключая функцию а и преобразуя граф опровержения обычным способом, получаем ответное утверждение !т (х, шефе (саг (х), зог! (сбг (х)))). Объединяя условное ветвление, которое мы заранее обеспечили, н элементы, созданные доказателем теорем, имеем в итоге рекурсивную программу пц, если х=п11, зог1х= щего(саг(х), зог!(сбг(х))) в противном случае 76. ИСПОЛЬЗОВАНИЕ ИСЧИСЛЕНИЯ ПРЕДИКАТОВ ПРИ РЕШЕНИИ ЗАДАЧ В ПРОСТРАНСТВЕ СОСТОЯНИЙ Если состояние задачи можно определить совокупностью правильно построенных формул исчисления предикатов, то эта совокупность может составлять описание состояния, используемое для решения задачи в пространстве состояний.
При такого рода описаниях операторы в пространстве состояний будут вычислениями, заменяющими одно множество правильно построенных формул другим. Множество целевых состояний можно тогда определить как множество, описываемое любой совокупностью п.п. формул, из которой следует некоторая целевая и.и. Формула. Аналогично можно с помощью п.п. Формулы применимости определить множество состояний, к которым применим данный оператор. В такой системе решения задач можно было 1.б. Исяользоааяае исчисления яредияатое яри решении задач 2йп бы использовать методы доказательства теорем в исчислении преднкаФов для проверки выполнения условий достижения цели и условий применимости операторов.
Представление в пространстве состояний для задачи об обезьяне и бананах, данное в гл. 3, легко модифицировать так, чтобы состояния описывались п.п. формулами. (Напомним, что в задаче об обезьяне и бананах обезьяна находится в комнате в некоторой точке а и в этой же комнате в точке Ь находится ящик. Над точкой с пола на недосягаемой высоте находится связка бананов.) Описание Яо начального состояния может состоять из четы. рех п.п. формул: ОХВОХ АТ (ящик, Ь) АТ (обезьяна, а) НВ Предикат О)ч)ВОХ имеет значение Т только тогда, когда обезьяна находится наверху ящика; предикат НВ ') имеет значение Т только тогда, когда обезьяна получает бананы; предикат'АТ имеет очевидную интерпретацию').
Целевой п.п. формулой будет просто НВ. Любое описание состояния, из которого следует НВ, соответствует целевому состоянию. У нас, как и прежде, есть четыре оператора: «подойти (ц)», «передвинуть (н)», «взобраться» и «схватить», Два первых— операторные схемы; конкретное их значение зависит от величины схемной переменной. При определении каждого оператора основными являются следующие элементы: правильно построенная формула применимости, описывающая условия, при которых этот оператор применим; правила преобразования множества п, п. формул, описывающих состояние, к которому применяется оператор, в новое множество п.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
