Pith. sign in

REVIEW 2 major objections 5 minor 21 references

Kleene algebra with commutativity conditions is undecidable

T0 review · 2 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Adding commutation equations between primitive symbols makes Kleene algebra's equality problem undecidable, even for algebras without induction axioms.

desk verdict The pre-Kleene undecidability result is likely correct but Theorem 18 is false as stated — the reduction needs an injectivity hypothesis on l' that is never supplied. read the letter →

arxiv 2411.15979 v1 pith:D7S6ZPYS submitted 2024-11-24 math.LO cs.CCcs.CLcs.LOcs.PL

Arthur Azevedo de Amorim , Cheng Zhang , Marco Gaboardi This is my paper · ORCID
classification math.LOcs.CCcs.CLcs.LOcs.PL MSC 03B2503D3568Q45
keywords Kleenealgebracommutativityconditionsequationaltheoryundecidabilitypre-Kleeneeffectiveinseparabilitytwo-countermachinesregularlanguages
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Kleene algebra gives a decidable equational theory for regular expressions, and it is widely used in program verification. This paper shows that adding commutativity conditions between primitive symbols—equations $e_1e_2 = e_2e_1$—makes the equality problem undecidable, and that this holds even in pre-Kleene algebras that do not satisfy the induction axioms. The proof encodes the halting behavior of two-counter machines as term inequalities and uses effective inseparability to rule out any decision procedure. This settles an open question from the 1990s; the problem is not merely undecidable but $\Sigma^0_1$-complete when equality is recursively enumerable. The result draws a sharp boundary on what automated tools can decide when program commands are allowed to commute.

What carries the argument

The central object is the transition term $R_M = \sum\{\llbracket \iota(q) \rrbracket q^l \mid q\in Q_M\}$, a single term in the free pre-Kleene algebra over the doubled machine alphabet $\ddot{\Sigma}_M$; strings over $\ddot{\Sigma}_M$ correspond to pairs of strings, so $R_M$ behaves as a relation on machine configurations. The paper introduces the notion of a representable relation on a prefix-free language $L$: a term $e$ is representable when its image under one step is finite and, for every finite set of start strings $\Lambda$, $\Lambda^r e \leq \Lambda \mathrm{Next}_e(\Lambda)^r + \Sigma^*\Sigma_\neq \rho$ for some residue term $\rho$. The key technical work is showing that $R_M$ is representable: it is finite-state, meaning its derivatives can be unfolded via the expansion lemma (Lemma 27), and it has bounded output, bounding the length of the right components of matched strings by a linear function of the left components. These properties let the completeness inequality be proved by expanding the star of $R_M$ finitely many times, without invoking the induction axioms.

What would settle it

Take a concrete two-counter machine $M$ that halts on input $0$ and outputs $1$, construct the terms $e_L$ and $e_R$ from Theorem 16, and check in a proof assistant whether $e_L \leq e_R$ holds using only pre-Kleene axioms; if the inequality fails for such an accepting machine, completeness is false.

Watch

Extended reading notes

Core claim

Equality in the free pre-Kleene algebra $T\ddot{\Sigma}$ over a discrete two-symbol commutable set is undecidable: there is no algorithm that, given two terms over two primitive symbols that do not commute with each other, decides whether they are provably equal from the pre-Kleene algebra axioms together with the commutativity conditions. The same holds for the free Kleene algebra $K\ddot{\Sigma}$ and, on the language side, for the algebra of regular languages $L\ddot{\Sigma}$ over the same commutable set. The paper therefore settles the equational theory of Kleene algebra with commutativity conditions on atomic terms, and it does so for the weaker pre-Kleene theory that omits induction axioms; Theorems 18 and 19 add that, when equality is recursively enumerable, the theory is $\Sigma^0_1$-complete. The proof maps each two-counter machine $M$ and input $n$ to two terms whose inequality holds exactly when $M$ halts on $n$ and outputs $1$; the accept and reject halting sets are effectively inseparable, so any decision procedure for equality would separate them.

Load-bearing premise

The argument relies on a technical property of the algebraic term that encodes the machine's transition relation—namely, that it can be unfolded finitely many times in a controlled way—and this property is asserted via closure lemmas whose side conditions are not verified step by step in the text.

Editorial extensions

