On Propositional Program Equivalence (extended abstract)

TL;DR

This paper explores propositional program equivalence within the framework of (Guarded) Kleene Algebra with Tests, focusing on decidability and practical verification of program transformations.

Contribution

It discusses recent advances in propositional equivalence using (G)KAT, highlighting decidability and practical verification methods.

Findings

Propositional equivalence is decidable and practically feasible.

(G)KAT provides a formal framework for reasoning about propositional program equivalence.

Recent developments improve verification of program transformations.

Abstract

General program equivalence is undecidable. However, if we abstract away the semantics of statements, then this problem becomes not just decidable, but practically feasible. For instance, a program of the form "if $b$ then $e$ else $f$" should be equivalent to "if not $b$ then $f$ else $e$" - no matter what $b$, $e$ and $f$ are. This kind of equivalence is known as propositional equivalence. In this extended abstract, we discuss recent developments in propositional program equivalence from the perspective of (Guarded) Kleene Algebra with Tests, or (G)KAT.