unification algorithm

Question

 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))}