Implementation of an algorithm for checking SR and injectivity

src/completion.ml

@@ -0,0 +1,147 @@
+(** Completion procedure *)
+
+open Terms
+open Basics
+open Extra
+
+(** total strict order *)
+type 'a order = 'a -> 'a -> bool
+
+let gt : 'a order -> 'a -> 'a -> bool = fun ord a b -> ord a b
+
+(** [ge ord] calculates the reflexive closure of [ord] *)
+let ge : 'a order -> 'a -> 'a -> bool = fun ord a b -> a = b || ord a b
+
+(** [ord_lex ord] calculates the lexicographic order corresponding to the
+    alphabetical order [ord] *)
+let ord_lex : 'a order -> ('a list) order = fun ord l1 l2 ->
+  let rec elim_comm l1 l2 = match (l1, l2) with
+    | h1 :: t1, h2 :: t2 -> begin match ord h1 h2 with
+        | false -> if h1 = h2 then elim_comm t1 t2 else assert false
+        | _     -> l1, l2
+      end
+    | _                  -> l1, l2 in
+  match elim_comm l1 l2 with
+  | [], _              -> false
+  | _, []              -> true
+  | h1 :: _, h2 :: _ -> ord h1 h2
+
+let get_sym : term -> sym = fun t -> match unfold t with
+  | Symb (s, _) -> s
+  | _          -> assert false
+
+(** [lpo ord] calculates the lexicographic path ordering corresponding to
+    the strict total order [ord] on the set of all function symbols *)
+let rec lpo : sym order -> term order = fun ord t1 t2 ->
+  let f, args = get_args t1 in
+  let f = get_sym f in
+  if List.exists (fun x -> ge (lpo ord) x t2) args then true
+  else
+    let g, args' = get_args t2 in
+    let g = get_sym g in
+    match ord f g with
+    | true  ->
+        if List.for_all (fun x -> gt (lpo ord) t1 x) args' then true
+        else
+          false
+    | false ->
+        if f = g then
+          List.for_all (fun x -> gt (lpo ord) t1 x) args' &&
+          ord_lex (lpo ord) args args'
+        else false
+
+(** [build_meta_type k] builds the type “∀(x₁:A₁) (x₂:A₂) ⋯ (xk:Ak), B” where
+    “x₁” through “xk” are fresh variables, “Ai = Mi[x₁,⋯,x(i-1)]”, “Mi” is a
+    new metavar of arity “i-1” and type “∀(x₁:A₂) ⋯ (x(i-1):A(i-1), TYPE”. *)
+let build_meta_type : int -> term = fun k ->
+  assert (k>=0);
+  let vs = Bindlib.new_mvar mkfree (Array.make k "x") in
+  let rec build_prod k p =
+    if k = 0 then p
+    else
+      let k = k-1 in
+      let mk_typ = Bindlib.unbox (build_prod k _Type) in
+      let mk = fresh_meta mk_typ k in
+      let tk = _Meta mk (Array.map _Vari (Array.sub vs 0 k)) in
+      let b = Bindlib.bind_var vs.(k) p in
+      let p = Bindlib.box_apply2 (fun a b -> Prod(a,b)) tk b in
+      build_prod k p
+  in
+  let mk_typ = Bindlib.unbox (build_prod k _Type) (*FIXME?*) in
+  let mk = fresh_meta mk_typ k in
+  let tk = _Meta mk (Array.map _Vari vs) in
+  Bindlib.unbox (build_prod k tk)
+
+type rule_ = sym * pp_hint * rule
+
+(** [cp builtins r1 r2] calculates the critical pairs of the rules r1 and r2
+    *)
+let cp : sym StrMap.t -> rule_ -> rule_ -> (term * term) list
+  = fun builtins (s1, h1, r1) (s2, h2, r2) ->
+  let arity1 = Bindlib.mbinder_arity r1.rhs in
+  let arity2 = Bindlib.mbinder_arity r2.rhs in
+  let cps = ref [] in
+  let rec to_m : int -> (meta option) array -> term -> tbox = fun k metas t ->
+    match unfold t with
+    | Vari x         -> _Vari x
+    | Symb (s, h)    -> _Symb s h
+    | Abst (a, t)    ->
+        let (x, t) = Bindlib.unbind t in
+        _Abst (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t))
+    | Appl (t, u)    -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u)
+    | Patt (i, n, a) ->
+        begin
+          let a = Array.map (to_m 0 metas) a in
+          let l = Array.length a in
+          match i with
+          | None   ->
+              let m = fresh_meta ~name:n (build_meta_type (l + k)) l in
+              _Meta m a
+          | Some i ->
+              match metas.(i) with
+              | Some m -> _Meta m a
+              | None   ->
+                  let m = fresh_meta ~name:n (build_meta_type (l + k)) l in
+                  metas.(i) <- Some m;
+                  _Meta m a
+        end
+    | _              -> assert false in
+  let metas1 = Array.init arity1 (fun _ -> None) in
+  let lhs1 = List.map (fun p -> Bindlib.unbox (to_m 0 metas1 p)) r1.lhs in
+  let lhs1 = Basics.add_args (Symb (s1, h1)) lhs1 in
+  let find_cp : term -> unit = fun t ->
+    let metas1 = Array.init arity1 (fun _ -> None) in
+    let metas2 = Array.init arity2 (fun _ -> None) in
+    let lhs2 = List.map (fun p -> Bindlib.unbox (to_m 0 metas2 p)) r2.lhs in
+    let lhs2 = Basics.add_args (Symb (s2, h2)) lhs2 in
+    let fn m =
+      let m = match m with Some m -> m | None -> assert false in
+      let xs = Array.init m.meta_arity (Printf.sprintf "x%i") in
+      let xs = Bindlib.new_mvar mkfree xs in
+      let e = Array.map _Vari xs in
+      TE_Some (Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m e)))
+    in
+    let te_envs1 = Array.map fn metas1 in
+    let te_envs2 = Array.map fn metas2 in
+    let rhs1 = Bindlib.msubst r1.rhs te_envs1 in
+    let rhs2 = Bindlib.msubst r2.rhs te_envs2 in
+    let to_solve = [(t, lhs2)] in
+    match Unif.(solve builtins false {no_problems with to_solve}) with
+    | None    -> ()
+    | Some cs ->
+        if cs <> [] then () else cps := (rhs1, rhs2) :: !cps in
+  Basics.iter find_cp lhs1; (* This only works for algebraic LHS *)
+  !cps
+
+(** [critical_pairs builtins rs] calculates the list of all critical pairs
+    of the rewrite system rs *)
+let rec critical_pairs : sym StrMap.t -> rule_ list -> (term * term) list
+  = fun builtins rs ->
+  match rs with
+  | [] -> []
+  | r :: rs' ->
+      let cps = critical_pairs builtins rs in
+      List.fold_left
+        (fun acc r' ->
+           cp builtins r r' @ cp builtins r' r @ acc)
+           (cp builtins r r @ cps) rs'

