Сошников Д.В. Лекции по ЛП

Подождите немного. Документ загружается.

Московский авиационный институт

(государственный T

Xнический университет)

Факультет прикладной математики

Кафедра вычислительной математики и программирования

Подготовка к экзамену по курсу «Логическое программирование»

Студент: И. К. Никитин

Преподаватели: Д. В. Сошников

М. А. Левинская

Москва, 2009

Содержание

I Основы 4

1 Парадигмы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Логика предикатов 1-го порядка . . . . . . . . . . . . . . . . . . . . . . . 7

2.1 Семантика логики предикатов . . . . . . . . . . . . . . . . . . . . 8

3 Исчисление предикатов 1-го порядка . . . . . . . . . . . . . . . . . . . . 9

4 Понятие о полноте . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

5 неразрешимость исчисления . . . . . . . . . . . . . . . . . . . . . . . . . 13

6 Нормальные формы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

7 Унификация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

7.1 Правила . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

8 Правило вывода modus tollens . . . . . . . . . . . . . . . . . . . . . . . . 18

8.1 modus tollens . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

8.2 Резолюция . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

9 Метод резолюции . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

9.1 Стратегии резолюции . . . . . . . . . . . . . . . . . . . . . . . . . 20

9.2 SLD-резолюция . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

10 SLD-интерпретатор . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

10.1 Стратегии обхода дерева вывода при поиске решений. . . . . . . 22

11 Cемантика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

12 Отрицание . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

12.1 SLDNF-резолюция . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

12.2 Предикат not . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

II Prolog 27

13 Пролог . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

13.1 Основные смысловые объекты программы . . . . . . . . . . . . . 27

14 Oбъекты . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

15 Операторы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

15.1 Операторы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

15.2 Представление и вычисление арифметических выражений . . . . 31

15.3 Определяемые пользователем операторы . . . . . . . . . . . . . . 32

15.4 Представление предикатов и правил структурными термами . . 33

16 Циклы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

16.1 repeat. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

16.2 for. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

17 Перебор и отсечение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

18 read, write, nl . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

19 asserta-setof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

19.1 asserta/assertz, retract . . . . . . . . . . . . . . . . . . . . . . . . . 39

19.2 ﬁndall, bagof/setoft . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

III Cтруктуры данных 42

20 Представление списков . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

21 Oбработки списков 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

21.1 определение длины . . . . . . . . . . . . . . . . . . . . . . . . . . 45

21.2 взятие n-ого элемента . . . . . . . . . . . . . . . . . . . . . . . . . 45

21.3 принадлежность элемента списку . . . . . . . . . . . . . . . . . . 45

21.4 добавление элемента . . . . . . . . . . . . . . . . . . . . . . . . . . 46

21.5 конкатенация списков . . . . . . . . . . . . . . . . . . . . . . . . . 46

21.6 применение extend . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

22 Oбработки списков 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

22.1 удаление элемента . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

22.2 определение подсписка . . . . . . . . . . . . . . . . . . . . . . . . 48

22.3 перестановки . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

23 Порядковое представление списков в Прологе . . . . . . . . . . . . . . . 50

23.1 Операции . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

24 Разностные списки . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

24.1 Разностный список . . . . . . . . . . . . . . . . . . . . . . . . . . 52

24.2 Хвостовая рекурсия . . . . . . . . . . . . . . . . . . . . . . . . . . 52

24.3 Хвостатизация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

24.4 Примеры . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

25 Деревья . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

26 Сбалансированные деревья . . . . . . . . . . . . . . . . . . . . . . . . . . 58

27 Представления графов . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

27.1 В глубину . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

27.2 В ширину . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

IV Методы 63

28 Генерации, проверки, ветви и границы . . . . . . . . . . . . . . . . . . . 63

28.1 Метод генерации и проверок . . . . . . . . . . . . . . . . . . . . . 63

28.2 Метод ветвей и границ . . . . . . . . . . . . . . . . . . . . . . . . 63

29 Сокращения перебора . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

30 Пространство состояний . . . . . . . . . . . . . . . . . . . . . . . . . . . 69

31 Операторы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

32 Символьные вычисления . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

33 Подходы к символьному упрощению выражений . . . . . . . . . . . . . 72

34 Языки . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

35 Условия . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

36 Расширение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

V Приложение 76

1 Общие вопросы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

2 Статистика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

3 Итоги . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78

I. Вопрос 1.1

I Основы логического программирования

1 Парадигмы

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

Декларативные языки программирования как альтернатива императивным. Логиче-

ское программирование как алгоритмическая модель, альтернативная модели Тью-

ринга — фон Неймана

Парадигма Принцип + −

Императивная Модель: Машина фон

Неймана основанная на

Тьюринге.

Программы представляют

из себя набор примитив-

ных инструкций, комбини-

руемых определённым об-

разом. Примитивные опе-

раторы

1. Присваивание

2. Ввод-вывод

Правила комбинирования

1. Композиция

2. Условная компози-

ция

3. Циклическая компо-

зиция

1. естественное

соответствие

архитектуре

1. непрозрачная

семантика

2. присваивание

3. контекст (об-

ласть видимо-

сти)

4. постановка за-

дачи

I. Вопрос 1.2

