Domain Reasoning in TopKAT

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 relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.