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

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

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

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

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

=== Задача 4.5 ===
Проверить вхождение одного списка в другой в качестве подсписка.
 ? check_sublist(x,y)

==== Решение ====
 check_sublist(nil, x)&nbsp;&larr;&nbsp;;
 check_sublist(x, x)&nbsp;&larr;&nbsp;;
 check_sublist(x1 . x, x1 . y)&nbsp;&larr;&nbsp;check_sublist(x, y);
 check_sublist(x1 . x, y1 . y)&nbsp;&larr;&nbsp;x1 &ne; y1, check_sublist(x1 . x, y);

=== Задача 4.6 ===
Обратить список.
 ? reverse(x,y)

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

== Расширение возможностей логического программирования ==

Повышение удобства работы.

=== Встроенные предикаты ===
Некоторые выражения удобно вычислять без использования SLR-резолюции.

==== Отношение равенства ====
Отношение равенства: =(2) — двуместный предикат.

Пример записи: t1 = t2

Что подразумевает равенство? Если интерпретатор видит, что очередной подцелью является равенство, то он пытается найти наиболее общий унификатор (НОУ), и, если он есть, то это успех. Другими словами, решается уравнение t1 = t2.

* Например, x + 2 = 3 + y, НОУ — {x/3, y/2} — успех
* Другой пример — 2 + 3 = 5, НОУ(2 + 3, 5) = &empty;, синтаксического совпадения не будет (требуется решение в свободной алгебре термов, без интерпретации)

==== Тождество ====
Тождество: ==(2)

Он круче. Будет успех, если t1 совпадает с t2.

==== Неравенство ====
Неравенство: &ne;(2)

Разрешаетя успешно, если нет НОУ.

==== Нетождество ====
Нетождество: =/=(2)

Разрешается успешно с пустой подстановкой, если t1 и t2 синтаксически различны.

=== Задача 4.8 (использование предиката нетождество) ===
Построить пересечение множеств, представленных бесповторными списками.
 ? common(x,y,z)

==== Решение ====
 common(nil, L, nil)&nbsp;&larr;&nbsp;;
 common(L, nil, nil)&nbsp;&larr;&nbsp;;
 common(x . L1, L2, x . L3)&nbsp;&larr;&nbsp;elem(x, L2), common(L1, L2, L3);
 common(x . L1, L2, L3)&nbsp;&larr;&nbsp;nonelem(x, L2), common(L1, L2, L3);
 
 nonelem(x, y . z)&nbsp;&larr;&nbsp;x =/= y, nonelem(x, z);
 nonelem(x, nil)&nbsp;&larr;&nbsp;;

=== Задача 4.10 (введение дооплнительных функций для хранения вспомогательной информации) ===
Построитьсписок L2,состоящий из тех и только тех элементов списка L1, которые содержатся в нем однократно.
 ? single(L1,L2)

==== Решение ====
Казалось бы, решение должно быть таким:
 single(x . L1, x . L2)&nbsp;&larr;&nbsp;nonelem(x, L1), single(L1, L2);
 single(x . L1, L2)&nbsp;&larr;&nbsp;elem(x, L1), single(L1, L2);
 single(nil, nil)&nbsp;&larr;&nbsp;;
Но эта программа решает дргую задачу — построение списка, в котором каждый из элементов списка L1 входит ровно один раз.
На самом деле, правильное решение следующее:
 single(L1, L2)&nbsp;&larr;&nbsp;R(L1, nil, L2);
 R(nil, L2, nil)&nbsp;&larr;&nbsp;;
 R(x . L2, L2, x . L3)&nbsp;&larr;&nbsp;nonelem(x, L1), nonelem(x, L2), R(L1, L2, L3);
 R(x . L1, L2, L3)&nbsp;&larr;&nbsp;elem(L1), R(L1, x . L2, L3)
 R(x . L1, L2, L3)&nbsp;&larr;&nbsp;elem(x, L2), R(L1, L2, L3);
В этом решении вводится дополнительный список, в котором хранятся те элементы, котрые входят в L1 более одного раза. Для хранения этого списка вводится дополнительная функция R, где он передаётся в качестве параметра.

== Домашнее задание ==
Задача 4.9

=== Задача 4.9 ===
Построить список L3, состоящий из всех тех и только тех элементов списка L1, которые не содержатся в списке L2
 ? sieve(L1 ,L2, L3)

