Unification

(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

Parameters: pat1, pat2, substitution

• If pat1 or pat2 are equal?, return substitution.
• Else if either pat1 or pat2 is a variable, call unify-var.
• Else if either pat1 or pat2 is an atom, return #f.
• Else the patterns are both lists. Call unify on corresponding parts of pat1 and pat2.
  • If #f results, return #f immediately.
  • Else a substitution results; replace substitution with this and continue.
  Return the final substitution.

Parameters: var, pat, substitution

• If substitution includes a value for var, call unify with that value and pat.
• Else if var is eq? to pat, return substitution.
• Else if var appears anywhere in pat, return #f. (the occurs-check step)
• Else add the binding var = pat to substitution, and return the new substitution.