Структуры данных и модели вычислений
Через обозначим результат подстановки термов
Подстановкой называется набор пар , где — переменные, а — термы.
Через обозначим результат подстановки термов в выражение вместо переменных .
Пусть — еще одна подстановка. Композиция двух подстановок и
определяется следующим образом: Подстановка может быть вычислена следующим образом. Составим из подстановок и последовательность
и проведем следующие две операции:
- Если некоторое совпадает с некоторым , то вычеркиваем пару .
- Если , то вычеркиваем пару .
Пример.
Пусть . Рассмотрим последовательность и по первому правилу вычеркиваем пары и , затем по второму правилу — пару . В результате получим
Подстановка называется унификатором термов , , если .
Наиболее общим унификатором термов ,
называется подстановка , такая, что любой другой их унификатор представляется в виде .
Пример.
Для термов , унификатором будет подстановка Будет ли она наиболее общим унификатором?
Пример.
Для термов и
наиболее общим унификатором будет подстановка . Результатом унификации будет терм
