Редактирование: Математическая Логика, 05 семинар (от 21 ноября)

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

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

[[Математическая Логика, 04 семинар (от 07 ноября)|Предыдущий семинар]] | [[Математическая Логика, 06 семинар (от 05 декабря)|Следующий семинар]]
== Логическое прграммирование ==

=== Логическая программа ===

'''Логическая программа''' состоит из '''логических утверждений''' ('''правил''') двух видов.

# A0&nbsp;&larr;&nbsp;A1,&nbsp;&hellip;,&nbsp;An;, где левая часть (A0)&nbsp;— заголовок, правая часть (A1,&nbsp;&hellip;,&nbsp;An;)&nbsp;— тело, Ai&nbsp;=&nbsp;P(t1,&nbsp;tn), i&nbsp;=&nbsp;0&hellip;n&nbsp;— правило. Имеет два способа истолкования:
## С точки зрения человека: если выполняются A1;,&nbsp;&hellip;&nbsp;,An, то выполняется A0. Например, если записано P(x)&nbsp;&larr;&nbsp;P(f(x)),&nbsp;R(c), то оно трактуется следующим образом: «Если предмет ''c'' обладает свойством ''R'' и ''f''(''x'') обладает свойством ''P'', то ''x'' обладает свойством ''P''»
## С точки зрения компьютера: чтобы решить задачу A0, необходимо сначала решить задачи A1,&nbsp;&hellip;,&nbsp;An. То есть, если интерпретировать предыдущий пример, то получим, что для решения задачи P(x) необходимо решить задачи R(x) и P(f(x))
# Программные утверждения второго рода — факты (такой способ принят в Прологе) <div class="definition">'''Факт'''&nbsp;— правило без тела.</div>
#: Факты записываются следующим образом: A0&nbsp;&larr;&nbsp;;, где левая часть (A0)&nbsp;— заголовок; A0&nbsp;— факт
## Интерпретация человеком: «я считаю, что A0 истинно»
## Интерпретация с точки зрения компьютера: «задача A0 априори решена»

Работа логической программы состоит в том, чтобы решить заданный набор задач ('''запрос''', '''целевое утверждение'''). Вид запроса:

?&nbsp;C1,&nbsp;&hellip;,&nbsp;Cn

где C1,&nbsp;&hellip;,&nbsp;Cn&nbsp;— '''атомы''', '''подцели'''.

# Интерпретация с точки зрения человека: при каких значениях переменных C1,&nbsp;&hellip;,&nbsp;Cn истинны (с точки зрения имеющихся утверждений)?
# Интерпретация с точки зрения компьютера: решить задачи C1,&nbsp;&hellip;,&nbsp;Cn, используя имеющиеся факты и знания

Как достигает этого компьютер?

=== Простенькое введение в логическое программирование ===

Некий учёный хочет построить дерево родственных отношений для персонажей какой-либо книги (например, Библии). Для этого он читает Библию и вносит эти утверждения в программу. Интересны пол и имя. Вот, после нескольких первых строк учёный вносит утверждение:
 Мужчина(Adam)&nbsp;&larr;&nbsp;;
Теперь он (учёный) может обратиться с запросом:
 ?&nbsp;Мужчина('Adam')
то есть, является ли мужчиной Адам. Другой пример запроса:
 ?&nbsp;Мужчина(x)
то есть, все, кто является мужчиной. Учёный читает Библию дальше:
 Женщина(Eve)&nbsp;&larr;&nbsp;;
Потом возникают брачные отношения:
 Муж(Adam, Eve)&nbsp;&larr;&nbsp;;
 Жена(Eve, Adam)&nbsp;&larr;&nbsp;;
Далее:
 Отец(Adam, Avel)
После этого надо записать, что Абель&nbsp;— сын Адама, Евы, а также тот факт, что Ева&nbsp;— мать Абеля.

Через несколько страниц учёный попадёт в затруднительное положение, поскольку вносить надо всё больше. Но можно описывать не все связи, можно описать правила:
 Сын(X, Y)&nbsp;&larr;&nbsp;Отец(Y, X);
