helm/software/matita/contribs/formal_topology/bin/comb.ml

   1 type t = M | I | C
   2 type w = t list
   3 type eqclass = w list
   4
   5 let rules =
   6  [ [I;I],   [I];
   7    [C;C],   [C];
   8    [M;M],   [];
   9    [M;C],   [I;M];
  10    [C;M],   [M;I];
  11 (*
  12 axiom leq_refl: ∀A. A ⊆ A.
  13 axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
  14 axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
  15
  16 axiom i_contrattivita: ∀A. i A ⊆ A.
  17 axiom i_idempotenza: ∀A. i (i A) = i A.
  18 axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
  19 axiom c_espansivita: ∀A. A ⊆ c A.
  20 axiom c_idempotenza: ∀A. c (c A) = c A.
  21 axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
  22 axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
  23 axiom m_saturazione: ∀A. A ⊆ m (m A).
  24 axiom m_puntofisso: ∀A. m A = m (m (m A)).
  25 axiom th1: ∀A. c (m A) ⊆ m (i A).
  26 axiom th2: ∀A. i (m A) ⊆ m (c A).
  27 lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
  28 lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
  29 *)
  30  ]
  31 ;;
  32
  33 let print_w w =
  34  String.concat ""
  35   (List.map (function I -> "i" | C -> "c" | M -> "-") w)
  36 ;;
  37
  38 let print_eqclass eqc =
  39  let eqc = List.sort compare eqc in
  40   prerr_endline (String.concat "=" (List.map print_w eqc))
  41 ;;
  42
  43 let print = List.iter print_eqclass;;
  44
  45 exception NoMatch;;
  46
  47 let apply_rule_at_beginning (lhs,rhs) l =
  48  let rec aux =
  49   function
  50      [],l -> l
  51    | x::lhs,x'::l when x = x' -> aux (lhs,l)
  52    | _,_ -> raise NoMatch
  53  in
  54   rhs @ aux (lhs,l)
  55 ;;
  56
  57 let (@@) l1 ll2 = List.map (function l2 -> l1 @ l2) ll2
  58 ;;
  59
  60 let rec apply_rule rule w =
  61  (try
  62    [apply_rule_at_beginning rule w]
  63   with
  64    NoMatch -> []) @
  65  match w with
  66     [] -> []
  67   | he::tl -> [he] @@ apply_rule rule tl
  68 ;;
  69
  70 let uniq =
  71  let rec aux l =
  72   function
  73      [] -> l
  74    | he::tl -> aux (if List.mem he l then l else he::l) tl
  75  in
  76   aux []
  77 ;;
  78
  79 let apply_rules w =
  80  let rec aux =
  81   function
  82      [] -> [w]
  83    | rule::rules -> apply_rule rule w @ aux rules
  84  in
  85   uniq (aux rules)
  86 ;;
  87
  88 let subseteq l1 l2 =
  89  List.for_all (fun x -> List.mem x l2) l1
  90 ;;
  91
  92 let (===) l1 l2 = subseteq l1 l2 && subseteq l2 l1;;
  93
  94 let simplify eqc =
  95  let rec aux l =
  96   let l' = uniq (List.flatten (List.map apply_rules l)) in
  97   if l === l' then l else aux l'
  98  in
  99   aux eqc
 100 ;;
 101
 102 let combine_class_with_classes l1 =
 103  let rec aux =
 104   function
 105      [] -> [l1]
 106    | l2::tl ->
 107       if List.exists (fun x -> List.mem x l2) l1 then
 108        uniq (l1 @ l2) :: tl
 109       else
 110        l2:: aux tl
 111  in
 112   aux
 113 ;;
 114
 115 let combine_classes l =
 116  let rec aux acc =
 117   function
 118      [] -> acc
 119    | he::tl -> aux (combine_class_with_classes he acc) tl
 120  in
 121   aux [] l
 122 ;;
 123
 124 let step (s : eqclass list) =
 125  let ns = ref [] in
 126   List.iter (function eqc -> ns := eqc::!ns) s;
 127   List.iter
 128    (function eqc ->
 129      List.iter
 130       (function x ->
 131         let eqc = simplify ([x] @@ eqc) in
 132          if not (List.exists (fun eqc' -> eqc === eqc') !ns) then
 133           ns := eqc::!ns
 134       ) [I;C;M]
 135    ) s;
 136   combine_classes !ns
 137 ;;
 138
 139 let classes = step (step (step (step [[[]]]))) in
 140  prerr_endline ("Numero di classi trovate: " ^ string_of_int (List.length classes));
 141  print classes
 142 ;;