If this is right

  • Equality in the free pre-Kleene algebra over a discrete two-symbol commutable set has no decision procedure, so complete equational reasoning about commuting program commands is impossible in general.
  • The undecidability survives dropping the induction axioms, so the obstruction is intrinsic to the base equations, not to the fixed-point rules for star.
  • When equality is recursively enumerable, the equational theory is $\Sigma^0_1$-complete, placing it on the same level as the halting problem.
  • The same reduction yields undecidability for the free Kleene algebra and for the regular-language algebra over the commutable set, so the hardness is independent of which semantic model is chosen.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The representability technique should adapt to partial commutation relations on more than two symbols, suggesting the undecidability frontier extends beyond the discrete case treated here.
  • Because the proof works in pre-Kleene algebras, any complete proof system for Kleene-algebra equality with commutation hypotheses would have to rely on more than the finite axiomatization, making completeness of practical verification calculi unlikely.
  • The reduction uses a two-symbol alphabet; whether a single fully-commutative primitive still yields undecidability is not addressed by the paper, and the current technique would need modification to settle that boundary case.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper proves that the equational theory of pre-Kleene algebras with commutativity conditions on atomic terms is undecidable, and that when equality is recursively enumerable it is Sigma-0-1-complete. The proof encodes the transition relation of a two-counter machine as a term RM over a doubled alphabet, uses a soundness argument in the algebra of regular languages, and develops a completeness argument that avoids the induction axioms of Kleene algebra by introducing finite-state and bounded-output terms. The undecidability conclusion is obtained from the effective inseparability of the accepting and rejecting halting sets of two-counter machines, following an adaptation of Kuznetsov's Sigma-0-1-completeness argument. The main technical contribution is a representability criterion for relations that allows the reflexive-transitive closure to be unfolded finitely many times in the pre-Kleene setting.

Significance. If the proof is completed, the paper settles a long-standing open question: undecidability of the equational theory of Kleene algebra with commutativity conditions on primitives, and it does so for the weaker theory of pre-Kleene algebras that do not satisfy the induction axioms. The representability framework built on finite-state and bounded-output terms is a novel and potentially reusable technique, and the explicit use of effective inseparability yields a sharp Sigma-0-1-completeness statement. The paper also provides a useful comparison with the independent work of Kuznetsov. However, as detailed below, the main undecidability theorem as stated is missing a hypothesis, so the central claim is not yet established by the manuscript in its current form.

major comments (2)
  1. [Theorem 18, Section 3] The proof of Theorem 18 uses the step 'l′(eL + eR) = l′(eR) implies l(eL + eR) = l(eR)' to rule out the rejecting case. This implication is not a consequence of the stated hypothesis that l′ is computable: it requires that l′ separates terms with different language interpretations, i.e., that l factors through l′ (or that l′ is injective on the relevant images of l). As stated, the theorem is false: if X is a singleton and l′ is the constant map, equality on X is decidable although the hypotheses are satisfied. The intended applications to T¨Σ, K¨Σ, and L¨Σ do satisfy the needed condition (for K¨Σ, the language interpretation factors through the quotient; for T¨Σ and L¨Σ, one can take l′ to be the identity or l respectively), but the statement and proof must be amended to include this condition. Theorem 19 inherits the same gap because it relies on the equivalence η(s)∈X= iff s∈A′.
  2. [Lemma 35, Section 5.3] The proof of Lemma 35 is a single sentence: 'To show that RM is finite state and had bounded output, we just appeal to the closure properties of such terms Lemmas 26 and 30. The rest is routine.' The side conditions of those closure lemmas are load-bearing for Theorem 16: for Lemma 26 one needs [RM]_0=0, and for Lemma 30 one needs, for each starred subexpression in the instruction encodings, that |π_l(s)|≥1 for every string s in the language of the base term being starred. These conditions are not verified in the text. They appear to be true for the encoding of Definition 13, but the verification should be written out because the representability of RM is the core of the completeness argument.
minor comments (5)
  1. [Footnote 1] The word 'Unviersity' should be 'University'.
  2. [Lemma 35] The phrase 'had bounded output' should be 'has bounded output'.
  3. [Theorem 18] The diagram described as 'T ¨Σ L¨Σ X, l, l′' is ambiguous; the intended commutative diagram should be drawn or described precisely, with explicit domains and codomains for l and l′ and the factorization condition stated.
  4. [Proof of Theorem 18] The line 'l(ρ)≤l(Σ∗_M)' should presumably be 'l(ρ)≤l(¨Σ∗_M)' for the comparison with the right-hand side of Theorem 15; as written, the inclusion is not the one needed.
  5. [Definition 12] The phrase 'view a term e∈T X as an element T ¨X' is missing 'of'; it should read 'as an element of T ¨X'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the proof is a direct reduction from effectively inseparable halting sets; all constructed terms and the residue rho are built by explicit algebraic expansions, not fitted to the conclusion.