«Если Y&nbsp;— отчец X, то X&nbsp;— отец Y». Или, другими словами, чтобы проверить, является ли X сыном Y, надо проверить, является ли Y отцом X. Тогда:
 Супруг(X, Y)&nbsp;&larr;&nbsp;Муж(X, Y);
 Супруг(X, Y)&nbsp;&larr;&nbsp;Жена(X, Y);

=== Задача 1.1 (Родитель(X, Y); введение спецзаписи для нескольких альтернатив) ===
Как описать Родитель(X, Y)?

==== Решение ====
 Родитель(X, Y)&nbsp;&larr;&nbsp;Отец(X, Y);
 Родитель(X, Y)&nbsp;&larr;&nbsp;Мать(X, Y);

Для облегчения записи используется следующий трюк:
 Родитель(X, Y)&nbsp;&larr;&nbsp;Отец(X, Y) |
                  Мать(X, Y);

=== Задача 1.2 (Дед(X, Y); введение в теле правила дополнительных переменных) ===
Как описать Дед(X, Y)?

==== Решение ====
 Дед(X, Y)&nbsp;&larr;&nbsp;Отец(X, Z), Родитель(Z, Y);

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

=== Задача 1.4 (Брат(X, Y); введение встроенного предиката &ne;) ===
Как описать Брат(X, Y)?

==== Решение ====
 Брат(X, Y)&nbsp;&larr;&nbsp;Родитель(Z, X), Родитель(Z, Y), Мужчина(X);

Достаточно ли полное это определение? Нет, получается, что я&nbsp;— брат сам себе: Брат(X, X)&nbsp;&larr;&nbsp;; Тогда, для решения этой проблемы и полного описания необходимо описать предикат неравенства. Как это сделать? Можно считать, что человек идентифицируется по имени, тогда можно написать сравнение строк, сравнение букв (букв конечное количество, поэтому это возможно). Второй вариант&nbsp;— встроенные средства языка: X&nbsp;&ne;&nbsp;Y. Тогда полное определение Брат(X, Y) будет иметь следующий вид:
 Брат(X, Y)&nbsp;&larr;&nbsp;Родитель(Z, X), Родитель(Z, Y), Мужчина(X), X&nbsp;&ne;&nbsp;Y;

=== Задача 1.5 (Предок(X, Y); введения способа рекурсивного определения) ===
Как описать Предок(X, Y)?

==== Решение ====
 Предок(X, Y)&nbsp;&larr;&nbsp;Родитель(X, Y) |
                Родитель(X, Z), Предок(Z, Y);

Вот Комсерг пишет, что Предок(X, Y)&nbsp;&larr;&nbsp;Родитель(X, Z1);&nbsp;&hellip;,&nbsp;Родитель(Zn&nbsp;&minus;&nbsp;1, Zn),&nbsp;Родитель(Zn, Y). То есть, что правило Предок есть транзитивное замыкание правила Родитель. Но это описывается рекурсией.

В каком порядке будет выполняться проверка? Согласно стратегии большинства интерпретаторов логических программ, утверждения выполняются в порядке их записи. Какие есть ещё варианты записи этого правила:
 Предок(X, Y)&nbsp;&larr;&nbsp;Предок(Z, Y), Родитель(X, Z);

С точки зрения логики всё правилоьно. Но с точки зрения интерпретатора в данном случае откладываются отложенные проверки правила Родитель.  Предыдущий способ описания является частным случаем рекурсии&nbsp;— итерацией. Тут же&nbsp;— чистая рекурсия.

== Домашнее задание (to be verified) ==
Задачи 1.3, 1.6

=== Задача 1.3 (Быть_отцом(x)) ===
Описать Быть_отцом(x)ф

==== Решение ====
 Быть_отцом(x)&nbsp;&larr;&nbsp;Отец(X, Y);
Существует Y такой, что X&nbsp;— отец Y
 
=== Задача 1.6 (Родственник(X, Y)) ===
Описать Родственник(X, Y)

