Алгоритми уніфікації

Алгоритми уніфікації — це алгоритми, задачею яких є перевірити чи є 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, то дана система не має розв’язків, а отже і не має уніфікатора.

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

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

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

Джерела

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.