Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness
Abstract
Guarded Kleene Algebra with Tests (GKAT) axiomatizes equivalence between uninterpreted WHILE programs. Like its predecessor Kleene Algebra with Tests (KAT), GKAT comes with a rich algebraic and coalgebraic theory, which gives rise to both completeness and decidability results. Unlike KAT, however, equivalence between GKAT terms can be decided in nearly linear time, for a fixed number of tests.
We study a fragment of GKAT that distinguishes programs that fail immediately from programs that perform some actions before failing, obtained by omitting the so called early termination axiom. Our main result is that this fragment also admits completeness and decidability results, and indeed the same results on the level of GKAT proper follow as a corollary. Our proof method reveals an interesting connection between the semantics of WHILE programs and a something called a "coequation" --- i.e., the categorical dual to an equation.
This is joint work with Todd Schmid, Alexandra Silva, and Dexter Kozen.
