<aside> 💡 Унификация — приведение чего-либо к единообразной системе или форме. Мы рассматриваем унификацию как механизм обобщения при выводе типов: она обрабатывает дерево термов (выражений) с метапеременными.
</aside>
<aside> 💡 Подстановка — отображение имён метапеременных в деревья термов
</aside>
<aside> 💡 Метапеременная — символ, который может быть заменен (отображен) на некоторое дерево путем применения подстановки
</aside>
<aside> 💡 Дерево термов с метапеременными — дерево или ориентированный ациклический граф, где
<aside> 💡 Домен подстановки — область определения подстановки, то есть множество метапеременных, к которым она применима. Обозначается 𝐷𝑜𝑚(σ), где σ — подстановка
</aside>
<aside> 💡 Применение подстановки к дереву — замена в дереве всех метапеременных из домена данной подстановки на соответствующие им деревья (до тех пор, пока такие метапеременные имеются)
</aside>
Пусть дано дерево термов с двумя мета-переменными: 𝑥 и 𝑦, а также подстановка σ, изображенная ниже. Применим данную подстановку. Применим σ к 𝑦, так как та принадлежит её домену, и получим новое дерево. На этом применение завершится, так как 𝑥 не принадлежит домену данной подстановки.
<aside> 💡 Более общая подстановка — подстановка $σ_0$ более общая, чем другая подстановка σ, если σ можно получить из $σ_0$ путем конкретизации в $σ_0$ некоторых метапеременных (это называется сужением).