unification algorithm implementation in c#
Algorithme d ’unification
Appliquons les transformations suivantes sur l ’ense
mble des
équations tant que l ’une d ’entre elles est applicab
le :
1. Transformer t =x en x = t si x est une variable
et t n ’est pas
une variable
2. Effacer les opérations de la forme x = x
3. Soit t ’ = t ’ ’ tel que t ’ et t ’ ’ ne soient pas des va
riables
si les fonctions de t ’ et t ’ ’ ne sont pas identiques
alors pas
d ’unification possible
sinon remplacer l ’équation f(x1 ’,x2 ’, ...xn ’) = f(x1 ’
’, x2 ’ ’,
xn ’ ’) par les équations x1 ’=x1 ’ ’
x2 ’=x2 ’ ’
............
xn ’ = xn ’ ’
4. Soit x =t une équation telle x a une autre occur
rence dans
l ’ensemble des équations
si x se trouve dans t alors pas d ’unification possible
sinon transformer toutes les équations en remplaçan
t tous
les x par t
•
f(g(x), y, k(x)), f(y, h(z), k(w))
On applique règle 3 :
g(x)=y
y=h(z)
k(x)=k(w)
On applique règle 1 :
y=g(x)
y=h(z)
k(x)=k(z)
on applique regle 4 :
y=g(x)
g(x)=h(z)
k(x)=k(z)
on applique regle 3 :
y=g(x)
Impossible unifier g(x)=h(z)
•
f(x, h(x)), f(g(y), z)
On applique règle 3 :
X=g(y)
H(x)=z
On applique règle 1 :
X=g(y)
Z=h(x)
Solution{x/g(y),z/h(g(y))}