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

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

[[Математическая Логика, 06 семинар (от 05 декабря)|Предыдущий семинар]] | Следующий семинар

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

Оператор отсечения указывает, какие ветви не должны проходиться при откате при SLD-резолюции. Имеет следующий смысл:
* A0 &larr; A1, &hellip;, Ak, !, Ak + 1, &hellip;, An — проверить A1, &hellip;, Ak и использовать Ak + 1, &hellip;, An

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

[[Image:Exclamation.png|thumb|400px|Как работает предикат отсечения]]
Пусть у нас выполняются SLD-вычисления, в результате которых в качестве тела одной из подстановок мы имеем список подцелей, содержащих «!». Как только интерпретатор получает запрос в качестве SLD-резольвенты, он ставит у предыдущего запроса «(*», после чего вычисления продолжаются обычным образом, до тех пор, пока «!» не станет самоц левой подцелью. После чего он ставит вторую пометку, «!» убирается из списка подцелей и вычисления продолжаются дальше. Когда делается откат с G4, он делается до G1 и вычисления продолжаются дальше. При этом также не проходятся другие ветви. Это делается для того, чтобы повысить эффективность порграммы. Также это позволяет организовывать программные конструкции.
 S0: if P then S1 else S2
 
 S0 &larr; P, !, S1 |
 S2;
Если P истинно, то задача решается только методом S1 иначе S2.

S0: while P do S1 od
 
 S0 &larr; P, !, S1, S0 |
 S0 &larr;
Если условие P истинно, то решается S1 и снова S0, если же P ложно, то S0 считается решённой.

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

=== Задача 2.1 ===
Вычисления наибольшего из двух чисел.
 ? max(x,y,z)

==== Решение ====
Если писать а императивном языке, то получим
 if x &ge; y then z = x else z = y
Тогда, путём прямой трансляции:
 max(x, y, z) &larr; x &ge; y, !, z = x;
 max(x, y, z) &larr; z = y;
Можно оптимизировать:
 max(x, y, y) &larr; x &lt; y, !;
 max(x, y, z) &larr; ;

=== Задача 2.3 ===
Вычисления объединения L3 множеств L1 и L2, представленных бесповторными списками.
 ? cup(L1, L2, L3)

==== Решение ====
 cup(L1, nil, L1) &larr; ;
 cup(L1, x . L2, L3) &larr; elem(x, L1), !, cup(L1, L2, L3)
 cup(L1, x . L2, x . L3) &larr; cup(L1, L2, L3);
Учитывая, что в объединении все элементы первого множества, то нужно позабодиться о том, чтобы там не повторялись элементы из второго списка, см. правило 2.

=== Задача 2.6 ===
Вычисления всех элементов целочисленного списка L1, квадраты которых не содержатся в этом списке.
 ? nonsquare(L1, L2)

==== Решение ====
Неправильное решение:
 nonsquare(nil, nil) &larr; ;
 nonsuare(x . L1, L2) &larr; z is x &times; x, elem(z, L1), !, nonsquare(L1, L2);
 nonsquare(x . L1, x . L2) &larr; nonsquare(L1, L2);
Неправильность легко проверяется на списке 4 . 2 . 1 . nil. 4 — подходит, идём дальше. 2 — подходит (так как проверка идёт на списке 2 . 1 . nil), но не должно. Ошибка. необходимо ввести дополнительный предикат. Правильное решение: 
 nonsquare(L1, L2) &larr; nonsq(L1, L1, L2);
 nonsq(L0, x . l1, L2) &larr; z is x &times; x, elem(z, L0), !, nonsq(L0, L1, L2);
 nonsq(L0, x . L1, x . L2) &larr;  nonsq()L0, L1, L2);
 nonsq(L, nil, nil) &larr; ;

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.us/wiki/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0%2C_07_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_19_%D0%B4%D0%B5%D0%BA%D0%B0%D0%B1%D1%80%D1%8F%29

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

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 41: / Строка 41: @@
 ==== Решение ====
-Если писать на императивном языке, то получим
+Если писать а императивном языке, то получим
  if x &ge; y then z = x else z = y
 Тогда, путём прямой трансляции: