Pith. sign in

REVIEW 6 minor 20 references

Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements

T0 review · 0 major / 6 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 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.

desk verdict Solid, refereeable paper on Kleene algebra with complements; the main theorems hold, but the abstract's counterexample is miscalculated. read the letter →

arxiv 2411.16397 v1 pith:Y353NY4K submitted 2024-11-25 cs.LO

Yoshiki Nakamura , Ryoma Sin'ya This is my paper · ORCID
classification cs.LO MSC 68Q7068Q1703B70
keywords Kleenealgebralanguageequationaltheorycomplementwords-to-lettersvaluationscoNP-completenessuniversalityproblemregularexpressions
open problems P versus NP
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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}$.

Load-bearing premise

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.

Editorial extensions

If this is right

  • $\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).

Reading between the lines

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

  • 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.
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

0 major / 6 minor

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).

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.

minor comments (6)
  1. [Abstract and §1] 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.
  2. [Lemma 46] 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.
  3. [Lemma 19 and Theorem 20] 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.
  4. [Corollary 8] 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.
  5. [Table 1] 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.
  6. [Throughout] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the words-to-letters valuation theorems and the word-fragment completeness theorem are proved from first principles; self-citations are contextual and not load-bearing.

full rationale

The central claims, Theorem 23 and Corollary 29 (sufficiency of words-to-letters valuations) and Theorem 45 (completeness of E2 for words over tilded-V1), are derived inside the paper from Lemmas 2, 18, 19, and 22, and from Lemmas 46, 47 and Claims 48, 49. No parameter is fitted to data, no clause of the target statement is imported as an axiom, and no valuation class is defined by the inequality it is supposed to decide. The bound l(t) is a syntactic notion computed from the extended word language [t] over tilded-V1, and the proof of Theorem 23 only uses the decomposition lemma to push a counterexample down to a finite words-to-letters valuation; this is a genuine reduction, not a consequence already contained in the definition of l(t). The completeness proof for Theorem 45 first proves soundness of E2 by direct semantic inequalities and then proves completeness by two separation lemmas; neither direction assumes E2-derivability. The only self-citations are [12], [13], and [14]: they are used to credit the conference version, to mention the 'words-to-letters' idea, and to record the first author's PSPACE result for unrestricted language equivalence (footnote a, Table 1, Section 1). These are contextual and are not premises of the new results proved here, so they do not load-bearingly close the derivation circle. The coNP-hardness reductions use the validity problem for propositional formulas in DNF, which is genuinely coNP-complete via Cook's theorem, so the hardness arguments are not circular in their source problem. The only notable defect is a non-circular local slip in the abstract's illustrative example: with v(x) = {x}, both xbar and xbar;xbar evaluate to V* \ {x}, so that valuation does not refute the equation; a refuting valuation needs v(x) to contain a word of length at least 2. This does not affect the theorems. Overall, the paper's derivation chain is self-contained with respect to its main claims, and no circular step can be exhibited.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

Pure mathematics paper: no fitted parameters, no data, no empirical quantities. The claims rest on standard mathematics plus the explicitly stated language-model semantics. The one notable defect is the background claim that the validity of DNF formulas is coNP-complete, which is false and is entered as an axiom because the hardness proofs state it as a background fact. The new technical objects (words-to-letters valuations, extended word languages) are definitional tools with their required properties proven inside the paper.

assumptions (4)
  • standard math Standard set-theoretic and arithmetical reasoning (ZFC-level), including induction on term structure.
    Used throughout; every proof in the paper is a standard mathematical proof.
  • domain assumption The language model semantics langX over arbitrary alphabets X, with complement defined as X-star set difference, is the object of study (Sect. 2.2).
    Defines LANG, the equational theory w.r.t. languages; all decidability and completeness results are relative to this semantics.
  • standard math Validity of arbitrary propositional formulas (TAUTOLOGY) is coNP-complete, following from Cook's theorem [6]; the paper instead cites validity of DNF formulas, which is in P.
    Load-bearing for the hardness direction of Cors. 8, 14, 21, and 26; as written the cited source problem is polynomial-time solvable, so the proofs need the TAUTOLOGY reading to go through.
  • standard math Regular expression language equivalence under the standard singleton-letter valuation is PSPACE-complete [7, 11, 17], and the language equivalence problem for KA{x,1} is decidable in PSPACE [13].
    Used in Remark 9, Remark 28, and the comparison table for the standard valuation; not load-bearing for the new decidability results.
invented entities (2)
  • Words-to-letters valuations v of angle bracket w0,...,wn-1 (Def. 17) independent evidence
    purpose: Replace arbitrary valuations by finite-alphabet valuations whose languages are subwords of a sequence of fresh letters, enabling brute-force and coNP algorithms for inclusion problems.
    Fully defined in the paper; the sufficiency property (Lem. 18, Thm. 23, Cor. 29) is proven internally, so this is a defined mathematical tool rather than a postulated entity.
  • Extended word language [t] over the alphabet of variables, complemented variables, and the non-empty constant (Lemma 2) independent evidence
    purpose: Decompose KA{x,1} terms into sets of words so that semantic arguments reduce to word-level analysis.
    Proven in Lemma 2; the decomposition is the backbone of most proofs. It is a proof device, not an empirically postulated object.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements." pith.science (2026). https://pith.science/paper/Y353NY4K

@misc{pith2026241116397,
  author       = {Pith},
  title        = {Pith review of: Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Y353NY4K}},
  note         = {Machine review of arXiv:2411.16397}
}
abstract