Логическая Модель: Математиче-

ская логика. Логика пре-

дикатов первого порядка.

Она достаточно формаль-

на и позволяет формули-

ровать свойства.

Программы пред-

ставляют собой стро-

го формализованную

постановку зада-

чи. Естественный

способ описания.

Выполнение инициа-

лизируется запросом

на нахождение зна-

чений переменных,

удовлетворяющих

какому-нибудь

предикаты или

формуле.

реализация: перевод

описания на декла-

ративном языке в

классический импе-

ративный алгоритм.

Функциональная Модель: λ –исчисление.

Процедуры манипули-

руют описание других

процедур.

формализм более вы-

сокого порядка чем

логическое програм-

мирование

реализация: перевод

описания на декла-

ративном языке в

классический импе-

ративный алгоритм.

Ситуационная Модель: Нормальные

алгоритмы Маркова.

Программа представляет

собой набор подстановок

применяемых в соответ-

ствии с определёнными

правилами ко входной

строке для получения

результата.

Стиль программирования, при котором решение задачи или алгоритм решения гене-

рируется компьютером автоматически, а для решения необходимо только формаль-

ное описание, называют декларативным

Эквивалентность моделей Множество потенциальных задач шире, чем множе-

ство алгоритмов. ∃ невычислимые функции, которые невозможно вычислить при

помощи алгоритмов в известных алгоритмических моделях.

Теоремма 1. Множества вычислимых функций в алгоритмических моделях:

I. Вопрос 1.3

• машина Тьюринга

• исчисление предикатов первого порядка

• Нормальные алгоритмы Маркова

• рекурсивные функции Черча

совпадают.

Док-во. Доказывается через эмуляцию.

Определение 1. Эффективно вычислимая функция – вычислимая при помощи на-

формального алгоритма как последовательность дискретных элементарных шагов,

детерминированная и конечная.

Теоремма 2 (Теорема Тьюринга-Чёрча). Множество функций вычислимых в со-

ответствующей алгоритмической модели. совпадает с множеством эффективно

вычислимых функций.

I. Вопрос 2.1

2 Логика предикатов 1-го порядка

Логика предикатов 1-го порядка. Семантика логики предикатов. Понятия выполни-

мости и общезначимости. Понятие логического следствия |=.

Определение 2. Логика высказываний (или пропозициональная логика) — это

формальная теория, основным объектом которой служит понятие логического

высказывания. С точки зрения выразительности, её можно охарактеризовать

как классическую логику нулевого порядка. Логика высказываний является простей-

шей логикой, максимально близкой к человеческой логике неформальных рассужде-

ний и известна ещё со времён античности.

Определение 3. Логика первого порядка (исчисление предикатов) – формальное

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

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

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

Логика предикатов первого порядка:

1. Предикаты (высказывание зависящее от параметров)

2. Связанные переменные и кванторы (∀, ∃)

3. Функциональные символы f(x

, . . . x

) как аргументы предикатов.

I. Вопрос 2.2

2.1 Семантика логики предикатов

Предполагают что ∃ область интерпретации D. Формулы:

• Замкнутые (не содержит вхождений свободных переменных)

– Придать значения из области интерпретации всем предметным константам

ℵ

: {a

} → D

– Придать смысл всем функциональным символам

ℵ

: {f

(n)

} → (D

→ D)

– Придать значения всем предикатным символам

ℵ

: {P

(n)

} → (D

→ {T, F})

Т.о. интерпретация ℵ = hD, ℵ

, ℵ

• Не замкнутые (зависит от некоторого набора переменных { x

, . . . x

})

– Однозначная интерпретация невозможна

– Вводится понятие оценки на наборе {a

, . . . a

}

Определение 4. Формула F называются общезначимой |= F если она истина

во всех интерпретациях.

Определение 5. Формула F называются выполнимой если она истина хотя бы

в одной интерпретации.

Определение 6. Формула B следует из формулы A

A |= B

если в любой интерпретации для которой истинно A оказывается истинным и B

Можно распространить на произвольное количество высказываний

, . . . A

|= B ⇔ A

∧ · · · ∧ A

|= B

Теоремма 3.

A |= B ⇔|= A ⊃ B

I. Вопрос 3.1

3 Исчисление предикатов 1-го порядка

Исчисление предикатов 1-го порядка. Понятие о формальной аксиоматической си-

стеме. Выводимость (`) в формальной аксиоматической системе. Правило вывода

modus ponens.

Определение 7. Формальная аксиоматическая система

1. Алфавит

A = {A

, . . . , A

}

некоторое конечное не пустое множество символов

2. Множество правильно построенных формул

Φ ⊆ A

∗

задаётся грамматикой

3. Множество аксиом

⊆ Φ

4. Правил вывода позволяют получить из нескольких правильно построенных

формул заключения

Определение 8. Вывод формулы f из множества формул Γ — после-

довательность {f

, . . . , f

= f} где f

получается применением правил вывода

к некоторым формулам из Γ ∪ {f

, . . . , f

= f}

Определение 9. В этом случае говорят, что формула f выводимая из

множества Γ

Γ ` f

Определение 10. Формула f выводимая в формальной аксиомати-

ческой системе

` f

если Γ

` f