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

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

Любому отношению можно сопоставить некоторое множество, и считать, что предикат проверяет, что кортеж из его аргументов принадлежит этому множеству. Множество всех отношений, определенных в программе, обозначим через `P`. Будем считать, что оно включает в себя также и все встроенные предикаты, на которые имеются ссылки в программе. Для удобства также будем считать, что запрос `G` содержит только одну цель, то есть имеет вид "?–`g(t)`", где `t` – это кортеж из `n` термов `(t_1,…,t_n)`. Логическую программу можно представить как пару `(P,G)`.

Спецификацией программы `S` является любое множество определений, которое точно задает содержимое каждого из отношений, встречающихся в программе, и, в частности, отношения в `G`. Это отношение будем называть основным специфицируемым отношением и обозначать как `R^{**}`.

Если `G` – это ?–подмнож([W,a],[a,b,c]), то `R^{**}="подмнож"`. Спецификация должна определить, какие кортежи из двух термов принадлежат отношению подмнож, а какие – нет. Если предикат подмнож(X,Y) означает, что множество X есть подмножество Y, то в запросе `G` спрашивается, для каких W множество {W,a} является подмножеством {a,b,c}. В данном случае `G` выделяет некоторое подотношение (интервал) относительно `R^{**}`, а именно {([a,a],[a,b,c]), ([b,a],[a,b,c]), ([c,a],[a,b,c])}. Другие кортежи из `R^{**}`, например, ([b],[b,d]), не запрашиваются `G`, и не принадлежат выделенному `G` интервалу.

Интервал, выделяемый запросом `G`: ?–`R^{**}(t)`, есть множество `{tΘ\ |\ tΘ∈R^{**}}` решений `G`, соответствующих спецификации `S`, причем каждое решение образуется подстановкой `Θ` в кортеж термов `t`. Этот интервал пуст, если `G` не имеет решений. Так как решение должно удовлетворять `S`, будем называть `tΘ` специфицируемым решением `G`.

Вычисляемое отношение программы `(P,G)` – это множество всех тех решений `G`, которые вычисляются из программы с помощью определений `P`. Это отношение обозначим через `R`, а решение из `R` назовем вычисляемым решением. Если решение `tΘ` не содержит переменных, оно принадлежит `R`, иначе его можно рассматривать как общее обозначение для всех подстановочных примеров, не содержащих переменных и принадлежащих `R`. Если вычисляемое отношение пусто, то программа неразрешима. Решение `tΘ` для запроса `G` вычислимо с помощью `P` тогда и только тогда, когда из `P` можно вывести `R^{**}(tΘ)`, используя, например, метод резолюции. Таким образом, `R={tΘ|\ P\ ⊨R^{**}(tΘ)}`.

Каждое вычисляемое программой решение должно быть правильно относительно данной спецификации. Это свойство называется частичной правильностью программы. Каждое решение, приписываемое запросу спецификацией, должно быть вычислимо с помощью программы. Это свойство называется полнотой программы. Если выполняются оба эти свойства, программа называется полностью правильной.

Если сама спецификация `S` записана на языке логики предикатов, то `R^{**}={T\ |\ S\ ⊨R^{**}(T)}`, где `T` – произвольный кортеж из `n` термов, а интервал `G` относительно спецификации `S` есть множество `{tΘ\ |\ S\ ⊨R^{**}(tΘ)}`.

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

Можно сказать также, что множество определений `P` является полным для `G`, то есть определений из `P` достаточно для вычисления всех решений из выделенного `G` интервала. Если `P` не является `G`-полным, это значит, что `P` содержит недостаточно информации о специфицируемом отношении `R^{**}`.

Множество определений `P` является полным относительно спецификации `S` тогда и только тогда, когда для всех `T`, если `S\ ⊨R^{**}(T)`, то `P\ ⊨R(T)`, то есть `P` полно для всех запросов, в том числе и для наиболее общей цели `G^{**}`: ?–`R^{**}(t)`, где `t` – кортеж из `n` различных переменных.

Если программа не является полностью правильной, то либо она вычисляет неверные решения, то есть содержит неверные представления о проблемной области, либо не в состоянии вычислить какое-либо правильное решение, то есть содержит недостаточно информации о проблемной области.

Рассмотрим следующую программу.

?-умножить(4,6,Z).
умножить(X,3,X).
умножить(W,2,24).
умножить(X,6,Z):-умножить(X,3,W),умножить(W,2,Z).

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

Если `S⊨P`, то программа `(P,G)` частично правильна относительно `S`.

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

Программа `(P,G)` является разрешимой, если с ее помощью вычисляется, по крайней мере, одно решение. Разрешимость не связана со спецификацией.

Для проверки разрешимости можно попытаться исполнить программу, но в принципе при исполнении разрешимой программы может быть и не получено решений, так как получение решений зависит от способа исполнения. Иногда разрешимость программы можно установить путем анализа спецификации `S`.

Пусть программа `(P,G)` является полной, тогда `(P,G)` является разрешимой, если `∃Θ\ S\ ⊨R^{**}(tΘ)`. Пусть программа `(P,G)` является частично правильной, тогда `(P,G)` неразрешима, если `∀Θ\ S\ ⊨¬R^{**}(tΘ)`.