Полное пространство вычислений

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

Определение 2. Стратегия управления стандартна, если правило вычисления и правило поиска стандартны.

Теоретически программа может иметь вычисления:

Успешные (удачные) – заканчиваются противоречием.

Неудачные – не хватает информации в БЗ.

Незавершенные – неудачное использование предиката отсечения.

Бесконечные – множество резольвент бесконечно.

Определение 3. Полным пространством вычислений называется множество всех вычислений, которое можно получить при помощи операции вызова процедуры, т.е. это перебор всех путей, которые могут иметь различные исходы.

Размеры и структура пространства зависят от стратегии управления. Наглядно пространство вычислений представляют в виде дерева вычислений. Корень дерева – исходное целевое утверждение. Вершины – резольвенты.

Пример. Построить полное пространство вычислений для задачи: получает-стипендию(сидоров)?

? Øполучает-стипендию(сидоров)

|

| {Х:=сидоров}

|

? Ø(студент(сидоров), сессия-сдана(сидоров)).

/\

/ \

Øсессия-сдана(сидоров) Ø(студент(сидоров),

| |

| |

ð. (Да) ð. (Да)

Для данной задачи построено полное множество вычислений, состоящее из 2 ветвей.

Левая ветвь соответствует стандартной стратегии управления.

Почему – последовательное применение резолюций.

Запись Х:=сидоров иллюстрирует замену формального параметра Х фактическим «Сидоров».

Определение 4. Подстановкой Θ (thita) называется множество присваиваний Θ = { Xi=ti | i=1¸n }, где ti- термы-значения.

Каждой переменной присваивается не более 1 терма-значения.

Замечание. В процессе вывода терм-значение может быть переменной величиной. X:=Y.

Существует соглашение: в качестве термов-значений принимать переменные из родительского предложения (из отрицания).

Например, для

Si: Ø(P1(t),P2(t,x)).

Sj: P2(Y,Z):-P3(Z)).

Θ = { Y:=t, Z:=x }.

Определение 5. Обозначим PΘ результат применения подстановки Θ к Р.

Р (рукописная русская Р) = РΘ называется подстановочным примером.

Если Р = Р₁Θ и Р = Р₂Θ то Р называется общим примером, а Θ – унификатором.

Например, для предикатов P(f(T),f(5),T) и P(X, f(Y), Y):

Θ = { X:=f(5), Y=5, T:=5 }, Р = P(f(5), f(5), 5).

В случае применения резолюции используют наиболее общий унификатор (НОУ=MGU). В системах резолютивного вывода НОУ строится автоматически.

Пусть P(t1) – активизированный системный вызов,

P(t2) – выбранная процедура,

t1 = (t11,…,t1n) – кортеж фактических параметров,

t2 = (t21,…,t2n) – кортеж формальных параметров,

Θ – унификатор.

При использовании системой алгоритма унификации Робинсона данными для алгоритма являются списки:

l1- список фактических параметров t1, l2 список формальных параметров t2, Θ – пустой список.

В процессе доказательства Θ наполняется присваиваниями вида { t2i:=t1i }.

Результатом алгоритма является НОУ – заключительное состояние списка Θ.

Алгоритм Робинсона циклический. Рассмотрим описание i- го шага.

1. Если t1i – переменная, не входящая в t2i, то Θ = Θ È { t1i:=t2i }.

2. Если t2i – переменная, не входящая в t1i, то Θ = Θ È { t2i:=t1i }.

3. Если t1i = (a1,…,am) и t2i = (b1,…,bm), то формируются множества {ai:=bi} или {bi:=ai} и присоединяются к Θ; L1È={ai}, L2È={bi}

4. Если t1i, t2i – одинаковые константы или одинаковые переменные,

то Θ, L1, L2 не обновляются и выполняется переход к шагу i+1.

5. В остальных случаях – работа алгоритма заканчивается.

Принцип резолюции для общего случая (предикаты ЛП содержат переменные и константы).

S1: Ø(A₁, …, A_k-1, A_k, A_k+1,…, A_n).

S2: А_k (консеквент) ¬ В₁, …, В_m (антеценденты).

Допустим, предложения S1, S2 содержат переменные, тогда с учетом спецификаций для выполнения шага вывода требуется:

1. Заменить общие переменные S1, S2 на новые (обычно переименовываются в S2).

2. Выбрать в S1 предикат, у которого предикатный символ совпадает с консеквентом в S2. Если такого предиката в S1 нет, то шаг вывода невозможен.

3. Найти НОУ Θ для Ak из S1 и S2. Если Ø$ Θ, то шаг вывода невозможен.

4. Построить резольвенту.

5. Применить Θ к резольвенте.