OCaml

Write the function formatTree : t -> string which returns a string representation of a tree. For example, with t0 thru t3 as above, we have

# (formatTree (Var 8));; - : string = "v8" # (formatTree t0);; - : string = "(v0 -> (C -> C))" # (formatTree t1);; - : string = "(C -> v1)" # (formatTree t2);; - : string = "((C -> v1) -> (C -> C))" # (formatTree t3);; - : string = "(C -> (v0 -> (C -> C)))"

This problem will be easier if you use the Lib.fmt function. For example, the call (Lib.fmt "v%d" 8) plugs the string representation of integer 8 into the integer hole %d in the format string, yielding "v8".

1. (1.5 Points) Write the function matchTrees : t -> t -> bool such that a call (matchTrees t1 t2) returns true if t1 and t2 are identical trees. Here are a few examples.

   # (matchTrees C C);; - : bool = true # (matchTrees (Var 4) (Var 4));; - : bool = true # (matchTrees (Var 4) (Var 28));; - : bool = false # (matchTrees t3 t3);; - : bool = true

   Problems 8 and 9 relate to substitutions, structures that are common in the field of mathematical logic. Let V = {v0, v1, ... } be a set of variables and let t0, t1, ... be trees as defined above. A substitution = { t0/v0, ..., tk/vk } is a set of tree/variable pairs t/v, pronounced "t for v", such that all of the variables to the right of a slash in are unique. For example, all of

   0 = {}

   1 = {(v0 -> (C -> C))/v1, (C -> v1)/v0}

   2 = {v0/v1}

   are well defined substitutions. For the purposes of problems 8 and 9, you should assume that the association t/v is represented as

   type binding = { tree : t ; var : int }

   and that the substitution {t0/v0, ..., tk/vk} is represented as a list of bindings

   type subst = binding list