(unify '(drop ?x ?y)
'(drop arnold q351)
'())
==> ((?y q351) (?x arnold))
(unify '(drop ?x ?y)
'(drop arnold q351)
'((?y c211)))
==> #f
(unify '(drop ?x ?y)
'(drop arnold (class cogs q351))
'((?x ?z)))
==> ((?y (class cogs q351)) (?z arnold) (?x ?z))
(unify '(drop arnold ?x)
'(drop arnold (class ?y q351))
'((?y ?z) (?z ?x)))
==> #f
unify
Parameters: pat1, pat2, substitution
pat1 or pat2 are equal?,
return substitution.
pat1 or pat2 is a variable,
call unify-var.
pat1 or pat2 is an atom,
return #f.
unify
on corresponding parts of pat1 and pat2.
#f results, return #f immediately.
substitution
with this and continue.
substitution.
unify-var
Parameters: var, pat, substitution
substitution includes a value for var,
call unify with that value and pat.
var is eq? to pat,
return substitution.
var appears anywhere in pat,
return #f. (the occurs-check step)
var = pat to substitution,
and return the new substitution.
Last updated: 8 February 1997
URL: http://www.indiana.edu/~gasser/Q351/unification.html
Comments:
gasser@cs.indiana.edu
Copyright 1997,
The Trustees of
Indiana University