|
Weak Kleene Algebra and Computation Trees
Ernie Cohen
Weak Kleene Algebra and Computation Trees
The Kleene algebra axioms are too strong for some program models of interest (e.g. models that mix demonic choice with angelic or probabilistic choice). This has led to proposals that weaken the right distributivity axiom to monotonicity, and possibly weaken or eliminate the right induction and left annihilation axioms (e.g. lazy Kleene algebra, probabilistic Kleene algebra, monodic tree Kleene algebra, etc.). We'll address some of the basic metatheoretic properties of these theories using rational trees modulo simulation equivalence.