==== Решение ====
 Родственник(X, Y)&nbsp;&larr;&nbsp;Предок(X, Y) |
                     Предок(Y, X) |
                     Предок(Z, X), Предок(Z, Y), X&nbsp;&ne;&nbsp;Y;

Далее&nbsp;— программные вещи.

== Структуры данных ==

Есть простые типы даннхы&nbsp;— строки, целые, …

Составные типы данных:
* В Си, Алголе, … основным составным типом является массив, отличительным признаком которого является произвольный доступ
* В Прологе, Лиспе основным составным типом является список, отличительным признаком которого является последовательный доступ

Список — более естественный тип данных с точки зрения рекурсии.

=== Описание списка с точки зрения логики предикатов ====
Есть nil — константа «пустой список»

Второй элемент, используемый для построения списков&nbsp; .(2) — двуместный функциональный символ, конструктор списков.

=== Синтаксис списков ===

Списком является всякий терм (?), удовлетворяющий одному из двух правил:
# nil&nbsp;— список
# t1&nbsp;.&nbsp;t2&nbsp;— список, если t1&nbsp;— любой терм, t2&nbsp;— список

'''Пример списка''': a&nbsp;.&nbsp;(b&nbsp;.&nbsp;(c&nbsp;.&nbsp;nil)))

Левый аргумент точки&nbsp;— заголовок, голова списка

Правый аргумент точки&nbsp;— хвост списка

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

Что такое (a&nbsp;.&nbsp;nil)&nbsp;.&nbsp;nil&nbsp;.&nbsp;nil

Если расставить скобки, то получим (a&nbsp;.&nbsp;nil)&nbsp;.&nbsp;(nil&nbsp;.&nbsp;nil), то есть, список из списка из элемента a.

Можно строить многомерные списки, деревья. Например, бинарное дерево: D1&nbsp;.&nbsp;D2&nbsp;.&nbsp;nil

Теперь решим две наиболее важные задачи в обработке списков:
# Написать программу, которая проверяет, что x является списком&nbsp;— list(x)
# Написать программу, которая проверяет, является ли y элементом списка x&nbsp;— elem(x, y)

list(nil)&nbsp;&larr;&nbsp;;
 list(x . y)&nbsp;&larr;&nbsp;list(y);
 elem(x, x . y)&nbsp;&larr;&nbsp;;
 elem(x, y . z)&nbsp;&larr;&nbsp;elem(x, z);

На примере второй программы рассмотрим, как работает интерпретатор. Рассмотрим, как выполняется запрос:
 ? elem(x, a . b . c . nil)
«что является элементом из списка (a, b, c)?»

Если имеется несколько подцепей, то он решает их по очереди.

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

* Унифицируем ли list(nil)? Нет, заголовки разные
* Унифицируем ли list(x . y)? Нет, заголовки разные
* Унифицируем ли elem(x, x . y)?
** elem(x1, x1 . y1) &larr; НОУ(x1, x1 . y1), elem(x, a . b . c . nil)) = {x1/a, x/a, y1/b . c . nil} = &Theta;1, то есть, унификатор существует. 
** Далее применяется подстановка. Тело пустое, подзадачи кончились.

Какой результат? Результат — применение всех подстановок к подцели. То есть, {x/a}.

Но решений может быть много. Тогда интерпретатор откатывается на шаг назад и смотрит, найдутся ли другие правила. И они находятся:
* elem(x2, y2 . z2)&nbsp;&larr;&nbsp;НОУ(elem(x2, y2 . z2), elem(x, a . b . c . nil)) = {x2/x, y2/a, z2/a . b . c . nil} = &Theta;2. И тогда новая задача получается так: выбрасываем подцель, подставляем тело в начало запроса и образуем новый запрос:
 ? elem(x2, z2)
и, применим к нему &Theta;2:
 ? elem(x, b . c . nil)
Чтобы решить весь запрос, достаточно решить этот запрос.
* Унифицируем ли list(nil)? Нет, заголовки разные
* Унифицируем ли list(x . y)? Нет, заголовки разные
* Применяем третье правило: &Theta;3 = {x3/b, x/b, y3/c . nil} — унификатор нашёлся. 
Выбрасываем исходную подцель, подставляем тело, применяем подстановку. В результате получили пустой список подцелей.

