Алгоритми уніфікації це алгоритми задачею яких є перевірити чи є 2 вирази уніфікованими і у випадку їх уніфікованості ви

Алгоритми уніфікації — це алгоритми, задачею яких є перевірити чи є 2 вирази уніфікованими і, у випадку їх уніфікованості, вирахувати їх найбільш спільний уніфікатор. Знайти уніфікатор означає знайти розв'язки системи.

Загальний випадок

Нехай E₁ = P(t₁, t₂,…,t_n), E₂ = P(s₁, s₂,…,s_n). Щоб уніфікувати E₁ і E₂ необхідно знайти такі значення змінних? щоб виконувались такі рівності:
t₁ = s₁, t₂ = s₂, … ,t_n = s_n
Тому для уніфікації E₁ і E₂ необхідно скласти систему рівнянь:
t₁ = s₁
t₂ = s₂
· · ·
t_n = s_n
і будемо розв′язувати задачу для неї.
Підстановка θ називається уніфікатором системи якщо для будь-якого i, такого що 1 ≤ i ≤ n, t_i і s_i рівні. Тобто фактично θ — це розв′язок системи в вільній алгебрі термів.

Приклад

Найбільш спільним уніфікатором системи рівнянь:
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'₁, t'₂, … , t'_n) = f(s'₁, s'₂, … , s'_n) замінюється на t'₁ = s'₁, t'₂ = s'₂, … ,t'_n = s'_n;
Якщо в системі є рівняння f(t'₁, t'₂, … , t'_n) = f(s'₁, s'₂, … , s'_n), де f ≠ g, то дана система не має розв’язків, тобто не має уніфікатора;
Рівняння s = x, де x — змінна, а s — стала, замінюється на x=s;
Рівняння s = s відкидається від системи;
Якщо в системі є рівняння s = x, і при чому x є змінною яка не залежить від s і зустрічається в інших рівняннях системи, то до всіх інших рівнянь застосовується заміна {x\s}
Якщо в системі є рівняння s = x, при чому x залежить від s, то дана система не має розв’язків, а отже і не має уніфікатора.

Теорема про уніфікацію

Яка б не була система рівнянь

Алгоритм уніфікації Мортеллі — Монтанарі завжди завершує роботу;
Якщо система уніфікована, то в результаті роботи алгоритму буде побудована приведена система, еквівалентна початковій;
Якщо система не уніфікована, то в результаті роботи алгоритму буде видане повідомлення про її неуніфікованість.

Джерела

В.А. Захаров "Математична логіка та теорія алгоритмів"^{[недоступне посилання з червня 2019]}