(* Congruence_Closure *)
(* Implement the "..." below and check that at least all PROPERTY equations hold. *)
(* Ground term datatype: a function symbol applied to sub-terms. This time no variables! *)
type term = App of (string * term list)
let rec subterms (App (c, ts)) = App (c, ts) :: List.concat (List.map subterms ts)
type equation = term * term
type signature = (string * int) list
(*
We suggest two ways to implement congruence closure
(of course, you only need to implement one way):
A) As presented in "Term Rewriting and All That" pp 62:
iterate over the list of equations by adding all reflexive, symmetric, transitive and congruence closures
B) Compute the equivalence classes of equivalent terms, you are allowed to change the type of closure to
closure :: signature -> equation list -> term list list
Start with the equivalent terms from the equation list, and implement merge for transitivity, and
congruence closure on equivalence classes.
A) is simpler, but B) is more fun :-)
*)
let closure (s:signature) (eqs:equation list) = ([]:equation list)
let sg = ([("f", 2); ("g", 1); ("a", 0); ("b", 0); ("c", 0)]:signature)
let f x y = App ("f", [x; y])
let g x = App ("g", [x])
let a = App ("a", [])
let b = App ("b", [])
let c = App ("c", [])
let s = App ("s", [])
let t = App ("t", [])
(* PROPERTIES *)
(* PROPERTY prop1 == True *)
let prop1 = List.mem (s, t) (closure sg [(f a b, a); (s, f (f a b) b); (t, a)])
(* PROPERTY prop2 == False *)
let prop2 = List.mem (s, t) (closure sg [(f a b, a); (s, f (f a b) b); (t, b)])