Логическое программирование

Логический алгоритм получается в результате выбора некоторой управляющей стратегии `C` для выполнения программы `(P,G)` и обозначается тройкой `(P,G,C)`.

Целью исполнения программы является порождение вычислений `Gamma`. Каждое вычисление представляет собой последовательность целей, начинающееся с исходной цели программы `G`. Вычисление `Gamma` является производимым из программы `(P,G)` при управлении C тогда и только тогда, когда исполнение `(P,G,C)` порождает каждую цель из `Gamma` за конечное число шагов; в противном случае вычисление `Gamma` называют непроизводимым при управлении `C`.

Вычисляемое решение `T` является производимым из программы `(P,G)` при управлении `C` тогда и только тогда, когда оно вычисляется некоторым производимым при `C` вычислением (т.е. решение `T` вычислимо за конечное время); в противном случае решение `T` называют непроизводимым.

Существует разница между тем, что логически вычислимо, и тем, что действительно вычислимо, когда программа исполняется конкретным способом. Возможность существования логически вычислимых решений, не являющихся производимыми, появляется всякий раз, когда стратегия управления несправедлива, то есть ее внимание не распределяется поровну между всеми имеющимися вычислениями. Последовательная стратегия поиска в глубину неизбежно несправедлива в силу того, что она обязана построить до конца текущее вычисление, прежде чем перейти к следующему. Стратегия поиска в ширину справедлива и все конечные вычисления (а, следовательно, и все вычисляемые решения) порождаются за конечное время. Но стратегия поиска в ширину не работает, если появляются встроенные предикаты, которые ведут себя так, как будто они реализованы бесконечным множеством фактов.

Вычисляемые решения могут стать непроизводимыми также, если управление `C` будет удалять вычисления в ходе выполнения программы (например, с помощью предикатов отсечения и удаления утверждений). Это эквивалентно стратегии неполного поиска, когда не все логические возможности программы `(P,G)` исследуются.

Завершаемость является простым понятием при традиционном программировании, так как оно предполагает единственно возможное вычисление и программа завершается в том и только том случае, когда это вычисление конечное. Сложнее определить завершаемость для логических программ, предполагающих несколько вычислений.

Исполнение `(P,G,C)` завершается тогда и только тогда, когда оно дает конечное множество вычислений, причем все они имеют конечную длину.

Введем обозначение `A⊢_C\ B`, означающее, что формула `B` выводима из формулы `A` с помощью резолюции, управляемой стратегией `C`. В частности, `P\ ⊢_C\ R^{**}(tΘ)` означает, что решение `tΘ` для цели `G`: ?–`R^{**}(t)` является производимым при управлении `C`.

Верификацию алгоритмов можно упростить, используя достаточные условия.

Для верификации программы будем использовать следующий критерий.

Рассмотрим программу

?-подмнож([W,a],[a,b,c]).                         % G
подмнож([],Y).                                    % P1
подмнож([A|X],Y):-принадлежит(A,Y),подмнож(X,Y).  % P2
принадлежит(A,[A|Z]).                             % P3
принадлежит(A,[B|Z]):-принадлежит(A,Z).           % P4

Спецификация S для нее состоит из следующих формул на языке логики предикатов:

`S_1`: `"подмнож"(x,y)⇔∀u\ (u∈x\ ⇒\ u∈y)`

`S_2`: `u∈x\ ⇔\ ∃v∃z\ (z=x\\v\ ∧\ (u=v\ ∨\ u∈z))`

`S_3`: `x=∅\ ⇔\ ¬∃v∃z(z=x\\v)`

Для вывода будем использовать следующие правила.

Если `S\ ⊨R⇔D_1` и `S\ ⊨D_1⇔D_2`, то `S\ ⊨R⇔D_2`.

Если `D_n` является дизъюнкцией `B_1∨…∨B_m`, то из `S` следует набор из `m` клауз:

…

Утверждения для отношения "подмнож" можно вывести так:

`D_1`: `∀u\ (u∈x\ ⇒\ u∈y)`

`D_2`: `∀u\ (∃v∃z\ (z=x\\v\ ∧\ (u=v\ ∨\ u∈z))\ ⇒\ u∈y)`

`D_3`: `¬∃v∃z(z=x\\v)\ ∨\ ∃v∃z\ (z=x\\v\ ∧\ ∀u\ ((u=v\ ∨\ u∈z)\ ⇒\ u∈y))`

`D_4`: `x=∅\ ∨\ ∃v∃z\ (z=x\\v\ ∧\ ∀u\ (u=v\ ⇒\ u∈y)\ ∨\ ∀u\ (u∈z\ ⇒\ u∈y))`

`D_5`: `x=∅\ ∨\ ∃v∃z\ (z=x\\v\ ∧\ v∈y\ ∧\ "подмнож"(z,y))`

Последняя формула дает клаузы, эквивалентные утверждениям на Прологе:

`P_1`: `"подмнож"(x,y)\ ←\ x=∅`

`P_2`: `"подмнож"(x,y)\ ←\ x=[v|z],\ v∈y,\ "подмнож"(z,y)`

Аналогично можно вывести утверждения для отношения "принадлежит":

`D_1`: `∃v∃z\ (z=x\\v\ ∧\ (u=v\ ∨\ u∈z))`

`D_2`: `∃v∃z\ ((z=x\\v\ ∧\ u=v)\ ∨\ (z=x\\v\ ∧\ u∈z))`

`P_3`: `u∈x\ ←\ x=[u|z]`

`P_4`: `u∈x\ ←\ x=[v|z],\ u∈\ z`

Таким образом, `S\ ⊨P`, а множество определений `P` является полным. Следовательно, программа `(P,G)` полностью правильна, и правильность не зависит от цели `G`.

Доказательство завершаемости `(P,G,C)` можно установить с помощью неформальных рассуждений. При рекурсивном обращении к предикатам "подмнож" и "принадлежит" один из аргументов уменьшается в размерах, поэтому исполнение программы не может привести к бесконечным вычислениям. Следовательно, исполнение завершается при любой исчерпывающей стратегии.

Этот метод верификации не всегда приводит к успеху, так как множество определений `P` может быть не полным или не следовать из спецификации. Тогда требуется тщательное рассмотрение конкретного запроса и конкретной стратегии управления.