Core Concepts
TopKAT, an extension of Kleene algebra with tests, is complete for reasoning about the domain and codomain of relations, even without additional axioms.
Abstract
The paper investigates the expressive power of TopKAT, an extension of Kleene algebra with tests (KAT), as a tool for reasoning about the domain and codomain of relations.
Key highlights:
TopKAT inherits many pleasant features of KAT, such as a decidable equational theory, but is incomplete with respect to relational models.
The authors show that TopKAT is complete with respect to domain and codomain comparison inequalities, which are crucial for encoding program logics like incorrectness logic and Hoare logic.
The authors prove this completeness result by leveraging the homomorphic structure of the reduction from TopKAT to KAT, which allows them to construct complete TopKAT interpretations from complete KAT interpretations.
The authors also show that this completeness result is tight, in the sense that it does not extend to the case where the terms contain the top element.
The new representation of the reduction technique could be of independent interest, as it simplifies several previous proofs and enables systematic generation of complete TopKAT interpretations.