CSE 472/572, Spring 2002 http://www.cse.buffalo.edu/∼rapaport/572.html

UNIFICATION EXAMPLE

Find MGU for W = {P(a,x,f(g(y))),P(z,f(z),f(u))}.

k W_{k}  σ_{k}  W_{k}  D_{k}  occurs
singleton?  check
0 W_{0} = W σ_{0} = {} no {a,z} true;
v_{0} = z,
t_{0} = a
σ_{1} = Compose({},{a/z})
= {a/z}
1 W_{1} = Subst({a/z},W_{0})
= {P(a,x,f(g(y))),P(a,f(a),f(u))} no {x,f(a)} true;
v_{1} = x,
t_{1} = f(a)
σ_{2} = Compose({a,z},{f(a)/x})
= {a/z,f(a)/x}
2 W_{2} = Subst({f(a)/x},W_{1})
= {P(a,f(a),f(g(y))),P(a,f(a),f(u))} no {g(y),u} true;
v_{2} = u,
t_{2} = g(y)
σ_{3} = Compose({a/z,f(a)/x},{g(y)/u})
= {a/z,f(a)/x,g(y)/u}
3 W_{3} = Subst({g(y)/u},W_{2})
= {P(a,f(a),f(g(y))),P(a,f(a),f(g(y)))}
= {P(a,f(a),f(g(y)))}  yes

Returns σ_{3} = {a/z,f(a)/x,g(y)/u} as MGU, with P(a,f(a),f(g(y))) as the common instance.

\begin{matrix}c \\ ◯ \end{matrix}2002, William J. Rapaport rapaport@cse.buffalo.edu file: 572/S02/unification.eg.08ap02.tex