Term matching

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 (t₁, ..., t_n), then

• u must be of the form f (u₁, ..., u_n);
  
• for each i there must exist a match of u_i with t_i;
  

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