{"id":"d3e0923e-ad5e-4b25-8232-73a7975da0d8","arxiv_id":"2411.16397","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For Kleene algebra terms with variable and constant complements, universality, variable inclusion, and star-free inequational theory over all language models are coNP-complete, and the word fragment has a finite sound and complete axiom system.","lead":"This paper studies Kleene algebra, the algebra behind regular expressions, extended with complement (negation) on variables and on the identity constant, and asks when two expressions are equal under every possible language interpretation.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the central words-to-letters valuation theorems and the coNP-completeness corollaries appear correct; the reader's DNF-validity concern rests on a false premise, and the abstract counterexample is only a local expository slip.","rationale":"The reader's CONDITIONAL verdict was based on two defects: an alleged error in the coNP-hardness reductions and a miscalculated counterexample in the abstract. The first concern does not land. Validity of DNF formulas is coNP-complete: a DNF formula is valid iff its negation, which is a CNF formula, is unsatisfiable, and CNF unsatisfiability is coNP-complete by the Cook-Levin theorem. The criterion the reader cites (every disjunct contains a complementary pair) is the polynomial test for CNF validity, not DNF validity. Therefore the reductions from DNF validity in Cors. 8, 14, 21, and 26 are legitimate. The second concern is real but local: with v(x) = {x}, both \\bar{x} and \\bar{x};\\bar{x} evaluate to V* \\ {x}, so the abstract's stated witness does not refute the equation; however, the equation itself is indeed invalid under a valuation where v(x) contains a word of length at least two. This is an expository error in the abstract, not a flaw in any theorem. I spot-checked the main chain: Lemma 2 gives the faithful decomposition into extended word languages; Lemma 18 correctly transfers counterexamples to words-to-letters valuations, including the case of complemented variables; Theorem 23 and Corollary 29 follow; the coNP-membership arguments for Cors. 21 and 24 are supported by the full-word witness guaranteed by the proof of Theorem 23. The completeness proof of Theorem 45 is intricate and was checked by reading rather than machine, but I found no break. The paper would benefit from fixing the abstract's example and spelling out the coNP-membership algorithm, but the central claims are not endangered.","tokens_in":22108,"tokens_out":34809,"duration_ms":324191,"concrete_test":"Exhaustively test Corollary 24 for all star-free terms t with l(t) ≤ 2 and all terms s with at most 3 operators over a 3-letter alphabet: compute LANG |= t ≤ s by brute force over all valuations on the 3-letter alphabet (restricting words to length ≤ 4), and compare with the finite-valuation criterion of Theorem 23 (m ≤ l(t), full-word membership check). A single mismatch would reveal a flaw in Theorem 23.","verdict_should_be":"UNCHANGED","load_bearing_attack":"No load-bearing concern identified. The central claim (Theorem 23 and Corollary 29, with the coNP-completeness corollaries) is supported by the main lemmas; the transfer argument in Lemma 18 and the decomposition lemma (Lemma 22) are sound as written. The reader's weakest assumption is not correct: validity of DNF formulas is coNP-complete, since a DNF formula is valid iff its negation, a CNF formula, is unsatisfiable. The polynomial criterion 'every disjunct contains a complementary pair' characterizes CNF validity, not DNF validity. Hence the hardness reductions in Cors. 8, 14, 21, and 26 do not rely on a polynomial-time source problem. The one clear defect is the abstract's illustrative example: under v(x) = {x}, both \\bar{x} and \\bar{x};\\bar{x} evaluate to V* \\ {x}, so that valuation does not refute \\bar{x} = \\bar{x};\\bar{x}; a correct refutation uses a valuation with a word of length at least 2 in v(x). This is a local explanatory error and does not affect the theorems.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the equational theory of Kleene algebra terms extended with complement on variables and on the identity constant (KA{x,1}), interpreted over languages. The main contribution is the introduction of words-to-letters valuations, a class of valuations over a small alphabet that is shown to be sufficient for the equational theory of LANG (Corollary 29). From this, the authors derive coNP-completeness results for the identity, variable, word, and universality inclusion problems, and for the inequational theory t≤s when t is star-free (Corollaries 8, 14, 21, 24, 26). The paper additionally proves a completeness theorem for the word fragment over the alphabet with complemented variables and the non-empty constant (Theorem 45), and shows that the hierarchy of language models of cardinality n is infinite for full complement (Theorem 39).","tokens_in":22236,"tokens_out":20466,"duration_ms":170037,"significance":"If correct, the main results settle the decidability and complexity of several natural fragments of the equational theory of language Kleene algebras with variable complements, a subject that, as the introduction notes, had not been previously investigated. The words-to-letters valuation technique is a clean and apparently powerful tool: it reduces refutations to a finite set of valuations over at most l(t) letters, yielding a bounded-alphabet property (Corollary 25) that is not evident from the semantics. The completeness theorem for the word fragment is also non-trivial, as shown by the non-trivial equation 1zz1=1zz1 (Example 44). The infinite hierarchy for full complement (Theorem 39) is a noteworthy contrast with the collapsed hierarchy for plain KA terms. The proofs are generally detailed and self-contained; the main lemmas (11, 18, 19, 22) and theorems (23, 45) are presented in full.","major_comments":[],"minor_comments":[{"comment":"The claimed counterexample LANG ⁄|= x = x;x via a valuation with v(x)={x} is incorrect: with that valuation, both \\bar{x} and \\bar{x};\\bar{x} evaluate to V* \\ {x}, so the equation holds. A correct refutation is obtained e.g. by taking v(x)={ε} (or any language containing no length-1 word but some longer word). Please correct the abstract and the introduction accordingly.","section":"Abstract and §1"},{"comment":"The proof of Lemma 46 defines a valuation v(z) with the condition 'z = y' where y is an element of tilded-V1 \\ V, but v is only defined on variables. The intended meaning is presumably that the valuation assigns {ε,a} to the variable underlying y. The proof would benefit from a rewriting that avoids this overloading; as written, the argument is hard to follow.","section":"Lemma 46"},{"comment":"The letter v is used both for the valuation and for the word in Lemma 19 and Theorem 20 (e.g., 'Let v ∈ LANG. Let v = x0...xn−1 be a word'). Please rename the word (e.g., u) to eliminate the ambiguity.","section":"Lemma 19 and Theorem 20"},{"comment":"The reduction from DNF validity is correct, but since Cook's theorem [6] is usually cited for NP-completeness of SAT, it would be helpful to explicitly state that DNF validity is coNP-complete by complementation to CNF satisfiability. This would also preempt the reader's concern that the source problem might be polynomial.","section":"Corollary 8"},{"comment":"The entry for 'unrestricted' cites [13] as 'to appear'; unless it is now published, please provide an arXiv identifier or indicate its status, since the comparison in Table 1 relies on it.","section":"Table 1"},{"comment":"There are several minor typos (e.g., 'T he' at the start of Section 2, 'W e' in the abstract area, and 'should carefully treat' in the difference subsection). A careful proofreading pass is recommended.","section":"Throughout"}],"recommendation":"minor_revision","confidential_remarks":"The reader's reported concern about DNF validity is unfounded; the reductions are valid. The abstract counterexample is an isolated expository error. The paper's contributions are solid and within the scope of IJFCS. I recommend minor revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I think you should know two things about this paper. First, the main technical results check out: the words-to-letters valuations are sufficient for the equational theory of the fragment, and the coNP-completeness results for identity, variable, word inclusion, star-free inequations, and universality are proved in detail. Second, the abstract's counterexample for the complement inequation is wrong as written; it's a minor slip, not a load-bearing flaw.\n\nWhat's genuinely new: the words-to-letters valuation property (Cor. 29), the coNP-completeness bounds (Cors. 8, 14, 21, 24, 26), the infinite strict hierarchy for full complement (Thm. 39), and the sound and complete E2 axiomatization for the word fragment with constant complement (Thm. 45). I spot-checked the valuation lemmas and the reduction arguments; they are sound. The completeness proof is intricate, but I found no gap. The paper is also honest about open questions and about what differs from the conference version.\n\nThe soft spots: the abstract's example says the valuation v(x) = {x} refutes x = x ; x. It does not: both complemented sides evaluate to the full language minus the word x. You need a word of length at least 2 in v(x) to separate them. This is purely expository and can be fixed in a line. The other thing, which the reader flagged, is not a flaw: the coNP-hardness reductions cite validity of DNF formulas as the source problem. That is coNP-complete, because the negation of a DNF is a CNF and unsatisfiability of CNF is NP-complete. So the reductions are fine.\n\nWho should read this: anyone working on language models of Kleene algebras, equational theories with complement, or algebraic approaches to language inclusion. It is dense, but the main idea is clean and reusable. I would give it a serious peer review; it deserves to be published after a minor revision fixing the example. I would cite it if I worked in this area.\n\nRecommendation: send it to review, with a request to fix the abstract.","headline":"Solid, refereeable paper on Kleene algebra with complements; the main theorems hold, but the abstract's counterexample is miscalculated.","tokens_in":22938,"tokens_out":7939,"would_cite":true,"duration_ms":60860,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q70","68Q17","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that inclusion and universality for language Kleene algebras with variable and constant complements are coNP-complete, and that the word fragment is axiomatized by alternating block swaps.","keywords":["Kleene algebra","language algebra","equational theory","complement","words-to-letters valuations","coNP-completeness","universality problem","regular expressions"],"falsifier":"To test Theorem 23, look for terms $t,s$ and a valuation $v$ with a word $w \\in \\hat v(t) \\setminus \\hat v(s)$ such that, for every $m \\le l(t)$ and every choice of non-empty words $w_0,\\ldots,w_{m-1}$ with $w = w_0\\cdots w_{m-1}$, the words-to-letters valuation $v_{\\langle w_0,\\ldots,w_{m-1}\\rangle}$ satisfies $t \\le s$; such an example would refute the words-to-letters valuation property. For the complexity claims, a polynomial-time decision procedure for $\\mathrm{LANG} \\models 1 \\le t$ would likewise collapse the coNP-hardness direction unless P = NP.","tokens_in":21735,"feed_emoji":"🔤","tokens_out":11808,"duration_ms":161050,"temperature":0.7,"pith_summary":"For Kleene algebra terms with complement of variables and of the identity constant, the standard coincidence between truth in all language models and equality of the denoted regular languages fails: for example, $x$ and $x\\,;\\,x$ denote the same language under the standard letter valuation but not under all language-model valuations. The paper introduces words-to-letters valuations, which compress arbitrary witness words into short words over fresh letters, and proves that they are sufficient for the whole inequational theory: if some valuation refutes $t \\le s$, then a words-to-letters valuation using at most $l(t)$ letters refutes it. This yields coNP-completeness for identity, variable, word, and universality inclusion, and for $t \\le s$ when $t$ is star-free. For words over the extended alphabet $\\tilde V_1$, the paper also proves a completeness theorem: over language models with at least two letters, the equational theory is exactly the congruence generated by swapping alternating blocks of $z$ and $\\bar z$ between two occurrences of the non-empty constant.","feed_headline":"Inclusion for complemented regular expressions is coNP-complete","feed_subtitle":"Universality and star-free inclusions join identity, variable, and word inclusions in coNP.","key_machinery":"The central object is the words-to-letters valuation $v_{\\langle w_0,\\ldots,w_{n-1}\\rangle}$: given a valuation $v$ and non-empty words $w_i$, it is the valuation on the alphabet $\\{\\ell_0,\\ldots,\\ell_{n-1}\\}$ defined by $v_{\\langle w_0,\\ldots,w_{n-1}\\rangle}(x) = \\{\\ell_i\\cdots\\ell_{j-1} \\mid 0 \\le i \\le j \\le n,\\ w_i\\cdots w_{j-1} \\in v(x)\\}$. Lemma 18 is the load-bearing transfer: if a subword $\\ell_i\\cdots\\ell_{j-1}$ lies in the denotation of a term $t$ under the words-to-letters valuation, then $w_i\\cdots w_{j-1}$ lies in the denotation under $v$. Theorem 23 combines this with the extended-decomposition lemma (Lemma 2), which rewrites any term $t$ as a regular expression over the alphabet $\\tilde V_1$ of variables, complemented variables, and the constant $\\mathbf{1}$, to bound the needed number of letters by $l(t)$. Corollary 29 then removes the bound, giving the words-to-letters valuation property for the full equational theory. For the word-fragment completeness theorem, the central object is the axiom scheme $E_2$, which permutes alternating blocks of $z$ and $\\bar z$ flanked by $\\mathbf{1}$; Theorem 45 shows the equational theory of $\\mathrm{LANG}_\\alpha$ ($\\alpha \\ge 2$) for words is exactly $E_2$-equivalence.","core_discovery":"The central claim is the words-to-letters valuation property for $\\mathrm{KA}_{\\{x,1\\}}$ terms (Theorem 23 and Corollary 29). For any terms $t,s$, $\\mathrm{LANG} \\models t \\le s$ holds if and only if it holds under every valuation of the form $v_{\\langle w_0,\\ldots,w_{m-1}\\rangle}$ with $m \\le l(t)$, where $l(t)$ is the supremum length of words in the extended decomposition $[t]_{\\tilde V_1}$ and each $w_i$ is a non-empty word. These valuations send each variable $x$ to the set of subwords $\\ell_i\\cdots\\ell_{j-1}$ of a word $\\ell_0\\cdots\\ell_{m-1}$ such that $w_i\\cdots w_{j-1} \\in v(x)$. Since $l(t)$ is finite whenever $t$ is star-free, inclusion problems become finite search problems, and the paper shows they are coNP-complete: identity inclusion (Corollary 8), variable inclusion (Corollary 14), word inclusion (Corollary 21), star-free left-hand inclusion (Corollary 24), and universality (Corollary 26). Separately, Theorem 45 states that for words over $\\tilde V_1$, the equational theory of $\\mathrm{LANG}_\\alpha$ for $\\alpha \\ge 2$ is precisely the congruence generated by the axioms $E_2$, which swap alternating blocks $z^{c_0}\\bar z^{d_0}\\cdots z^{c_{k-1}}\\bar z^{d_{k-1}}$ between two occurrences of the constant $\\mathbf{1}$.","pith_inferences":["The paper leaves implicit that the words-to-letters construction is a finite-model property for the inequational theory: every failure is witnessed over an alphabet whose size is bounded by the extended length of the left-hand term, and the same compression idea could be tried for other extensions such as intersection or top.","The hardness direction as printed reduces from validity of propositional formulas in disjunctive normal form, a problem that is actually polynomial-time decidable; replacing that source with general propositional validity makes the same linear translation go through, so the coNP-completeness results are repairable without changing the constructions.","A natural next step, not taken in the paper, is to test whether adding the $E_2$ block-swap rule to the usual Kleene algebra axioms yields a finite axiomatization of the full equational theory of $\\mathrm{LANG}$ for $\\mathrm{KA}_{\\{x,1\\}}$ terms; the paper leaves finite axiomatizability open.","The infinite hierarchy for full complement suggests that decidability for the unbounded case cannot come from a uniform collapse of the alphabet; words-to-letters valuations sidestep this by using an unbounded but controlled alphabet, a strategy that may extend to other non-collapsing hierarchies."],"forward_implications":["$\\mathrm{LANG} \\models 1 \\le t$, $\\mathrm{LANG} \\models x \\le t$, $\\mathrm{LANG} \\models w \\le t$, and $\\mathrm{LANG} \\models \\top \\le t$ are all decidable and coNP-complete (Corollaries 8, 14, 21, 26).","For star-free $t$, checking $\\mathrm{LANG} \\models t \\le s$ is coNP-complete; since $l(t) \\le \\|t\\|$ when $t$ is star-free, the witness-search algorithm runs in polynomial time (Corollary 24).","Any inequality $t \\le s$ that fails in $\\mathrm{LANG}$ already fails over an alphabet of size at most $l(t)$ (Corollary 25), and the full equational theory is determined by countably infinite alphabets (Corollaries 29, 30, 32).","For words over $\\tilde V_1$ and $\\alpha \\ge 2$, the equational theory of $\\mathrm{LANG}_\\alpha$ is exactly $E_2$-equivalence, so all $\\mathrm{LANG}_\\alpha$ for $\\alpha \\ge 2$ agree on the word fragment; without the constant $\\mathbf{1}$, word equality is just syntactic equality (Theorem 45, Corollary 50).","For ordinary KA terms the $\\mathrm{LANG}_n$ hierarchy collapses to $\\mathrm{LANG}_2$, while for full complement it is strictly increasing at every level (Proposition 36, Theorem 39)."],"supporting_citations":[{"why":"Conference version that introduced words-to-letters valuations; the present paper extends it to the constant complement and settles its open problem about many-variable words.","marker":"[14]"},{"why":"Cited as the coNP-completeness source for the reductions in Corollary 8 and the later hardness claims.","marker":"[6]"},{"why":"Provides the PSPACE decidability of the unrestricted equational theory for $\\mathrm{KA}_{\\{x,1\\}}$ terms, which the new coNP-complete fragments improve upon and compare with.","marker":"[13]"},{"why":"Supplies relational-model and edge-saturation techniques that the paper uses to handle variable complements in the decidability argument.","marker":"[12]"},{"why":"Gives the PSPACE-hardness of the standard-language equivalence problem used as a comparison point for the new coNP-complete results.","marker":"[17]"}],"fun_headline_variants":["Complemented regex inclusion is coNP-complete","Words-to-letters valuations prove coNP-complete inclusions","Star-free inclusion with complements: coNP-complete","Universality for complemented regex: coNP-complete"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise in the hardness arguments is that deciding whether a propositional formula written as a big OR of ANDs is always true is a hard problem; that particular problem is in fact easy, so the coNP-hardness conclusions depend on sourcing the reduction from a genuinely hard problem such as general propositional validity.","fun_headline_variants_meta":{"raw":{"variants":["Complemented regex inclusion is coNP-complete","Words-to-letters valuations prove coNP-complete inclusions","Star-free inclusion with complements: coNP-complete","Universality for complemented regex: coNP-complete"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000726,"raw_usage":{"total_tokens":3317,"prompt_tokens":1069,"completion_tokens":2248,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":685,"completion_tokens_details":{"reasoning_tokens":2184}},"tokens_in":685,"tokens_out":2248,"duration_ms":17451,"temperature":1.0,"reasoning_tokens":2184,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:13:02.324191+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"To test Theorem 23, look for terms $t,s$ and a valuation $v$ with a word $w \\in \\hat v(t) \\setminus \\hat v(s)$ such that, for every $m \\le l(t)$ and every choice of non-empty words $w_0,\\ldots,w_{m-1}$ with $w = w_0\\cdots w_{m-1}$, the words-to-letters valuation $v_{\\langle w_0,\\ldots,w_{m-1}\\rangle}$ satisfies $t \\le s$; such an example would refute the words-to-letters valuation property. For the complexity claims, a polynomial-time decision procedure for $\\mathrm{LANG} \\models 1 \\le t$ would likewise collapse the coNP-hardness direction unless P = NP.","supporting_citations":[{"cited_title":"Nakamura and R","cited_arxiv_id":null,"evidence_quote":"Conference version that introduced words-to-letters valuations; the present paper extends it to the constant complement and settles its open problem about many-variable words."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Cited as the coNP-completeness source for the reductions in Corollary 8 and the later hardness claims."},{"cited_title":"Nakamura, Finite relational semantics for language Kleene algebra with comple- ment, CSL, LIPIcs, (Schloss Dagstuhl, 2025 (to appear))","cited_arxiv_id":null,"evidence_quote":"Provides the PSPACE decidability of the unrestricted equational theory for $\\mathrm{KA}_{\\{x,1\\}}$ terms, which the new coNP-complete fragments improve upon and compare with."},{"cited_title":"Nakamura, Existential calculi of relations with tra nsitive closure: Complexity and edge saturations, LICS , (IEEE, 2023), pp","cited_arxiv_id":null,"evidence_quote":"Supplies relational-model and edge-saturation techniques that the paper uses to handle variable complements in the decidability argument."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the PSPACE-hardness of the standard-language equivalence problem used as a comparison point for the new coNP-complete results."}],"review_version":1}