Математическая Логика, 07 семинар (от 19 декабря)
Материал из eSyr's wiki.
(Содержимое страницы заменено на «== From Ebaums Inc to MurkLoar. == We at EbaumsWorld consider you as disgrace of human race. Your faggotry level exceeded any imaginab...») |
(Отмена правки № 1338 участника 91.121.7.211 (обсуждение)) |
||
| Строка 1: | Строка 1: | ||
| - | == | + | [[Математическая Логика, 06 семинар (от 05 декабря)|Предыдущий семинар]] | Следующий семинар |
| - | + | ||
| - | + | == Оператор отсечения «!» === | |
| - | + | ||
| + | Оператор отсечения указывает, какие ветви не должны проходиться при откате при SLD-резолюции. Имеет следующий смысл: | ||
| + | * A<sub>0</sub> ← A<sub>1</sub>, …, A<sub>k</sub>, !, A<sub>k + 1</sub>, …, A<sub>n</sub> — проверить A<sub>1</sub>, …, A<sub>k</sub> и использовать A<sub>k + 1</sub>, …, A<sub>n</sub> | ||
| + | |||
| + | Символ «!» обычно обозначает требование единственности, поэтому он и выбран, так как доказательство строится единственным возможным способом. | ||
| + | |||
| + | [[Image:Exclamation.png|thumb|400px|Как работает предикат отсечения]] | ||
| + | Пусть у нас выполняются SLD-вычисления, в результате которых в качестве тела одной из подстановок мы имеем список подцелей, содержащих «!». Как только интерпретатор получает запрос в качестве SLD-резольвенты, он ставит у предыдущего запроса «(*», после чего вычисления продолжаются обычным образом, до тех пор, пока «!» не станет самоц левой подцелью. После чего он ставит вторую пометку, «!» убирается из списка подцелей и вычисления продолжаются дальше. Когда делается откат с G<sub>4</sub>, он делается до G<sub>1</sub> и вычисления продолжаются дальше. При этом также не проходятся другие ветви. Это делается для того, чтобы повысить эффективность порграммы. Также это позволяет организовывать программные конструкции. | ||
| + | S<sub>0</sub>: if P then S<sub>1</sub> else S<sub>2</sub> | ||
| + | |||
| + | S<sub>0</sub> ← P, !, S<sub>1</sub> | | ||
| + | S<sub>2</sub>; | ||
| + | Если P истинно, то задача решается только методом S<sub>1</sub> иначе S<sub>2</sub>. | ||
| + | |||
| + | S<sub>0</sub>: while P do S<sub>1</sub> od | ||
| + | |||
| + | S<sub>0</sub> ← P, !, S<sub>1</sub>, S<sub>0</sub> | | ||
| + | S<sub>0</sub> ← | ||
| + | Если условие P истинно, то решается S<sub>1</sub> и снова S<sub>0</sub>, если же P ложно, то S<sub>0</sub> считается решённой. | ||
| + | |||
| + | === Задача 1 === | ||
| + | Вычислить ответы на запрос G : ? A(x) к программе П | ||
| + | A(y) ← B(y), C(a<sub>2</sub>, y); | ||
| + | A(x) ← D(a<sub>1</sub>, x), C(x,y); | ||
| + | B(u) ← D(u, v), !, E(v); | ||
| + | B(v) ← E(a<sub>5</sub>); | ||
| + | E(a<sub>2</sub>) ← ; | ||
| + | E(a<sub>3</sub>) ← ; | ||
| + | E(z) ← ; | ||
| + | D(u, a<sub>1</sub>) ← C(u, f(u)); | ||
| + | D(u, u) ← ; | ||
| + | D(x, a<sub>2</sub>) ← ; | ||
| + | C(z, a<sub>3</sub>) ← ; | ||
| + | |||
| + | === Задача 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) ← ; | ||
| + | |||
| + | {{Математическая Логика}} | ||
Текущая версия
Предыдущий семинар | Следующий семинар
Содержание |
[править] Оператор отсечения «!» =
Оператор отсечения указывает, какие ветви не должны проходиться при откате при 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) ← ;
|
|
Ссылки
Официальная страница курса | Задачи
Проведение экзамена | Решение задач: Решение задач методички | Решение задач варианта экзамена 2004 года | Алгоритмы решения задач
