One-sorted Program Algebras

TL;DR

This paper introduces a generalized one-sorted algebraic framework that extends Kleene algebra with domain (KAD), aiming to retain properties of Kleene algebra with tests (KAT) while avoiding some of KAD's limitations.

Contribution

It proposes a new generalized framework for KAD that embeds KAT's equational theory and incorporates natural properties of the domain operator.

Findings

The generalized framework embeds KAT's equational theory.

Natural properties of the domain operator can be added without losing results.

A variant using residuals for test complementation is considered.

Abstract

Kleene algebra with tests, KAT, provides a simple two-sorted algebraic framework for verifying properties of propositional while programs. Kleene algebra with domain, KAD, is a one-sorted alternative to KAT. The equational theory of KAT embeds into KAD, but KAD lacks some natural properties of KAT. For instance, not each Kleene algebra expands to a KAD, and the subalgebra of tests in each KAD is forced to be the maximal Boolean subalgebra of the negative cone. In this paper we propose a generalization of KAD that avoids these features while still embedding the equational theory of KAT. We show that several natural properties of the domain operator of KAD can be added to the generalized framework without affecting the results. We consider a variant of the framework where test complementation is defined using a residual of the Kleene algebra multiplication.