full rationale

The derivation chain is a genuine many-one reduction. Theorem 16 constructs rho from the representability machinery (Lemmas 21, 22, 31, 34), and soundness (Theorem 15) is proved by direct language-theoretic reasoning. The undecidability argument then uses the standard effective inseparability of halting sets (Theorem 17) and, for the Sigma-0-1-completeness refinement, external propositions attributed to Kuznetsov, not to the authors' own prior work. The only self-citation in the paper (reference [21], on incorrectness logic) is mentioned in the introduction for motivation and is not load-bearing. The skeptic's concern about Theorem 18 requiring injectivity of l' is a correctness or hypothesis-strength issue in the abstract reduction statement, not a circular dependency: no step of the proof assumes the decidability or undecidability result as an input, and no fitted parameter is renamed as a prediction. The paper is self-contained in the relevant sense, and the score is therefore 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no free parameters and no new postulated entities; the central claim is established by reduction from known undecidable problems. The axioms listed are background computability-theory facts and one external result used for the completeness strengthening. The framework concepts (commutable sets, finite-state terms, bounded-output terms) are definitions within standard algebra, not additional assumptions.

assumptions (3)
  • domain assumption Two-counter machines are equivalent in expressive power to Turing machines, so the halting and output problem for two-counter machines is undecidable.
    Used in Section 3 to justify the reduction from effectively inseparable sets A and B; cited to Hopcroft et al. [10], not proved in the paper.
  • standard math The halting-with-output sets A and B for two-counter machines are effectively inseparable.
    Stated as Theorem 17 and proved in the appendix by a standard diagonalization argument; this is background computability theory that the reduction depends on.
  • standard math Kuznetsov's propositions on effective inseparability and Sigma-0-1-completeness can be applied to the constructed sets A' and B.
    Used in Theorem 19 to strengthen undecidability to Sigma-0-1-completeness; imported from [17] and not reproved in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Kleene algebra with commutativity conditions is undecidable." pith.science (2026). https://pith.science/paper/D7S6ZPYS

@misc{pith2026241115979,
  author       = {Pith},
  title        = {Pith review of: Kleene algebra with commutativity conditions is undecidable},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/D7S6ZPYS}},
  note         = {Machine review of arXiv:2411.15979}
}
read the original 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

21 extracted references · 13 canonical work pages

  1. [1]

    Netkat: semantic foundations for networks

    Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. Netkat: semantic foundations for networks. ACM SIGPLAN Notices , 49(1):113–126, January 2014. https://doi.org/10.1145/2578855.2535862 doi:10.1145/2578855.2535862

    arXiv 2014

  2. [2]

    Kleene Algebra with Tests and Program Schematology

    Allegra Angus and Dexter Kozen. Kleene Algebra with Tests and Program Schematology . USA, June 2001

    work page 2001

  3. [3]

    Partial derivatives of regular expressions and finite automaton constructions

    Valentin Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theoretical Computer Science , 155(2):291--319, March 1996. https://doi.org/10.1016/0304-3975(95)00182-4 doi:10.1016/0304-3975(95)00182-4

    doi:10.1016/0304-3975(95)00182-4 1996

  4. [4]

    An algebra of alignment for relational verification

    Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo. An algebra of alignment for relational verification. (arXiv:2202.04278), July 2022. arXiv:2202.04278 [cs]. URL: http://arxiv.org/abs/2202.04278, https://doi.org/10.48550/arXiv.2202.04278 doi:10.48550/arXiv.2202.04278

    work page Pith review arXiv doi:10.48550/arxiv.2202.04278 2022

  5. [5]

    Transductions and Context-Free Languages

    Jean Berstel. Transductions and Context-Free Languages . Vieweg+Teubner Verlag, Wiesbaden, 1979. https://doi.org/10.1007/978-3-663-09367-1 doi:10.1007/978-3-663-09367-1

    work page doi:10.1007/978-3-663-09367-1 1979

  6. [6]

    Partial Commutation and Traces

    Volker Diekert and Yves M \'e tivier. Partial Commutation and Traces . In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages : Volume 3 Beyond Words , pages 457--533. Springer, Berlin, Heidelberg, 1997. https://doi.org/10.1007/978-3-642-59126-6_8 doi:10.1007/978-3-642-59126-6_8

    doi:10.1007/978-3-642-59126-6_8 1997

  7. [7]

    A coalgebraic decision procedure for netkat

    Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for netkat. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’15, page 343–355, New York, NY, USA, January 2015. Association for Computing Machinery. https://doi.org/10.1145/2676726.267701...

    arXiv 2015

  8. [8]

    On the decidability of some problems about rational subsets of free partially commutative monoids

    Alan Gibbons and Wojciech Rytter. On the decidability of some problems about rational subsets of free partially commutative monoids. Theoretical Computer Science , 48:329--337, January 1986. https://doi.org/10.1016/0304-3975(86)90101-5 doi:10.1016/0304-3975(86)90101-5

    work page doi:10.1016/0304-3975(86)90101-5 1986

