[Toss-devel-svn] SF.net SVN: toss:[1462] trunk/Toss/Formula

[<luk...@us...>]

Revision: 1462
          http://toss.svn.sourceforge.net/toss/?rev=1462&view=rev
Author:   lukaszkaiser
Date:     2011-05-27 22:09:16 +0000 (Fri, 27 May 2011)

Log Message:
-----------
Corrections to subst_rels, tnf_fv over fixed-points and more tests.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOpsTest.ml

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-05-26 23:14:21 UTC (rev 1461)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-05-27 22:09:16 UTC (rev 1462)
@@ -604,20 +604,7 @@
   let cdefs = List.map (fun (n, (v, f)) -> (n, ([], v, f))) defs in
   map_to_atoms_expr (subst_r cdefs) r
 
-(* Helper function: fixed-point up to [n] *)
-let rec fp_n print n f x =
-  let nx = f x in
-  if nx = x then x else 
-    if n = 0 then 
-      let msg = (print x) ^ " " ^ (print nx) in
-      failwith ("fixpoint not reached: " ^ msg)
-    else
-      fp_n print (n-1) f nx
 
-(* Substitute recursively in [r] relations defined in [defs]. *)
-let subst_rels_expr defs r =
-  fp_n real_str (List.length defs) (subst_once_rels_expr defs) r
-
 (* Substitute recursively in [phi] relations defined in [defs]. *)
 let subst_rels defs phi =
   let rels f = 
@@ -650,27 +637,51 @@
 	  let (d, ds) = (List.hd otherc, (List.tl otherc) @ selfc) in
 	  rec_subst_rels (subst_once_defs [d] ds) (subst_once_fm [d] phi)
 	else
-	  let sovar n = so_var_of_string ("|" ^ n) in
+	  (* Here we must replace a simultaneous least fixed-point with
+	     single ones. In the future we should probably add simultaneous
+	     fixed-points to our logic. For now we use the Bekic principle, cf
+	     "Finite Model Theory and Descriptive Complexity", Lemma 3.3.41,
+	     at www.logic.rwth-aachen.de/pub/graedel/FMTbook-Chapter3.pdf *)
+	  let sovar vs n = 
+	    let m = if Array.length vs = 1 then n else "|" ^ n in
+	    mso_or_so_var_of_string m in
 	  let sorels rels = function 
-	    | Rel (m, rvs) when List.mem m rels -> SO (sovar m, rvs)
+	    | Rel (m, rvs) when List.mem m rels -> 
+	      let mv = (sovar rvs m :> var) in
+	      if Array.length rvs = 1 then In (rvs.(0), to_mso mv) else
+		SO (to_so mv, rvs)
 	    | x -> x in
 	  let do_lfp (n, (calls, vs, f)) =
 	    let va = Array.of_list (List.map fo_var_of_string vs) in
 	    let nf = map_to_atoms (sorels [n]) f in
-	    (n, ([], vs, Lfp ((sovar n :> [mso_var | so_var]), va, nf))) in
+	    (n, ([], vs, Lfp (sovar va n, va, nf))) in
 	  let (d, ds) = do_lfp (List.hd selfc), List.tl selfc in
 	  rec_subst_rels (subst_once_defs [d] ds) (subst_once_fm [d] phi) in
   let res_phi = rec_subst_rels cdefs phi in
