## Saturday, November 2, 2013

### Term matching

Extending one substitution with another can only work if the two substitutions are consistent with each other.
exception Term_match_exc

let extend_subst s1 s2 =
let f acc (x, t)=
try
let u = List.assoc x acc in
if t = u then acc
else raise Term_match_exc
with Not_found -> (x, t)::acc
in List.fold_left f s1 s2

A pattern match of a term u by a term t is a substitution that transforms t into u. If t is a variable s then the substitution (s, u) is an obvious pattern match for example. More generally though, if t is of the form f (t1, ..., tn), then
• u must be of the form f (u1, ..., un);
• for each i there must exist a match of ui with ti;
and all the matches must be mutually compatible for a solution to exist.
let term_match (t1, t2) =
let rec term_match' subst = function
| (Var v, t) -> extend_subst [v, t] subst
| (t, Var v) -> raise Term_match_exc
| (Term (f, l), Term (g, r)) ->
if f = g then
List.fold_left term_match' subst (List.combine l r)
else raise Term_match_exc
in term_match' [] (t1, t2)

For example, a pattern match of h(y(z, k(x, s))) and h(y(l(m, n,o()), k(t(), u))) is {(x,t()),(z, l(m,n,o()), (s, u)}.