source: src/utilities/fixpoints.ma @ 2327

Last change on this file since 2327 was 2174, checked in by tranquil, 8 years ago
  • factored out script for (axiomatised) fixpoint computation
  • ERTL → LTL pass
File size: 785 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
24axiom the_fixpoint : ∀latt.fixpoint latt.
Note: See TracBrowser for help on using the repository browser.