Show all 21 references
  1. [9]

    Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman

    C. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent kleene algebra. volume 5710, page 399–414, September 2009. https://doi.org/10.1007/978-3-642-04081-8_27 doi:10.1007/978-3-642-04081-8_27

    2009 doi

  2. [10]

    Hopcroft, R

    J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation . Addison-Wesley series in computer science. Addison-Wesley, 2001. URL: https://books.google.com/books?id=omIPAQAAMAAJ

    2001

  3. [11]

    Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness , volume 12077 of Lecture Notes in Computer Science , page 381–400

    Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness , volume 12077 of Lecture Notes in Computer Science , page 381–400. Springer International Publishing, Cham, 2020. URL: ht...

    2020 doi

  4. [12]

    Concurrent kleene algebra: Free model and completeness

    Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent kleene algebra: Free model and completeness. In Amal Ahmed, editor, Programming Languages and Systems , Lecture Notes in Computer Science, page 856–882, Cham, 2018. Springer International Publishing. http...

    2018 doi

  5. [13]

    On kleene algebras and closed semirings

    Dexter Kozen. On kleene algebras and closed semirings. In Branislav Rovan, editor, Mathematical Foundations of Computer Science 1990 , volume 452, pages 26--47. Springer-Verlag, Berlin/Heidelberg, 1990. https://doi.org/10.1007/BFb0029594 doi:10.1007/BFb0029594

    1990 doi

  6. [14]

    Kleene algebra with tests and commutativity conditions , volume 1055 of Lecture Notes in Computer Science , page 14–33

    Dexter Kozen. Kleene algebra with tests and commutativity conditions , volume 1055 of Lecture Notes in Computer Science , page 14–33. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. URL: http://link.springer.com/10.1007/3-540-61042-1_35, https://doi.org/10.1007/3-540-610...

    1996 doi

  7. [15]

    On the complexity of reasoning in kleene algebra

    Dexter Kozen. On the complexity of reasoning in kleene algebra. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997 , pages 195--202. IEEE Computer Society, 1997. https://doi.org/10.1109/LICS.1997.614947 doi:10.1109/L...

    1997

  8. [16]

    Left-handed completeness

    Dexter Kozen and Alexandra Silva. Left-handed completeness. Theoretical Computer Science , 807:220--233, February 2020. https://doi.org/10.1016/j.tcs.2019.10.040 doi:10.1016/j.tcs.2019.10.040

    2020 doi

  9. [17]

    Kuznetsov

    Stepan L. Kuznetsov. On the complexity of reasoning in kleene algebra with commutativity conditions. In Erika \' A brah \' a m, Clemens Dubslaff, and Silvia Lizeth Tapia Tarifa, editors, Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru,...

    2023 doi

  10. [18]

    A. K. McIver, E. Cohen, and C. C. Morgan. Using Probabilistic Kleene Algebra for Protocol Verification , volume 4136 of Lecture Notes in Computer Science , page 296–310. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. URL: http://link.springer.com/10.1007/11828563_20, ht...

    2006 doi

  11. [19]

    On Probabilistic Kleene Algebras, Automata and Simulations , volume 6663

    Annabelle McIver, Tahiry Rabehaja, and Georg Struth. On Probabilistic Kleene Algebras, Automata and Simulations , volume 6663. May 2011. https://doi.org/10.1007/978-3-642-21070-9_20 doi:10.1007/978-3-642-21070-9_20

    2011 doi

  12. [20]

    Kleene coalgebra

    A.M Silva. Kleene coalgebra . s.n.; UB Nijmegen host, S.l.; Nijmegen, 2010. URL: http://hdl.handle.net/2066/83205

    2010

  13. [21]

    On incorrectness logic and kleene algebra with top and tests

    Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and kleene algebra with top and tests. (arXiv:2108.07707), August 2022. arXiv:2108.07707 [cs]. URL: http://arxiv.org/abs/2108.07707, https://doi.org/10.48550/arXiv.2108.07707 doi:10.48550/arXiv.2...

    2022 doi arXiv

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.