+(* 0: 7 4 0.312 3 5 7
+ 1: 29 6 0.549 3 8 16 24 29
+ 2: 120 10 25.525 3 8 19 39 66 95 113 119 120
+ 3: > 327 >9 3 8 19 39 75 134 208 274
+ 4: > 657 >9 3 8 19 39 75 139 245
+ 5: > 526 >8 3 8 19 39 75 139 245
+ 6: > 529 >8
+ 7: > 529 >8
+ 8: > 529 >8
+
+(CMM?)+ | (MM?C)+
+
+cCw = Cw
+-Cw = MCw
+cMw = CMw
+-MMw = -w
+-MCw = MMCw
+iw = w
+
+
+ s <= s' s <= s' s <= s' s <= s'
+=========== =========== ============ ==========
+ ws <= Cws' Cs <= Cs' CMs' <= Ms Ms' <= MCs
+
+ s <= s' s <= s'
+=========== ============
+ s <= MMs' Ms' <= Ms
+
+*)
+
type t = M | I | C
type w = t list
type eqclass = w list
+type dir = Le | Ge
+
let rules =
- [ [I;I], [I];
- [C;C], [C];
- [M;M], [];
- [M;C], [I;M];
- [C;M], [M;I];
-(*
-axiom leq_refl: ∀A. A ⊆ A.
-axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
-axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
-
-axiom i_contrattivita: ∀A. i A ⊆ A.
-axiom i_idempotenza: ∀A. i (i A) = i A.
-axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
-axiom c_espansivita: ∀A. A ⊆ c A.
-axiom c_idempotenza: ∀A. c (c A) = c A.
-axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
-axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
-axiom m_saturazione: ∀A. A ⊆ m (m A).
-axiom m_puntofisso: ∀A. m A = m (m (m A)).
-axiom th1: ∀A. c (m A) ⊆ m (i A).
-axiom th2: ∀A. i (m A) ⊆ m (c A).
-lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
-lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
-*)
+ [ [I], Le, [];
+ [C], Ge, [];
+ [I;I], Ge, [I];
+ [C;C], Le, [C];
+ [I], Le, [I];
+ [I], Ge, [I];
+ [C], Le, [C];
+ [C], Ge, [C];
+ [C;M], Le, [M;I];
+ [C;M;I], Le, [M;I]; (* ??? *)
+ [I;M], Le, [M;C];
+ [I;M;C], Ge, [I;M]; (* ??? *)
+ [M;M;M], Ge, [M];
+ [M;M], Ge, [];
+ [M], Le, [M];
+ [M], Ge, [M];
+ (* classical
+ [M;M], Le, [];
+ [C;M], Ge, [M;I];
+ *)
]
;;
-let print_w w =
- String.concat ""
- (List.map (function I -> "i" | C -> "c" | M -> "-") w)
+let inject =
+ let cache = Hashtbl.create 5393 in
+ function w ->
+ try
+ Hashtbl.find cache w
+ with
+ Not_found ->
+ let rec aux acc =
+ function
+ [] -> acc
+ | he::tl -> aux (4 * acc + (match he with I -> 1 | C -> 2 | M -> 3)) tl
+ in
+ let res = 0, aux 0 w, w in
+ Hashtbl.add cache w res;
+ res
;;
-let print_eqclass eqc =
- let eqc = List.sort compare eqc in
- prerr_endline (String.concat "=" (List.map print_w eqc))
-;;
+module VL =
+ struct
+ type t = eqclass
+ let compare = compare
+ let hash = Hashtbl.hash
+ let equal = (=)
+ end
-let print = List.iter print_eqclass;;
+module GL = Graph.Imperative.Digraph.Concrete(VL);;
-exception NoMatch;;
+let swap = function Le -> Ge | Ge -> Le;;
-let apply_rule_at_beginning (lhs,rhs) l =
- let rec aux =
- function
- [],l -> l
- | x::lhs,x'::l when x = x' -> aux (lhs,l)
- | _,_ -> raise NoMatch
- in
- rhs @ aux (lhs,l)
+let rec new_dir dir =
+ function
+ [] -> dir
+ | M::tl -> new_dir (swap dir) tl
+ | (C|I)::tl -> new_dir dir tl
;;
-let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2
+let string_of_w w =
+ let s =
+ String.concat ""
+ (List.map (function I -> "i" | C -> "c" | M -> "-") w)
+ in
+ if s = "" then "." else s
;;
-let rec apply_rule rule w =
- (try
- [apply_rule_at_beginning rule w]
- with
- NoMatch -> []) @
- match w with
- [] -> []
- | he::tl -> [he] @@ apply_rule rule tl
+let string_of_w' w =
+ let s =
+ String.concat ""
+ (List.map (function I -> "i" | C -> "c" | M -> "m") w)
+ in
+ if s = "" then "E" else s
;;
-let uniq =
- let rec aux l =
- function
- [] -> l
- | he::tl -> aux (if List.mem he l then l else he::l) tl
+let string_of_eqclass l = String.concat "=" (List.map string_of_w l);;
+
+let name_of_eqclass l = String.concat "_" (List.map string_of_w' l);;
+
+exception NoMatch;;
+
+let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2;;
+
+let uniq l =
+ let rec aux acc = function
+ | [] -> acc
+ | h::[] -> h::acc
+ | h1::h2::tl when h1=h2 -> aux (h2::acc) tl
+ | h1::tl (* when h1 <> h2 *) -> aux (h1::acc) tl
in
- aux []
+ List.rev (aux [] (List.sort compare l))
;;
-let apply_rules w =
- let rec aux =
- function
- [] -> [w]
- | rule::rules -> apply_rule rule w @ aux rules
- in
- uniq (aux rules)
+let rec apply_rule_at_beginning (lhs,dir',rhs) (w,dir) =
+ if dir <> dir' then
+ raise NoMatch
+ else
+ let rec aux =
+ function
+ [],w -> w
+ | x::lhs,x'::w when x = x' -> aux (lhs,w)
+ | _,_ -> raise NoMatch in
+ let w' = aux (lhs,w) in
+ if List.length rhs < List.length lhs then rhs @@ [w']
+ else rhs @@ apply_rules (aux (lhs,w),new_dir dir lhs)
+and apply_rules (w,_ as w_and_dir) =
+ if w = [] then [[]]
+ else
+ let rec aux =
+ function
+ [] -> []
+ | rule::tl ->
+ (try apply_rule_at_beginning rule w_and_dir
+ with NoMatch -> [])
+ @
+ aux tl
+ in
+ aux rules
;;
-let subseteq l1 l2 =
- List.for_all (fun x -> List.mem x l2) l1
+let apply_rules (w,dir as w_and_dir) =
+ List.map (fun w' -> w,dir,w')
+ (uniq (apply_rules w_and_dir))
;;
-let (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;
+let step (l : w list) =
+ uniq
+ (List.flatten
+ (List.map
+ (function w ->
+ List.map (fun x -> x@w)
+ (if List.length (List.filter (fun w -> w = M) w) >= 5 then
+ [[I];[C]]
+ else
+ [[I];[C];[M]])
+ ) l))
+;;
-let simplify eqc =
- let rec aux l =
- let l' = uniq (List.flatten (List.map apply_rules l)) in
- if l === l' then l else aux l'
+let mapi f l =
+ let rec aux acc i =
+ function
+ [] -> acc
+ | he::tl ->
+ if i mod 1000 = 0 then
+ begin
+ print_string ("@" ^ string_of_int i ^ " ");
+ flush stdout;
+ end;
+ aux (f he :: acc) (i+1) tl
in
- aux eqc
+ let res = List.rev (aux [] 1 l) in
+ print_newline ();
+ res
;;
-let combine_class_with_classes l1 =
- let rec aux =
+let iteri f l =
+ let rec aux i =
function
- [] -> [l1]
- | l2::tl ->
- if List.exists (fun x -> List.mem x l2) l1 then
- uniq (l1 @ l2) :: tl
- else
- l2:: aux tl
+ [] -> ()
+ | he::tl ->
+ if i mod 1000 = 0 then
+ begin
+ print_string ("@" ^ string_of_int i ^ " ");
+ flush stdout;
+ end;
+ f he; aux (i+1) tl
in
- aux
+ aux 1 l;
+ print_newline ();
;;
-let combine_classes l =
- let rec aux acc =
- function
- [] -> acc
- | he::tl -> aux (combine_class_with_classes he acc) tl
+let normalize canonical (l : w list) =
+ print_endline (string_of_int (List.length l) ^ " nodes to be normalized");
+ let rec aux all l =
+ let rels =
+ List.flatten
+ (mapi (fun x -> apply_rules (x,Le) @ apply_rules (x,Ge)) l) in
+ let arcs =
+ mapi
+ (function (x,rel,y) ->
+ let x = canonical x(*(inject x)*) in
+ let y = canonical y(*(inject y)*) in
+ match rel with Le -> x,y | Ge -> y,x) rels in
+ let res = uniq arcs in
+ let nodes = uniq (l @ List.map (fun (_,_,n) -> n) rels) in
+ let new_nodes = List.filter (fun n -> not (List.mem n all)) nodes in
+ let new_nodes = List.filter (function n -> [n] = canonical n) new_nodes in
+ if new_nodes = [] then
+ res
+ else
+ uniq (res @ aux nodes new_nodes)
in
- aux [] l
+ aux l l
;;
-let step (s : eqclass list) =
- let ns = ref [] in
- List.iter (function eqc -> ns := eqc::!ns) s;
- List.iter
- (function eqc ->
- List.iter
- (function x ->
- let eqc = simplify ([x] @@ eqc) in
- if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
- ns := eqc::!ns
- ) [I;C;M]
- ) s;
- combine_classes !ns
+let visualize graph =
+ let module GL =
+ struct
+ include GL;;
+ let edge_attributes _ = []
+ let default_edge_attributes _ = []
+ let get_subgraph _ = None
+ let vertex_attributes v = [`Label (string_of_eqclass (GL.V.label v))]
+ let vertex_name v = name_of_eqclass (GL.V.label v)
+ let default_vertex_attributes _ = []
+ let graph_attributes _ = []
+ end in
+ let module D = Graph.Graphviz.Dot(GL) in
+ let ch = open_out "/tmp/comb.dot" in
+ D.output_graph ch graph;
+ close_out ch;
+ ignore (Unix.system ("tred /tmp/comb.dot > /tmp/red.dot"));
+ ignore (Unix.system ("dot -Tps /tmp/red.dot > /tmp/red.ps"));
+ (*Unix.system ("ggv /tmp/red.ps");*)
;;
-let classes = step (step (step (step [[[]]]))) in
- prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
- print classes
+let w_compare s1 s2 =
+ let c = compare (List.length s1) (List.length s2) in
+ if c = 0 then compare s1 s2 else c
+;;
+
+exception Found of GL.V.t;;
+
+let rec iter n cgraph (canonical: w -> GL.V.t) =
+ print_endline ("STEP " ^ string_of_int n);
+ let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in
+ let nodes = step (List.map List.hd nodes) in
+(*let nodes = [[C;M];[C;M;C;M];[C;M;C;M;C;M];[C;M;C;M;C;M;C;M];[C;M;C;M;C;M;C;M;C;M]] in*)
+(*let nodes = [[C;I;C;I;C;I]] in*)
+ (*let nodes = step (List.concat nodes) in*)
+(*List.iter (fun x -> prerr_endline ("#@ " ^ string_of_w x)) nodes;*)
+ let arcs = normalize canonical nodes in
+ iteri (fun (x,y) -> if x <> y then GL.add_edge cgraph x y) arcs;
+(*List.iter (fun (x,y) -> prerr_endline (string_of_eqclass x ^ " -> " ^ string_of_eqclass y)) arcs;*)
+
+ print_endline ("<scc>");
+ let classes,norm =
+ let module SCC = Graph.Components.Make(GL) in SCC.scc cgraph in
+ let xxx =
+ let module SCC = Graph.Components.Make(GL) in SCC.scc_array cgraph in
+ print_endline ("</scc>");
+ let get_canonical n =
+ try List.sort w_compare (List.concat (xxx.(norm n)))
+ with Not_found -> n
+ in
+ let nodes = GL.fold_vertex (fun n l -> n::l) cgraph [] in
+ print_endline "get_canonical";
+ let nodes = mapi (fun n -> n,get_canonical n) nodes in
+ print_endline "/get_canonical";
+ print_endline ("collapse " ^ string_of_int (List.length nodes));
+ iteri
+ (function (n,n') ->
+ let succ = GL.succ cgraph n in
+ let pred = GL.pred cgraph n in
+ GL.remove_vertex cgraph n;
+ let add_edge s t = if s <> t then GL.add_edge cgraph s t in
+ List.iter (fun s -> add_edge n' (get_canonical s)) succ;
+ List.iter (fun p -> add_edge (get_canonical p) n') pred)
+ nodes;
+ print_endline (string_of_int classes ^ " classes");
+ print_endline ("-----");
+ print_endline "visualize";
+ visualize cgraph;
+ print_endline ("/////");
+ GL.iter_vertex (fun l -> print_endline ("?" ^ string_of_eqclass l)) cgraph;
+ let canonical =
+ function (*_,_,*)w ->
+ try
+ GL.iter_vertex (fun l -> if List.mem w l then raise (Found l)) cgraph;
+ [w]
+ with
+ Found l -> l in
+ if n > 0 then
+ iter (n - 1) cgraph canonical
+ else
+ ()
+in
+ let cgraph = GL.create () in
+ GL.add_vertex cgraph [[]];
+ iter 9 cgraph (fun w(*(_,_,w)*) -> [w])
;;
projects / helm.git / blobdiff