Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Kleene algebra with commutativity conditions is undecidable

Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi

Abstract

We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.

Kleene algebra with commutativity conditions is undecidable

Abstract

We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.

Paper Structure

This paper contains 12 sections, 3 theorems, 48 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Kleene Algebra and Commutable Sets
  3. Commuting conditions
  4. Regular Languages
  5. Undecidability via Effective Inseparability
  6. Representing Relations
  7. Proving Representability
  8. Automata theory
  9. Bounded-Output Terms
  10. Putting Everything Together
  11. Conclusion and Related Work
  12. Detailed Proofs

Key Result

Theorem 9

Given a two-counter machine $M$ and some configuration $s \leq T_M$, we can compute a term $\rho$ with the following property. If $s \to _{R_M}^* c_1$, then the following inequality is valid in pre-Kleene algebra: $sR_M^* \leq \Sigma _M^*(C_M + c_1)_r + \Sigma _M^* \Sigma _M^{ \neq } \rho .$

Figures (1)

  • Figure 1: Algebraic constructions on commutable sets

Theorems & Definitions (16)

  • Example 1
  • Remark 2
  • Definition 3
  • Remark 4: Embedding algebras
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8: Running a two-counter machine
  • Theorem 9: Completeness
  • Theorem 10: Undecidability
  • ...and 6 more