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

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

Перейти к: навигация, поиск

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

Содержание

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

Оператор отсечения указывает, какие ветви не должны проходиться при откате при 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

Если условие 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 года | Алгоритмы решения задач


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