Алгоритми уніфікації
Алгоритми уніфікації — це алгоритми, задачею яких є перевірити чи є 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, то дана система не має розв’язків, а отже і не має уніфікатора.
Теорема про уніфікацію
Яка б не була система рівнянь
- Алгоритм уніфікації Мортеллі — Монтанарі завжди завершує роботу;
- Якщо система уніфікована, то в результаті роботи алгоритму буде побудована приведена система, еквівалентна початковій;
- Якщо система не уніфікована, то в результаті роботи алгоритму буде видане повідомлення про її неуніфікованість.
Джерела
- В.А. Захаров "Математична логіка та теорія алгоритмів"[недоступне посилання з червня 2019]