Domain Reasoning in TopKAT
Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi

TL;DR
This paper investigates the completeness of TopKAT, an extension of Kleene algebra with tests, showing it is complete for domain comparisons but incomplete for arbitrary term comparisons, affecting certain program logic applications.
Contribution
It provides a detailed analysis of the completeness properties of TopKAT, highlighting its limitations and strengths in relational models for program reasoning.
Findings
TopKAT is complete for (co)domain comparison of KAT terms.
TopKAT is incomplete for (co)domain comparison of arbitrary TopKAT terms.
Incompleteness has limited impact on reasoning about under-approximate specifications.
Abstract
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