-  let simpfpvars = List.map (fun (n, _) -> "|" ^ n) cdefs in (*TODO:reoccurs?*)
-  let rec simp_def_lfp acc fpvar fpvs fpdef =
-    if List.mem fpvar acc && List.mem (var_str fpvar) simpfpvars then
-      SO (to_so (fpvar :> var), fpvs)
-    else
-      let smap = { identity_map with map_Lfp = simp_def_lfp (fpvar :: acc) } in 
-      Lfp (fpvar, fpvs, map_formula smap fpdef) in
-  map_formula { identity_map with map_Lfp = simp_def_lfp []} res_phi
+  if syntax_ok res_phi then
+    let simpfpvars = (* TODO: is it ok to simplify all these? name clashes? *)
+      List.concat (List.map (fun (n, _) -> [n; "|" ^ n]) cdefs) in 
+    let rec simp_def_lfp acc fpvar fpvs fpdef =
+      if List.mem fpvar acc && List.mem (var_str fpvar) simpfpvars then
+	match mso_or_so_var_of_string (var_str fpvar) with
+	  | `MSO v -> In (fpvs.(0), `MSO v)
+	  | `SO v -> SO (`SO v, fpvs)
+      else
+	let smap = { identity_map with map_Lfp = simp_def_lfp (fpvar::acc) } in 
+	Lfp (fpvar, fpvs, map_formula smap fpdef) in
+    map_formula { identity_map with map_Lfp = simp_def_lfp []} res_phi
+  else failwith ("subst_defs: non-stratified recursion?\n" ^ (str res_phi))
 
 
+(* Substitute recursively in [r] relations defined in [defs]. *)
+let rec subst_rels_expr defs = function
+  | RVar _ | Const _ | Fun _ as x -> x
+  | Times (r1, r2) -> Times (subst_rels_expr defs r1, subst_rels_expr defs r2)
+  | Plus (r1, r2) -> Plus (subst_rels_expr defs r1, subst_rels_expr defs r2)
+  | Char (phi) -> Char (subst_rels defs phi)
+  | Sum (vs, phi, r) -> Sum (vs, subst_rels defs phi, subst_rels_expr defs r)
+
+
 (* --- AType with variables over given relations, no repetition, equality --- *)
 
 let atp rels vars_in =
@@ -1567,13 +1578,19 @@
 
 let rec push_quant f = push_in_quant (flatten_sort (f))
 
-let tnf_fv ?sizes phi =
+let tnf_fv_nofp ?sizes phi =
   let fv = free_vars phi in
   let psi = rename_quant_avoiding [] (Ex (fv, phi)) in
   match mso_last (flatten (del_vars_quant fv (tnf psi))) with
     | Or fl -> Or (List.map (order_by_fv_phi sizes []) fl)
     | f -> order_by_fv_phi sizes [] f
 
+let tnf_fv ?sizes phi =
+  let tnf_lfp fprel fpvs fpdef = Lfp (fprel, fpvs, tnf_fv_nofp ?sizes fpdef) in
+  let psi = map_formula { identity_map with map_Lfp = tnf_lfp } phi in
+  tnf_fv_nofp ?sizes psi
+
+
 (* Assign emptyset to the MSO-variable v by replacing "x in X" with "false".  *)
 let assign_emptyset v phi =
   let replace_by_emptyset v = function

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-26 23:14:21 UTC (rev 1461)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-05-27 22:09:16 UTC (rev 1462)
@@ -332,6 +332,16 @@
 	     " (|S(x, y) or Q(x) or |R(x, y)))) and " ^
 	     "lfp |S(x, y) = ((|S(x, y) or Q(x) or lfp |R(x, y) =" ^ 
 	     " (|R(x, y) or P(x) or |S(x, y))))");
+       defs_eq
+	 [("T", (["x"], formula_of_string "P(x) or ex y (E(x, y) and T(y))"))]
+	 "T(x)" "lfp T(x) = (P(x) or ex y (E(x, y) and y in T))";
+       defs_eq
+	 [("R", (["x"], formula_of_string "S(x) or ex y (E(x, y) and R(y))"));
+	  ("S", (["x"], formula_of_string "R(x) or ex y (F(x, y) and S(y))"))]
+	 "R(x) and S(x)"
+	 ("(lfp R(x) = ((lfp S(x) = (x in R or ex y (F(x, y) and y in S)) or "^
+             " ex y (E(x, y) and y in R))) and lfp S(x) = ((lfp R(x)= (x in S"^
+	     " or ex y (E(x, y) and y in R)) or ex y (F(x, y) and y in S))))");
      );
 
    "atp, mintp" >::


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.