source: src/utilities/fixpoints.ma @ 2896

Last change on this file since 2896 was 2700, checked in by sacerdot, 7 years ago
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
File size: 806 bytes
Line 
1include "common/Graphs.ma".
2
3record 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
11definition valuation ≝ λlatt : property_lattice.label → latt.
12definition rhs ≝ λlatt : property_lattice.valuation latt → latt.
13definition equations ≝ λlatt : property_lattice.label → rhs latt.
14
15record 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
24definition fixpoint_computer : Type[1] ≝ ∀latt.fixpoint latt.
Note: See TracBrowser for help on using the repository browser.