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

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

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

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

Содержание

Оператор отсечения «!» =

Оператор отсечения указывает, какие ветви не должны проходиться при откате при SLD-резолюции. Имеет следующий смысл:

  • A0 ← A1, …, Ak, !, Ak + 1, …, An — проверить A1, …, Ak и использовать Ak + 1, …, An

Символ «!» обычно обозначает требование единственности, поэтому он и выбран, так как доказательство строится единственным возможным способом.

Как работает предикат отсечения
Как работает предикат отсечения

Пусть у нас выполняются SLD-вычисления, в результате которых в качестве тела одной из подстановок мы имеем список подцелей, содержащих «!». Как только интерпретатор получает запрос в качестве SLD-резольвенты, он ставит у предыдущего запроса «(*», после чего вычисления продолжаются обычным образом, до тех пор, пока «!» не станет самоц левой подцелью. После чего он ставит вторую пометку, «!» убирается из списка подцелей и вычисления продолжаются дальше. Когда делается откат с G4, он делается до G1 и вычисления продолжаются дальше. При этом также не проходятся другие ветви. Это делается для того, чтобы повысить эффективность порграммы. Также это позволяет организовывать программные конструкции.

S0: if P then S1 else S2

S0 ← P, !, S1 |
     S2;

Если P истинно, то задача решается только методом S1 иначе S2.

S0: while P do S1 od

S0 ← P, !, S1, S0 |
S0 &larr ;

Если условие P истинно, то решается S1 и снова S0, если же P ложно, то S0 считается решённой.

Задача 1

Вычислить ответы на запрос G : ? A(x) к программе П A(y) ← B(y), C(a2, y); A(x) ← D(a1, x), C(x,y); B(u) ← D(u, v), !, E(v); B(v) ← E(a5); E(a2) ← ; E(a3) ← ; E(z) ← ; D(u, a1) ← C(u, f(u)); D(u, u) ← ; D(x, a2) ← ; C(z, a3) ← ;

Задача 2.1

Вычисления наибольшего из двух чисел.

? max(x,y,z)

Решение

Если писать а императивном языке, то получим

if x ≥ y then z = x else z = y

Тогда, путём прямой трансляции:

max(x, y, z) ← x ≥ y, !, z = x;
max(x, y, z) ← z = y;

Можно оптимизировать:

max(x, y, y) ← x < y, !;
max(x, y, z) ← ;

Задача 2.3

Вычисления объединения L3 множеств L1 и L2, представленных бесповторными списками.

? cup(L1, L2, L3)

Решение

cup(L1, nil, L1) ← ;
cup(L1, x . L2, L3) ← elem(x, L1), !, cup(L1, L2, L3)
cup(L1, x . L2, x . L3) ← cup(L1, L2, L3);

Учитывая, что в объединении все элементы первого множества, то нужно позабодиться о том, чтобы там не повторялись элементы из второго списка, см. правило 2.

Задача 2.6

Вычисления всех элементов целочисленного списка L1, квадраты которых не содержатся в этом списке.

? nonsquare(L1, L2)

Решение

Неправильное решение:

nonsquare(nil, nil) ← ;
nonsuare(x . L1, L2) ← z is x × x, elem(z, L1), !, nonsquare(L1, L2);
nonsquare(x . L1, x . L2) ← nonsquare(L1, L2);

Неправильность легко проверяется на списке 4 . 2 . 1 . nil. 4 — подходит, идём дальше. 2 — подходит (так как проверка идёт на списке 2 . 1 . nil), но не должно. Ошибка. необходимо ввести дополнительный предикат. Правильное решение:

nonsquare(L1, L2) ← nonsq(L1, L1, L2);
nonsq(L0, x . l1, L2) ← z is x × x, elem(z, L0), !, nonsq(L0, L1, L2);
nonsq(L0, x . L1, x . L2) ←  nonsq()L0, L1, L2);
nonsq(L, nil, nil) ← ;


Математическая Логика


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16


Календарь

Сентябрь
24 25 26
Октябрь
02 03 10 17 24 31
Ноябрь
07 14 21 28
Декабрь
05 12 19
Семинары

01 02 03 04 05 06 07


Календарь

Сентябрь
26
Октябрь
10 24
Ноябрь
07 21
Декабрь
05 19

Ссылки
Официальная страница курса | Задачи
Проведение экзамена | Решение задач: Решение задач методички | Решение задач варианта экзамена 2004 года | Алгоритмы решения задач


Эта статья является конспектом лекции.
Личные инструменты
Разделы