Задача унификации

Материал из WikiGrapp
Версия от 15:21, 20 октября 2009; Glk (обсуждение | вклад) (Создана новая страница размером '''Задача унификации''' (''Unification problem'') - По двум описаниям <math>X</math> и <math>Y</math> о...)
(разн.) ← Предыдущая версия | Текущая версия (разн.) | Следующая версия → (разн.)
Перейти к навигации Перейти к поиску

Задача унификации (Unification problem) - По двум описаниям [math]\displaystyle{ X }[/math] и [math]\displaystyle{ Y }[/math] определить, можно ли найти объект [math]\displaystyle{ Z }[/math], который удовлетворяет обоим описаниям.

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

Литература

[Евстигнеев-Касьянов/94]