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

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

Версия 00:14, 22 января 2008

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

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

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

• A₀ ← A₁, …, A_k, !, A_{k + 1}, …, A_n — проверить A₁, …, A_k и использовать A_{k + 1}, …, A_n

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

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

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

S0: if P then S1 else S2

S0 ← P, !, S1 |
     S2;

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

S0: while P do S1 od

S0 ← P, !, S1, S0 |
S0 ←

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

Задача 1

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

Задача 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) ← ;