### 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

Of course, the definition of

`('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 _ -> vand 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 ()