Задача унификации: различия между версиями

Материал из WEGA
Перейти к навигации Перейти к поиску
(Создана новая страница размером '''Задача унификации''' (''Unification problem'') - По двум описаниям <math>X</math> и <math>Y</math> о...)
 
Нет описания правки
Строка 1: Строка 1:
'''Задача унификации''' (''Unification problem'') -  
'''Задача унификации''' (''[[Unification problem]]'') - По двум описаниям <math>X</math> и <math>Y</math> определить, можно ли найти объект <math>Z</math>, который удовлетворяет обоим описаниям.
По двум описаниям <math>X</math> и <math>Y</math> определить, можно ли найти
объект <math>Z</math>,
который удовлетворяет обоим описаниям.


Обычно уточняется как
Обычно уточняется как задача нахождения по данным двум ''[[терм|термам]]'', содержащим переменные, такой подстановки термов вместо переменных, которая превратила бы исходные термы в идентичные. В том случае, когда такая подстановка для термов существует, она называется ''[[унификатор|унификатором]]'', а термы называются ''[[унифицируемый терм|унифицируемыми]]''.
задача нахождения по данным двум ''термам'', содержащим
Если термы унифицируемы, то у них может быть много унификаторов, но всегда существует и единствен
переменные, такой подстановки термов вместо переменных,
''наибольший общий унификатор'', из которого с помощью композиций подстановок можно получить все другие унификаторы.
которая превратила бы исходные термы в идентичные. В том
случае, когда такая подстановка для термов существует, она
называется ''унификатором'', а термы называются ''унифицируемыми''.
Если термы унифицируемы, то у них может быть много
унификаторов, но всегда существует и единствен
''наибольший общий унификатор'', из которого с помощью композиций
подстановок можно получить все другие унификаторы.
==Литература==
==Литература==
[Евстигнеев-Касьянов/94]
[Евстигнеев-Касьянов/94]

Версия от 18:03, 20 октября 2009

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

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

Литература

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