Ignore:
Timestamp:
Sep 6, 2011, 3:49:31 PM (8 years ago)
Author:
mulligan
Message:

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1192 r1193  
    88(* vertex sets *)
    99axiom vertex_set: Type[0].
     10axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
     11axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
     12axiom vs_subset: vertex_set → vertex_set → bool.
    1013
    1114(* vertex maps *)
    12 axiom vertex_map: Type[0].
     15axiom vertex_map: Type[0] → Type[0].
     16axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    1317
    1418definition interference_graph ≝ graph label.
     
    3539  interference_graph → option vertex.
    3640axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    37 axiom ig_ipp: interference_graph → vertex → list vertex.
     41axiom ig_ipp: interference_graph → vertex → vertex_set.
    3842axiom ig_iph: interference_graph → vertex → list Register.
    39 axiom ig_ppp: interference_graph → vertex → list vertex.
     43axiom ig_ppp: interference_graph → vertex → vertex_set.
    4044axiom ig_pph: interference_graph → vertex → list Register.
    4145definition ig_ppedge ≝ vertex × vertex.
Note: See TracChangeset for help on using the changeset viewer.