## Saturday, October 19, 2013

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


## Tuple matching

Here is an algorithm that can be used to match tuples. For example, on matching (a, b, (c, d)) against (1, 2, (3, 4)) we'd hope to get the set (a = 1, b = 2, c = 3, d = 4).
module type S = sig

type expr =
| E_var of string
| E_const of int
| E_tuple of expr list

val const : int -> expr
val var : string -> expr
val tuple : expr list -> expr

val tuple_match : (string * expr) list -> expr -> expr -> (string * expr) list
val tuple_of_expr : expr -> expr

end

module Expr : S =
struct

type expr =
| E_var of string
| E_const of int
| E_tuple of expr list

let var s = E_var s
let const i = E_const i
let tuple t = E_tuple t

let as_tuple = function
| E_tuple l as t -> t
| _ ->  failwith "Tuple expected"

let rec tuple_match acc x y =
match x with
| E_var (s) -> (s, y)::acc
| E_tuple ((h::t)) ->
let (E_tuple l) = as_tuple y in
let acc = tuple_match acc (tuple t) (tuple (List.tl l)) in
tuple_match acc h (List.hd l)
| E_tuple [] -> acc
| _ as unk -> failwith "Match failure"

end

For example,
(* (a, b, t) |- (1, 2, (3, 4)) *)
let x = Expr.tuple
[Expr.var "a"; Expr.var "b"; Expr.var "t" ] in
let y = Expr.tuple [Expr.const 1; Expr.const 2;
Expr.tuple [Expr.const 3; Expr. const 4] ] in
Expr.tuple_match [] x y
;;

in the top-level prints
- : (string * Expr.expr) list =
[("a", Expr.E_const 1); ("b", Expr.E_const 2);
("t", Expr.E_tuple [Expr.E_const 3; Expr.E_const 4])]

whereas
(* (a, b, (c, d)) |- (1, 2, (3, 4))*)
let x = Expr.tuple
[Expr.var "a"; Expr.var "b";
Expr.tuple [Expr.var "c"; Expr.var "d"]] in
let y = Expr.tuple
[Expr.const 1; Expr.const 2;
Expr.tuple [Expr.const 3; Expr. const 4]] in
Expr.tuple_match [] x y
;;

results in this
- : (string * Expr.expr) list =
[("a", Expr.E_const 1); ("b", Expr.E_const 2); ("c", Expr.E_const 3);
("d", Expr.E_const 4)]