Аноним

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

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


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