<<
>>

Унификация

Унификация — это процесс, в котором для достижения совпадения с образцом (в ходе резолюции) выполняется конкретизация переменных, то есть их связывание со значениями. В результате двум термам придается одинаковый смысл.
Базовым выражением, смысл которого определен унификацией, является выражение эквивалентности: в языке Prolog цель б = 1 пытается унифицировать термы б и 1. Цель достигается (считается истиной), если унификация оказывается успешной, и терпит неудачу в противном случае. Таким образом, мы можем изучить унификацию в языке Prolog, экспериментируя с эффектом эквивалентности:

Язык Prolog

663

На основе экспериментов сформулируем следующие правила унификации для системы Prolog:

1. Константа унифицируется лишь сама с собой: me = me успех, но me = you отказ.

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

3. Структурированный терм (например, функция, применяемая к аргументам) унифицируется с другим термом только тогда, когда у него такое же имя функции, такое же число аргументов и аргументы могут быть рекурсивно унифицированы. Например, f(a, X) унифицируется с f(Y, b), с конкретизацией b для X и а для Y.

Вариация для второго правила, когда унифицируются две неконкретизированные переменные, имеет вид:

?- X = Y.

X = _23 Y = _23

Число 23 в данном случае ассоциируется с областью памяти, зарезервированной для этой переменной. Таким образом, унификация приводит к тому, что неконкретизированные переменные начинают совместно использовать память (то есть становятся алиасами друг для друга).

Унификация в Prolog позволяет получить очень короткие выражения для многих операций.

Создадим пару Prolog-программ для операций append и reverse над списками. Поскольку в языке Prolog список можно представлять термом, таким как [X | Y], где X и Y — переменные, здесь нет нужды возвращать голову или хвост списка с помощью встроенной функции. Достаточно установить [X|Y] = [1, 2, 3], и неконкретизированные переменные X и Y вернут заголовок как X, а хвост как Y за счет унификации. Если нужно добавить к списку [ 1, 2, 3 ], скажем, 0, мы просто пишем [ 0 | [1,2,3] ]; например:

?- X = [0|[1, 2, 3]].

X = [0, 1, 2, 3]

Таким образом, мы можем использовать переменные в терме как входные или как выходные параметры, а формулы языка Prolog могут «запускаться» как назад, так и вперед, хотя процедурная интерпретация формул Хорна не говорила нам об этом! Действительно, унификация может использоваться, чтобы сократить выражения. Начиная с того места, где стоит операция =, мы позволяем резолюции вызывать унификацию автоматически, записывая образцы, прямо унифицируемые в параметрах головы. Например, можно записать: cons(X, Y, [X|Y])

Появление образца [X|Y] вместо третьей переменной автоматически унифицирует его с переменной, используемой в этом месте цели. Этот процесс можно назвать как вызов, направленный на образец.

Теперь запишем процедуру append: append(X, Y, Z) :- X = [], Y = Z. append(X,Y,Z) :-

X = [A|B], Z = [A|W], append(B, Y, W).

664

Глава 21. Логическое программирование

Первая формула заявляет, что добавление любого списка к пустому списку просто воспроизводит тот же список. Вторая формула утверждает, что добавление списка с головой А и хвостом В к списку У дает список, головой которого также является А, а хвост — это В с добавленным У.

Перезаписывая это с помощью вызова, направленного на образец, получаем чрезвычайно краткую форму: аррепС([], У, Y).

аррепС([А|В], У, [А|Ы]) :- аррепС(В, У, Ы).

Подобное добавление может выполняться и с другой стороны. При формировании конкретного списка оно способно обнаружить все способы добавления для двух списков:

Prolog использует первую формулу и сопоставляет X пустому списку [], а У — конечному списку. Затем он продолжает поиск решений с помощью второй формулы, сопоставляя X с [А|В] и устанавливая подцель аррепС(В, У, Ы) при Ы = [2]. Далее поиск начинается снова с В вместо X. Таким образом, В сначала сопоставляется с [] а У с [2], формируя X = [1 | []] = [1]. Затем В сопоставляется с новым [А|В] по второй формуле и т. д.

В заключение дадим определение в языке Prolog для реверса списка: ^е^е([],[]).

reverse([H|T], L) :- reverse(T, L1), аррепС^1, [Н], L).

<< | >>

Еще по теме Унификация:

  1. 4. Международная унификация права
  2. 3. Унификация и гармонизация законодательства Скандинавских стран
  3. Тема 4. Функции сравнительного правоведения
  4. Тема 9. Правовые системы Скандинавских стран
  5. 2.4.
  6. 1.3.5.
  7. 2.1.
  8. 1. Сущность хранения на товарном складе
  9. 4.6.
  10. 2. Сравнительное правоведение и международное частное право
  11. 1.1.2.
  12. 1.3.
  13. 3. Основные тенденции развития обязательственного права
  14. 4. Особенности современного американского права
  15. 1. Сравнительное правоведение и международное публичное право