3.3Унификация термов



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

Унификация термов осуществляется в ходе исполнения вызовов предикатов, в момент создания значений недоопределённых множеств, а также во время глобальных операций с общими переменными. Кроме того, унификация термов может быть вызвана явно с помощью встроенного предиката «унифицировать термы»:

L== R.

Встроенный предикат '==' разрешается использовать с произвольным количеством аргументов:

'==(V1.....Vk).

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

Унификация различных несвязанных переменных вызывает их «сцепление» (отождествление): в дальнейшем любое связывание одной из сцепленных переменных автоматически вызывает такое же связывание всех сцепленных с ней переменных.

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

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

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

Проверкой вхождения называется специальная операция, осуществляемая в ходе унификации, предотвращающая (запрещающая) связывание переменной с составными термами, содержащими эту переменную. В соответствии с семантикой Пролога, проверка вхождения не распространяется на переменные в составе миров, являющихся компонентами унифицируемых термов.

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

Пример.
Унификация двух составных термов:

{region:X,name:" Baikal" | Restl} {name:Y,object:' lake', region: "Siberia"}

В ходе унификации элементы одного множества будут унифицированы с элементами другого в соответствии с заданными именами элементов. Результатом унификации станут подстановки X="Siberia", Y="Baikal", на месте переменной Restl окажется значение G недоопределённого множества, включающего одну-единственную пару object:'lake'. Остальные позиции кортежа G (кроме первой, которая всегда содержит set) будут заполнены z.



Содержание