Задача унификации: различия между версиями
Перейти к навигации
Перейти к поиску
Glk (обсуждение | вклад) (Создана новая страница размером '''Задача унификации''' (''Unification problem'') - По двум описаниям <math>X</math> и <math>Y</math> о...) |
KEV (обсуждение | вклад) Нет описания правки |
||
| (не показана 1 промежуточная версия этого же участника) | |||
| Строка 1: | Строка 1: | ||
'''Задача унификации''' (''Unification problem'') | '''Задача унификации''' (''[[Unification problem]]'') — По двум описаниям <math>X</math> и <math>Y</math> определить, можно ли найти объект <math>Z</math>, который удовлетворяет обоим описаниям. | ||
По двум описаниям <math>X</math> и <math>Y</math> определить, можно ли найти | |||
объект <math>Z</math>, | |||
который удовлетворяет обоим описаниям. | |||
Обычно уточняется как | Обычно уточняется как задача нахождения по данным двум ''[[терм|термам]]'', содержащим переменные, такой подстановки термов вместо переменных, которая превратила бы исходные термы в идентичные. В том случае, когда такая подстановка для термов существует, она называется ''[[унификатор|унификатором]]'', а термы называются ''[[унифицируемый терм|унифицируемыми]]''. | ||
задача нахождения по данным двум ''термам'', содержащим | Если термы унифицируемы, то у них может быть много унификаторов, но всегда существует и единствен | ||
переменные, такой подстановки термов вместо переменных, | ''наибольший общий унификатор'', из которого с помощью композиций подстановок можно получить все другие унификаторы. | ||
которая превратила бы исходные термы в идентичные. В том | |||
случае, когда такая подстановка для термов существует, она | |||
называется ''унификатором'', а термы называются ''унифицируемыми''. | |||
Если термы унифицируемы, то у них может быть много | |||
унификаторов, но всегда существует и единствен | |||
''наибольший общий унификатор'', из которого с помощью композиций | |||
подстановок можно получить все другие унификаторы. | |||
==Литература== | ==Литература== | ||
* Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994. | |||
Текущая версия от 14:54, 18 февраля 2011
Задача унификации (Unification problem) — По двум описаниям [math]\displaystyle{ X }[/math] и [math]\displaystyle{ Y }[/math] определить, можно ли найти объект [math]\displaystyle{ Z }[/math], который удовлетворяет обоим описаниям.
Обычно уточняется как задача нахождения по данным двум термам, содержащим переменные, такой подстановки термов вместо переменных, которая превратила бы исходные термы в идентичные. В том случае, когда такая подстановка для термов существует, она называется унификатором, а термы называются унифицируемыми. Если термы унифицируемы, то у них может быть много унификаторов, но всегда существует и единствен наибольший общий унификатор, из которого с помощью композиций подстановок можно получить все другие унификаторы.
Литература
- Евстигнеев В.А., Касьянов В.Н. Теория графов: алгоритмы обработки деревьев. — Новосибирск: Наука. Сиб. отд-ние, 1994.