wqo1.ml 3.43 KB
Newer Older
SimonHalfon's avatar
SimonHalfon committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
(* WQO Effectif *)
module type Effective_WQO = 
  sig
    type xX
    val ord: xX -> xX -> bool
    type idl	
    val idl_inclusion: idl -> idl -> bool
  end ;;

(* WQO Effectif Extra, genere automatiquement *)
module type Effective_WQO_Extra =
  sig
    include Effective_WQO

    type filter = xX
    type upc = filter list
    type dwc = idl list

    val pf: xX -> filter		   
    val create_upc: filter -> upc
    val create_dwc: idl -> dwc
    val upc_inclusion: upc -> upc -> bool
    val dwc_inclusion: dwc -> dwc -> bool
    val upc_union: upc -> upc -> upc
    val dwc_union: dwc -> dwc -> dwc 
  end ;;

(* WQO Ideally Effective *)    
module type Ideally_Effective_WQO = 
  sig
    include Effective_WQO_Extra

    val filter_intersection: filter -> filter -> upc
    val filter_complement: filter -> dwc
    val filter_X: upc
    
    val pi: xX -> idl
    val idl_intersection: idl -> idl -> idl
    val idl_complement: idl -> upc
    val idl_X: dwc
  end ;;

(* WQO Ideally Effective Extra *)
module type Ideally_Effective_WQO_Extra = 
  sig
    (* Fully Effective *)
    include Ideally_Effective_WQO
    (* Operations on UPC and DWC *)
    val upc_intersection: upc -> upc -> upc
    val dwc_intersection: dwc -> dwc -> dwc
    val upc_complement: upc -> dwc
    val dwc_complement: dwc -> upc
  end ;;





  (* ====================== FUNCTORS: STEP 1 ======================= *)



module Effective_2_Extra (X: Effective_WQO): Effective_WQO_Extra
  with type xX = X.xX and type idl = X.idl =
  struct
    include X

    type filter = xX
    type upc = filter list
    type dwc = idl list

    let pf x = x
    let create_upc f = [f]
    let create_dwc i = [i]
    let upc_inclusion u1 u2 = List.for_all (fun x -> List.exists (fun y -> ord y x) u2) u1
    let dwc_inclusion d1 d2 = List.for_all (fun i -> List.exists (fun j -> idl_inclusion i j) d2) d1
    let upc_union = (@)
    let dwc_union = (@)
  end ;;			   

  
(* WQO des Entiers Naturels *)    
type nat_idl = N of int | Om ;;

module Nat: Effective_WQO with type xX = int and type idl = nat_idl =
  struct
    type xX = int
    let ord x y = x <= y
    type idl = nat_idl
    let idl_inclusion i j = match (i,j) with
      | (Om, j) -> j = Om
      | (j, Om) -> true
      | (N(n), N(m)) -> ord n m
  end ;; 			  


module NE = Effective_2_Extra (Nat) ;;






  
  (* ====================== FUNCTORS: STEP 2 ======================= *)


module Ideally_2_Extra (X: Ideally_Effective_WQO): Ideally_Effective_WQO_Extra
       with type xX = X.xX and type idl = X.idl =
  struct
    include X

    let upc_intersection = (@) (* Some code ... *)
    let dwc_intersection = (@) (* Some code ... *)			     

    let rec upc_complement = function
      | [] -> idl_X
      | f::u -> dwc_intersection (filter_complement f) (upc_complement u)
				 
    let rec dwc_complement = function
      | [] -> filter_X
      | i::d -> upc_intersection (idl_complement i) (dwc_complement d)
  end ;;



module NI: Ideally_Effective_WQO with type xX = int and type idl = nat_idl =
  struct
    include NE

    let filter_intersection n m = [max n m]
    let filter_complement n = if n = 0 then [] else [N(n-1)]
    let filter_X = [0]

    let pi n = N(n)
    let idl_intersection i j = min i j
    let idl_complement = function
      | Om -> []
      | N(n) -> [n+1]
    let idl_X = [Om]
  end ;;		  
		
		     							      
module NIE = Ideally_2_Extra (NI) ;;
  




(* PROBLEME: les fonctions auxiliaires de NAT et NI ne sont plus visibles dans NIE ! *)