==== Решение ====
 sieve(L1, nil, L1) &larr; ;
 sieve(x . L1, L2, x . L3) &larr; nonelem(x, L2), nonelem(x, L3), sieve(L1, L2, L3);
 sieve(x . L1, L2, L3) &larr; sieve(L1, L2, L3);

== Предикаты, расширяющие вычислительные возможности логических программ ==

=== Предикаты сравнения ===

Для данных типа INTEGER разумно ввести операции сравнения: &lt;, &le;, &ge;, &gt;. Тогда мы должны описать операционную семантику. Если текущая подцель — сравнение, то тогда он спрашивает, а правда ли, что t1, t2 — числа, и если числа, то правда, что выполняется отношение сравнения для этих чисел? Если да, то успех с пустой подстановкой.

Пример:
* ? 2 &le; 3 &rarr; success
* ? x &le; x + 1 &rarr; failure — сравнивать можно только чилса
* 1 &le; 2 + 3 &rarr; failure; — в правой части — выражение

=== Задача 1.1 (применение функций сравнения) ===
Проверить, является ли заданный целочисленный список L упорядоченным. 
 ? ordered(L)

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

=== Задача 1.2 ===
Для заданного целочисленного списка L отыскать его наибольший элемент.
 ? max(L,x)

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

Подсчитаем количество операций. В худшем случае их будет 2len(L). Если мы модифицируем решение (сделав рекурсию хвостовой), то получим линейную сложность:

max(x . nil, x) &larr; ;
 max(x . L, y) &larr; max3(L, x, y);
 max3(nil, x, x) &larr;
 max3(x . L, y, z) &larr; x &le; y, max3(L, y, z);
 max3(x . L, y, z) &larr; max3(L, x, z);

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

=== Вычислительные функции ===

Есть функции +, &minus;, &times;, div, mod, … Но их надо заставить вычислиться.

Предикат, который занимается вычислениями: is(2)

? t1 is t2
 &darr; {t1/val(t2)}
 success

Спецификация операционной семантики:
# t1 &isin; Var
# t2 — арифметическое выражение, имеющеезначение, которое можно вычислить (val(t2))
# Выполнить подстановку t1/val(t2)

Пример:
 ? x is 3 &times; (2 + 1)
 &darr; {x/9}
 success

? x is y + 1
 failure
y — переменная, у неё неопределённое значение

? x is x + 1
 failure

? y = 3 + 2, z + 1 = 4 + u, x is z + y
 &darr; {y/3 + 2}
 ? z + 1 = 4 + u, x is z + (3 + 2)
 &darr; {z/4, u/1}
 ? x is 4 + (3 + 2)
 &darr; {x/9}
 success

=== Задача 2.2 (Применение арифметических предикатов) ===
Вычисления суммы элементов целочисленного списка L. 
 ? sum(L,x)

==== Решение ====
 sum(nil, 0) &larr; ;
 sum(x . l, y) &larr; sum(L, z), y is x + z;

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. 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_06_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_05_%D0%B4%D0%B5%D0%BA%D0%B0%D0%B1%D1%80%D1%8F%29

@@ Строка 78: / Строка 78: @@
  R(nil, L<sub>2</sub>, nil)&nbsp;&larr;&nbsp;;
  R(x . L<sub>2</sub>, L<sub>2</sub>, x . L<sub>3</sub>)&nbsp;&larr;&nbsp;nonelem(x, L<sub>1</sub>), nonelem(x, L<sub>2</sub>), R(L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>);
- R(x . L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>)&nbsp;&larr;&nbsp;elem(x, L<sub>1</sub>), R(L<sub>1</sub>, x . L<sub>2</sub>, L<sub>3</sub>)
+ R(x . L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>)&nbsp;&larr;&nbsp;elem(L<sub>1</sub>), R(L<sub>1</sub>, x . L<sub>2</sub>, L<sub>3</sub>)
  R(x . L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>)&nbsp;&larr;&nbsp;elem(x, L<sub>2</sub>), R(L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>);
 В этом решении вводится дополнительный список, в котором хранятся те элементы, котрые входят в L<sub>1</sub> более одного раза. Для хранения этого списка вводится дополнительная функция R, где он передаётся в качестве параметра.

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

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

Просмотры

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

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты