Substitutions on terms with variables

Substitutions on terms with variables

This picks up on the earlier terms with variables blog entry. Remember the term_trav function? I'll recall it here but this time sharpen it up a bit with named parameters.

let rec term_trav ~f ~g ~x ~v = function
  | Term (a, tl) -> 
    let l = List.map (term_trav ~f ~g ~x ~v) tl in
    let res = List.fold_right g l x in
    f (a, res)
  | Var b -> v b

Application of substitutions

Substitutions are modeled as values of type ('b, ('a, 'b) term) list. Application of a substitution is about the finding of some of the variables of a term and replacing them with different terms to find the term's image under the substitution.

let apply_substitution subst t = 
  term_trav 
    ~f:(fun (f, l) -> Term (f, l)) 
    ~g:(fun x acc -> x::acc) 
    ~x:[] 
    ~v:(fun s -> try List.assoc s subst with _ -> Var s) 
    t

Of course, the definition of apply_substitution is equivalent to this one

let rec apply_substituion' subst = function
  | Term (f, ns) -> Term (f, List.map (apply_subst subst) ns)
  | Var x as v -> try List.assoc x subst with _ -> v

and I guess is more efficient too (in that a fold_right has been eliminated). 

For example, this program

let s = ["x", term_of_string "g(z)"] in
print_term (apply_substitution s (term_of_string "f (x, y, x)"))

shows that f (x, y, x) -> f (g(z), y, g(z)) under the substitution {(x, g(z))}.  

Composition of substitutions

If sig1 and sig2 are two substitutions, we can compute their composite sig1 o sig2 like this

let compose_subst sig1 sig2 =
  (List.map (fun (v, t) -> (v, apply_substitution sig1 t)) sig2)
  @(let vs = List.map fst sig2 in 
    List.filter (fun (x, t) -> not (List.mem x vs)) sig1)

That's quite subtle! Informally this is saying : first apply to the terms in sig2, the substitutions of sig1. Then, filter out those substitutions in sig1 that are in variables modified by sig2. The result is the concatenation of those lists. 

Here's an example. If sig1={(x, g(x,y))} and sig2={(y, h(x,z)), (x, k(x))} then we'd expect sig1 o sig2 = {(y, h(g(x,y), z)), (x, k(g(x, y)))}. The following program can be used to test our expectations.

 let sig1 = ["x", term_of_string "g (x, y)"] in
let sig2 = ["y", term_of_string "h (x, z)"; "x", term_of_string "k(x)"] in
let subst=compose_subst sig1 sig2 in
print_string "y -> " ; print_term (List.assoc "y" subst) ; print_newline ();
print_string "x -> " ; print_term (List.assoc "x" subst) ; print_newline ()