Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests

TL;DR

This paper demonstrates how Kozen and Tiuryn's substructural logic for program correctness can be embedded into an expanded form of Kleene algebra with tests, residuals, and adjoint operators, unifying logical reasoning with algebraic structures.

Contribution

It introduces an embedding of Kozen and Tiuryn's logic into a residuated Kleene algebra with tests, expanding the algebraic framework for reasoning about program correctness.

Findings

Kozen and Tiuryn's logic embeds into the algebraic structure.

The expansion includes residuals and adjoint operators.

This unifies logical and algebraic reasoning for program correctness.

Abstract

Kozen and Tiuryn have introduced the substructural logic $\mathsf{S}$ for reasoning about correctness of while programs (ACM TOCL, 2003). The logic $\mathsf{S}$ distinguishes between tests and partial correctness assertions, representing the latter by special implicational formulas. Kozen and Tiuryn's logic extends Kleene altebra with tests, where partial correctness assertions are represented by equations, not terms. Kleene algebra with codomain, $\mathsf{KAC}$, is a one-sorted alternative to Kleene algebra with tests that expands Kleene algebra with an operator that allows to construct a Boolean subalgebra of tests. In this paper we show that Kozen and Tiuryn's logic embeds into the equational theory of the expansion of $\mathsf{KAC}$ with residuals of Kleene algebra multiplication and the upper adjoint of the codomain operator.