test_kb

test_kb_wasm/build.sh

@@ -0,0 +1,11 @@
+
+../ocamlopt -c terms.mli
+../ocamlopt -c terms.ml
+../ocamlopt -c equations.mli
+../ocamlopt -c equations.ml
+../ocamlopt -c orderings.mli
+../ocamlopt -c orderings.ml
+../ocamlopt -c kb.mli
+../ocamlopt -c kb.ml
+../ocamlopt -c kbmain.ml
+../ocamlopt terms.cmx equations.cmx orderings.cmx kb.cmx kbmain.cmx

test_kb_wasm/clean.sh

@@ -0,0 +1,2 @@
+
+rm -f *.cmi *.cmx *.o a.out*

test_kb_wasm/equations.ml

@@ -0,0 +1,100 @@
+(****************** Equation manipulations *************)
+
+open Terms
+
+type rule =
+  { number: int;
+    numvars: int;
+    lhs: term;
+    rhs: term }
+
+(* standardizes an equation so its variables are 1,2,... *)
+
+let mk_rule num m n =
+  let all_vars = union (vars m) (vars n) in
+  let counter = ref 0 in
+  let subst =
+    List.map (fun v -> incr counter; (v, Var !counter)) (List.rev all_vars) in
+  { number = num;
+    numvars = !counter;
+    lhs = substitute subst m;
+    rhs = substitute subst n }
+
+
+(* checks that rules are numbered in sequence and returns their number *)
+
+let check_rules rules =
+  let counter = ref 0 in
+  List.iter (fun r -> incr counter;
+                 if r.number <> !counter
+                 then failwith "Rule numbers not in sequence")
+       rules;
+  !counter
+
+
+let pretty_rule rule =
+  print_int rule.number; print_string " : ";
+  pretty_term rule.lhs; print_string " = "; pretty_term rule.rhs;
+  print_newline()
+
+
+let pretty_rules rules = List.iter pretty_rule rules
+
+(****************** Rewriting **************************)
+
+(* Top-level rewriting. Let eq:L=R be an equation, M be a term such that L<=M.
+   With sigma = matching L M, we define the image of M by eq as sigma(R) *)
+let reduce l m r =
+  substitute (matching l m) r
+
+(* Test whether m can be reduced by l, i.e. m contains an instance of l. *)
+
+let can_match l m =
+  try let _ = matching l m in true
+  with Failure _ -> false
+
+let rec reducible l m =
+  can_match l m ||
+   (match m with
+    | Term(_,sons) -> List.exists (reducible l) sons
+    |         _     -> false)
+
+(* Top-level rewriting with multiple rules. *)
+
+let rec mreduce rules m =
+  match rules with
+    [] -> failwith "mreduce"
+  | rule::rest ->
+      try
+        reduce rule.lhs m rule.rhs
+      with Failure _ ->
+        mreduce rest m
+
+
+(* One step of rewriting in leftmost-outermost strategy,
+   with multiple rules. Fails if no redex is found *)
+
+let rec mrewrite1 rules m =
+  try
+    mreduce rules m
+  with Failure _ ->
+    match m with
+      Var n -> failwith "mrewrite1"
+    | Term(f, sons) -> Term(f, mrewrite1_sons rules sons)
+
+and mrewrite1_sons rules = function
+    [] -> failwith "mrewrite1"
+  | son::rest ->
+      try
+        mrewrite1 rules son :: rest
+      with Failure _ ->
+        son :: mrewrite1_sons rules rest
+
+
+(* Iterating rewrite1. Returns a normal form. May loop forever *)
+
+let rec mrewrite_all rules m =
+  try
+    mrewrite_all rules (mrewrite1 rules m)
+  with Failure _ ->
+    m

test_kb_wasm/equations.mli

@@ -0,0 +1,18 @@
+open Terms
+
+type rule =
+  { number: int;
+    numvars: int;
+    lhs: term;
+    rhs: term }
+
+val mk_rule: int -> term -> term -> rule
+val check_rules: rule list -> int
+val pretty_rule: rule -> unit
+val pretty_rules: rule list -> unit
+val reduce: term -> term -> term -> term
+val reducible: term -> term -> bool
+val mreduce: rule list -> term -> term
+val mrewrite1: rule list -> term -> term
+val mrewrite1_sons: rule list -> term list -> term list
+val mrewrite_all: rule list -> term -> term

test_kb_wasm/kb.ml

