On Propositional Program Equivalence (extended abstract)

2025/07/10 by Kappé, Tobias
#FOS: Computer and information sciences #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2507.07480

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.

Citations

• A General Completeness Theorem for Skip-free Star Algebras
• Kleene algebra with commutativity conditions is undecidable
• A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
• Kleene Algebra with Dynamic Tests: Completeness and Complexity
• Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity
• A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
• An Elementary Proof of the FMP for Kleene Algebra
• Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete (Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions)
• A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
• Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
• A Coalgebraic Approach to Kleene Algebra with Tests
• Kleene algebra with tests
• Efficiency of a Good But Not Linear Set Union Algorithm
• Letters to the editor: go to statement considered harmful

Related

• Alternative Characterizations for Strong Equivalence of Logic Programs
• A Common View on Strong, Uniform, and Other Notions of Equivalence in Answer-Set Programming
• Strong Equivalence Made Easy: Nested Expressions and Weight Constraints
• Kleene algebra with tests
• Semantical Characterizations and Complexity of Equivalences in Answer Set Programming