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

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

Версия от 18:03, 20 января 2008; ESyr01 (Обсуждение | вклад)
(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

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

Содержание

Задача 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-резолюции.

Отношение равенства

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

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

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

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

Тождество

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

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

Неравенство

Неравенство: ≠(2)

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

Нетождество

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

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

Задача 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(L1), nonelem(L2), R(L1, L2, L3);
R(x . L1, L2, L3) ← elem(L1), R(L1, x . L2, L3)
R(x . L1, L2, L3) ← elem(x, L2), R(L1, L2, L3);

В этом решении вводится дополнительный список, в котором хранятся те элементы, котрые входят в L1 более одного раза. Для хранения этого списка вводится дополнительная функция 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 разумно ввести операции сравнения: <, ≤, ≥, >. Тогда мы должны описать операционную семантику. Если текущая подцель — сравнение, то тогда он спрашивает, а правда ли, что t1, t2 — числа, и если числа, то правда, что выполняется отношение сравнения для этих чисел? Если да, то успех с пустой подстановкой.

Пример:

  •  ? 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;

Подсчитаем количество операций. В худшем случае их будет 2len(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(2)

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

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

  1. t1 ∈ Var
  2. t2 — арифметическое выражение, имеющеезначение, которое можно вычислить (val(t2))
  3. Выполнить подстановку t1/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;

Шаблон:Математическая логика

Личные инструменты
Разделы