План лекций (очень подробный), страница 7

a1&...&an. Пусть p - полученное множество хорновских дизъюнктов, а q -

формула, соответствующая запросу. Пару <p,q> будем также называть

программой (или формульным представлением программы).

Декларативная семантика программы - это характеризация (описание

на некотором языке) множества ответов программы без указания алгоритма

их построения (ответ на вопрос: ЧТО вычисляет программа?). Декларатив-

ная семантика Пролога формулируется в терминах логического следования,

а именно: ответом программы <p,q> называется подстановка

б={x1:=t1,...,xn:=tn} термов на места всех переменных q, удовлетворяю-

щая условию: p|=qб. Если подстановка б является пустым множеством

(т.е. q не содержит переменных и p|=q), то ответ б понимается как

"да". Вопрос: если даны p и q, то что можно сказать о б?

Т22 (о главном свойстве наименьшей эрбрановской модели). Пусть Р

- множество хорновских дизъюнктов и атом a является элементом эрбра-

новского базиса bp. Тогда a принадлежит mp <=> p|=a. Д. Множество

дизъюнктов pu{їa} невыполнимо <=> оно ложно во всех эрбрановских ин-

терпретациях <=> формула їa ложна во всех эрбрановских моделях p <=> А

принадлежит mp.

Замечание. t22 утверждает, что 1) Мр - это множество основных

атомов, являющихся теоремами по отношению к системе аксиом p; 2) mp -

это множество запросов q, являющихся основными атомами, на которые

программа <p,q> отвечает "да".

Пусть hpq - множество основных термов, построенных с использова-

нием всех функциональных символов из <p,q>; bpq - множество всех ос-

новных атомов, построенных из предикатов, встречающихся в p и термов,

встречающихся в hpq; mpq - множество основных атомов, образованное по

правилам построения наименьшей эрбрановской модели, но с учетом hpq

вместо hp (т.е. Р* - множество основных примеров дизъюнктов, получен-

ных подстановками термов из hpq в p). Тогда mpq - эрбрановская интерп-

ретация для q.

Т23 (о декларативной семантике). Пусть <p,q> - программа. Если б

- некоторая подстановка термов из hpq на места всех переменных q, то б

является ответом программы <=> mpq |= qб. Д. К множеству Р добавим

"фиктивный" дизъюнкт a(t1,...,tn)>a(t1,...,tn), где термы t1,...,tn

содержат все функциональные символы и константы, входящие в q, но не

входящие в p, а А - предикатный символ, не встречающийся в <p,q>. По-

лученное множество дизъюнктов назовем p'. Пусть б - подстановка из ус-

ловия теоремы. Тогда p|=qб <=> p'|=qб <=> mp'|=qб <=> mpq |= qб (с

учетом тождественной истинности добавленного дизъюнкта, Т22 и правил

построения наименьшей эрбрановской модели).

Замечание. Т23 характеризует не все ответы программы.

$4. sld-резолюция.

Композиция подстановок: операция, сопоставляющая двум последова-

тельным подстановкам - одновременную.

Т24 (о композициях подстановок): тождественная (пустая) подста-

новка является левой и правой единицей; (aб1)б2 = a(б1б2); композиция

ассоциативна. Д. ...

Пусть <p,q> - программа, q±&...&bk&...&bm, cб&...&an>a - эле-

мент p и aб = bkб. Тогда sld-резольвентой с подстановкой б называется

конъюнкция (возможно, "пустая": из 0 элементов) q'б, где q' получается

из q заменой bk на a1&...&an.

sld-последовательностью для программы <p,q> q0

называется последовательность троек (qi,ci,бi), ії

такая что ci - элемент p, qi - sld-резольвента q1———c1, б1

qi-1 и ci c подстановкой бi, q0=q (каждая из ії

формул qi называется текущим запросом). q2———c2, б2

Если qn - пустая конъюнкция, то sld-после- ...

довательность называется sld-выводом программы ії

<p,q>, строящим подстановку б'=б1...бn и вычис- qn———cn, бn

ляющим подстановку б на места всех переменных q,

являющуюся подмножеством б'.

t25 (о корректности sld-резолюции). Если sld-вывод для программы

<p,q> вычисляет б, то б - ответ этой программы. Д.: индукция по длине

вывода.

При построении sld-последовательности может быть фиксировано (для

всех текущих запросов одновременно) некоторое правило выбора bk из

qi±&...&bk&...&bm. А именно, пусть r(m) - функция, сопоставляющая

каждому натуральному числу m натуральное число k: 1<=k<=m. Тогда

sld-последовательность с правилом выбора r есть такая sld-последова-

тельность, в которой на каждом шаге выбирается bk, k=r(m).

t26 (о полноте sld-резолюции с правилом выбора). Если б - ответ

программы <p,q>, то существует sld-вывод этой программы с фиксирован-

ным правилом выбора подцели, вычисляющий подстановку б. Д.: 2 случая:

1) б - подстановка термов из hpq на места всех переменных q - Д. сле-

дует из Т о декларативной семантике; 2) qб содержит переменные - сво-

дится к 1). В случае 1 строится дерево, соответствующее mpq. Разбирая

это дерево (удаляя контрарные пары), получим sld-вывод для программы

<p,q>.

Следствие. sld-резолюция без правила выбора также полна.

Замечание. Можно без потери общности считать фиксированным прави-

ло выбора r(m)=1.

Понятия: наиболее общего унификатора (НОУ); множества рассогласо-

ваний; алгоритма унификации (АУ) (см. Чень, Ли: "Мат. логика и автома-

тическое доказательство теорем").

Т27 (об АУ). Если w - унифицируемое множество выражений, то АУ

выдает сообщение "б - НОУ" и б действительно есть НОУ. Д.: см. Чень,Ли.

sld-последовательность с НОУ есть такая sld-последовательность, в

которой на каждом шаге в качестве унифицирующей подстановки выбирается

НОУ.

Т28 (о полноте sld-резолюции с НОУ). Если sld-вывод для программы

<p,q> вычисляет подстановку б1, то для этой программы существует

sld-вывод с НОУ такой же длины, вычисляющий подстановку б2 = б1 б. Д.:

индукцией по длине вывода. В построенном sld-выводе все "избыточные"

подстановки "сдвигаются" к концу, образуя б.

Замечание. sld-выводы с НОУ строят не все ответы программы.

$5. Процедурная семантика Пролога.

Процедурная (императивная) семантика программы - это описание

процесса построения ее ответов (ответ на вопрос: КАК вычисляет прог-

рамма?). Процедурная семантика Пролога формулируется в терминах поиска

sld-выводов. sld-дерево (дерево вычислений) - это растущее сверху вниз

дерево, каждая ветвь которого - sld-последовательность с правилом вы-

бора r(m)=1 и с НОУ, причем непосредственно ниже каждой тройки

(q,c,б), где q±&...&bn, располагаются все тройки, содержащие прог-

раммные утверждения c1,...,cl, головы которых унифицируемы с b1.

Замечания. 1) sld-дерево содержит все возможные sld-последова-

тельности; 2) ветви sld-дерева могут быть выводами, тупиковыми (не

имеющими продолжений) или бесконечными; 3) каждый sld-вывод (и только

он) вычисляет некоторый ответ программы; 4) престановка программных

утверждений не влияет на конечность/бесконечность дерева и на множест-

во вычисляемых ответов; 5) перестановка атомов в теле программного ут-

верждения влияет на конечность/бесконечность дерева, но не влияет на