Last change
on this file since 2919 was
2700,
checked in by sacerdot, 7 years ago

 exponential function dropped in favour of standard library
 fixpoint computation and graph colouring abstracted in the backend,
axiomatized in the compiler
 minor speedups in Policy.ma

File size:
806 bytes

Line  

1  include "common/Graphs.ma". 

2  

3  record property_lattice : Type[1] ≝ 

4  { l_property :> Type[0] 

5  ; l_bottom : l_property 

6  ; l_equal : l_property → l_property → bool 

7  ; l_included : l_property → l_property → bool 

8  ; l_is_maximal : l_property → bool 

9  }. 

10  

11  definition valuation ≝ λlatt : property_lattice.label → latt. 

12  definition rhs ≝ λlatt : property_lattice.valuation latt → latt. 

13  definition equations ≝ λlatt : property_lattice.label → rhs latt. 

14  

15  record fixpoint (latt : property_lattice) : Type[0] ≝ 

16  { fix_lfp :1> equations latt → valuation latt 

17  ; fix_correct : 

18  ∀eqs : equations latt. 

19  let sol ≝ fix_lfp eqs in 

20  ∀l : label. 

21  l_included latt (eqs l sol) (sol l) (* inclusion suffices for correctness *) 

22  }. 

23  

24  definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt. 

Note: See
TracBrowser
for help on using the repository browser.