Унификацией называется операция сравнения (отождествления) нескольких формул, связывающая переменные в составе формул сопоставленными с ними подформулами.
Унификация термов осуществляется в ходе исполнения вызовов предикатов, в момент создания значений недоопределенных множеств, а также во время глобальных операций с общими переменными. Кроме того, унификация термов может быть вызвана явно с помощью встроенного предиката "унифицировать термы":
L == R.
Встроенный предикат '==' разрешается использовать с произвольным количеством аргументов:'=='(V1,...,Vk).
Унификация несвязанной переменной с константой, составным термом или миром вызывает "связывание" этой переменной - замену всех вхождений этой переменной соответствующим элементом данных или миром.
Унификация различных несвязанных переменных вызывает их "сцепление" (отождествление): в дальнейшем любое связывание одной из сцепленных переменных автоматически вызывает такое же связывание всех сцепленных с ней переменных.
В Акторном Прологе область действия операций связывания и сцепления переменной всегда ограничена множеством ее вхождений, принадлежащих некоторым конкретным акторам.
В Акторном Прологе допускается унификация целых и вещественных чисел. Унификация целого и вещественного чисел заканчивается успехом тогда и только тогда, когда вещественное число обозначает целую величину, равную унифицируемому с ней целому числу.
Константы и составные термы несопоставимы между собой (их унификация невозможна). Невозможна также унификация констант и составных термов с экземплярами классов. Унификация термов, обозначающих миры, возможна лишь в том случае, если они обозначают один и тот же мир. Спейсер не может быть унифицирован ни с какой другой константой, кроме себя.
Проверкой вхождения называется специальная операция, осуществляемая в ходе унификации, предотвращающая (запрещающая) связывание переменной с составными термами, содержащими эту переменную. В соответствии с семантикой Акторного Пролога, проверка вхождения не распространяется на переменные в составе миров, являющихся компонентами унифицируемых термов.
В максимальной версии языка в ходе унификации осуществляется проверка вхождения. В быстрой версии проверка вхождения используется только во время глобальных операций с общими переменными. В минимальной версии языка проверка вхождения не используется, однако во время глобальных операций, при обнаружении переменной, связанной с термом, содержащим эту переменную, допускается вызов исключительных ситуаций.
{region:X,name:"Baikal"|Rest1}
{name:Y,object:'lake',region:"Siberia"}
В ходе унификации элементы одного множества будут унифицированы с элементами другого в соответствии с заданными именами элементов. Результатом унификации станут подстановки X="Siberia", Y="Baikal", на месте переменной Rest1 окажется значение G недоопределенного множества, включающего одну-единственную пару object:'lake'. Остальные позиции кортежа G (кроме первой, которая всегда содержит set) будут заполнены z.Ссылки: актор 7.1, встроенный предикат 8, глобальные операции 7.2, данные 3, значение терма 3, имя элемента 3.2.3, исключительная ситуация 7.5, исполнение предиката 6.3.1, константа 3.1, мир 5.1, недоопределенное множество 3.2.3, несвязанная переменная 3.1, переменная 2.1.1, принадлежать актору 7.2, составной терм 3.2, спейсер 3.1, терм 3, число 3.1, элемент множества 3.2.3.
Следующий:
4. СТРУКТУРА ПРОГРАММЫ
Предыдущий:
3.2.3. НЕДООПРЕДЕЛЕННЫЕ МНОЖЕСТВА
3. ОПРЕДЕЛЕНИЕ ДАННЫХ
КОРНЕВАЯ СТРАНИЦА
ОГЛАВЛЕНИЕ
СПИСОК ПОНЯТИЙ ЯЗЫКА (ИНДЕКС)