Алгоритми уніфікації — це алгоритми, задачею яких є перевірити чи є 2 вирази уніфікованими і, у випадку їх уніфікованості, вирахувати їх найбільш спільний уніфікатор. Знайти уніфікатор означає знайти розв'язки системи.
Загальний випадок
Нехай E1 = P(t1, t2,…,tn), E2 = P(s1, s2,…,sn). Щоб уніфікувати E1 і E2 необхідно знайти такі значення змінних? щоб виконувались такі рівності: t1 = s1, t2 = s2, … ,tn = sn Тому для уніфікації E1 і E2 необхідно скласти систему рівнянь: t1 = s1 t2 = s2 · · · tn = sn і будемо розв′язувати задачу для неї. Підстановка θ називається уніфікатором системи якщо для будь-якого i, такого що 1 ≤ i ≤ n, ti і si рівні. Тобто фактично θ — це розв′язок системи в вільній алгебрі термів.
Приклад
Найбільш спільним уніфікатором системи рівнянь: f(c, x) = f(y, g(y)) g(y) = z
f (c, g(c)) = f (c, g(c)) g(c) = g(c)
Тоді θ = {x/g(c), y/c, z/g(c)}.
Алгоритм Мартеллі — Монтанарі Це недетермінований алгоритм, який складається з шести правил, які можуть застосовуватись в будь-якому порядку поки або жодне з правил застосувати не можна (побудована приведена система рівнянь) або застосовується правило, яке робить уніфікацію неможливою.
Список правил Рівняння f(t'1, t'2, … , t'n) = f(s'1, s'2, … , s'n) замінюється на t'1 = s'1, t'2 = s'2, … ,t'n = s'n; Якщо в системі є рівняння f(t'1, t'2, … , t'n) = f(s'1, s'2, … , s'n), де f ≠ g, то дана система не має розв’язків, тобто не має уніфікатора; Рівняння s = x, де x — змінна, а s — стала, замінюється на x=s; Рівняння s = s відкидається від системи; Якщо в системі є рівняння s = x, і при чому x є змінною яка не залежить від s і зустрічається в інших рівняннях системи, то до всіх інших рівнянь застосовується заміна {x\s} Якщо в системі є рівняння s = x, при чому x залежить від s, то дана система не має розв’язків, а отже і не має уніфікатора.
Теорема про уніфікацію
Яка б не була система рівнянь Алгоритм уніфікації Мортеллі — Монтанарі завжди завершує роботу; Якщо система уніфікована, то в результаті роботи алгоритму буде побудована приведена система, еквівалентна початковій; Якщо система не уніфікована, то в результаті роботи алгоритму буде видане повідомлення про її неуніфікованість.
Джерела
В.А. Захаров "Математична логіка та теорія алгоритмів"