{"id":"aacbb595-b46a-4bec-9b03-178e1962a27b","arxiv_id":"2411.15979","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The equational theory of Kleene algebra with commutativity conditions on primitives is undecidable, and this holds already for pre-Kleene algebras without induction axioms, with Sigma-0-1 completeness.","lead":"This paper proves that equality of terms in Kleene algebra with commutativity conditions is undecidable, settling a thirty-year open question. The proof works even for weaker pre-Kleene algebras that omit the induction axioms, so the boundary of decidability is now known more sharply.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 18's reduction requires injectivity of l', which is neither stated nor supplied; as stated the theorem is refuted by a constant l' onto a singleton, and the 'In particular' proofs for T¨Σ and K¨Σ are incomplete.","rationale":"The reader identified Lemma 35 as the weakest assumption, specifically the unverified side conditions for finite-state and bounded-output closure. I checked those side conditions: they do hold for RM, so Lemma 35 is a minor exposition gap rather than a real hole. The most load-bearing concern is instead in Theorem 18, the paper's main undecidability result. Its statement is too permissive: l' is only required to be computable, but the proof needs l' to be injective (or at least to reflect language inequality). Without that, l'(e_L+e_R)=l'(e_R) does not imply l(e_L+e_R)=l(e_R), so the proof cannot rule out rejecting machines mapping to equal pairs. A concrete counterexample is a singleton X with constant l', which satisfies the stated hypothesis but has decidable equality, so the theorem is false as written. The paper's 'In particular' claims for T¨Σ and K¨Σ could be salvaged either by explicitly choosing an injective computable section of the language interpretation or by giving the direct reduction from soundness/completeness. Since the underlying mathematical construction appears sound and the gap is repairable, the appropriate verdict remains conditional on a revised statement/proof, matching the reader's CONDITIONAL verdict but for a different reason.","tokens_in":105,"tokens_out":39125,"duration_ms":949058,"concrete_test":"Check whether Theorem 18's hypothesis as stated admits a constant l' onto a singleton X; if so, equality on X is decidable, refuting the theorem. Then test the proof's inference by constructing two distinct languages a,b with l'(a)=l'(b) under such an l'; if the inference 'l'(a)=l'(b) implies a=b' fails, the reduction does not separate the effectively inseparable sets. Finally, verify whether the paper supplies any computable injective section l' for X = T¨Σ or X = K¨Σ; if none is supplied, the proof of the 'In particular' cases is incomplete.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 18's hypothesis is insufficient: l' is only required to be computable, but the proof's step 'l'(e_L+e_R)=l'(e_R) implies l(e_L+e_R)=l(e_R)' requires injectivity. The theorem is false as stated; e.g., take X a singleton and l' constant. For the paper's specific conclusions about T¨Σ and K¨Σ, no injective computable l' is provided or constructed, leaving the reduction incomplete. This is a genuine logical gap in the main proof, unlike the merely terse Lemma 35 whose side conditions can be verified.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":36,"tokens_out":14979,"duration_ms":246871,"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":[{"comment":"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′.","section":"Theorem 18, Section 3"},{"comment":"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.","section":"Lemma 35, Section 5.3"}],"minor_comments":[{"comment":"The word 'Unviersity' should be 'University'.","section":"Footnote 1"},{"comment":"The phrase 'had bounded output' should be 'has bounded output'.","section":"Lemma 35"},{"comment":"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.","section":"Theorem 18"},{"comment":"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.","section":"Proof of Theorem 18"},{"comment":"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'.","section":"Definition 12"}],"recommendation":"major_revision","confidential_remarks":"The missing hypothesis in Theorem 18 is a serious but fixable flaw: the theorem as stated is refuted by a constant map, yet the intended applications satisfy the needed factorization condition. I recommend major revision rather than rejection, because the central mathematical framework and the completeness proof via representability appear sound and the gap can be repaired by amending the theorem statement and proof. The paper should also explicitly verify the side conditions in Lemma 35; the current one-sentence proof is too terse for a load-bearing lemma. The claimed extension to pre-Kleene algebras is significant and deserves careful review once these points are addressed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear Colleague,\n\nHere's my take. The new result — undecidability for pre-Kleene algebras with commutativity conditions — is genuinely new and stronger than Kuznetsov's, and the derivative/bounded-output apparatus is a real technical contribution. The paper is also candid about Kuznetsov's independent work.\n\nBut the main reduction in Theorem 18 has a load-bearing gap. The theorem claims that any computable l' from L¨Σ to X makes equality on X undecidable. That is false as stated: take X a singleton and l' constant. The proof moves from l'(e_L+e_R)=l'(e_R) to l(e_L+e_R)=l(e_R), which requires l' to be injective on the languages involved. That injectivity is neither stated nor supplied. Consequently the 'In particular' claims for T¨Σ, K¨Σ, and L¨Σ are not proven, since no injective computable l' is exhibited for those algebras. This is a genuine logical gap, not a terseness issue.\n\nThe other concern I'd flag is Lemma 35: the proof that RM is finite-state and bounded-output is dispatched as 'routine' by appeal to Lemmas 26 and 30. The side conditions probably hold, but they are not verified. That is a minor issue compared to Theorem 18.\n\nThe technique of using derivatives without induction axioms is worth studying, and the completeness machinery is carefully built. I think the paper deserves a serious referee, but the authors should be required to fix the reduction, either by adding and proving an injectivity hypothesis for the concrete algebras, or by restructuring the argument.\n\nFor a reading group I'd bring it as a cautionary example of how a subtle missing hypothesis can break a reduction.\n\nBest.","headline":"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.","tokens_in":22092,"tokens_out":3657,"would_cite":false,"duration_ms":32902,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B25","03D35","68Q45"],"pacs":[],"model":"deepseek-v4-flash","headline":"Adding commutation equations between primitive symbols makes Kleene algebra's equality problem undecidable, even for algebras without induction axioms.","keywords":["Kleene algebra","commutativity conditions","equational theory","undecidability","pre-Kleene algebra","effective inseparability","two-counter machines","regular languages"],"falsifier":"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.","tokens_in":21250,"feed_emoji":"🧮","tokens_out":10596,"duration_ms":90150,"temperature":0.7,"pith_summary":"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.","feed_headline":"Commuting atoms make Kleene algebra undecidable","feed_subtitle":"A 30-year open question falls, and the result holds even without induction axioms.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Posed the open decidability question and proved the $\\Pi^0_1$-completeness of the regular-language model with commutations, the baseline this paper supersedes.","marker":"[15]"},{"why":"Kozen's proof of undecidability for $*$-continuous Kleene algebras with commutativity conditions is the model for the soundness direction of the reduction.","marker":"[14]"},{"why":"Kuznetsov's independent undecidability proof introduced the effective-inseparability argument that the paper adapts to derive $\\Sigma^0_1$-completeness in the weaker pre-Kleene setting.","marker":"[17]"},{"why":"Antimirov's partial-derivative construction for regular expressions underlies the finite-state automata and the expansion lemma used to reason without induction axioms.","marker":"[3]"},{"why":"Kozen's closed semirings paper supplies the pre-Kleene algebra that fails the induction axioms, establishing that the weaker theory is strictly weaker.","marker":"[13]"},{"why":"Gives the equivalence between two-counter machines and Turing machines, which the encoding of halting computations relies on.","marker":"[10]"}],"fun_headline_variants":["Commuting atoms make Kleene algebra equality undecidable","No algorithm for equality in Kleene algebra with commuting atoms","Undecidable even without induction: commuting atoms in Kleene algebra","Kleene algebra equalities undecidable with commuting atoms","Atomic commutativity: Kleene algebra equality is undecidable"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Commuting atoms make Kleene algebra equality undecidable","No algorithm for equality in Kleene algebra with commuting atoms","Undecidable even without induction: commuting atoms in Kleene algebra","Kleene algebra equalities undecidable with commuting atoms","Atomic commutativity: Kleene algebra equality is undecidable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000821,"raw_usage":{"total_tokens":3537,"prompt_tokens":832,"completion_tokens":2705,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":448,"completion_tokens_details":{"reasoning_tokens":2620}},"tokens_in":448,"tokens_out":2705,"duration_ms":17415,"temperature":1.0,"reasoning_tokens":2620,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:41:14.431886+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"On the complexity of reasoning in kleene algebra","cited_arxiv_id":null,"evidence_quote":"Posed the open decidability question and proved the $\\Pi^0_1$-completeness of the regular-language model with commutations, the baseline this paper supersedes."},{"cited_title":"Hopcroft, R","cited_arxiv_id":null,"evidence_quote":"Gives the equivalence between two-counter machines and Turing machines, which the encoding of halting computations relies on."}],"review_version":1}