src/sr.ml

@@ -5,6 +5,7 @@ open Console
 open Terms
 open Print
 open Extra
+open Files
 
 (** Logging function for typing. *)
 let log_subj =
@@ -69,6 +70,64 @@ let build_meta_type : int -> term = fun k ->
   let tk = _Meta mk (Array.map _Vari vs) in
   Bindlib.unbox (build_prod k tk)
 
+(** Translation from Xml-light
+    (https://opam.ocaml.org/packages/xml-light/xml-light.2.4/) to Lambdapi **)
+
+(** [find_trs xml] finds the Xml node corresponding to the TRS in an Xml node
+    obtained from a CPF file. In a valid CPF file generated from external
+    tools for the Knuth-Bendix completion, there is exactly one such node. **)
+let find_trs : Xml.xml -> Xml.xml = fun xml ->
+  let rec find_tag : string -> Xml.xml -> Xml.xml option = fun s xml ->
+    if Xml.tag xml = s then Some xml
+    else
+      let rec iter f = function
+        | []      -> None
+        | x :: xs -> match f x with
+            | None -> iter f xs
+            | y    -> y in
+      iter (find_tag s) (Xml.children xml)
+  in
+  match find_tag "completionInput" xml with
+  | None      -> assert false
+  | Some xml  ->
+      match find_tag "trs" xml with
+      | None     -> assert false
+      | Some xml -> xml
+
+(** [get_only_child xml] returns the only child of an Xml node given **)
+let get_only_child : Xml.xml -> Xml.xml = fun xml ->
+  match Xml.children xml with
+  | [xml] -> xml
+  | _     -> assert false
+
+(** [get_term sign xml] translates an Xml node of tag name "var" or "funapp"
+    into a term according to the signature state of the original system **)
+let rec get_term : Sign.t -> Xml.xml -> term = fun sign xml ->
+  match Xml.tag xml with
+  | "var"    -> (* to finish *) assert false
+  | "funapp" -> begin match Xml.children xml with
+      | []        -> assert false
+      | f :: args ->
+          match get_only_child f with
+          | Xml.Element _   -> assert false
+          | Xml.PCData str  ->
+              let args = List.map (get_arg sign) args in
+              let s, path =
+                match String.split_on_char '_' str with
+                | ["c"; path; s] ->
+                    s, String.split_on_char '.' path
+                | _              -> assert false in
+              let sign = PathMap.find path Sign.(!loaded) in
+              let sym =
+                try symb (Sign.find sign s) with Not_found -> assert false in
+              List.fold_left (fun u v -> Appl (u, v)) sym args
+      end
+  | _        -> assert false
+
+(** [get_arg xml] translates an Xml node of tag name "arg" into a term **)
+and get_arg : Sign.t -> Xml.xml -> term = fun sign xml ->
+  get_term sign (get_only_child xml)
+
 (** [check_rule builtins r] check whether rule [r] is well-typed. The program
     fails gracefully in case of error. *)
 let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit

src/subject_reduction.ml

@@ -0,0 +1,43 @@
+open Terms
+open Print
+open Basics
+
+module Eset = Set.Make(
+  struct
+    type t = (term * term) 
+    let compare = Pervasives.compare
+  end)
+
+exception No_relation
+
+(** [find_relation t] calculates a pair of {!type:term} [A] and {!type:Eset.t}
+    [E] such that t:A[E] holds and raises the exception [No_relation] if
+    such a pair does not exist. Note that such a pair is unique if it exists
+    **)
+let find_relation : term -> (term * Eset.t) = fun t ->
+  let t = unfold t in
+  match t with
+  | Symb (s, _) -> (!s.sym_type, Eset.empty)
+  | Appl (_, _) ->
+      (* Check if t is of the form ft₁...tn” *)
+      let rec appl_aux : term list -> term -> (sym * term list) = fun acc t ->
+        match t with 
+        | Appl (t1, t2) -> appl_aux (t2 :: acc) t1
+        | Symb (s, _)   -> (s, acc)
+        | _             -> raise No_relation in 
+      let (s, ts) = appl_aux [] t in
+      let rs = List.map find_relation ts in
+      let rec cal_relation t tlist rs es = match tlist with
+        | []       -> (t, es)
+        | t1 :: ts -> begin
+            match t with
+            | Prod (a, b) ->
+                let t' = Bindlib.subst b t1 in
+                let (a1, e1) :: rs' = rs in
+                let es' = Eset.add (a1, a) (Eset.union es e1) in
+                cal_relation t' ts rs' es'
+            | _           -> raise No_relation 
+            end
+      in
+      cal_relation s.sym_type ts rs Eset.empty
+  | _           -> raise No_relation