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

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

Предыдущий семинар | Следующий семинар

Содержание 1 Задача 4.5 1.1 Решение 2 Задача 4.6 2.1 Решение 3 Расширение возможностей логического программирования 3.1 Встроенные предикаты 3.1.1 Отношение равенства 3.1.2 Тождество 3.1.3 Неравенство 3.1.4 Нетождество 3.2 Задача 4.8 (использование предиката нетождество) 3.2.1 Решение 3.3 Задача 4.10 (введение дооплнительных функций для хранения вспомогательной информации) 3.3.1 Решение 4 Домашнее задание 4.1 Задача 4.9 4.1.1 Решение 5 Предикаты, расширяющие вычислительные возможности логических программ 5.1 Предикаты сравнения 5.2 Задача 1.1 (применение функций сравнения) 5.2.1 Решение 5.3 Задача 1.2 5.3.1 Решение 5.4 Вычислительные функции 5.5 Задача 2.2 (Применение арифметических предикатов) 5.5.1 Решение

[править] Задача 4.5

Проверить вхождение одного списка в другой в качестве подсписка.

? check_sublist(x,y)

[править] Решение

check_sublist(nil, x) ← ;
check_sublist(x, x) ← ;
check_sublist(x1 . x, x1 . y) ← check_sublist(x, y);
check_sublist(x1 . x, y1 . y) ← x1 ≠ y1, check_sublist(x1 . x, y);

[править] Задача 4.6

Обратить список.

? reverse(x,y)

[править] Решение

reverse(nil, nil) ← ;
reverse(x . y, z) ← reverse(y, z1), concat(z1, x . nil, z);

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

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

[править] Встроенные предикаты

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

[править] Отношение равенства

Отношение равенства: =⁽²⁾ — двуместный предикат.

Пример записи: t₁ = t₂

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

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

[править] Тождество

Тождество: ==⁽²⁾

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

[править] Неравенство

Неравенство: ≠⁽²⁾

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

[править] Нетождество

Нетождество: =/=⁽²⁾

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

[править] Задача 4.8 (использование предиката нетождество)

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

? common(x,y,z)

[править] Решение

common(nil, L, nil) ← ;
common(L, nil, nil) ← ;
common(x . L1, L2, x . L3) ← elem(x, L2), common(L1, L2, L3);
common(x . L1, L2, L3) ← nonelem(x, L2), common(L1, L2, L3);

nonelem(x, y . z) ← x =/= y, nonelem(x, z);
nonelem(x, nil) ← ;

[править] Задача 4.10 (введение дооплнительных функций для хранения вспомогательной информации)

Построитьсписок L2,состоящий из тех и только тех элементов списка L1, которые содержатся в нем однократно.

? single(L1,L2)

[править] Решение

Казалось бы, решение должно быть таким:

single(x . L1, x . L2) ← nonelem(x, L1), single(L1, L2);
single(x . L1, L2) ← elem(x, L1), single(L1, L2);
single(nil, nil) ← ;

Но эта программа решает дргую задачу — построение списка, в котором каждый из элементов списка L1 входит ровно один раз. На самом деле, правильное решение следующее:

single(L1, L2) ← R(L1, nil, L2);
R(nil, L2, nil) ← ;
R(x . L2, L2, x . L3) ← nonelem(x, L1), nonelem(x, L2), R(L1, L2, L3);
R(x . L1, L2, L3) ← elem(x, L1), R(L1, x . L2, L3)
R(x . L1, L2, L3) ← elem(x, L2), R(L1, L2, L3);

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

[править] Домашнее задание

Задача 4.9

[править] Задача 4.9

Построить список L3, состоящий из всех тех и только тех элементов списка L1, которые не содержатся в списке L2

? sieve(L1 ,L2, L3)

[править] Решение

sieve(L1, nil, L1) ← ;
sieve(x . L1, L2, x . L3) ← nonelem(x, L2), nonelem(x, L3), sieve(L1, L2, L3);
sieve(x . L1, L2, L3) ← sieve(L1, L2, L3);

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

[править] Предикаты сравнения

Для данных типа INTEGER разумно ввести операции сравнения: <, ≤, ≥, >. Тогда мы должны описать операционную семантику. Если текущая подцель — сравнение, то тогда он спрашивает, а правда ли, что t₁, t₂ — числа, и если числа, то правда, что выполняется отношение сравнения для этих чисел? Если да, то успех с пустой подстановкой.

Пример:

•  ? 2 ≤ 3 → success
•  ? x ≤ x + 1 → failure — сравнивать можно только чилса
• 1 ≤ 2 + 3 → failure; — в правой части — выражение

[править] Задача 1.1 (применение функций сравнения)

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

? ordered(L)

[править] Решение

ordered(nil) ← ;
ordered(x . nil) ← ;
ordered(x . y . L) ← x ≤ y, ordered(y . L);

[править] Задача 1.2

Для заданного целочисленного списка L отыскать его наибольший элемент.

? max(L,x)

[править] Решение

max(x . nil, x) ← ;
max(x . L, x) ← max(L, y), y ≤ x;
max(x . L, y) ← max(L, y), x < y;

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

max(x . nil, x) ← ;
max(x . L, y) ← max3(L, x, y);
max3(nil, x, x) ←
max3(x . L, y, z) ← x ≤ y, max3(L, y, z);
max3(x . L, y, z) ← max3(L, x, z);

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

[править] Вычислительные функции

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

Предикат, который занимается вычислениями: is⁽²⁾

? t1 is t2
   ↓ {t1/val(t2)}
success

Спецификация операционной семантики:

1. t₁ ∈ Var
2. t₂ — арифметическое выражение, имеющеезначение, которое можно вычислить (val(t₂))
3. Выполнить подстановку ^t₁/_val(t2)

Пример:

? x is 3 × (2 + 1)
   ↓ {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
   ↓ {y/3 + 2}
? z + 1 = 4 + u, x is z + (3 + 2)
   ↓ {z/4, u/1}
? x is 4 + (3 + 2)
   ↓ {x/9}
success

[править] Задача 2.2 (Применение арифметических предикатов)

Вычисления суммы элементов целочисленного списка L.

? sum(L,x)

[править] Решение

sum(nil, 0) ← ;
sum(x . l, y) ← sum(L, z), y is x + z;