WWW.LIB.KNIGI-X.RU
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - Электронные материалы
 

Pages:   || 2 |

«ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ САНКТ-ПЕТЕРБУРГСКИЙ НАЦИОНАЛЬНЫЙ ИССЛЕДОВАТЕЛЬСКИЙ УНИВЕРСИТЕТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ И.А. Бессмертный ОСНОВЫ ...»

-- [ Страница 1 ] --

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ

ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ

САНКТ-ПЕТЕРБУРГСКИЙ НАЦИОНАЛЬНЫЙ ИССЛЕДОВАТЕЛЬСКИЙ

УНИВЕРСИТЕТ ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ,

МЕХАНИКИ И ОПТИКИ

И.А. Бессмертный

ОСНОВЫ ЛОГИЧЕСКОГО

ПРОГРАММИРОВАНИЯ

Учебное пособие Санкт-Петербург 201_ И.А.Бессмертный. Основы логического программирования – СПб: НИУ ИТМО, 201_. – 100 с.

Настоящее учебное пособие разработано в рамках дисциплины «Логическое программирование», преподаваемой на кафедре вычислительной техники НИУ ИТМО и включает в себя основные принципы пропозициональной логики, логики первого порядка, троичной логики и логики высшего порядка. Рассматриваются проблемы дедуктивного и индуктивного логического вывода в Прологе и Лямбда-Прологе.

Для студентов специальностей 231000.68.19, Рекомендовано к печати ученым советом факультета КТиУ __.__.201_, протокол №_.

В 2009 году Университет стал победителем многоэтапного конкурса, в результате которого определены 12 ведущих университетов России, которым присвоена категория «Национальный исследовательский университет».

Министерством образования и науки Российской Федерации была утверждена Программа развития государственного образовательного учреждения высшего профессионального образования «Санкт-Петербургский государственный университет информационных технологий, механики и оптики» на 2009–2018 годы.



Санкт-Петербургский государственный университет информационных технологий, механики и оптики, 201_ Игорь Александрович Бессмертный ОГЛАВЛЕНИЕ Словарь терминов

Введение

Пропозициональная логика и логика первого порядка.......... 11 1.

1.1. Поиск доказательств в пропозициональной логике и логике первого порядка

1.1.1. Императивный и декларативный подходы к программированию

1.1.2. Поиск доказательства

1.1.3. Подстановка значений

1.1.4. Бэктрэкинг

1.1.5. Порядок подцелей

1.1.6. Нотация Пролога

1.1.7. Унификация

1.1.8. Помимо Пролога

1.1.9. Исторические заметки

1.2. Структуры данных

1.2.1. Списки

1.2.2. Типы предикатов

1.2.3. Типы списков

1.2.4. Членство в списке и неравенство

1.2.5. Простые предикаты для обработки списков

1.2.6. Сортировка

1.2.7. Предикаты для обработки отсортированных списков... 42 1.2.8. Условные утверждения

1.2.9. Отсечение

1.2.10. Отрицание как неудача

1.2.11. Арифметика в Прологе

Задание на лабораторную работу №1

1.3.

Проблемы реализации машины вывода

2.

Индукция

2.1.

От логического к операционному смыслу

2.1.1.

Индукция правил

2.1.2.

Дедукции и доказательства

2.1.3.

Инверсия

2.1.4.

Операционные свойства

2.1.5.

Прямой вывод и насыщение

2.1.6.

Операционные семантики

2.2.

Развитие выбора

2.2.1.

Дефиниционные интерпретаторы

2.2.2.

Порядок подцелей

2.2.3.

Порядок целей (более абстрактный подход)............... 65 2.2.4.





Полнота

2.2.5.

Завершенность

2.2.6.

Задание на лабораторную работу №2

2.3.

Проблемы поиска решений

3.

Бэктрекинг

3.1.

Дизъюнкция и ложь

3.1.1.

Нормальная форма программ

3.1.2.

Равенство

3.1.3.

Явный бэктрекинг

3.1.4.

Корректность

3.1.5.

Завершенность

3.1.6.

Метаинтерпретатор для явного бэктрекинга............... 78 3.1.7.

Абстрактные машины

3.1.8.

Унификация

3.2.

Использование унификации в поиске доказательства 81 3.2.1.

Подстановки

3.2.2.

Композиция подстановок

3.2.3.

Унификация

3.2.4.

Корректность

3.2.5.

Задание на лабораторную работу №3

3.3.

Троичная логика и логика высшего порядка

4.

Троичная логика

4.1.

4.1.1. Разновидности логик, используемых в интеллектуальных системах

Модель базы знаний в троичной логике

4.1.2.

Логический вывод в троичной логике

4.1.3.

Объяснение результатов рассуждений в троичной 4.1.4.

логике 97 Визуализация результатов обработки правил........... 100 4.1.5.

4.1.6. Временные характеристики логического вывода в троичной логике

Логика высшего порядка

4.2.

Функциональное программирование и разновидности 4.2.1.

логик 105 Лямбда-Пролог

4.2.2.

Вывод с импликациями

4.2.3.

Задание на лабораторную работу №4

4.3.

Литература

Приложение 1. Описание программы SWI-Prolog

Словарь терминов Атомарный предикат (атомарное высказывание) – предикат, который может принимать быть истинным или ложным, от структуры которого мы абстрагируемся.

Антецедент правила = предпосылка – условия правила, утверждения, истинность которых имеет результатом истинность консеквента правила.

Арность – число аргументов предиката.

Бэктрекинг – поиск с возвратами в случаях неудачи.

Доказательство – рассуждение по определенным правилам, обосновывающее какое-либо утверждение.

Дедукция – логический вывод, выполняемый от общего частному.

Дизъюнкт Хорна – дизъюнкция литералов с не более чем одним положительным литералом.

Индукция – логический вывод от частного к общему.

Индукция на структуре дедукции (индукция правил) – логический вывод, … Квантор – общее название логических операций, ограничивающих область истинности какого-либо предиката.

Квантор всеобщности – условие, которое верно для всех обозначенных элементов.

Квантор существования – условие, которое истинно, по крайней мере, для одного из обозначенных элементов.

Консеквент правила – утверждение, истинность которого устанавливается правилом; результат работы правила.

Логика второго порядка – логика, в которой предикат может быть переменной.

Логика первого порядка – логика, оперирующая с предикатами, имеющими аргументы. К множеству возможных вариантов предикатов применяются кванторы существования и всеобщности.

Определенный дизъюнкт (definite clause) – дизъюнкт Хорна с ровно одним положительным литералом.

Пропозициональная логика (логика нулевого порядка) – логика, относящаяся к высказываниям или предположениям, состоящим из атомов.

Явная дизъюнктивная форма – форма логической программы, в которой каждой цели соответствует консеквент ровно одного правила.

–  –  –

Логическое программирование – подход к программированию, основанный на дедукции, а не на вычислениях. Граница между этими двумя парадигмами не является жесткой – функциональные языки могут иметь элементы логического вывода, а языки логического программирования – процедурные элементы (императивные аспекты). Для понимания логического программирования следует идентифицировать, чем вычисления отличаются от дедукции. При вычислениях мы начинаем с исходных выражений и, используя набор правил (программу), генерируем результат.

В качестве примера можно привести использование правила сложения двузначных чисел:

16+27 суммируем младшие разряды (1+2+1) 3 суммируем старшие разряды с единицей переноса 43 В случае дедукции мы стартуем от некоторой гипотезы и в соответствии с фиксированным набором правил (аксиом и правил) пытаемся проверить истинность этой гипотезы. Таким образом, вычисления не требуют изобретательности, в то время, как дедукция – это творческий процесс. Так, доказательство теоремы Ферма an+bncn при n2 потребовало 357 лет напряженной работы.

Философы, математики в течение столетий, а в последнее время также и ученые в области компьютерных наук пытались соединить вычисления с дедукцией или, по меньшей мере, понять, как соотнести их друг с другом. В частности, Джордж Буль (1815-1864) успешно перевел множество классов логических умозаключений в исчисление высказываний в виде алгебры логики (булевой алгебры). Однако в ХХ веке стало ясно, что не все, о чем мы можем рассуждать, является механически вычислимым, даже если мы следуем хорошо определенному набору формальных правил.

В рамках данного курса мы попытаемся сопоставить два подхода к программированию. Первое наблюдение состоит в том, что вычисления могут рассматриваться как ограниченная форма дедукции, поскольку они устанавливают теоремы. Например, 16+27=43 это одновременно результат вычислений и арифметическая теорема. Аналогично, дедукцию можно рассматривать как форму вычислений, если мы устанавливаем стратегию поиска доказательства, удаляя возможность выдвигать гипотезы из дедуктивного процесса. Последняя идея как раз и лежит в основе логического программирования.

Вычислительный процесс в логической программе заключается в поиске доказательства на основе фиксированной стратегии. Зная, в чем состоит стратегия, мы можем реализовать конкретный алгоритм в логике и следовать алгоритму при поиске доказательства. В данном учебном пособии использованы материалы из курсов логического программирования проф. Франка Пфеннинга из университета Карнеги-Меллон [1], а также проф.

Алекса Симпсона из университета Эдинбурга (www.inf.ed.ac.uk/teaching/courses/lp/).

Области применения логического программирования – это задачи поиска решений в условиях множества различных вариантов и ограничений.

В основном это задачи планирования и управления [2]:

Автономное планирование и составление расписаний.

Программа Remote Agent, разработанная в NASA, используется для комплексного управления работой космических аппаратов, удаленных далеко за пределы околоземной орбиты, в т.ч. диагностики и устранения неисправностей по мере их возникновения.

Ведение игр. Программа Deep Blue компании IBM стала первой программой, которой удалось победить чемпиона мира в шахматном матче.

Автономное управление. Система компьютерного зрения Alvinn была обучена вождению автомобиля, придерживаясь полосы движения. На протяжении 2850 миль система обеспечивала управлении автомобилем в течение 98% времени.

Диагностика. Медицинские диагностические программы (экспертные системы) сумели достигнуть уровня опытного врача в нескольких областях медицины.

Планирование снабжения. Во время кризиса в Персидском заливе в 1991г. В армии США была развернута система DART (Dynamic Analysis and Re-planning), которая обеспечивала автоматизированное планирование поставок и составление графика перевозок, охватывая одновременно до 50000 автомобилей, людей и грузы. Разработчики этой системы заявили, что одно это применение окупило их 30-летние инвестиции в искусственный интеллект.

Из отечественных разработчиков, использующих логическое программирование и язык следует упомянуть Prolog, петербургскую компанию Solvo (www.solvo.ru), специализирующуюся на проектах автоматизации складской и транспортно-логистической деятельности.

1. Пропозициональная логика и логика первого порядка

1.1. Поиск доказательств в пропозициональной логике и логике первого порядка Императивный и декларативный подходы к 1.1.1.

программированию Логическое программирование – это декларативный стиль программирования, где программист говорит, что он хочет вычислить, но не указывает явно, как это вычислить. Задача интерпретатора (или компилятора) – самостоятельно построить требуемые вычисления. Такой подход используется, в частности, в языке программирования Prolog (далее мы будем также использовать слово Пролог) и в СУБД на основе языка запросов SQL. В противоположность декларативному стилю, процедурный стиль программирования означает, что программист явно описывает все шаги вычислений.

Идеалистический взгляд на логическое программирование выглядит следующим образом:

Логическая программа понимается как коллекция допустимых свойств (записанных в виде логических формул) об окружающем мире (или, скорее, о мире программы).

Пользователь в качестве запроса (query) предоставляет логическую формулу, устанавливающую свойство, которое может или не может иметь место в этом мире.

Система самостоятельно устанавливает, является ли запрошенное свойство последовательностью допустимых свойств в программе.

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

Пропозициональная логика (логика нулевого порядка) – логика, оперирующая с бинарными высказываниями, которые могут принимать значение истина или ложь, от внутренней структуры которых мы абстрагируемся. Пропозициональная формула состоит из атомов и логических связок, включающих в себя конъюнкцию, дизъюнкцию, отрицание, а также скобки, определяющие порядок применения логических связок.

Логика предикатов (логика первого порядка) – логика, также оперирующая с бинарными высказываниями (предикатами), которые имеют один или более аргументов. Число аргументов предиката называется его арностью. Принципиальное отличие логики первого порядка от пропозициональной логики состоит в том, что предикат представляет собой множество экземпляров, которые определяются значениями аргументов. Следовательно, здесь уже невозможно обойтись булевыми связками, а необходимо использовать кванторы существования ( ) и всеобщности ( ).

Пропозициональная логика – частный случай логики первого порядка, когда арность всех предикатов равна нулю. В свою очередь, логика предикатов является частным случаем логики высшего порядка.

Рассмотрим простой пример логической программы в пропозициональной логике, состоящей из следующих высказываний:

windy % в Волхове ветрено volkhov windy % в Кронштадте ветрено kronstadt petersburg % Кронштадт в Петербурге kronstadt petersburg rainy % В Петербурге дождливо rainy windy umbrella_useless % Если ветреное и дождливо, зонтик бесполезен % мы из Кронштадта kronstadt

То же самое на Прологе выглядит так:

windy :- volkhov.

windy :- kronstadt.

petersburg :- kronstadt.

rainy :- petersburg.

umbrella_useless :- windy, rainy.

kronstadt.

Запрос может выглядеть следующим образом:

?- umbrella_useless.

Рис. 1.1. К примеру программы в пропозициональной логике При попытке найти решение здесь мы сталкиваемся с тем, что у нас нет данных относительно Волхова, находимся ли мы в этом городе или нет. Попытка сопоставить утверждение windy с утверждением volkhov потерпит неудачу. На рис. 1.2. приведено дерево решений для данной задачи.

Рис. 1.2. Дерево решений для цели umbrella_useless

Модифицируем программу следующим образом:

windy :- volkhov.

windy :- kronstadt.

petersburg :- kronstadt.

rainy :- petersburg.

umbrella_useless :- windy, rainy.

kronstadt.

volkhov :- fail.

Теперь запрос ?- umbrella_useless.

будет завершаться успехом. В дальнейшем мы рассмотрим, как различать отрицание и неудачу поиска решения. Заметим, что в данном контексте мы не детализируем смысл утверждений petersburg и volkhov. Это может быть наше местоположение, либо просто указание географической точки. В первом случае мы не запрещаем одновременное нахождение в двух местах. Дерево решений для модифицированной программы приведено на рис. 1.3.

Рис. 1.3. Дерево решений для модифицированной программы Поскольку логическое программирование – это поиск доказательств, изучение логического программирования означает изучение способов доказательств. Здесь мы будем придерживаться подхода Мартина-Лёфа [3]. Несмотря на то, что этот автор изучал логику скорее как основу для функционального, чем логического программирования, его идеи являются фундаментальными и пригодны для обеих парадигм.

В основе доказательства лежит рассуждение как объект знания. Мы признаем некоторое суждение, если располагаем подтверждением для него. Разновидностью подтверждения, которая нас интересует, является доказательство, отображаемое как дедукция с использованием правила вывода в форме J1,..., J n R, J где R – правило, J1,…,Jn – предпосылки (антецеденты) правила, J – суждение, порождаемое правилом (консеквент).

Мы можем прочитать это следующим образом:

Если J1 и…и Jn, то J, если правило R верно.

Наиболее общим суждением является истинность высказывания А, записываемое как А истинно. Поскольку мы будем оперировать почти исключительно с истинностью высказываний (за исключением разд., посвященного троичной логике), окончание истинно мы можем опустить. Другими примерами суждений высказываний являются А ложно, А истинно в момент t (субъект темпоральной логики) и К знает А (К знает, что А истинно, субъект эпистемологии).

Чтобы дать простые примеры исчисления высказываний, мы будем придерживаться нотации языка Prolog. Запись p(t1,t2,…,tn) означает предикат, имеющий арность n, а t1,t2,…,tn – аргументы предиката. Аргументы могут быть константами либо переменными.

В последнем случае они должны начинаться с прописной буквы.

Такой элементарный предикат называется атомом, т.е.

минимальной единицей знаний.

Для первых примеров исчисления высказываний в логике первого порядка мы используем числа Пеано.

Между десятичными числами и числами Пеано устанавливается следующее соответствие:

0 = 0; 1 = p(0); 2 = p(p(0)); 3 = p(p(p(0))); 4 = p(p(p(p(0))));...

Определим правила для определения четности чисел Пеано.

Предикат even имеет арность (число аргументов), равную 1 и устанавливает четность аргумента:

even ( N ) evz evs even (0) even ( p ( p ( N ))) Первое правило evz устанавливает, что нуль – четное число.

Это правило не имеет условия и поэтому является аксиомой. Второе правило evs утверждает, что число p(p(N)) является четным, если N четно. Здесь N является схематической переменной правила логического вывода: каждый экземпляр правила, в котором N заменяется конкретным значением, представляет собой верное рассуждение. Других правил для определения четности здесь нет, следовательно, мы можем думать, что эти два правила определяют предикат even исчерпывающим образом. Ниже приведен простой пример дедукции, из которой вытекает четность числа 4.

–  –  –

1.1.2. Поиск доказательства Интерпретация логических последовательностей заключается в назначении истинных значений атомам (утверждениям, которые могут принимать значения истина или ложь, внутренняя структура которых нас не интересует). Формула F является истинной в интерпретации T, если из T следует F (оператор обозначает логическое следование entailment):

T F Формула F истинна в том и только том случае, если это вытекает из стандартных таблиц истинности.

Формула G будет обозначать логическую последовательность формул F1, F2, …, Fn:

F1, F2, …, Fn G в том и только том случае, если для всех интерпретаций T если T F1 и … и T Fn то T В качестве примера рассмотрим логическую последовательность poor happy, ¬happy ¬poor Существует 4 интерпретации (poor, happy; ¬poor, happy; poor, ¬happy; ¬poor, ¬happy). В тех из них, где левая часть истинна, действует правая формула.

Бедный человек счастлив; если человек несчастлив, значит, он не беден.

Следующее высказывание не является логической последовательностью:

poor happy, ¬poor ¬happy Для интерпретации, где poor = ложь, а happy = истина, левая часть истинна, а правая – ложна.

Бедный человек счастлив, но из этого не следует, что если человек богат, то несчастен.

Идея программы в пропозиционной логике состоит в том, что программа представляется в виде списка пропозиционных формул F1, F2, …, Fn, а цель задается другой формулой G. Задача системы состоит в том, чтобы установить F1, F2, …, Fn G.

Если из F1, F2, …, Fn следует G, система ответит yes, иначе no.

В принципе система может проверить логическую последовательность путем построения таблицы истинности, по одной строке на каждую возможную интерпретацию. Если программа и запрос содержат n атомов, результирующая таблица истинности будет иметь 2n строк. Этот метод расточителен с точки зрения вычислительной сложности, которая растет экспоненциально, и задача становится нерешаемой.

Для того, чтобы задача стала решаемой, следует:

ограничить формулы в логических программах определенными дизъюнктами (definite clauses);

использовать поиск доказательства (proof search) для определения логической последовательности.

Определенный дизъюнкт имеет одну из двух форм:

(в Прологе факт q.) q p1 … pk q (в Прологе правило q :- p1,…, pk.), где p1,…, pk – атомы (атомарные утверждения). Логическая программа – это список F1, F2, …, Fn определенных дизъюнктов.

Цель – это список g1,…, gm атомов. Задача системы логического вывода состоит в том, чтобы установить, имеет ли место логическая последовательность F1, F2, …, Fn g1,…, gm.

Для перехода от правил логического вывода к логическому программированию следует определить конкретную стратегию.

Существуют две фундаментальные идеи: мы можем осуществлять поиск, двигаясь в обратном направлении от гипотезы к аксиомам, выстраивая дерево поиска, либо мы можем двигаться вперед от аксиом, применяя правила до тех пор, пока не достигнем гипотезы.

Первый способ называется обратным (goal directed), а второй – прямым (forward reasoning) логическим выводом. В литературе, посвященной логическому программированию, можно встретить термины сверху вниз для обратного вывода и снизу вверх для прямого вывода. Логическое программирование обычно связывают с обратным выводом; этот подход доминирует с момента появления Пролога, наиболее популярного языка логического программирования.

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

В качестве примера рассмотрим гипотезу even(p(p(0))).

Выполним логическую программу, состоящую из двух вышеописанных правил evz и evs, чтобы подтвердить или опровергнуть эту гипотезу. Заметим, что только одно правило соответствует данной гипотезе и это правило evs.

Доказательство гипотезы выглядит следующим образом:

even (0) evs even ( p ( p (0))) и единственной подцелью является even(0).

Приняв подцель even(0), мы видим, что только правило evz удовлетворяет этой цели.

Более того, это правило не имеет предпосылок, так что вычисление завершается успехом и имеет в качестве доказательства следующее:

–  –  –

В самом начале текущая цель: [umbrella_useless].

Первый атом в цели, umbrella_useless, не является аксиомой.

Единственное правило в программе, которое может быть использовано для порождения umbrella_useless, это windy rainy umbrella_useless. Заменяем текущую цель на [windy, rainy].

Первый атом в цели, windy, не является аксиомой. Правила, которые могут быть использованы для вывода windy, это volkhov windy kronstadt windy Используем сначала первое правило и заменяем цель на [volkhov, rainy].

Первый атом цели, volkhov, не является аксиомой, и в программе нет правил, которые могли быть использованы, чтобы породить volkhov. Иными словами, мы не находимся в Волхове.

Следовательно, проверка данной цели неудачна, и выполняется бэктрекинг (возврат к другой альтернативе). Мы восстанавливаем текущую цель [windy, rainy].

Мы уже видели, что первый атом цели windy, не является аксиомой, а первое правило volkhov windy не порождает решения для windy.

Следовательно, мы пытаемся применить второе правило, удовлетворяющее цели windy:

kronstadt windy Заменяем текущую цель на [kronstadt, rainy].

Первый атом цели, kronstadt, это аксиома. Следовательно, эта подцель решена, мы удаляем ее и списка цели и заменяем текущую цель на [rainy].

Продолжая таким образом мы получаем успешные решения:

Текущая цель: [rainy] Текущая цель: [petersburg] Текущая цель: [kronstadt] Текущая цель: [] Теперь поиск породил пустой список для текущей цели. Это означает, что поиск цели umbrella_useless завершился успешно.

1.1.3. Подстановка значений

В рассмотренном примере на запрос цели дается ответ yes, если доказательство найдено, или ответ no, если все попытки найти доказательство закончились неудачей. Возможно также, что поиск доказательства никогда не завершится. Как в таком случае можно написать логическую программу, которая сможет выдать результат?

В качестве примера рассмотрим программы для вычисления сумм и разностей чисел Пеано. Начнем с задания отношений и затем проиллюстрируем, как они могут быть использованы в вычислениях. В нашем случае это отношение plus(m,n,p), которое должно иметь место, если m+n=p. Мы используем следующие рекуррентные выражения (m + 1) + n = (m + n) + 1 0+n = n, которые позволяют сделать обратный отсчет первого аргумента до нуля. Таким образом, мы получим правила plus( M, N, S ) ps; pz.

plus( p ( M ), N, p ( S )) plus (0, N, N )

На Прологе это записывается следующим образом:

plus(0,N,N).

plus(p(M),N,p(S)) :- plus(M,N,S).

Теперь поставим цель в форме plus(p(0), p(0), R), где R – неизвестно.

Данная цель может быть прочитана как вопрос:

Существует ли такое R, для которого отношение plus(p(0), p(0), R) имеет место? Поиск не только конструирует подтверждение цели, но и находит значение t неизвестного R, при котором plus(p(0), p(0), t) истинно.

Для заданной цели plus(p(0), p(0), R) может быть применено только правило ps, поскольку в правиле pz первый аргумент 0 не соответствует первому аргументу p(0) цели. Мы также видим, что R должна иметь форму p(P), но пока не знаем, чему должно быть равно P.

...

plus(0, p(0), P) ps при R p( P).

plus( p(0), p(0), R) Данное правило порождает подцель plus(0, p(0), P), которой удовлетворяет только правило pz, из которого следует, что P должно быть равно p(0).

–  –  –

1.1.4. Бэктрэкинг В некоторых случаях при поиске доказательства цели соответствует консеквент более чем одного правила. Эта ситуация носит название точка выбора (choice point). При достижении точки выбора мы выбираем первое из правил в порядке их следования.

Если попытка доказательства для этого правила терпит неудачу, мы пытаемся применить следующее правило и т.д. Данный процесс называется поиск в возвратом после неудачи (backtracking). В примере с зонтиком мы видели, что не всегда поиск развивается линейно, но не акцентировали на этом внимания.

В качестве примера рассмотрим цель plus(M, p(0), p(p(0))), чтобы найти такое M, при котором M + 1 = 2, а M = 2 – 1. Этот пример демонстрирует, что мы можем использовать одну и ту же логическую программу (в данном случае определение предиката plus) в разных направлениях (вместо сложения – вычитание).

Консеквент правила pz, plus(0,N,N) не удовлетворяет цели, поскольку второй и третий аргумент цели отличаются друг от друга, а в данном правиле они совпадают.

Только правило ps может быть применено, и в результате мы получим:

...

plus( M1, p(0), p(0)) ps при M p( M1 ).

plus( M, p(0), p( p(0))) В этой точке оба правила, ps и pz удовлетворяют подцели plus(M1, p(0), p(0). Поскольку правило ps расположено в списке правил первым, далее следует...

plus( M 2, p(0),0) ps при M 1 p( M 2 ) plus( M 1, p(0), p(0)) ps при M p( M 1 ).

plus( M, p(0), p( p(0))) В этой точке никакие правила не могут быть применены, и эта попытка терпит неудачу. Поэтому мы возвращаемся к предыдущей точке выбора и пытаемся применить второе правило, pz.

–  –  –

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

Рассмотрим, к примеру, правило умножения times(m,n,p), которое должно быть истинным, если m*n=p.

Построим для этого правила следующую рекурсию 0*n =0 (m + 1) * n = (m * n) + n в виде двух продукционных правил:

–  –  –

Легко видеть, что этот процесс является бесконечным, и вычисление никогда не завершится.

Данный пример иллюстрирует, что порядок решения подцелей может иметь сильное влияние на вычисления. Здесь поиск решения либо завершается за два шага, либо никогда не заканчивается, что является следствием фиксированной последовательности извлечения правил. Стандартное решение состоит в обработке подцелей слева направо. Здесь мы видим общий феномен логического программирования: две дефиниции, полностью эквивалентные с точки зрения логики, могут сильно различаться с операционной точки зрения. Это явление также наблюдается и в функциональном программировании: две реализации одной и той же функции могут иметь существенно отличающуюся сложность.

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

1.1.6. Нотация Пролога

На сегодняшний день наиболее широко используемым языком логического программирования является Prolog, под которым понимается семейство близких друг к другу языков. Существует несколько хороших учебников, практических руководств и программных реализаций, как коммерческих, так и бесплатных.

Хорошими ресурсами для получения ответов на вопросы являются Интернет-сообщества, в частности, news://comp.lang.prolog. В рамках данного курса мы будем придерживаться реализации SWIProlog (www.swi-prolog.org), хотя рассматриваемые примеры могут выполняться практически на любом диалекте Пролога, поскольку мы будем избегать использования более сложных и продвинутых возможностей языка.

Двумерное представление продукционных правил, которое использовалось нами ранее, не вполне укладывается в текстовый формат.

Нотация Пролога для правила J1,..., J n R J выглядит следующим образом:

J J1, …, Jn.

Здесь имя правила опущено, а направленная влево стрелка в текстовом файле заменяется на конструкцию « :- ». Эта запись может быть прочитана как J если J1 и … и Jn. В терминах Пролога продукционное правило называется утверждением (clause), где J – это голова утверждения, а J1, …, Jn – тело. Таким образом, вместо того, чтобы сказать «поиск продукционного правила, чей консеквент соответствует гипотезе» мы говорим «поиск утверждения, голова которого соответствует цели».

В качестве примера представим рассмотренные ранее программы в нотации Пролога.

even(0).

even(p(p(N))) :- even(N).

plus(p(M), N, p(P)) :- plus(M,N,P).

plus(0, N, N).

times(0, N, 0).

times(p(M), N, P) :times(M, N, P), plus(P, N, Q).

В процессе определения истинности цели (доказательства гипотезы) утверждения обрабатываются в порядке их следования в программе. Подцели решаются также в том порядке, в каком они представлены в теле утверждения.

1.1.7. Унификация В процессе поиска очень важно установить, соответствует ли гипотеза консеквенту продукционного правила (или в терминах Пролога, унифицируется ли цель с головой утверждения). Данная операция является нетривиальной, поскольку правило может содержать … переменные, а цель также может иметь переменные.

В качестве примера рассмотрим цель plus(p(0), p(0), R) и утверждение plus(p(M), N, p(P)) plus(M, N, P).

Мы должны найти такие значения переменных M, N и P, для которых plus(p(0), p(0), R) = plus(p(M), N, p(P)).

Если не создавать для решения данной задачи специальный алгоритм, первое, что приходит в голову, это интуитивная идея, заключающаяся в том, чтобы установить соответствие каждого аргумента цели с каждым аргументом головы утверждения. Если один из них – переменная, то она должна получить значение аргумента, с которым производится сопоставление. В данном случае устанавливаем M = 0, N = p(0) и R = p(P). Значение P является неизвестным и R остается переменной. Применяя эти уравнения к телу утверждения, получаем утверждение plus(0, p(0), P), которое становится подцелью с другой логической переменной P. Чтобы достичь данной подцели, мы должны решить уравнение plus(0, p(0), P) = plus(0, N, N), из которого получаем N = p(0) и P = p(0).

Данный процесс называется унификацией (unification), и уравнения, которые мы создаем для переменных, представляют унификатор (unifier). Процесс унификации имеет несколько скрытых моментов. Один из них заключается в том, что переменные в утверждении (которые на самом деле являются … переменными в продукционном правиле) должны переименовываться, чтобы становиться новыми переменными каждый раз, когда утверждение используется, чтобы разные экземпляры правила не конфликтовали друг с другом.

Другой момент … уравнением N = p(p(N)), которое не имеет решений:

правая часть будет иметь на два … больше, следовательно, левая и правая часть никогда не будут одинаковыми. К сожалению, Prolog не принимает во внимание данную проблему и решает такие уравнения построением циклического терма. Это может проявиться, если мы построим запрос plus(0, N, p(N)):

«Существует ли такое n, чтобы 0 + n = n + 1».

Мы обсудим поведение Пролога позже в данном курсе при рассмотрении аспектов, связанных с эффективностью. Правда, эти аспекты противоречат принципам логического программирования.

1.1.8. Помимо Пролога

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

Только таким путем мы можем вогнать парадигму логического программирования в свои рамки без отклонения от того, что делает его изящным: элегантной логической основы.

Грубо говоря, мы многократно в рамках данного курса повторяем следующие шаги, стремясь к невероятно богатому языку, способному на поиск с откатами, параллельный поиск, насыщение и даже доказательство корректности для многих программ в гармоничном целом.

1. Конструировать логики в основательной и философски звучащей манере.

2. Изолировать фрагменты логики, основываясь на критериях поиска доказательств.

3. Дать неформальное описание операционного поведения.

4. Расширять технологии программирования и идиомы.

5. Формализовать операционную семантику.

6. Реализовать интерпретатор высокого уровня.

7. Изучить свойства языка в целом.

8. Разработать технологии моделирования рассуждений.

9. Идентифицировать ограничения и рассмотреть, как они могут быть преодолены логическими или операционными средствами.

10. Переход к п. 1.

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

1.1.9. Исторические заметки

Разработка языка Prolog началась в 1970 г. Аланом Колмероэ и Робертом Ковальским. Колмероэ работал над специализированным доказателем теорем для обработки текстов, который постепенно трансформировался в язык общего назначения. Название Prolog является сокращением от "PROgramming in LOGic". Этот язык был разработан в Марселе в 1972 г.

В 1987 г. в университете г. Амстердама была создана свободно распространяемая реализация языка, называемая SWI-Prolog. Эта реализация постоянно развивается и широко используется всеми университетами в учебных целях.

Приблизительно в это же время компания Borland создала свой вариант языка и компилятор Turbo Prolog, отличающийся от SWIProlog строгой статической типизаций, т.е. обязательным декларированием предикатов, списков и др. В середине 90-х гг.

прошлого века датская компания Prolog Development Center (PDC) приобрела права на Turbo Prolog и в 1996 г. выпустила первую версию компилятора объектно-ориентированного языка Visual Prolog.

В начале 1980-х гг. в Венгрии в Центре компьютерных исследований и инноваций (SZKI) был создан модульный Пролог MPROLOG.

Основанная в 1980 г. британская компания Logic Programming Associates (LPA) создала язык micro-Prolog, первый в мире Пролог, предназначенный для микрокомпьютеров. В настоящее время эта фирма разрабатывает реализацию Win-Prolog, работающую под ОС MS Windows, и которая позволяет создавать программы с графическим пользовательским интерфейсом.

Хорошим вводным учебником для начинающих является книга Клоксина и Меллиша «Программирование на языке Prolog» [4], а для тех, кто уже знает, как программировать, – книга Стерлинга и Шапиро «Искусство программирования на языке Prolog» [5].

1.2. Структуры данных1.2.1. Списки

Списки определяются двумя конструкторами: пустой список nil и конструктор cons, который берет элемент и присоединяет его к списку, формируя новый список. Например, список a,b,c может быть представлен как cons(a, cons(b, cons(c, nil))). В нотации Пролога пустой список обозначается как [], а cons(h,t) – [h|t].

Существует последовательная нотация для списков, где a,b,c записывается как [a,b,c]. Это также может быть записано в виде [a | [b | [c | [] ]]] или [a,b | [c, []]]. Заметим, что все эти нотации будут преобразованы в одно и то же внутреннее представление, использующее nil и cons. Мы будем использовать в дальнейшем только нотацию Пролога для представления списков.

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

1.2.2. Типы предикатов

Вернемся к определению утверждения plus, рассмотренного в подразд. 1.1, изменив порядок следования двух утверждений.

plus(0, N, N).

plus(p(0), N, p(P)) :- plus(M, N, P).

Если применить к термам, используемым здесь, конструкторы списков, первое утверждение выглядит неверным. Например, если мы зададим такую цель plus(p(0), [a, b, c], p([a, b, c]), то получим полный абсурд: что может означать суммирование 1 и списка? Что означает выражение p([a, b, c])? Это ни список, ни число.

С позиций современных языков программирования ответ очевиден: в приведенном выше определении отсутствуют типы данных. К сожалению, большинство диалектов Пролога, за исключением, пожалуй, Visual Prolog (www.visual-prolog.com) не различают термы разных типов. Исторически сложилось, что эти языки имели всего один тип термов, поскольку каждый тип мог быть определен как унарный предикат. Пока это так, нет необходимости использовать практические преимущества отличать осмысленные предложения от не имеющих смысла (meaningless).

Это можно пояснить следующим примером, в котором определяется предикат для натуральных чисел с помощью правил и модифицировать рассмотренный ранее пример правила для сложения:

nat ( N ) plus( M, N, P ) pz ps.

plus(0, N, N ) plus( p( M ), N, p( P )) Одна из проблем теперь состоит в том, что, к примеру, plus(0, nil, nil) даст ложь, в то время как это в действительности не имеет смысла. Многие проблемы, которые обнаруживаются при отладке и трасировке Пролог-программ, происходят из-за того, что утверждения, которые не имеют смысла, ошибочно интерпретируются как истина или ложь и некорректно завершаются успехом либо неудачей. Если мы транслируем вышеприведенные правила в Пролог, то получим nat(0).

nat(p(N)) :- nat(N).

plus(0, N, N) :- nat(N).

plus(p(M), N, p(P)) :- plus(M, N, P).

Ни один уважающий себя программист не напишет предикат plus таким образом. Вместо этого он опустит проверку типа в первом утверждении, и программа вернется к первоначальному варианту. Основная разница между этими двумя вариантами заключается в том, будет ли бессмысленное утверждение интерпретироваться как ложь (с проверкой типа) или как истина (без проверки типа).

Программист должен при этом аннотировать предикат для соответствующего применения:

% plus(m, n, p) если и только если m + n = p % для натуральных m, n, p plus(0, N, N).

plus(p(M), N, p(P)) :- plus(M, N, P).

Для программиста может быть предпочтительным, чтобы вместо неформального комментария было формальное декларирование типов и ошибка на этапе компиляции вместо молчаливого успеха или неудачи на этапе выполнения.

Таким свойством обладает Visual Prolog, однако, его очень строгая дисциплина декларирования типов аргументов существенно отдаляет его от чистого логического программирования. Этим, видимо, объясняется то обстоятельство, что обладая существенно более широким функционалом по сравнению с другими диалектами, Visual Prolog практически не используется при изучении основ логического программирования на Прологе.

1.2.3. Типы списков

Начнем рассмотрение списков с предикатов определения списков:

list([]).

list([X | Xs]) :- list(Xs).

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

Однако мы можем легко проверить, является ли некоторый список списком натуральных чисел:

natlist([]).

natlist([N | Ns]) :- nat(N), natlist(Ns).

Универсальный тест однотипности всех элементов списка может быть построен на основе проверки принадлежности каждого элемента некоторому предикату P:

plist(P, []).

plist(P, [X | Xs]) :- P(X), plist(P, Xs).

Такая конструкция является допустимой в некоторых реализациях Пролога, хотя она противоречит базовым принципам логического программирования, поскольку P это предикат, являющийся аргументом другого предиката plist. Это реальность логического программирования логики высшего порядка. В Прологе цель goal P(X) – это метавызов, часто записываемый как call(P(X)). Мы будем избегать его использования до того, как изучим логическое программирование высшего порядка.

1.2.4. Членство в списке и неравенство В качестве второго примера рассмотрим предикат, определяющий принадлежность элемента списку.

В синтаксисе Пролога это выглядит следующим образом:

member(X, [X | Ys]).

member(X, [Y | Ys]) :- member(X, Ys).

Заметим, что в первом утверждении мы опустили проверку, является ли Ys корректным списком, сделав это частью предположения, что второй аргумент предиката member является списком.

Уже такой очень простой предикат содержит скрытые места.

Чтобы их показать, зададим цель (приглашение в командной строке Пролога обычно выглядит как «?-») ?- member(X, [a, b, a, c]).

Если при этом интерпретатор Пролога выдает приглашение ?-, это означает, что он предлагает найти альтернативные решения, которые можно получить, введя в командной строке точку с запятой.

Указанная выше цель породит четыре результата в следующем порядке:

X = a;

X = b;

X = a;

X = c.

Возможно это покажется неожиданным, но запрос ?- member(a, [a, b, a, c]).

завершится успехом дважды, для первого и для второго включения элемента а в список.

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

Что же нужно делать, если требуется найти только первое вхождение элемента в список? К сожалению, здесь нет простого ответа, потому что наиболее очевидное решение требует сравнения на неравенство, что может быть проблемой, если хотя бы одна из переменных не определена. В нотации Пролога member1(X, [X | Ys]).

member1(X, [Y | Ys]) :- X \= Y, member1(X, Ys).

Когда X и Y определены, все работает, как ожидается, генерируя только одно решение для запроса ?- member1(a, [a, b, a, c]).

Однако, когда мы спросим ?- member1(X, [a, b, a, c]).

мы получим только один ответ, а именно, X = a. Причина состоит в том, что когда мы переходим ко второму утверждению, мы присваиваем Y значение a, а Ys получает значение [b, a, c], и тело утверждения приобретает вид X \= a, member1(X, [b, a, c]).

Здесь мы имеем проблему, заключающуюся в том, что мы не можем детерминировать неравенство X и a, поскольку X по-прежнему переменная. Пролог интерпретирует s t как невозможность унификации. Поскольку X и a унифицировать невозможно, подцель завершается неудачей, и никаких дальнейших решений не порождается. Если интерпретатор Пролога не проверяет, присвоены ли значения переменным, проверка на неравенство всегда завершается успехом.

На основе сказанного можно принять два решения. Одно заключается в том, чтобы ограничить использование неравенств случаями, когда аргумента не имеют переменных. В этих случаях неравенство может быть легко установлено без особых проблем.

Это решение принято в Прологе, и мы будем его придерживаться.

Второе решение состоит в том, чтобы отложить проверку на неравенство s t до тех пор, пока мы не сможем установить их неравенство (в этом случае проверка будет успешной) или равенство (тогда поверка закончится неудачей). Последнее решение требует намного более продвинутой операционной семантики, поскольку некоторые цели могут быть отложены на долгий срок, пока аргументы сравнения не получат значения. Это общая тема конструктивного отрицания в (constructive negation) ограничительном логическом программировании (constraint logic programming).

Неравенство связано с более общим вопросом отрицания, поскольку s t это отрицание равенства, простого предиката, определяемого как выражение X = X.

1.2.5. Простые предикаты для обработки списков

После того, как мы обнаружили, что предикат member порождает ряд интересных вопросов, исследуем некоторые другие предикаты для работы со списками. Начнем с предиката prefix(xs,ys), который завершается успехом, если xs является префиксом списка ys.

Определение данного предиката довольно простое:

prefix([], Ys).

prefix([X | Xs], [X | Ys]) :- prefix(Xs, Ys).

Аналогично можно написать предикат для проверки суффикса:

suffix(Xs, Xs).

suffix(Xs, [Y | Ys]) :- suffix(Xs, Ys).

Примечательно, что эти предикаты можно использовать различным образом. Мы можем проверить, является ли один список префиксом другого, а также можем извлечь префиксы из списка. Например, приведенный ниже запрос находит все префиксы списка [a,b,c,d].

?- prefix(Xs,[a,b,c,d]).

Xs = [];

Xs = [a];

Xs = [a,b];

Xs = [a,b,c];

Xs = [a,b,c,d].

Более общий предикат для работы с частью списка это append(xs, ys, zs), который выполняется успешно, если zs это результат объединения xs и ys.

append([], Ys, Ys).

append([X|Xs],Ys,[X|Zs]) :- append(Xs, Ys, Zs).

Предикат также может выполняться в разных append направлениях, как объединять списки, так и разделять их.

Мы можем использовать его для альтернативного определения предикатов prefix и suffix:

prefix2(Xs, Ys) :- append(Xs, _, Ys).

suffix2(Xs, Ys) :- append(_, Xs, Ys).

Здесь мы используем анонимные переменные ‘_’, конкретное значение которых нам безразлично, и которые успешно унифицируются с любыми переменными или константами. Во время выполнения программы Пролог автоматически присваивает им имена. Заметим, что если в утверждении встречаются несколько знаков подчеркивания, для них создаются разные анонимные переменные.

Например, если мы хотим определить подсписок как суффикс префикса (подсписок в середине списка), мы должны задать имя для промежуточной переменной вместо того, чтобы оставить ее анонимной:

sublist(Xs,Ys) :- prefix(Ps,Ys),suffix(Xs, Ps).

………………….

1.2.6. Сортировка

В качестве несколько более сложного примера используем рекурсивное определение быстрой сортировки. Здесь мы можем видеть разницу между спецификацией и реализацией.

Спецификация для сортировки sort(xs, ys) просто означает, что ys это упорядоченная перестановка списка xs. Однако, эта спецификация бесполезна в качестве реализации: мы не намерены перебирать все возможные перестановки, пока не буде найдена отсортированная последовательность.

Вместо этого мы реализуем собственную версию быстрой сортировки, смоделированную на основе известных алгоритмов в функциональном программировании. Здесь мы используем встроенный в Пролог тип данных integer вместо использовавшихся ранее унарных предикатов. Целые числа в Прологе могут сравниваться так же, как и в других языках программирования, причем предикаты сравнения записываются в инфиксной нотации (n = m, n m и т.д.). Для того, чтобы сравнение имело смысл, оба аргумента должны быть представлены целыми числами и не должны оставаться переменными. В противном случае возникает ошибка этапа выполнения. В других диалектах Пролога, в частности в PDC-Prolog, используются термины свободная (free) переменная, если ей не присвоено значение и связанная (bound), если в результате унификации переменная получила значение. В отличие от процедурного программирования, переменная может получить значение только один раз, и переприсвоение переменной других значений не допускается.

Быстрая сортировка заключается в том, что хвост входного списка разделяется на два подсписка: один содержит элементы, которые меньше или равны первому элементу списка, другой – элементы, которые больше первого элемента. Данная операция рекурсивно повторяется для полученных двух списков, а результат это объединение двух отсортированных подсписков.

quicksort([], []).

quicksort([X0|Xs], Ys) :partition(Xs, X0, Ls, Gs), quicksort(Ls, Ys1), quicksort(Gs, Ys2), append(Ys1, [X0|Ys2], Ys).

Разделение списка относительно первого элемента Х0 также является несложным:

partition([], _, [], []).

partition([X|Xs], X0, [X|Ls], Gs) :X = X0, partition(Xs, X0, Ls, Gs).

partition([X|Xs], X0, Ls, [X|Gs]) :X X0, partition(Xs, X0, Ls, Gs).

Заметим, что второй и третий предикаты используют операции сравнения и завершаются неудачей, если аргументы сравнения являются свободными переменными или не содержат целые числа.

Предикат partition(xs, x0, ls, gs) наследует от вызывающего предиката quicksort ограничения по состоянию переменных и типам данных: первый аргумент должен быть списком целых чисел, а второй – целым скаляром. Если эти условия выполнены, и предикат partition завершается успехом, последние два аргумента всегда будут списками целых чисел.

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

Может показаться, что проверка X X0 в последнем утверждении является излишней, поскольку обращение к этому предикату происходит в случае, если сравнение X = X0 в предыдущем предикате было неудачным. Однако, это не тот случай, поскольку в случае бэктрекинга мы можем перейти ко второму утверждению даже если ранее первое утверждение завершилось успехом, что неизбежно приведет к некорректному результату. Например, цель ?- quicksort([2,1,3], Ys) ошибочно возвратит Ys=[2,1,3] в качестве альтернативного решения.

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

1.2.7. Предикаты для обработки отсортированных списков

Реализация над двумя списками X={x} и Y={y} операций пересечения, разности и объединения предполагает в среднем развертывание nxny/2 вершин дерева поиска (список Y сканируется до первого появления искомого значения), где nx, ny — количество фактов в множествах X и Y соответственно. Для операции соединения развертывается nxny вершин, поскольку соединение представляет собой декартово произведение с фильтрацией.

Операции дополнения и фильтрации в языке SWRL являются простыми, поскольку здесь не допускается вложенный поиск, как SUBSELECT в СУБД, и требуют развертывания только nx вершин.

Ниже приведен текст предиката list::ntersection, входящего в состав библиотеки list языка Visual Prolog 7.2 (http://www.visualprolog.com/). Здесь и далее вместо множеств мы будем говорить и списках. Во-первых, список — это агрегат данных, с которым манипулирует Prolog; во-вторых, списки допускают повторяющиеся значения, сохранение которых необходимо в некоторых операциях.

predicates intersection : (Elem* ListA, Elem* ListB) - Elem* IntersectionAB.

clauses intersection([],_) = [].

intersection([X|Xs],Ys) = [X|intersection(Xs,Ys)]:isMember(X,Ys), !.

intersection([_|Xs],Ys) = intersection(Xs,Ys).

Предикат list::isMember вызывает извлечение в среднем ny/2 элеменов списка Y, для каждого элемента списка X, что и обуславливает низкую скорость работы данного предиката.

Отсортируем списки X={x} и Y={y} по возрастанию значений.

В этом случае оба списка можно обрабатывать совместно, и дерево поиска будет состоять из nx+ny вершин. Таким образом, ожидаемое ускорение обусловлено переходом от квадратичной к линейной зависимости сложности поиска от числа фактов. Предикат нахождения пересечения отсортированных списков intersectSorted представлен ниже.

predicates intersectSorted : (Elem* ListX, Elem* ListY) - Elem* IntersectionXY.

clauses intersectSorted([],_) = [] :-!.

intersectSorted(_,[]) = [] :-!.

intersectSorted([Y|Xs],[Y|Ys]) = [Y|intersectSorted(Xs,[Y|Ys])] :

-!.

intersectSorted([X|Xs],[Y|Ys]) = intersectSorted([X|Xs],Ys) :- XY,!.

intersectSorted([_|Xs],[Y|Ys]) = intersectSorted(Xs,[Y|Ys]).

Похожим образом реализуется операция вычитания множествX Y differenceSorted:

predicates differenceSorted : (Elem* ListX, Elem* ListY) Elem* ListXExceptListY.

clauses differenceSorted([],_) = [] :-!.

differenceSorted(R,[]) = R :-!.

differenceSorted([X|Xs],[X|Ys]) = differenceSorted(Xs,[X|Ys]) :-!.

differenceSorted([X|Xs],[Y|Ys]) = [X|differenceSorted(Xs,[Y|Ys])] :XY,!.

differenceSorted([X|Xs],[_Y|Ys]) = differenceSorted([X|Xs],Ys).

Операция объединения множеств состоит из суммы двух вычитаний множеств плюс их пересечение:

X Y = (X - Y) + (Y - X) + (X Y), т.е. требует пять операций.

Создание отдельного предиката unionSorted для операции объединения позволит сократить размерность данной задачи:

predicates unionSorted : (Elem* ListX, Elem* ListY) - Elem* UnionXY.

clauses unionSorted([],R) = R :-!.

unionSorted(R,[]) = R :-!.

unionSorted([X|Xs],[X|Ys]) = unionSorted(Xs,[X|Ys]) :-!.

unionSorted([X|Xs],Ys) = [X|unionSorted(Xs,Ys)].

Наиболее часто в процессе интерпретации условий правил требуется соединение двух множеств кортежей (x1,x2,xm) и (y1,y2,...,yk) по совпадению значений переменных xi = yj. В реляционной алгебре данной функции соответствует операция INNER JOIN. Количество развертываемых вершин дерева поиска для данной операции в случае наивного вывода составляет nxny,а для соединения отсортированных списков N = nx + ny+ SUM(nxinyj, xi=yj, (nxi 1 nyj 1)), (1.1) где nxi, nyj,- количество повторяющихся значений в первом и втором списке соответственно. Если пренебречь возможностью повторения одних и тех же значений в обоих списках (nxi1 nyj1), а также пренебречь случаями (nxi 1 nyj=0) и (nxi=0

nyj1), то формулу (1.1) можно упростить:

N = nx + ny+ dx+ dy, (1.2) где dx, dy,- число дубликатов значений в списках X и Y соответственно Ниже представлен текст предиката, реализующего данную операцию над двумя множествами кортежей {(x1,x2)} и {(y1,y2)} по совпадению x1 = y1.

predicates innerJoinSorted:(t{X,X}* ListX, t{X,X}* ListY, t{X,X,X}* JoinXY) t{X,X,X}* JoinXYfinal.

innerJoinSorted1:(t{X,X}, t{X,X}*, t{X,X}*, t{X,X,X}*) procedure (i,i, o,o).

clauses innerJoinSorted([], _, Final) = Final :- !.

innerJoinSorted([t(X1,X2)|Xresidue],Y,In)=innerJoinSorted(Xresidue, YtoLookUp,Out) :innerJoinSorted1(t(X1, X2), Y, YtoLookUp, XY), Out = list::append(XY, In).

innerJoinSorted1(_, [], [], []) :- !.

innerJoinSorted1(t(X1,_X2),[t(Y1,Y2)|Yresidue], [t(Y1,Y2)|Yresidue],[ ]) :-X1Y1, !.

innerJoinSorted1(t(X1,X2), [t(Y1,_)|Yresidue],YlookUp,XY) :X1 Y1, !, innerJoinSorted1(t(X1,X2), Yresidue, YlookUp, XY).

innerJoinSorted1(t(X1,X2),[t(Y1,Y2)|Yresidue],[t(Y1,Y2)|YlookUp], [t (X1,X2,Y2)|XY]) :innerJoinSorted1(t(X1,X2),Yresidue,YlookUp,XY).

В таблице 1.1 обобщены данные о каждой из реляционных операций и их сложности, измеряемой числом развертываемых вершин дерева поиска.

–  –  –

1.2.8. Условные утверждения Рассмотрим очень простой пример нахождения минимума двух чисел:

minimum(X, Y, X) :- X = Y.

minimum(X, Y, Y) :- X Y.

Чтобы избежать излишней проверки во втором предикате, мы можем использовать условное утверждение, записываемое как A - B ; C и которое решает цель А. Если А завершается успехом, все точки поиска, созданные при решении А,удаляются и мы переходим к решению B. Если А завершается неудачей, мы переходим к цели С вместо B. Существует сокращенная форма A - B, которая эквивалентна записи A - B; fail, где fail – это цель, которая всегда неуспешна.

Используя условные утверждения, мы можем переписать этот предикат более изящно:

minimum(X, Y, Z) :- X = Y - Z = X ; Z = Y.

Цена, которую мы платим за это изящество – отход от чистого логического программирования, и по мере возможности условных утверждений следует избегать. По сути, условное утверждение – конструкция, аналогичная оператору IF – THEN – ELSE в процедурных языках.

1.2.9. Отсечение

Условные утверждения базируются на двух идеях:

ограничение поиска первым решением и ветвление поиска на основе этого первого решения.

Более мощный примитив для реализации той же идеи – это отсечение (cut), которое, кстати, не связано со словом cut в теории доказательств. Отсечение появляется в цепочке утверждений и фиксирует выбор, сделанный в каждом из предыдущих утверждений. Для иллюстрации рассмотрим корректную реализацию предиката minimum в Прологе.

minimum(X, Y, Z) :- X = Y, !, Z = X.

minimum(X, Y, Y).

Первое утверждение постулирует, что если x меньше или равно y, то минимум это x. Более того, мы фиксируем данное утверждение, что минимум это x и в случае бэктрекинга (поиска с возвратами) мы не будем пытаться использовать второе утверждение (которое, естественно, будет неправильным).

Если мы допускаем метавызовы в утверждениях, мы можем определить условное утверждение A - B ; C с использованием отсечения:

if_then_else(A, B, C) :- A, !, B.

if_then_else(A, B, C) :- C.

Использование отсечения в первом утверждении удаляет все точки выбора, созданные во время поиска первого успешного решения для A и тем самым фиксирует первое утверждение if_then_else. Решение для B будет создавать точки выбора и отката как обычно, однако, в случае неудачи попыток использовать второе утверждение if_then_else не будет.

Если A завершится неудачей, очередь до отсечения не дойдет, и будет сделана попытка обращения ко второму утверждению (поскольку не зафиксировано первое утверждение), и будет выполняться C.

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

Различают красное и зеленое отсечения. Зеленые отсечения используют исключительно для повышения эффективности программы, удаляя излишние точки выбора, в то время как красные отсечения полностью меняют логику программы. Возвращаясь к коду утверждения minimum, мы можем видеть, что это красное отсечение, поскольку второй предикат не имеет смысла сам по себе, а только как результат неудачной попытки применения первого предиката.

Ниже приведен пример зеленого отсечения для немного измененного утверждения minimum:

minimum(X, Y, Z) :- X = Y, !, Z = X.

minimum(X, Y, Y) :- X Y.

Здесь удаление отсечения не меняет логики программы.

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

Таким образом, используя отсечение, мы сообщаем Прологу, что здесь может быть единственное решение, либо решения нет совсем.

Общая ошибка применения отсечения может быть пояснена следующей попыткой сделать предикат minimum более эффективным.

% ЭТО НЕКОРРЕКТНЫЙ КОД

minimum(X, Y, X) :- X = Y, !.

minimum(X, Y, Y).

На первый взгляд, здесь нет ничего неверного, однако данный код очевидно некорректен. Чтобы убедиться в этом, достаточно указать цель ?- minimum(5,10,10).

которая завершится успехом, поскольку в первом утверждении будет неудача.

1.2.10. Отрицание как неудача

Один из интересных способов использования отсечений является реализация с его помощью отрицания как конечной неудачи. Мы говорим, что А ложно, если цель А потерпела неудачу.

Используя технику высшего порядка, мы можем реализовать отрицание А следующим образом:

\+(A) :- A, !, fail.

\+(A).

Второе утверждение кажется полностью противоречащим определению отрицания, поэтому мы должны интерпретировать эту программу с точки зрения операционной логики. Чтобы решить \+(A), мы сначала должны решить цель A. Если получаем неудачу, переходим ко второму утверждению, которое всегда успешно. Это означает, что если A завершается неудачей, то его отрицание будет успешным без унификации переменных. Если же A успешно, то мы двигаемся дальше и достигаем предиката fail, а поскольку там было отсечение, обращения ко второму утверждению не будет.

Здесь также унификации переменных не будет, так как цель завершилась неудачей.

Одна из существенных проблем с отрицанием как неудачей состоит в режиме использования переменных в цели. Так, \+(A) успешно, если нет успешных решений A. И наоборот, \+(A) завершается неудачей, если есть успешное решение A. Это означает, что свободные переменные могут вести себя не так, как ожидается. Например, цель ?- \+(X = a).

всегда дает неудачу. В соответствии с обычной интерпретацией свободных переменных это может означать, что не существует такого терма t, который был бы не равен константе a. Очевидно, что данная интерпретация некорректна, в то время как цель ?- \+(b = a).

будет успешной.

Данный пример напоминает проанализированную ранее ситуацию с неравенствами.

Когда цель не может быть достигнута, отрицание как неудача должно рассматриваться с недоверием и скорее как неверное, чем правильное.

Таким образом, логические программы, содержащие неравенства, отрицание как неудачу или отсечения содержат много тонких моментов, в результате чего их поведение может быть непредсказуемым.

1.2.11. Арифметика в Прологе

Как было показано выше, целые числа являются встроенным типом данных в Прологе с предопределенными предикатами, такими как = или. Чтобы узнать больше о других встроенных предикатах, следует обращаться к руководству по языку Пролог. В любом диалекте Пролога есть встроенные операции сложения, вычитания, умножения и деления. В общем, эти операции могут быть выполнены с использованием специального предиката вида “t is e”, который выполняет арифметическое выражение e и унифицирует результат с термом t. Если e не может быть представлено в виде числа, порождается сообщение об ошибке этапа выполнения. В качестве примера ниже приведено определение длины списка, использующее целые числа, как встроенный тип integer в Прологе.

length([], 0).

length([X|Xs], N) :- length(Xs, N1), N is N1+1.

1.3. Задание на лабораторную работу №1

Тема лабораторной работы: Исследование списковых структур данных в Прологе. Цель работы – Изучение методов работы со списками. Метод выполнения работы – индивидуальный с элементами выбора. Выбору подлежит предметная область, самостоятельно выбираемая студентом. Студент должен создать для выбранной предметной области не менее двух списков и создать правила для объединения, пересечения, соединения, вычитания.

Содержание отчета:

1. Описание предметной области.

2. Список фактов и правил в нотации Пролога.

3. Результаты работы правил для заданной предметной области.

4. Трасса и состояния стека для одного из результатов.

2. Проблемы реализации машины вывода Индукция 2.1.

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

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

2.1.1. От логического к операционному смыслу

Логическая программа может иметь множество интерпретаций.

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

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

Разные интерпретации логических программ связаны между собой. Сила связи зависит от присутствия или отсутствия чисто операционных конструкций, таких как условные утверждения или отсечения, и от деталей операционной семантики, которые еще не обсуждались.

Наиболее непосредственное свойство это корректность (soundness) операционной семантики: если запрос А завершается успешно с подстановкой, то результат применения подстановки в А (записываемое как А) является истинным в логической семантике. Другими словами, А имеет доказательство. Сказанное верно для логической программы, но может быть неверным в плане присутствия логических переменных совместно с отрицанием как неудачей, как было рассмотрено ранее.

Другое свойство – полнота (completeness) операционной семантики: если есть экземпляр запроса А, который имеет решение, запрос завершается успехом. Этого не случается до тех пор, пока логическая программа не завершится, даже если доказательство имеется.

Однако здесь есть несколько промежуточных точек. Например, свойство недетерминистической полноты (non-deterministic completeness) говорит о том, что если интерпретатору было уже позволено выбрать, какое правило использовать следующим вместо того, чтобы использовать первое подходящее, то интерпретатор может быть полным. Чисто логические программы в этом смысле полные. Это очень важно, потому что это позволяет нам интерпретировать конечную неудачу как общую неудачу доказательства цели: если интерпретатор возвращает ответ «нет», он ищет все возможные альтернативы. Только если ни одна из них не ведет к доказательству, и интерпретатор является недетерминистически полным, мы убеждаемся, что доказательства нет.

Далее в рамках курса мы определим более формально корректность и недетерминистическую полноту чистых логических программ. Это соответствует изучаемой тематике, поскольку, когда мы хотим моделировать рассуждения с помощью логической программы, очень важно понимать, на каком уровне абстракции это рассуждение ведется: имеем ли мы в виду логическое или же операционное значение, включая поведение программы при поиске с возвратами? Или, возможно, недетерминистическое операционное значение? Ошибка здесь ведет к неправильной интерпретации теорем, которые мы доказываем либо к большому объему ненужной работы. Мы будем иметь в виду эти аспекты, используя различные формы рассуждений.

2.1.2. Индукция правил

–  –  –

plus( M, N, S ) pz; ps.

plus(0, N, N ) plus( p( M ), N, p( S )) Наша цель – доказать, что сумма четных чисел – четное число.

Не вполне очевидно, как можно выразить данное свойство реляционными спецификациями.

Например, мы могли бы сказать:

Для любых m, n и s, если even(m), even(n) и plus(m,n,s), то even(s).

Или же мы могли явно потребовать существования суммы s и факта, что s четно:

Для любых m, n если even(m) и even(n) то существует s такое, что plus(m,n,s) и even(s).

Если бы мы знали, что plus это функция, которая полностью определяет действие над этими двумя переменных (что означает «Для любых m и n существует единственное s такое, что plus(m,n,s)»), то эти два определения были бы эквивалентными.

Мы будем доказывать это с помощью второй формы. Первая идея для этого доказательства – проверить определение plus и увидеть, что оно определено структурно относительно первого аргумента m: правило pz отвечает за 0, а правило ps редуцирует s(m) в m. Это означает индукцию относительно m. Тем не менее, при обработке предиката m может быть произвольным термом, а значит, плохим кандидатом на индукцию.

Читая текст теоремы, мы видим, что четность m задана в качестве исходной предпосылки. Это означает, что мы имеем дедукцию even(m), использующую только два правила evz и evs, поскольку мы рассматриваем эти два правила в качестве исчерпывающего определения предиката even(m), что позволяет нам выполнять индукцию на основе дедукции even(m). Это иногда называют индукцией правил (rule induction). Если мы хотим проверить свойство для всех доказательств суждения, мы рассматриваем каждое правило в действии. Мы можем принять это свойство для всех предпосылок правила и должны показать, что оно удовлетворяет его заключению. Если мы можем показать это для всех правил, мы можем быть уверены, что это свойство должно удовлетворять всем дедукциям.

В нашем доказательстве нам нужны имена для дедукций.

Используем буквы D, E и т.д. для обозначения дедукций и двумерную нотацию D J если D это дедукция от J.

Теорема 2.1.

Для любых m, n, если even(m) и even(n), то существует такое s, что plus(m,n,s) и even(s).

–  –  –

2.1.3. Дедукции и доказательства Во время чтения предыдущего текста может возникнуть вопрос: Почему мы должны были выполнить индуктивное доказательство вручную? Если это логическое программирование на основе фиксированной стратегии, то почему мы не использовали операционную семантику для выполнения доказательства?

К сожалению, поиск в логическом программировании имеет серьезные ограничения, вследствие чего может использоваться лишь как язык программирования, обладая такими свойствами как корректность (soundness) и недетерминистическая завершенность (non-deterministic completeness). Ограничения лежат как в формах программ, так и в формах запросов. Так, в логике, лежащей в основе Пролога, правила устанавливают только атомарные (atomic) предикаты. Более того, мы можем строить запросы только в виде конъюнкций атомарных утверждений, возможно, с переменными.

Это означает, что запросы являются экзистенциальными (existential): мы спрашиваем, существуют ли некоторые значения переменных, такие, что существует доказательство результирующего утверждения? Например, в запросе ?plus(p(0), p(p(0)), S) мы одновременно спрашиваем значение s переменной S и доказательство того, что plus(p(0), p(p(0)), s).

С другой стороны, теорема, представленная выше, является изначально универсальной, и только внутри нее мы видим экзистенциальный квантор: «Для всех m и n и для каждой дедукции D – even(m) и дедукции Е – even(n) существуют s, дедукция F – plus(m,n,s) и дедукция G – even(s)».

Разница также отражается в структуре доказательства. В ответе на запрос в логическом программировании мы используем только продукционные правила, которые прямо определяют предикаты. В доказательстве теоремы о сложении четных чисел мы вместо этого используем индукцию, чтобы показать что существуют дедукции plus(m,n,s) и even(s). Если посмотреть на доказательство этой теоремы внимательно, можно видеть, что оно содержит алгоритм построения этих дедукций из имеющихся, но не для конструирования обратного поиска для логического программирования. Как мы увидим позже, индукционное доказательство данной теоремы возможно также и в логическом программировании, однако оно не может быть найдено путем логического поиска.

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

2.1.4. Инверсия

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

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

В качестве примера докажем, что разность списков может быть определена единственным способом, если она существует.

Повторим здесь определение правил для объединения списков и будем здесь использовать нотацию Пролога [] для пустых списков и [x|xs] для списка, имеющего голову x и хвост xs.

Теорема 2.2.

Для всех xs и zs, а также для всех ys и ys’, если append(xs, ys, zs) и append(xs, ys’, zs) то ys = ys’.

–  –  –

2.1.5. Операционные свойства До этого момента мы не описывали формально операционные семантики логических программ. Следовательно, мы не можем строго доказать операционные свойства, но мы можем приблизиться к этому, привлекая интуитивные семантики.

Рассмотрим, пожалуй, наименее удачную спецификацию предиката digit для десятичных цифр от 0 до 9 в унарной нотации.

Например, мы можем вывести, что 0 это цифра, используя второе правило 9 раз снизу вверх, а затем завершить дедукцию первым правилом.

В нотации Пролога эти правила выглядит так:

digit(p(p(p(p(p(p(p(p(p(0)))))))))).

digit(N) :- digit(p(N)).

Будучи корректным логически, это не будет работать корректно, поскольку не может завершиться при любом аргументе, большим 9.

Теорема 2.3. Любой запрос ?- digit(n) при n 9 не завершается.

Доказательство: методом индукции. Если n 9, то первое утверждение не может быть использовано. Следовательно, цель digit(n) должна быть редуцирована в подцель digit(p(n)) вторым правилом. Однако, p(n) 9, если n 9, и в процессе индукции гипотеза подцели не завершится. Следовательно, исходная цель также не завершится.

2.1.6. Прямой вывод и насыщение

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

В вышеприведенном примере мы начинали с базы, содержащей только цифру digit(p(p(p(p(p(p(p(p(p(0)))))))))).

Применяя второе правило с этой цифрой, как предпосылкой, мы получаем цифру digit(p(p(p(p(p(p(p(p(0))))))))) и так далее до digit(0). С этого места все попытки применить правила дадут только те факты, которые уже известны: база знаний насыщена. Мы видим, следуя логике, что только числа от 0 до 9 являются цифрами, а все остальные – нет.

В этом примере операционные семантики прямого вывода, основанные на насыщении, работали хорошо для данных правил, а обратный вывод – нет. Существует класс алгоритмов, которые выглядят простыми для описания через насыщение и существенно более сложными для обратного логического вывода, и наоборот.

Мы вернемся к прямому выводу и насыщению позже, когда будем рассматривать, как его можно интегрировать с обратным выводом в логическом смысле.

Операционные семантики 2.2.

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

2.2.1. Развитие выбора

Чтобы расширить дистанцию между логической и операционной семантикой, мы должны развить серию выборов, которая будет зафиксирована, когда поиск доказательства будет завершен. Мы будем придерживаться следующей последовательности.

1. Выбор подцелей слева направо. В терминах продукционных правил это означает, что сначала мы ищем доказательство первой предпосылки, затем второй и т.д.

2. Выбор утверждений от первого к последнему и бэктрекинг.

В терминах продукционных правил это значит, что если применимы более одного правила, мы начинаем с первого, затем переходим ко второму и т.д.

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

4. Отсечение. Это не имеет аналога на уровне продукционных правил. Мы должны специфицировать, как мы приходим к конкретным выборам пока не встретили отсечение или другую управляющую конструкцию, например, условное утверждение.

5. Другие встроенные предикаты. Пролог имеет встроенные предикаты для арифметики, ввода-вывода, изменения программы во время выполнения, вызовы внешних функций и многое другое, что мы не будем описывать формально.

Все это полезно не только чтобы перейти к непосредственно к наиболее точной и низкоуровневой семантике, потому что мы часто хотели бы рассуждать о свойствах программ, которые не зависят от этих деталей. Мы уже видели один набор примеров: мы можем рассуждать о логической семантике, чтобы установить такие свойства, как четность суммы двух четных чисел. В этом случае нас интересуют только успешные вычисления, а как мы нашли решение, нас не интересует. Другой пример – это отсечение: если программа не содержит ни одного отсечения, конечная сложность семантики, которая ее использует, не гарантируется.

2.2.2. Дефиниционные интерпретаторы

Мы можем написать интерпретатор для языка на том же самом языке (или на очень похожем языке). Это будет дефиниционный интерпретатор (definitional interpreter), метаинтерпертатор или метациркулярный интерпретатор. Может оказаться невозможным полностью описать поведение языка, который мы изучаем, потому что это может зависеть от поведения языка, на котором мы пишем описание (метаязык), и эти два языка могут быть одним и тем же!

Затем мы преобразуем дефиниционный интерпретатор, удаляя некоторые из продвинутых свойств языка, который мы определяем, и таким образом мы объясняем более сложные конструкции с помощью более простых, удаляя циркулярные (тавтологические) аспекты. Мы можем продолжать этот процесс, пока не достигнем желаемого уровня спецификации.

Для Пролога (правда, это не чистый язык логического программирования) простейший метаинтерпретатор (который при этом вряд ли будет достойным своего имени) выглядит так:

solve(A) :- A.

Чтобы интерпретировать аргумент для его резолюции как цели, мы просто выполняем его, используя средства метавызовов Пролога.

Это не приближает нас к пониманию внутреннего устройства интерпретатора, но ставит перед нами первый вопрос: как мы представляем логическую программу и цель при выполнении в дефиниционном интерпретаторе? В Прологе ответ простой: мы понимаем запятую, разделяющую подцели утверждения, как бинарную функцию конъюнкции символов, и мы понимаем константу true, которая всегда возвращает истину, всего лишь как константу. Кто-то может понимать это как репликацию языка предикатов в язык функциональных символов или не делать различий между ними. Код, приведенный выше, если его формально рассматривать, используя логику высшего порядка, использует последний подход: логические связки являются данными и могут быть обработаны как данные. В следующем интерпретаторе мы используем первый подход: мы по-прежнему будем понимать запятую как разделитель подцелей в метаязыке, но мы также используем ее как символ функции для описания конъюнкции в объектном (описываемом) языке. В отличие от кода выше, мы не будем смешивать два подхода. Логическая константа true также будет пониматься как предикатная константа с тем же именем.

solve(true).

solve((A,B)) :- solve(A), solve(B).

solve(P) :- clause(P,B), solve(B).

Во втором утверждении голова правила solve((A,B)) использует инфиксную нотацию и может быть записана следующим образом: solve(‘,’(A,B)). Дополнительная пара скобок нужна, чтобы предикат solve не был ошибочно принят за предикат с двумя аргументами.

Предикат clause/2 это встроенный предикат Пролога.

Подцель clause(P,B) будет унифицировать P с головой каждого утверждения в программе, а B – с соответствующим телом утверждения. Другими словами, если clause(P,B) успешно, то P :- B это экземпляр утверждения в текущей программе. Пролог будет пытаться унифицировать P и B с утверждениями в текущей программе с первого до последнего, так что показанный выше метаинтерпретатор будет работать корректно в соответствии с интуитивной семантикой, которая рассматривалась ранее.

Здесь имеет место небольшое количество стандартизации:

утверждение P в правиле с пустым телом рассматривается как P :- true.

Первый интерпретатор на самом деле не объясняет ничего:

порядок, в котором подцели решаются в объектном языке, тот же самый, что и в метаязыке, в соответствии со вторым утверждением.

Порядок, в котором утверждения проверяются, это тот порядок, в котором они присутствуют в clause. Унификация цели и головы утверждения также наследуется объектным языком из метаязыка с помощь унификации, выполняемой предикатом clause(P,B) между его первым аргументом и головой утверждения в программе.

2.2.3. Порядок подцелей

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

Предикат solve теперь получает два аргумента, solve(A,S), где A – это цель, а S – стек пока еще не решенных целей. Мы начинаем с пустого стека, представляющего истину (true).

solve(true, true).

solve(true, (A, S)) :- solve(A, S).

solve((A, B), S) :- solve(A, (B, S)).

solve(P, S) :- clause(P, B), solve(B, S).

Рассмотрим каждое утверждение в действии. Если цель достигнута, и стек пуст, резолюция цели завершается успехом.

solve(true, true).

Если текущая цель решена, а стек цели не пуст, мы извлекаем ближайшую подцель A и решаем ее.

solve(true, (A, S)) :- solve(A, S).

Если цель это конъюнкция, мы решаем первый конъюнкт, помещая второй в стек цели.

solve((A, B), S) :- solve(A, (B, S)).

Если цель атомарная, мы унифицируем ее с головой всех утверждений, решая тело утверждения как подцель.

solve(P, S) :- clause(P, B), solve(B, S).

Неявно мы проверяем, является ли P атомарным, поскольку в противном случае утверждение clause(P,B) завершится неудачей.

2.2.4. Порядок целей (более абстрактный подход)

Интерпретатор, рассмотренный выше, работает в чистом Прологе так, как и предполагается. Теперь мы хотели бы доказать его свойства, такие, как полнота: если он доказывает solve(А,true), то это тот случай, когда А истинно. Чтобы сделать это, целесообразно модифицировать данный интерпретатор в логическую форму, чтобы можно было использовать индукцию на дедуктивной структуре строгим образом.

Первый шаг – определение нашей первой логической связки:

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

Когда мы определяем логические связки, мы следуем точно тем же идеям как для определения атомарных высказываний: мы определяем их через продукционные правила, специфицируя, что служит доказательством их истинности.

Эти правила называются вводными правилами (introductory rules), потому что они вводят логическую связку в решение.

Следующим определим новое суждение в высказываниях. В отличие от, это бинарное суждение относительно двух высказываний. Запишем это в виде A / S и будем читать как A при S (A under S). Включим его в логическую форму solve(A,S).

Первые три правила остаются неизменными, а мы переопределим только правила для solve/2.

Последнее правило это на самом деле целое семейство правил, по одному для каждого правила, устанавливающего истинность атома P:

Мы записываем предпосылку как, если m=0, принимая как пустую конъюнкцию.

Очень важно, что определение истинности (A true) и доказуемости в стратегии поиска на основе стека (A / S) не зависят друг от друга, так что мы можем связывать их прямо.

Заметим, что каждое правило в новом суждении A / S имеет либо одну, либо ни одной предпосылки. Другими словами, если мы выполняем поиск доказательства, управляемый целью, вопрос о порядке подцелей не возникает. Он явно решается введением стека подцелей. Теперь мы можем считать эти правила как определение отношения перехода (transition), читая каждое правило от консеквента к предпосылкам. Это отношение перехода является все еще недетерминистским, потому что более чем одно правило может соответствовать атомарному предикату, но мы будем разрешать это так же, как мы поступали с другими аспектами семантики более явно.

2.2.5. Полнота Чтобы показать полноту нового суждения относительно истины, мы покажем, что если A / T, то A true. Этого, однако, в общем недостаточно, чтобы доказывать методом индукции, поскольку A – это конъюнкция, предпосылка будет иметь непустой стек, и гипотеза индукции не может быть применена. Вместо этого обобщим гипотезу индукции. Это обычно очень сложный шаг; в этом случае, однако, не очень сложно увидеть, что обобщение возможно.

Теорема 2.4.

Если A / S то A true и S true.

Доказательство: Методом индукции на структуре дедукции D A / S.

Случай 1:

–  –  –

Если m=0, то правило для P не имеет предпосылок, и мы можем заключить, что P true без инвертированных шагов.

2.2.6. Завершенность Теорема завершенности для системы со стеком подцелей устанавливает, что если A true, то A / T. Понять, как обобщить это, гораздо сложнее, но тем не менее, следующие конструкции работают.

–  –  –

Случай 3:

Это похоже на предыдущий случай за исключением того, что мы должны повторить m-1 раз. Кто-то может формализовать это как внешнюю индукцию, но мы не будем это делать здесь.

–  –  –

Эта форма теоремы завершенности является недетерминистской теоремой, поскольку выбор, которое правило следует применить в случае атомарной цели, остается недетерминистским. Более того, связывание схематичных переменных в правиле это «магия»: мы принимаем для целей семантики на данном уровне, что все цели достигнуты и семантики получат верные значения. Мы рассмотрим, как эти альтернативы могут быть решены, в следующем разделе.

Задание на лабораторную работу №2 2.3.

Тема лабораторной работы: Исследование индуктивного вывода в Прологе. Цель работы – Изучение методов индуктивного вывода на структуре дедукций. Метод выполнения работы – индивидуальный с элементами выбора. Выбору подлежит предметная область, самостоятельно выбираемая студентом.

Студент должен создать для выбранной предметной области не менее 10 фактов и не менее двух правил, порождающих индукции.

Содержание отчета:

Описание предметной области.

5.

Список фактов и правил в нотации Пролога.

6.

Результаты в виде сгенерированных аксиом.

7.

Доказательство для одного из результатов.

8.

3. Проблемы поиска решений Бэктрекинг 3.1. 3.1.1. Дизъюнкция и ложь

Когда нашей целью было представить явно выбор подцели слева направо, мы вводили в качестве связок конъюнкцию и truth.

Это позволило нам сделать явным порядок подцелей в предложениях, которые интерпретируются.

Здесь мы попытаемся сделать явным выбор правил.

Для этих целей будет удобным ввести две новые логические связки:

дизъюнкцию AB и ложь. Эти связки могут быть легко определены с помощью вводных правил.

Мы можем понимать ложность как дизъюнкции нулевых альтернатив.

3.1.2. Нормальная форма программ Иногда полезно показать семантику программ в нормальной форме. Форма представления в предыдущем разделе могла бы быть немного проще, если бы мы считали предопределенной форму явной конъюнкции для программ, где каждое продукционное правило имеет в точности одну предпосылку. Преобразование в нормальную форму при наличии конъюнкции и истины достаточно простое: если правило имеет много предпосылок, мы соединяем их в одну предпосылку. Если у правила нет предпосылок, мы ставим в качестве условия истину (. Достаточно просто доказать, что это преобразование сохраняет смысл правила.

Если семантики, представлены в качестве суждения A / S, каждый шаг поиска будет детерминистским, исключая селекцию правила для применения и то, как конкретизировать схематические правила. Мы не будем обсуждать сейчас последнее: будем считать, что все цели … (ground), и рассматривать программы, в которых все цели и подцели ground.

Простое условие, что правила избегают выбора, когда встречаются атомарные предикаты, означает, что каждая цель соответствует голове в точности одного правила. Тогда, если мы имеем цель P, правило, которое мы должны применить, уникально детерминировано. Чтобы достичь этого, мы должны преобразовать программу в явную дизъюнктивную форму. Позже мы рассмотрим систематический путь создания такой формы как часть компиляции логической программы.

В качестве примера рассмотрим обычный предикат member.

Имеются две причины того, что этот предикат не представлен в явной дизъюнктивной форме. Первая состоит в том, что здесь нет утверждения для member(t, []), нарушающего требование, что здесь должно быть ровно одно утверждение для каждой ground цели.

Вторая – это то, что для целей member(t, [t | ys]), оба утверждения могут быть применены, и здесь вновь нарушается наше требование.

Перепишем это в несколько шагов. Во-первых, мы устраняем то, что X встречается в первом правиле дважды, заменяя это явной проверкой X = Y.

Теперь, когда два правила имеют одинаковый консеквент, мы можем комбинировать их в одно, используя дизъюнкцию.

Наконец, добавим утверждение для отсутствующего случая, с предпосылкой ложь.

Теперь программа приведена в явную дизъюнктивную форму с предположением, что второй аргумент – список.

В Прологе дизъюнкция AB обозначается точкой с запятой, а

- словом fail, так что программа приобретает вид:

member(X, []) :- fail.

member(X, [Y | Ys]) :- X = Y ; member(X, Ys).

В Прологе принято окружать точку с запятой пробелами, чтобы более отчетливо отличать ее от запятой.

3.1.3. Равенство Преобразование программы в явную дизъюнктивную форму требует использовать равенство, как показано в предыдущем примере правила member. Мы записываем для высказывания, означающего, что s и t равны, используя следующее вводное правило:

Мы также можем использовать s t, чтобы указать, что два терма различны, в качестве вида рассуждения.

3.1.4. Явный бэктрекинг Предположим, что программа представлена в дизъюнктивной нормальной форме, а главный выбор состоит в том, чтобы доказать AB в качестве цели. Операционная семантика Пролога предписывает, что мы пытаемся сначала решить A и только если решение завершится неудачей, пытаемся решить B. Это предполагает, что в дополнение к стеку цели S, мы добавляем другой аргумент который хранит дальнейшие F, (неиспользованные) возможности. Мы называем F продолжением неудачи (failure continuation), потому что в него записывается то, что должно делаться, если цель A завершится неудачей. Мы записываем новое рассуждение как A / S / F и читаем его так: Или А при S или F. Более формально мы устанавливаем корректность в форме: If A / S / F then (AS) F true. Это утверждение также может помочь нам создавать правила для рассуждений.

Напишем правила для конъюнкции и истины. Они не меняются сильно, а только обеспечивают продолжение неудачи.

Правила для атомарных предикатов P тоже простые, поскольку мы принимаем истинность данных правила в явной дизъюнктивной форме.

Далее, напишем правило для дизъюнкции.

По аналогии с конъюнкцией и истиной, появляется искушение написать следующие два некорректных правила:

Попытаемся понять случай доказательства корректности для первого правила. Доказательство корректности выполняется методом индукции на структуре дедукции для A / S / F. Для этого первого из некорректных правил мы должны показать, что если (A S) (B F) истина, то ((A B) S) F истина. Инвертируя эти правила для дизъюнкции, мы видим, что или A S истина, или В истина, или F истина. В среднем случае (В истина) мы не имеем достаточно информации, чтобы заключить, что ((A B) S) F истина, и доказательство терпит неудачу.

Неудача доказательства корректности также подсказывает, как построить корректное правило: мы должны объединить попарно альтернативу В со стеком цели S и восстановить S, когда мы делаем бэктрек, рассматривая В.

Стек цели S’ во втором правиле отбрасывается, поскольку применяется к цели, которая не может быть успешной. Вместо этого мы восстанавливаем стек цели S, сохраненный с В.

Необходимо отметить, что здесь остался один случай, который не покрыт правилами:

нет правила для, так что общая цель терпит неудачу, если текущая цель неудачна, и здесь нет дальнейших альтернатив.

Наконец, нам нужны два правила для равенства, где мы привлекаем равенство (s = t) и неравенство (s t) в наши языки для рассуждений.

В реализации Пролога это не вызовет сложностей, поскольку мы принимаем все цели ground, так что мы всегда можем сказать, равны два терма или нет.

3.1.5. Корректность Доказательство корректности следует уже известным шаблонам.

–  –  –

Случаи: Доказательства случаев равенства оставим читателю.

3.1.6. Завершенность Естественно, данный набор правил не является завершенным.

Например, такое правило Не может быть найдено с помощью поиска, поскольку нет доказательства даже если есть простое доказательство, что diverge истина:

Тем не менее, интересно, что данный набор правил является полным в слабом смысле, а именно, что может быть редуцировано до, из которого следует отсутствие доказательства, что А истина.

Один из способов приблизиться к этому формально, это добавить еще один аргумент и использовать четырехместное суждение:

A / S / F / J, где J либо истина (если доказательство может быть найдено), либо ложь (если попытка доказать завершится неудачей в конечное время).

3.1.7. Метаинтерпретатор для явного бэктрекинга На основе идеи, рассмотренной выше, мы можем превратить систему вывода в Пролог-программу, которая может сказать нам в явной форме, что поиск завершается успехом или неудачей в конечное время.

–  –  –

Имея программу в явной дизъюнктивной форме, такую, как member(X, []) :- fail.

member(X, [Y|Ys]) :- X = Y ; member(X, Ys).

мы можем задать цель:

–  –  –

Каждый запрос будет завершаться успехом только один раз, поскольку наш метаинтерпретатор находит только первое решение.

3.1.8. Абстрактные машины Метаинтерпретатор, в котором выбор обеих подцелей и бэктрекинг делаются в явной форме, приближается к спецификации абстрактной машины. Чтобы увидеть, как правила вывода могут рассматриваться в качестве правил преобразования, представим A / S / F как состояние машины. Каждое правило для этого рассуждения имеет только одну предпосылку, так что каждое правило, прочитанное от консеквента к предпосылке, может рассматриваться, как правило преобразования для абстрактной машины.

Анализируя правила, мы можем видеть, что для каждого состояния имеется уникальное преобразование состояния, за исключением:

Состояние является финальным, поскольку не 1.

существует предпосылок, удовлетворяющих правилу.

Вычисление завершается.

Состояние является финальным, поскольку нет 2.

правил, которые можно применить. Вычисление заканчивается неудачей.

Состояние P/S/F вызывает уникальное преобразование 3.

(в соответствии с требованием, что есть уникальное правило для каждой атомарной цели P), правда, как найти экземпляр правила, остается неформальным.

В следующем разделе мы сделаем процесс применения правила более точным, а также допустим цели со свободными переменными в Прологе.

Унификация 3.2.

В данном разделе будет сделан исключительно важный шаг в сторону выбора цели и конкретизации правил в явной операционной семантике. Совместимость описания алгоритма для проблемы, называемой унификацией, который на основе двух термов t и s пытается найти подстановку для свободных переменных такую, что t = s, если подстановка существует.

Напоминаем, что мы записываем t для результата применения подстановки в терм t.

3.2.1. Использование унификации в поиске доказательства

–  –  –

Ясно, что только консеквент второго правила соответствует цели. На какой вопрос мы должны ответить, чтобы прийти к этому утверждению?

Первая попытка могла бы быть такой:

«Имеется такой экземпляр правила, что его консеквент удовлетворяет цели».

Когда мы говорим экземпляр, мы понимаем под ним результат подстановки значений вместо переменных, встречающихся в правиле, предложении или выражению. Мы можем видеть, что эта спецификация не вполне верна: нам необходимо конкретизировать также и цель, поскольку S должно иметь форму p(S1) для пока еще неизвестного S1. Подцель в таком случае должна быть plus(0, p(p(0)), S1) в соответствии с конкретизаций правила 0 для M, p(p(0)) для N и S1 для S.

Вторая попытка может выглядеть так:

«Существует экземпляр правила и экземпляр цели такие, что они равны».

Данная формулировка также несостоятельна. Например, подстановка p(p(p(p(0)))) для S в цели и S в правиле вместе с подстановкой для M и N, как в предыдущем варианте, будет также делать цель и консеквент правила идентичными, но это абсолютно неверно. Проблема в том, что здесь заявляется больше, чем может быть сделано: использование S1 для S в правиле, с другой стороны, оставляет переменную свободной. S1 будет детерминировано позже при поиске и других унификациях. Чтобы обозначить это, определяем, что t1 более общее, чем t2, если t1 может быть конкретизировано в t2.

Третья попытка будет такой:

«Найти более общий экземпляр правила и цели такие, что консеквент правила равен конкретизированной цели».

В терминах подстановок это звучит так: найти 1 и 2 такие, что S’1 = S2, а любой другой экземпляр S’ и S это экземпляр S’1.

В терминах описания алгоритма будет более удобным, если мы слегка переопределим проблему следующим образом:

«Сначала переименуем переменные в правиле таким образом, что они будут отличаться от переменных в цели. Затем найдем одну, наиболее общую подстановку, которая унифицирует переименованный консеквент с целью».

Здесь унификация подстановки является наиболее общей, если любая другая унифицирующая подстановка является экземпляром.

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

3.2.2. Подстановки Начиная спецификацию подстановок, мы используем нотацию FV(t) для множества всех переменных в выражении.

–  –  –

Мы постулируем, что все xi уникальны. Порядок следования пар в постановках безразличен, и мы считаем перестановки подстановок равными. Мы обозначаем доменом (domain) от dom()={ x1,…,xn}. Похожим образом мы называем множество переменных, встречающихся в выражении подстановки ti, со-доменом (соdomain) в виде.

Важное общее допущение состоит в том, домен и со-домен в подстановке несмежные.

Допущение: Все подстановки допустимы (valid), что означает dom()cod() = для любой подстановки.

Это по большому счету единственный способ выполнения. Более общее допущение – это то, что все подстановки идемпотентны (идемпотентность – свойство объекта, состоящее в том, что любые действия над объектом не изменяют его), но мы верим, что вышеописанное более удобно для наших ограниченных целей.

Заметим, что допустимые подстановки не могут содержать пары x/x, поскольку это нарушает приведенное выше допущение.

Кроме того, такие пары не являются необходимыми, потому что их действие – это идентичность, которая также может быть достигнута, если просто их опустить.

Применение подстановки к выражению t можно достаточно просто определить композиционно:

–  –  –

3.2.3. Композиция подстановок Во время поиска дедукции и даже при решении проблемы унификации мы получаем информацию поэтапно. Это означает, что мы конструируем частичную подстановку, применяем ее, а затем конструируем подстановку в результат. Общее решение состоит в композиции этих двух подстановок. Мы записываем это как.

Главное свойство, которое нам нужно: для любого t имеем (t)=t(). Чтобы это свойство могло поддерживать наши общие допущения о подстановках, мы специфицируем предусловие, что dom()dom() =. Мы определяем композицию как подстановки слева направо, пока не встретим пустую подстановку (.).

(t/x, ) = t/x, = (.) Во-первых, заметим, что dom()=dom() dom(), который является объединением несмежных доменов. Во-вторых, cod()=(cod()-dom()) cod(), так что cod() dom() =, как можно видеть с помощью вычислений. Другими словами, – это допустимая подстановка.

Можно легко проверить, что желаемое свойство составления подстановок имеет место. Нам также будет необходимо соответствующее свойство, устанавливающее, что композиция подстановок ассоциативна при подходящих допущениях.

–  –  –

Доказательство: Допустимость уже была показана выше.

Первое равенство следует из индукции на структуре выражения t, второе – из индукции на структуре.

Случай: t=x для переменной x. Тогда мы различаем два подслучая.

–  –  –



Pages:   || 2 |
Похожие работы:

«Емельянова Юлиана Андреевна НАСЕЛЕНИЕ СЕВЕРО-ЗАПАДНОГО ПОБЕРЕЖЬЯ БАЙКАЛА В РАННЕМ БРОНЗОВОМ ВЕКЕ Специальность 07.00.06 – археология Автореферат диссертации на соискание ученой степени кандидата исторических наук Барнаул – 2010 Работа выполнена на кафедре истории ГОУ ВПО "Иркутский...»

«Содержание Введение Предварительные условия Требования Используемые компоненты Условные обозначения Общие сведения Поддержка возможностей Конфигурация VRF Обзор общего использования для осведомленного о VRF межсетевого экрана IOS Неподдерживаемая кон...»

«ПОЛИТИЧЕСКИЕ ПАРТИИ И ПЕРЕХОД К ДЕМОКРАТИИ Начальный курс демократического партийного строительства для лидеров, организаторов и активистов политических партий Национальный демократическ...»

«Кайгородова Мария Евгеньевна ГЕНДЕРНО ОРИЕНТИРОВАННЫЙ МЕДИАТЕКСТ ЖУРНАЛЬНОЙ ОБЛОЖКИ: КОГНИТИВНО-СЕМИОТИЧЕСКИЙ АСПЕКТ Специальность 10.02.19 – теория языка АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата филологических наук Барнаул 2012 Диссертация выполнена на кафедре английского языка ФГБОУ ВПО "Алтай...»

«ISSN 0536 – 1036. ИВУЗ. "Лесной журнал". 2014. № 6 ЛЕСНОЕ ХОЗЯЙСТВО УДК 630*631.634 БОЛОТА В ЛЕСАХ РОССИИ И ИХ ИСПОЛЬЗОВАНИЕ © Б.В. Бабиков, д-р с.-х. наук, проф. С.-Петербургский государственный лесотехнический университет им. С.М. Кирова, пер...»

«НОРМЫ НАКОПЛЕНИЯ ТВЕРДЫХ БЫТОВЫХ ОТХОДОВ Чухлебов А.А., И.А. Иванова Воронежский государственный архитектурно-строительный университет Воронеж, Россия THE RATE OF ACCUMULATION OF SOLID WASTE Chukhlebov AA, I.A. Ivanova Voronezh State University of Architecture and...»

«НЕКРАСОВ ВЯЧЕСЛАВ ЛАЗАРЕВИЧ ЭНЕРГЕТИЧЕСКАЯ ПОЛИТИКА СССР В 1961-1974 гг. Специальность 07.00.02 – Отечественная история Автореферат диссертации на соискание ученой степени кандидата исторических наук Сургут – 2007 Работа выполнена на кафедре истории ГОУ ВПО "Сургутский государственный педагогический университ...»

«Ultima ratio Вестник Академии ДНК-генеалогии Proceedings of the Academy of DNA Genealogy Moscow-Boston Volume 9, No. 1 April 2016 Академия ДНК-генеалогии Boston-Moscow-Tsukuba ISSN 1942-7484 Вестник Академии ДНК-генеалогии. Научно-публицистическое издание Академии ДНК-ген...»

«Ф Е Д Е Р А Л Ь Н О Е АГЕНТСТВО ПО Т Е Х Н И Ч Е С К О М У Р Е Г У Л И Р О В А Н И Ю И М Е Т Р О Л О Г И И СВИДЕТЕЛЬСТВО IL ж об у т в е р ж д е н и и ти па ср ед ств и зм е р е н и й RU.C.27.007.A № 43128 Срок действия до 01 мая 2014 г.Н И Е О А И Т П С Е С ВИ М Р Н Й А М Н В Н Е И А РДТ ЗЕЕИ Микроскопы инструментальные ИМЦЛ 100x50,А ИГТВТЛ ЗООИЕЬ Открытое акционерное о...»

«Сибирское отделение РАН Государственная публичная научно-техническая библиотека КАДРОВЫЙ ПОТЕНЦИАЛ БИБЛИОТЕК Сборник научных трудов Новосибирск УДК 021.7 ББК Ч 73р7 К13 Печатается по постановлению реда...»

«РОССИЙСКАЯ ФЕДЕРАЦИЯ ИРКУТСКАЯ ОБЛАСТЬ БРАТСКИЙ РАЙОН КАЛТУКСКОЕ МУНИЦИПАЛЬНОЕ ОБРАЗОВАНИЕ ДУМА КАЛТУКСКОГО СЕЛЬСКОГО ПОСЕЛЕНИЯ РЕШЕНИЕ № 45 от 26.12.2013 г. О внесении дополнения в п.1 решения Думы № 30 от 29.08.2013г. "Об утверждении генерального...»

«Труды Нижегородского государственного технического университета им. Р.Е. Алексеева № 5(102) УДК 331.1 В.И. Дементьев, Ю.Г. Кабалдин СХЕМА ОТНОШЕНИЙ СУБЪЕКТОВ ТРУДОВОЙ ДЕЯТЕЛЬНОСТИ В СФЕРЕ...»

«198 Актуальные проблемы исторических исследований: взгляд молодых учёных. 2011 П.Е. Азарова * Советские праздники как механизм социализации городской молодежи Западной Сибири (1921 – первая половина 19...»

«руО ОТКРЫТОЕАКЦИОНЕРНОЕ ОБЩЕСТВО "РОССИЙСКИЕ ЖЕЛЕЗНЫЕДОРОГИ" (ОАО "РЖД") РАСПОРЯЖЕНИЕ " 1 " апреля 2014г. №814р Москва Обутверждении Технологической инструкции Техническое обслуживание электровозов итепловозов вэксплуатации В целях актуализации требований при проведении рабо...»

«Горбунков Владимир Иванович ОСОБЕННОСТИ ОПТИЧЕСКОГО ИЗЛУЧЕНИЯ ЗАКРЫТОЙ РТУТНОЙ БАКТЕРИЦИДНОЙ ЛАМПЫ Специальность 01.04.05 – оптика Автореферат диссертации на соискание ученой степени кандидата физико-математических наук Томск 2010 Работа выполнена на кафедре теоретической и общей эле...»

«Документ предоставлен КонсультантПлюс Утвержден и введен в действие Приказом Федерального агентства по техническому регулированию и метрологии от 29 ноября 2012 г. N 1647-ст НАЦИОНАЛЬНЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ КАРТОФЕЛЬ СЕМЕННОЙ ПРИЕМКА И МЕТОДЫ АНАЛИЗА Seed potatoes. Acceptance rules and meth...»

«ВОЗБУЖДЕНИЕ ДЕЛА О БАНКРОТСТВЕ ВЕРХОВНЫЙ СУД РОССИЙСКОЙ ФЕДЕРАЦИИ ОПРЕДЕЛЕНИЕ от 31 июля 2015 г. № 305-ЭС15-32291 Резолютивная часть объявлена 27.07.2015. Полный текст изготовлен 31.07.2015. Судебная коллегия по экономическим спорам Вер...»

«NETAPP TECHNICAL REPORT Flash Cache (PAM-II) and PAM: наилучшие методы использования Paul Updike, NetApp Январь 2010| TR-3832 Коротко о главном: Performance Acceleration Module (PAM) и Flash Cache (ранее PAM II) это программное и аппаратное решение, которое позволяет вам улучшить показатели производительности контроллера системы хранения NetA...»

«УДК 378.147.85:004.9 © Богданова Т.Л. КОМПЬЮТЕРНОЕ МОДЕЛИРОВАНИЕ ФИЗИЧЕСКИХ ЯВЛЕНИЙ КАК ФОРМА НАУЧНО-ИССЛЕДОВАТЕЛЬСКОЙ РАБОТЫ СТУДЕНТОВ ТЕХНИЧЕСКИХ ВУЗОВ Постановка проблемы. Одной из важнейших задач современной высшей школы является формирование личности, способной ориентироваться в возрастающем пот...»

«Российская академия наук Сибирское отделение Государственная публичная научно-техническая библиотека ОРГАНИЗАЦИОННО-ТЕХНОЛОГИЧЕСКАЯ ДОКУМЕНТАЦИЯ ГПНТБ СО РАН Сохранность фондов 2-е изд. перераб. и доп. Новосибирск УДК 025.7/8 ББК 78.36 О-64 Организационно-те...»

«Государственный комитет Российской Федерации по строительству и жилищнокоммунальному комплексу (Госстрой России) Государственное унитарное предприятие "Ростовский научноисследовательский институт ордена Трудового красного знамени академии коммунального хозяйства им. К.Д. Памфилова" ГУП РНИИ АКХ Согласовано: ФЕД...»

«  ФЕДЕРАЛЬНОЕ АГЕНТСТВО   ПО ТЕХНИЧЕСКОМУ РЕГУЛИРОВАНИЮ И МЕТРОЛОГИИ     НАЦИОНАЛЬНЫЙ ГОСТ Р   СТАНДАРТ   РОССИЙСКОЙ ФЕДЕРАЦИИ       Интегрированная логистическая поддержка экспортируемой продукции военного назначения ПЛАНИРОВАНИЕ МАТЕРИАЛЬНО-ТЕХНИЧЕСКОГО ОБЕСПЕЧЕНИЯ Основные положения   И...»

«Ф Е Д Е Р А Л Ь Н О Е АГЕНТСТВО ПО ТЕ Х Н И Ч Е С КО М У РЕГУЛИРО ВАНИЮ И М ЕТРО ЛО ГИИ СВИДЕТЕЛЬСТВО об утв ер ж д е н и и типа средств изм ерений RU.С.27.007.А № 43127 Срок действия до 01 апреля 2015 г...»

«Теплофизика и аэромеханика, 2012, том 19, № 5 УДК 536.3 Изменение оптических свойств системы “оксидная пленкаметалл” в процессе роста пленки: компьютерное моделирование* С.П. Русин Объединенный институт высоких температур РАН, Москва E-mail: sprusin@yandex.ru Представлены результаты компьютерн...»

«ISSN 0202-3205 МИНИСТЕРСТВО ПУТЕЙ СООБЩЕНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ ПУТЕЙ СООБЩЕНИЯ (МИИТ) Кафедра "Организация, технология и управление строительством" А.Ф. АКУРАТОВ, К.В. СИМОНОВ КОНЦЕПТУАЛЬНЫЕ ОСНОВЫ ПРОЕКТИРОВАНИЯ И СТРОИТЕЛЬСТВА ЖЕЛЕЗНЫХ ДОРОГ В РЕГИОНЕ З...»

«Письмо Федеральной службы государственной статистики от 31.05.2005 № 01-02-9/381 О ПОРЯДКЕ ПРИМЕНЕНИЯ И ЗАПОЛНЕНИЯ УНИФИЦИРОВАННЫХ ФОРМ ПЕРВИЧНОЙ УЧЕТНОЙ ДОКУМЕНТАЦИИ № КС-2, КС...»








 
2017 www.lib.knigi-x.ru - «Бесплатная электронная библиотека - электронные материалы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.