Сравнение неосновных термов

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

Для этой проверки в Прологе имеется системный предикат ==/2. Цель (X = = Y)? выполнена, если Х и Y – идентичные константы, идентичные переменные или структуры с одним и тем же главным функтором и одинаковой арностью, а для соответствующих аргументов Xи Y структур Х и Y соотношение X= =Y выполняется рекурсивно. В противном случае цель (X = = Y) не выполнена. Например, цель (X = =5) не выполнена (в отличие от цели Х = 5).

Имеется также системный предикат, значение которого противоположно значению предиката = =. Цель Х \ = = Y? выполнена в тех случаях, когда Х и Y не являются идентичными термами.

Предикат \ = == может быть использован в определении отношения not_occurs_in( Sub, Term), истинного, если терм Sub не входит в терм Term. Данное отношение требуется для построения алгоритма унификации с проверкой на вхождение. Предикат not_occurs_in (Sub, Term) является металогическим предикатом, анализирующим структуру. Он используется в реализующей унификацию с проверкой на вхождение программе 10.6, варианте программы 10.5.

unify (Termi, Term2)

Term1 и Term2 унифицируемы с проверкой на вхождение.

unify (X,Y)

var(X), var(Y), X = Y.

unify (X,Y)

var(X), nonvar(Y), not_occurs_in(X,Y), X = Y.

umfy(X,Y)

var(Y), nonvar(X), not_occurs_in(X,Y), Y = X.

unify (X,Y)

nonvar(X), nonvar(Y), constant(X), constant(Y), X = Y.

unify (X,Y)

nonvar(X), nonvar(Y), compound(X), compound(Y),

term„unify(X,Y).

not_occurs_in(X,Y)

var(Y),X\= =Y.

not occurs in (X,Y)

nonvar(Y), constant (Y).

not_occurs_in(X,Y)

nonvar(Y), compound (Y), functor(Y,F,N),

not_occurs_in(N, X, Y).

not_occurs_in(N,X,Y)

N > 0, arg(N,Y,Arg), not_occurs_m(X,Arg), Nl: = N - 1,

not occurs in(N 1 ,X,Y).

not_occurs_in (0, X, Y)

.

term_unify(X,Y) См. программу 10.5.

Программа 10.6. Алгоритм унификации с проверкой на вхождение.

Заметим, что при определении предиката not_occurs_in область определения не ограничена основными термами. Снять подобное ограничение в случае программы 9.2, задающей отношение Subterm, не так просто. Рассмотрим вопрос Subterm (Х,У)?. Он успешно решается программой 9.2 сопоставлением переменной Х терма У

Определим металогический предикат occurs_in (Sub. Term) обладающий требуемыми свойствами.

Наличие предиката = = позволяет использовать программу 9.2, задающую предикат Subterm как основу определения предиката occurs_in. Механизм возврата порождает все подтермы данного терма, и каждый подтерм проверяется на совпадение с переменной. Записью программы является программа 10.7(а).

occurs Jn (Suh, Term)

Sub является подтермом (возможно, неосновного) терма Term.

а: С использованием предиката = =

occurs_.in(X,Term) 

subterm (Sub, Term), X = = Sub.

в: С использованием предиката freeze

occurs_in(X,Term) 

freeze(X,Xf), freeze(Term, Termf),

subterm (Xf, Termi). subterm (X, Term) См. программу 9.2.

Программа 10.7. Вхождение.

Исходное определение предиката Subterm корректно только для основных термов. Однако добавление типовых металогических тестов, подобных использованным при определении отношения no_occurs_in в программе 10,6, позволяет легко преодолеть это затруднение.