arXiv · 0801.2368
Feasibly Reducing KAT Equations to KA Equations
Abstract
Kleene algebra (KA) is the algebra of regular events. Familiar examples of Kleene algebras include regular sets, relational algebras, and trace algebras. A Kleene algebra with tests (KAT) is a Kleene algebra with an embedded Boolean subalgebra. The addition of tests allows one to encode {\tt while} programs as KAT terms, thus the equational theory of KAT can express (propositional) program equivalence. More complicated statements about programs can be expressed in the Hoare theory of KAT, which suffices to encode Propositional Hoare Logic. That the equational theory of KAT reduces to the equational theory of KA has been shown by Cohen et al. Unfortunately, their reduction involves an exponential blowup in the size of the terms involved. Here we give an alternate feasible reduction.
Explore related subjects
Keep this discovery
James Worthington. 2008-01-15. Feasibly Reducing KAT Equations to KA Equations. https://arxiv.org/abs/0801.2368
Cite the original work for its findings. Save a collection to share your selection of sources.