Откат (поиск с возвратом)( backtracking)

На программу можно взглянуть с логической точки зрения или с процедурной точки зрения.

Цель используется для запуска процесса выполнения программы. Можно рассматривать цель как вызов процедуры. Чтобы цель была доказана, надо, чтобы вызываемая ею процедура была успешно выполнена. Обычно аргументы вызова процедуры – выражения, которые подставляются вместо формальных параметров, являющихся именами переменных. Но Пролог позволяет формальным параметрам самим быть термами. Поэтому процесс вызова “логической” процедуры включает совмещение термов, являющихся аргументами вызова, с термами из заголовков процедур. Этот процесс называется унификацией. Унификация является ключевым компонентом любых алгоритмов вывода в логике первого порядка.

Унификацией называется процесс нахождения наиболее общей подстановки, делающей два терма одинаковыми.

Если унификация оканчивается неудачно из-за того, что никакая подстановка не смогла совместить аргументы вызова и термы заголовков, то вызова не произойдет, но будет сделана попытка совмещения с другим определением процедуры, если оно есть. (Это называется “вызов с поиском по образцу”, или поиск с возвратом).

Можно сказать, что унификация – это взаимное приведение двух структур к общему виду. В результате унификации возникают связи переменных, делающих сравниваемые структуры идентичными. Унификация двух предикатов не обязана быть единственно возможной. В этом случае выбирается наиболее общаяподстановка. Она то и называется унификацией. Применяя принцип резолюции для доказательства цели, мы неизменно используем алгоритм, который всегда приводит к наиболее общемуунификатору( Most General Unifier –MGU-НОУ), или сообщает о невозможности это сделать, если множество – не унифицируемо, то есть если предикаты унифицируемы, то НОУ всегда существует и при этом только один! Если унификатора нет, то вывод невозможен. В процессе работы внутренних унификационных подпрограмм происходит означивание (связывание) переменных.

Замечания:

· если оба значения в момент конкретизации известны, то знак равенства используется как оператор сравнения map=map, и в результате получаем успех, или неуспех, если map=lamp,например;

· Если одно из значений является переменной,то знак равенства может быть как оператором присваивания, так и оператором сравнения.

Например, X=map.Если X была свободная переменная, то присваивание. Если X – означенная переменная, то знак равенства означает сравнение.

В процессе унификации мы находим нужную подстановку.

Подстановкой Q называется множество присваиваний вида X=t, где X-переменная, t-терм. Каждой переменной присваивается не более одного значения. Подстановка, которая привела к тому, что два предиката стали идентичными, называется унификатором.

Например, Unify(P1,P2)=Q, где P1 и P2-предикаты.

Если P1Q=P2Q, тогда Q – унификатор, а P1 и P2- стали идентичными.

Определим, какая подстановка приведет к тому, что предложенные ниже предикаты станут идентичными?

1 Р(1) и Р(1)?

Q={}-?

Q={}-пустое множество, так как нет замены переменных.

Общий пример Р(1)

2 Р(х) и Р(1)?

Q={x:=1}

Общий пример Р(x)Q=P(1)Q=P(1)

3 P(x) и P(y)

Q={x:=y}

Общий пример P(y)

4 P(x,x) P(1,y)

x:=1 y:=x:=1

Q={x:=1,y:=1}

Общий пример P(1,1)

Алгоритм унификации – это основа вычислительной модели ЛП. Он включает в себя связывание вызова с конкретным предложением. Унификация реализует процедуры передачи параметров, выбор варианта(case),создание структуры, доступ к структуре, присваивание переменным конкретного значения во время связывания Переменная становится свободной, когда сопоставление оказывается неуспешным, или цель оказывается успешно выполненной.

Алгоритм унификации основан на решении системы равенств. На вход подают два терма Т1 и Т2 Результат работы алгоритма – так называемый наиболее общий унификатор двух термов, если термы унифицируемы, или отказ, если они не унифицируемы.

Замечание1:

1) Унификация составных объектов:

· с простой переменной - для передачи целого набора значений как единого объекта. Например:

name(“liz”,”petrova”) сопоставляется с X.

X=name(“liz”,”petrova”).

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

name(“liz”,”petrova”) сопоставляется с name(X,Y)

X=liz

Y=petrova

2) использование знака равенства для унификации составных объектов (а не только при сопоставлении цели с заголовком предложения) Фактически Пролог выполняет операции присваивания для унификации объектов по разные стороны знака равенства. Это свойство полезно для нахождения значений аргументов составного объекта.