We investigate the equational theory for Kleene algebra terms with variable complements and constant complements -- (language) complement where it applies only to variables or constants -- w.r.t. languages. While the equational theory w.r.t. languages coincides with the language equivalence (under the standard language valuation) for Kleene algebra terms, this coincidence is broken if we extend the terms with complements. In this paper, we prove the decidability of some fragments of the equational theory: the universality problem is coNP-complete, and the inequational theory $t \le s$ is coNP-complete when $t$ does not contain Kleene-star. To this end, we introduce words-to-letters valuations; they are sufficient valuations for the equational theory and ease us in investigating the equational theory w.r.t. languages. Additionally, we show a completeness theorem of the equational theory for words with variable complements and the non-empty constant.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

20 extracted references · 20 canonical work pages

  1. [1]

    Andr´ eka, S

    H. Andr´ eka, S. Mikul´ as and I. N´ emeti, The equational t heory of Kleene lattices, Theoretical Computer Science 412(52) (2011) 7099–7108

    work page 2011

  2. [2]

    S. L. Bloom, Z. ´Esik and G. Stefanescu, Notes on equational theories of rela tions, algebra universalis 33(1) (1995) 98–126

    work page 1995

  3. [3]

    Brunet, Reversible Kleene lattices, MFCS, LIPIcs 83, (Schloss Dagstuhl, 2017), pp

    P. Brunet, Reversible Kleene lattices, MFCS, LIPIcs 83, (Schloss Dagstuhl, 2017), pp. 66:1–66:14

    work page 2017

  4. [4]

    Brunet, A complete axiomatisation of a fragment of lan guage algebra, CSL, LIPIcs 152, (Schloss Dagstuhl, 2020), p

    P. Brunet, A complete axiomatisation of a fragment of lan guage algebra, CSL, LIPIcs 152, (Schloss Dagstuhl, 2020), p. 11:1–11:15

    work page 2020

  5. [5]

    J. H. Conway, Regular Algebra and Finite Machines (Chapman and Hall, 1971)

    work page 1971

  6. [6]

    S. A. Cook, The complexity of theorem-proving procedure s, STOC , (ACM, 1971), p. 151–158

    work page 1971

  7. [7]

    H. B. Hunt III, D. J. Rosenkrantz and T. G. Szymanski, On th e equivalence, con- tainment, and covering problems for the regular and context -free languages, Journal of Computer and System Sciences 12(2) (1976) 222–268

    work page 1976

  8. [8]

    S. C. Kleene, Representation of events in nerve nets and fi nite automata, tech. rep., RAND Corporation (1951)

    work page 1951

Show all 20 references
  1. [9]

    Kozen and F

    D. Kozen and F. Smith, Kleene algebra with tests: Complet eness and decidability, CSL, LNCS 1258, (Springer, 1996), pp. 244–259

    1996

  2. [10]

    McNaughton and H

    R. McNaughton and H. Yamada, Regular expressions and st ate graphs for automata, IRE Transactions on Electronic Computers EC-9(1) (1960) 39–47

    1960

  3. [11]

    A. R. Meyer and L. J. Stockmeyer, The equivalence proble m for regular expressions with squaring requires exponential space, SWAT, (IEEE, 1972), pp. 125–129

    1972

  4. [12]

    Nakamura, Existential calculi of relations with tra nsitive closure: Complexity and edge saturations, LICS , (IEEE, 2023), pp

    Y. Nakamura, Existential calculi of relations with tra nsitive closure: Complexity and edge saturations, LICS , (IEEE, 2023), pp. 1–13

    2023

  5. [13]

    Nakamura, Finite relational semantics for language Kleene algebra with comple- ment, CSL, LIPIcs, (Schloss Dagstuhl, 2025 (to appear))

    Y. Nakamura, Finite relational semantics for language Kleene algebra with comple- ment, CSL, LIPIcs, (Schloss Dagstuhl, 2025 (to appear))

    2025

  6. [14]

    Nakamura and R

    Y. Nakamura and R. Sin’ya, Words-to-letters valuation s for language Kleene algebras with variable complements, AFL, EPTCS 386, (EPTCS, 2023), pp. 185–199

    2023

  7. [15]

    K. C. Ng, Relation algebras with transitive closure, Ph D thesis, University of Cali- fornia (1984)

    1984

  8. [16]

    Pous and J

    D. Pous and J. Wagemaker, Completeness theorems for Kle ene algebra with top, CONCUR, LIPIcs 243, (Schloss Dagstuhl, 2022), pp. 26:1–26:18

    2022

  9. [17]

    L. J. Stockmeyer and A. R. Meyer, Word problems requirin g exponential time (pre- liminary report), STOC , (ACM, 1973), pp. 1–9

    1973

  10. [18]

    Tarski, On the calculus of relations, The Journal of Symbolic Logic 6(3) (1941) 73–89

    A. Tarski, On the calculus of relations, The Journal of Symbolic Logic 6(3) (1941) 73–89

    1941

  11. [19]

    Thompson, Programming techniques: Regular express ion search algorithm, Com- munications of the ACM 11(6) (1968) 419–422

    K. Thompson, Programming techniques: Regular express ion search algorithm, Com- munications of the ACM 11(6) (1968) 419–422

    1968

  12. [20]

    Zhang, A

    C. Zhang, A. A. de Amorim and M. Gaboardi, On incorrectne ss logic and Kleene alge- bra with top and tests, Proceedings of the ACM on Programming Languages 6(POPL) (2022) p. 29:1–29:30

    2022

Pith tools

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