Что же будет подставлено вместо x? &Theta;2&Theta;3|x = {x/b} — b является элементом a . b . c . nil.

Быть может, есть другие варианты, откатываемся на шаг назад:

* 4 правило: &Theta;4 = {x4/x, y4/b, z4/c . nil}
 ? elem(x, c . nil)
* &Theta;5 = {x5/c, x/c, y5/nil}
Получили пустой список подзадач.

{x/c} — третий ответ на вопрос.

Откат на шаг назад.

&Theta;6 = {x6/x, y6/с, z6/nil}

Образован новый запрос:
 ? elem(x , nil)

3, 4 правила не подходят, унификатора не будет — в заголовке сложный терм с точкой, а у нас nil. Значит, failure, то есть неправильный порядок применений. Откат на шаг назад (backtracking), больше вариантов нет, …, откатываемся до корня и отвечаем, что получены три решения.

=== Задача 3 (Построение дерева вычислений) ===
Построить дерево вычислений запроса G, обращенного к программе P.
 G: R(y), P(z);
 P: 1. R(y) &larr; P(y), Q(y);
    2. P(a) &larr; ;
    3. P(b) &larr; ;
    4. Q(a) &larr; ;
    5. Q(f(x)) &larr; Q(f(f(x)));

==== Решение ====
[[Изображение:Matlog_5sem_task3.png|640px]]

Ответ: &Theta;1&Theta;2&Theta;3&Theta;4|y, z = {y/a, z/a}, &Theta;1&Theta;2&Theta;3&Theta;5|y, z = {y/a, z/b}

=== Задача 4.1 ===
Выделить заголовок x списка L.
 ? head(L,x)

==== Решение ====
 ? head(x . y, x)&nbsp;&larr;&nbsp;;

=== Задача 4.4 ===
Построить конкатенацию (последовательное соединение) списков.
 ? concat(x,y,z)

==== Решение ====
 concat(x, nil, x)&nbsp;&larr;&nbsp;;
 concat(nil, y, y)&nbsp;&larr;&nbsp;;
 concat(x . x1, y, x . z1)&nbsp;&larr;&nbsp;concat(x1, y, z1);

== Домашнее задание ==
Задача 4.2, 4.3

=== Задача 4.2 ===
Выделить хвост y списка L.
 ? tail(L, y)

==== Решение ====
 tail(y . nil, y)&nbsp;&larr;&nbsp;;
 tail(x . L, y)&nbsp;&larr;&nbsp;tail(L, y);

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%2C_05_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_21_%D0%BD%D0%BE%D1%8F%D0%B1%D1%80%D1%8F%29

Редактирование: Математическая Логика, 05 семинар (от 21 ноября)

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 39: / Строка 39: @@
  Жена(Eve, Adam)&nbsp;&larr;&nbsp;;
 Далее:
- Отец(Adam, Abel)
+ Отец(Adam, Avel)
-После этого надо записать, что Авель&nbsp;— сын Адама, Евы, а также тот факт, что Ева&nbsp;— мать Авеля.
+После этого надо записать, что Абель&nbsp;— сын Адама, Евы, а также тот факт, что Ева&nbsp;— мать Абеля.
 Через несколько страниц учёный попадёт в затруднительное положение, поскольку вносить надо всё больше. Но можно описывать не все связи, можно описать правила:
  Сын(X, Y)&nbsp;&larr;&nbsp;Отец(Y, X);
-«Если Y&nbsp;— отец X, то X&nbsp;— отец Y». Или, другими словами, чтобы проверить, является ли X сыном Y, надо проверить, является ли Y отцом X. Тогда:
+«Если Y&nbsp;— отчец X, то X&nbsp;— отец Y». Или, другими словами, чтобы проверить, является ли X сыном Y, надо проверить, является ли Y отцом X. Тогда:
  Супруг(X, Y)&nbsp;&larr;&nbsp;Муж(X, Y);
  Супруг(X, Y)&nbsp;&larr;&nbsp;Жена(X, Y);