@@ -0,0 +1,173 @@
+open Terms
+open Equations
+
+(****************** Critical pairs *********************)
+
+(* All (u,subst) such that N/u (&var) unifies with M,
+   with principal unifier subst *)
+
+let rec super m = function
+    Term(_,sons) as n ->
+      let rec collate n = function
+        [] -> []
+      | son::rest ->
+          List.map (fun (u, subst) -> (n::u, subst)) (super m son)
+          @ collate (n+1) rest in
+      let insides = collate 1 sons in
+        begin try
+          ([], unify m n) :: insides
+        with Failure _ ->
+          insides
+        end
+  | _ -> []
+
+
+(* Ex :
+let (m,_) = <<F(A,B)>>
+and (n,_) = <<H(F(A,x),F(x,y))>> in super m n
+==> [[1],[2,Term ("B",[])];                      x <- B
+     [2],[2,Term ("A",[]); 1,Term ("B",[])]]     x <- A  y <- B
+*)
+
+(* All (u,subst), u&[], such that n/u unifies with m *)
+
+let super_strict m = function
+    Term(_,sons) ->
+      let rec collate n = function
+        [] -> []
+      | son::rest ->
+          List.map (fun (u, subst) -> (n::u, subst)) (super m son)
+          @ collate (n+1) rest in
+      collate 1 sons
+    | _ -> []
+
+
+(* Critical pairs of l1=r1 with l2=r2 *)
+(* critical_pairs : term_pair -> term_pair -> term_pair list *)
+let critical_pairs (l1,r1) (l2,r2) =
+  let mk_pair (u,subst) =
+     substitute subst (replace l2 u r1), substitute subst r2 in
+  List.map mk_pair (super l1 l2)
+
+(* Strict critical pairs of l1=r1 with l2=r2 *)
+(* strict_critical_pairs : term_pair -> term_pair -> term_pair list *)
+let strict_critical_pairs (l1,r1) (l2,r2) =
+  let mk_pair (u,subst) =
+    substitute subst (replace l2 u r1), substitute subst r2 in
+  List.map mk_pair (super_strict l1 l2)
+
+
+(* All critical pairs of eq1 with eq2 *)
+let mutual_critical_pairs eq1 eq2 =
+  (strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1)
+
+(* Renaming of variables *)
+
+let rename n (t1,t2) =
+  let rec ren_rec = function
+    Var k -> Var(k+n)
+  | Term(op,sons) -> Term(op, List.map ren_rec sons) in
+  (ren_rec t1, ren_rec t2)
+
+
+(************************ Completion ******************************)
+
+let deletion_message rule =
+  print_string "Rule ";print_int rule.number; print_string " deleted";
+  print_newline()
+
+
+(* Generate failure message *)
+let non_orientable (m,n) =
+    pretty_term m; print_string " = "; pretty_term n; print_newline()
+
+
+let rec partition p = function
+    [] -> ([], [])
+  | x::l -> let (l1, l2) = partition p l in
+            if p x then (x::l1, l2) else (l1, x::l2)
+
+
+let rec get_rule n = function
+    [] -> raise Not_found
+  | r::l -> if n = r.number then r else get_rule n l
+
+
+(* Improved Knuth-Bendix completion procedure *)
+
+let kb_completion greater =
+  let rec kbrec j rules =
+  let rec process failures (k,l) eqs =
+(****
+     print_string "***kb_completion "; print_int j; print_newline();
+     pretty_rules rules;
+     List.iter non_orientable failures;
+     print_int k; print_string " "; print_int l; print_newline();
+     List.iter non_orientable eqs;
+***)
+    match eqs with
+      [] ->
+        if k<l then next_criticals failures (k+1,l) else
+        if l<j then next_criticals failures (1,l+1) else
+        begin match failures with
+            [] -> rules (* successful completion *)
+          | _  -> print_string "Non-orientable equations :"; print_newline();
+                  List.iter non_orientable failures;
+                  failwith "kb_completion"
+        end
+    | (m,n)::eqs ->
+        let m' = mrewrite_all rules m
+        and n' = mrewrite_all rules n
+        and enter_rule(left,right) =
+          let new_rule = mk_rule (j+1) left right in
+          pretty_rule new_rule;
+          let left_reducible rule = reducible left rule.lhs in
+          let (redl,irredl) = partition left_reducible rules in
+          List.iter deletion_message redl;
+          let right_reduce rule =
+            mk_rule rule.number rule.lhs
+                    (mrewrite_all (new_rule::rules) rule.rhs) in
+          let irreds = List.map right_reduce irredl in
+          let eqs' = List.map (fun rule -> (rule.lhs, rule.rhs)) redl in
+          kbrec (j+1) (new_rule::irreds) [] (k,l) (eqs @ eqs' @ failures) in
+(***
+        print_string "--- Considering "; non_orientable (m', n');
+***)
+        if m' = n' then process failures (k,l) eqs else
+        if greater(m',n') then enter_rule(m',n') else
+        if greater(n',m') then enter_rule(n',m') else
+        process ((m',n')::failures) (k,l) eqs
+
+  and next_criticals failures (k,l) =
+(****
+    print_string "***next_criticals ";
+    print_int k; print_string " "; print_int l ; print_newline();
+****)
+    try
+      let rl = get_rule l rules in
+      let el = (rl.lhs, rl.rhs) in
+        if k=l then
+          process failures (k,l)
+                  (strict_critical_pairs el (rename rl.numvars el))
+        else
+          try
+            let rk = get_rule k rules in
+            let ek = (rk.lhs, rk.rhs) in
+              process failures (k,l)
+                      (mutual_critical_pairs el (rename rl.numvars ek))
+          with Not_found -> next_criticals failures (k+1,l)
+    with Not_found -> next_criticals failures (1,l+1)
+  in process
+  in kbrec
+
+
+(* complete_rules is assumed locally confluent, and checked Noetherian with
+  ordering greater, rules is any list of rules *)
+
+let kb_complete greater complete_rules rules =
+    let n = check_rules complete_rules
+    and eqs = List.map (fun rule -> (rule.lhs, rule.rhs)) rules in
+    let completed_rules =
+      kb_completion greater n complete_rules [] (n,n) eqs in
+    print_string "Canonical set found :"; print_newline();
+    pretty_rules (List.rev completed_rules)

test_kb_wasm/kb.mli

@@ -0,0 +1,17 @@
+open Terms
+open Equations
+
+val super: term -> term -> (int list * (int * term) list) list
+val super_strict: term -> term -> (int list * (int * term) list) list
+val critical_pairs: term * term -> term * term -> (term * term) list
+val strict_critical_pairs: term * term -> term * term -> (term * term) list
+val mutual_critical_pairs: term * term -> term * term -> (term * term) list
+val rename: int -> term * term -> term * term
+val deletion_message: rule -> unit
+val non_orientable: term * term -> unit
+val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
+val get_rule: int -> rule list -> rule
+val kb_completion:
+    (term * term -> bool) -> int -> rule list -> (term * term) list
+    -> int * int -> (term * term) list -> rule list
+val kb_complete: (term * term -> bool) -> rule list -> rule list -> unit

test_kb_wasm/kbmain.ml

@@ -0,0 +1,71 @@
+(* TEST
+   modules = "terms.ml equations.ml orderings.ml kb.ml"
+*)
+
+open Terms
+open Equations
+open Orderings
+open Kb
+
+(****
+let group_rules = [
+  { number = 1; numvars = 1;
+    lhs = Term("*", [Term("U",[]); Var 1]); rhs = Var 1 };
+  { number = 2; numvars = 1;
+    lhs = Term("*", [Term("I",[Var 1]); Var 1]); rhs = Term("U",[]) };
+  { number = 3; numvars = 3;
+    lhs = Term("*", [Term("*", [Var 1; Var 2]); Var 3]);
+    rhs = Term("*", [Var 1; Term("*", [Var 2; Var 3])]) }
+]
+****)
+
+let geom_rules = [
+  { number = 1; numvars = 1;
+    lhs = Term ("*",[(Term ("U",[])); (Var 1)]);
+    rhs = Var 1 };
+  { number = 2; numvars = 1;
+    lhs = Term ("*",[(Term ("I",[(Var 1)])); (Var 1)]);
+    rhs = Term ("U",[]) };
+  { number = 3; numvars = 3;
+    lhs = Term ("*",[(Term ("*",[(Var 1); (Var 2)])); (Var 3)]);
+    rhs = Term ("*",[(Var 1); (Term ("*",[(Var 2); (Var 3)]))]) };
+  { number = 4; numvars = 0;
+    lhs = Term ("*",[(Term ("A",[])); (Term ("B",[]))]);
+    rhs = Term ("*",[(Term ("B",[])); (Term ("A",[]))]) };
+  { number = 5; numvars = 0;
+    lhs = Term ("*",[(Term ("C",[])); (Term ("C",[]))]);
+    rhs = Term ("U",[]) };
+  { number = 6; numvars = 0;
+    lhs = Term("*",
+            [(Term ("C",[]));
+             (Term ("*",[(Term ("A",[])); (Term ("I",[(Term ("C",[]))]))]))]);
+    rhs = Term ("I",[(Term ("A",[]))]) };
+  { number = 7; numvars = 0;
+    lhs = Term("*",
+            [(Term ("C",[]));
+             (Term ("*",[(Term ("B",[])); (Term ("I",[(Term ("C",[]))]))]))]);
+    rhs = Term ("B",[]) }
+]
+
+let group_rank = function
+    "U" -> 0
+  | "*" -> 1
+  | "I" -> 2
+  | "B" -> 3
+  | "C" -> 4
+  | "A" -> 5
+  | _ -> assert false
+
+let group_precedence op1 op2 =
+  let r1 = group_rank op1
+  and r2 = group_rank op2 in
+    if r1 = r2 then Equal else
+    if r1 > r2 then Greater else NotGE
+
+let group_order = rpo group_precedence lex_ext
+
+let greater pair =
+  match group_order pair with Greater -> true | _ -> false
+
+let _ =
+  kb_complete greater [] geom_rules