Solving of Regular Equations Revisited (extended version)

Kenny Zhuo Ming Lu; Martin Sulzmann

REVIEW 4 major objections 3 minor 23 references

Solving of Regular Equations Revisited (extended version)

T0 review · 4 major / 3 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Solving regular equations by bijective parse-tree coercions makes unambiguous equation systems yield unambiguous regular expressions, covering DFA conversion and subtraction.

desk verdict Solid paper with a genuinely new unambiguity result, but Theorem 25 rests on omitted coercions that must be supplied before the proof is complete. read the letter →

arxiv 1908.03710 v1 pith:GZMYK4HL submitted 2019-08-10 cs.FL

Martin Sulzmann , Kenny Zhuo Ming Lu This is my paper · ORCID

classification cs.FL MSC 68Q45

keywords regularequationsexpressionsparsetreesunambiguityderivativesofsubtractionlanguagesshufflecoercions

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

The paper tries to establish that the classical procedure for solving regular equations—replace $s\cdot R+T$ by $s^*\cdot T$, then substitute and normalize—has a parse-tree meaning: every solving step is a bijection on parse trees, so it cannot create or destroy ambiguity. Starting from a set of equations in which each leading literal appears once and the trailing term is either $\varepsilon$ or empty (non-overlapping equations), the final regular expressions are unambiguous. This matters because it gives a direct guarantee that the derivative-based conversion of a deterministic finite automaton to a regular expression produces an unambiguous expression, and it gives subtraction of two regular expressions a direct algebraic construction with the same guarantee. The paper also expresses the shuffle operation by a finite equation system and proves correctness coinductively, though the shuffle equations overlap and no unambiguity claim is made for them.

What carries the argument

The load-bearing mechanism is the bijective coercion. A coercion is a first-order function over parse-tree values built from constructors Eps, Sym, Seq, Inl, Inr, Fold, with a big-step evaluation semantics; bijectivity means an inverse coercion exists. The solver's three moves each get one: the elimination step has an explicit recursive coercion and its inverse, substitution contexts have coercions that navigate to the replaced subterm and unroll the Fold node, and each equivalence law (E1)-(E7) is supposed to supply a coercion preserving parse trees. These compose into a single transformation from equation parses to solution parses. The condition that keeps distinct parses from ever collapsing is the non-overlapping shape of the equations, which makes the initial parse tree unique per word.

What would settle it

Solve the non-overlapping system $R\approx x\cdot R+y$ (with an auxiliary equation $S\approx\varepsilon$) and check whether the resulting expression $x^*\cdot y$ has two distinct parse trees for any word; Theorem 25 predicts none. More directly, inspect the omitted normalization coercions for laws such as associativity and commutativity: if a concrete rewriting step maps two distinct parse trees onto one tree, or has no inverse on a reachable tree, the transfer argument fails.

Watch

Extended reading notes

Core claim

The central discovery is an annotated solving calculus. Equations and substitutions carry parse trees, and each rewrite step is implemented by an explicitly given coercion between parse trees: one for the fixpoint step that converts a parse of $s\cdot R+T$ into a parse of $s^*\cdot T$, one for each algebraic normalization law, and one for substitution contexts that replaces a variable occurrence by its definition while dropping the Fold constructor. The paper proves the fixpoint-step coercion and the substitution-coercion construction in detail and states the normalization coercions; it then proves by composition that the full solving process maps a parse tree of any equation variable to a parse tree of the corresponding solution. Because every coercion is claimed to be invertible, distinct parse trees remain distinct, so unambiguous equations yield unambiguous solutions. The result is stated for non-overlapping equations: $R\approx x_1\cdot R_1+\cdots+x_n\cdot R_n+t$ with distinct $x_i$ and $t\in\{\varepsilon,\varphi\}$, where at most one parse tree can exist for any word. Theorem 25 then concludes that the solved expression for each variable is unambiguous.

Load-bearing premise

The whole argument depends on every algebraic rewriting law used during normalization having a one-to-one, onto transformation of parse trees, but the paper fully writes out that transformation for only one of the laws and says the others work in the same way.

Editorial extensions

If this is right

Every deterministic finite automaton converted by the derivative-based equation method yields an unambiguous regular expression, so the expression can be used for deterministic matching.
Subtraction of two regular expressions can be computed directly by solving one finite set of derivative equations, with an unambiguous result and no round trip through automata.
The shuffle of two regular expressions is expressible as a finite equation system with coinductively verified correctness, but no unambiguity guarantee is claimed because the shuffle equations are overlapping.
When equations are in strict order, the syntactic form of the solution is independent of the order in which equations are solved; otherwise, reordering changes the syntactic shape while preserving the language.

Reading between the lines

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

The bijectivity invariant is more general than the specific law set: any rewriting calculus for regular expressions whose laws are implemented by inverse parse-tree transformations would push unambiguity forward from source to result; the paper does not state this generalization.
The annotated solving process can be read as a parser: a word is accepted by the solved expression exactly when the forward coercion produces a parse tree, so the coercions supply a direct parsing algorithm for unambiguous solutions without constructing an automaton.
The overlapping equations in the shuffle construction suggest a weakened non-overlapping condition—repeated leading literals might still preserve unambiguity when the alternatives lead to provably identical parse trees; testing this would extend the theorem to a class of systems the paper leaves open.
Because equation solving and state elimination are equivalent conversions, as the paper notes from the literature they cite, the unambiguity guarantee should transfer to state-elimination outputs as well; this transfer is not developed in the paper.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Short version: this is a worthwhile paper with a real new result—Brzozowski-style solving of DFA characteristic equations yields unambiguous regular expressions—but the proof of Theorem 25 has a load-bearing hole that the authors need to plug. The paper is worth serious refereeing, but not acceptance as is.

The good parts first. The paper gives a concise and clean specification of the solving algorithm, and the parse-tree coercion framework is a nice way to make the connection between equations and solutions precise. The non-overlapping criterion for unambiguity is simple and genuinely useful. The subtraction, shuffle, and intersection equations are derived honestly, and the bisimulation proofs look sound. The authors also openly note the isomorphism of their subtraction/shuffle method with product automata, which is the right thing to do.

The soft spot is Theorem 25. It relies on Lemma 20, which claims that every normalization step (E1)-(E7) has a bijective coercion. The proof only gives the coercion for (E1) and says the rest are 'similar'. That is not enough for a proof, especially since the theorem hinges on coercions being bijections. Worse, the definition of bijective (Definition 18) is one-sided: it requires g(v)⇓u whenever f(u)⇓v, which only gives a left inverse and does not rule out extra parse trees in the solution that are not in the image of f. To transfer unambiguity from equations to solutions, you need a full two-sided bijection, or at least surjectivity onto every parse tree of the solution. This is a real gap, not a stylistic nitpick. I believe it can be filled—the coercions for associativity, commutativity, and distributivity are natural isomorphisms on parse trees—but the authors need to write them down and prove surjectivity.

The stress-test note also flags the hole grammar for (E6) as possibly requiring product contexts. I checked the normalization argument in Theorem 11, and I think the sum-context grammar is sufficient there, so I would not press that point. The other issues—parser soundness in Appendix B and the unreferenced implementation repo—are minor presentation concerns. The parser section is a sketch, and the implementation lacks a commit hash or raw data, but those are not load-bearing for the main mathematics.

Bottom line: this paper deserves a serious referee. I would conditionally accept with a request to complete Lemma 20 and strengthen the bijectivity definition. The unambiguity result for DFAs is new and useful, and the algebraic methods for subtraction and shuffle are worth having on record. I'd cite it.

Referee Report

4 major / 3 minor

Summary. The paper revisits the classical method of solving systems of regular equations via Arden's Lemma. It formalizes a rewrite system with Arden and substitution steps and a normalization component, and then gives a computational interpretation of solving in terms of coercions on parse trees. The central theoretical claim is that if the initial equation system is non-overlapping, then any solution obtained by the solving rules is unambiguous; this is applied to show that Brzozowski's algebraic method yields unambiguous regular expressions from DFAs. The paper also proposes direct derivative-based equation methods for subtraction and shuffle, with a bisimulation proof for subtraction and a proof sketch for shuffle, and reports on a Haskell implementation with heuristics and benchmarks.

Significance. The computational interpretation of solving steps as parse-tree coercions is a genuinely useful idea: it connects algebraic equation solving with standard notions of regular-expression ambiguity and gives a clean route to unambiguity guarantees for DFA-to-regular-expression conversion. The subtraction method and the accompanying bisimulation argument are elegant, and the implementation with ordering heuristics is a valuable practical addition. However, the main theorem currently rests on proof obligations that are explicitly left to ``details omitted for brevity,'' and at least one exhibited coercion inverse is written incorrectly. The paper's significance is therefore conditional on completing the coercion framework; the underlying approach appears sound and likely repairable.

major comments (4)

[Section 4, Lemma 20]
[Section 4, Definition 18]
[Section 3, Definition 9 and proof of Theorem 11]
[Section 6.3, Theorem 40]

minor comments (3)

[Section 3, proof of Theorem 11]
[Section 4, Proposition 14]
[Section 3, Definition 10]

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Theorem 25 transfers an independently proved uniqueness property via explicit coercions; omissions are proof gaps, not self-referential reductions.

full rationale

The central derivation chain is not circular. Theorem 25 does not define unambiguity of solutions into the non-overlapping condition by construction; Proposition 17 gives an independent deterministic-parse proof (Appendix A.1), and Proposition 24 transfers uniqueness through explicitly constructed coercions. The transfer requires bijectivity: Lemma 19 supplies the Arden coercion and its inverse, and Lemma 22 supplies substitution coercions by induction on the context. Lemma 20 spells out the coercion only for rule (E1) and says 'Coercions for rules (E2-5) can be defined similarly. Details are omitted for brevity.' That is a proof gap, not circularity: even if one of the omitted coercions is not bijective, the failure would be a correctness gap, not a reduction of the conclusion to its own premise. The citations to the authors' earlier parsing work in Proposition 14 are not load-bearing for Theorem 25, since the unambiguity and solution-transfer arguments do not invoke the parser-completeness result. Subtraction and shuffle correctness are established by bisimulation over the generated equations against the standard expansion theorem; reusing the same expansion identities to verify the equations is a normal coalgebraic proof strategy, not the equation system presupposing its own solution semantics. There are no fitted parameters, no renamed predictions, and no self-citation chain that forces the claimed outcome.

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

No fitted parameters. The only non-standard assumptions are the completeness of the normalization calculus and the omitted bijectivity proofs for several coercions. The Fold parse-tree constructor is a notational device within the paper's formal system, not an additional postulated entity.

assumptions (4)

standard math Arden's Lemma (Lemma 5): from R ≈ S·R + T with ε ∉ S one obtains R ≡ S*·T; the paper uses only the right-to-left direction.
Invoked in Section 3, rule (Arden), the essential solving step.
standard math Brzozowski's finiteness theorem (Theorem 32): descendants of a regular expression under derivatives fall into finitely many similarity classes.
Used in Section 6 to guarantee D(r) and D(s) are finite, so the subtraction and shuffle equation systems are finite and well-defined.
ad hoc to paper The normalization rules (E1)-(E7) can bring every right-hand side into normal form, and each rule carries a bijective parse-tree coercion.
This is the load-bearing unproven detail in Lemma 20 and Theorem 25; only the coercion for (E1) is fully shown.
domain assumption Deterministic finite automata are total, so characteristic equations contain exactly one summand x·R_{δ(q,x)} for each symbol x, with distinct leading symbols.
Needed to make EM non-overlapping in Section 5, Corollary 1.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Solving of Regular Equations Revisited (extended version)." pith.science (2026). https://pith.science/paper/GZMYK4HL

@misc{pith2026190803710,
  author       = {Pith},
  title        = {Pith review of: Solving of Regular Equations Revisited (extended version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GZMYK4HL}},
  note         = {Machine review of arXiv:1908.03710}
}

read the original abstract

Solving of regular equations via Arden's Lemma is folklore knowledge. We first give a concise algorithmic specification of all elementary solving steps. We then discuss a computational interpretation of solving in terms of coercions that transform parse trees of regular equations into parse trees of solutions. Thus, we can identify some conditions on the shape of regular equations under which resulting solutions are unambiguous. We apply our result to convert a DFA to an unambiguous regular expression. In addition, we show that operations such as subtraction and shuffling can be expressed via some appropriate set of regular equations. Thus, we obtain direct (algebraic) methods without having to convert to and from finite automaton.

Figures

Figures reproduced from arXiv: 1908.03710 by the authors.

**Figure 1.** Default solving order vs Delgado-Morais heuristics vs Cycle Counting Heuristics Definition 46 (In-coming, out-going and looping regular expressions) Let E = {R1 ≈ α1, . . . , Rn ≈ αn}. We define the in-coming regular expressions, out-going regular expressions and looping regular expression of the regular language symbol Ri as inRE(E, Ri) = {r|Rj ≈ αj ∈ E ∧ Ri 6= Rj ∧ αj = r · Ri + α ′ j for some α ′ j } outRE(E, Ri… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

23 extracted references · 22 canonical work pages

[1]

Implementation of state elimi nation using heuris- tics

Jae-Hee Ahn and Yo-Sub Han. Implementation of state elimi nation using heuris- tics. In Proc. of CIAA’09, pages 178–187. Springer, 2009

work page 2009
[2]

Enumera tion and generation with a string automata representation

Marco Almeida, Nelma Moreira, and Rog´ erio Reis. Enumera tion and generation with a string automata representation. Theoretical Computer Science, 387(2):93 – 102, 2007. Descriptional Complexity of Formal Systems

work page 2007
[3]

Dean N. Arden. Delayed-logic and ﬁnite-state machines. I n 2nd Annual Symposium on Switching Circuit Theory and Logical Design, Detroit, Mi chigan, USA, October 17-20, 1961 , pages 133–151, 1961

work page 1961
[4]

Claus Brabrand and Jakob G. Thomsen. Typed and unambiguou s pattern match- ing on strings using regular expressions. In Proc. of PPDP’10 , pages 243–254. ACM, 2010

work page 2010
[5]

Brzozowski

Janusz A. Brzozowski. Derivatives of regular expression s. J. ACM , 11(4):481–494, 1964. 17

work page 1964
[6]

Brzozowski and Edward J

Janusz A. Brzozowski and Edward J. McCluskey. Signal ﬂow g raph techniques for sequential circuit state diagrams. IEEE Trans. Electronic Computers, 12(2):67–76, 1963

work page 1963
[7]

A general frame- work for the derivation of regular expressions

Pascal Caron, Jean-Marc Champarnaud, and Ludovic Mignot . A general frame- work for the derivation of regular expressions. RAIRO - Theor. Inf. and Applic. , 48(3):281–305, 2014

work page 2014
[8]

Approximation to the smallest regular expression for a given regular language

Manuel Delgado and Jos´ e Morais. Approximation to the smallest regular expression for a given regular language. In Proc. of CIAA’04, pages 312–314. Springer, 2004

work page 2004

Show all 23 references

[9]

Greedy regular expressio n matching

Alain Frisch and Luca Cardelli. Greedy regular expressio n matching. In Proc. of ICALP’04, pages 618– 629. Springer, 2004

2004
[10]

Using proofs by coinduction to ﬁnd ”t raditional” proofs

Clemens Grabmayer. Using proofs by coinduction to ﬁnd ”t raditional” proofs. In Proc. of CALCO’05, pages 175–193. Springer, 2005

2005
[11]

From ﬁnite automata to regular expressions and back - A summary on descriptional complexity

Hermann Gruber and Markus Holzer. From ﬁnite automata to regular expressions and back - A summary on descriptional complexity. Int. J. Found. Comput. Sci. , 26(8):1009–1040, 2015

2015
[12]

State elimination heuristics for short regu lar expressions

Yo-Sub Han. State elimination heuristics for short regu lar expressions. Fundam. Inf., 128(4):445–462, October 2013

2013
[13]

Hopcroft, Rajeev Motwani, and Jeﬀrey D

John E. Hopcroft, Rajeev Motwani, and Jeﬀrey D. Ullman. Introduction to Au- tomata Theory, Languages, and Computation (3rd Edition) . Addison-Wesley Long- man Publishing Co., Inc., Boston, MA, USA, 2006

2006
[14]

Kenny Z. M. Lu and Martin Sulzmann. Solving Regular Expre ssion Equations. http://github.com/luzhuomi/regex-symb
[15]

State e limination ordering strategies: Some experimental results

Nelma Moreira, Davide Nabais, and Rog´ erio Reis. State e limination ordering strategies: Some experimental results. In Proc. of DCFS’10, volume 31 of EPTCS, pages 139–148, 2010

2010
[16]

Converting deterministic ﬁnite aut omata to regular expres- sions

Christoph Neumann. Converting deterministic ﬁnite aut omata to regular expres- sions. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.2597, March 2005

2005
[17]

Bonsangue, and Jan J

Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutt en. Coinductive proof techniques for language equivalence. In Proc. of LATA’13, pages 480–492. Springer, 2013

2013
[18]

Elements of Automata Theory

Jacques Sakarovitch. Elements of Automata Theory . Cambridge University Press, 2009

2009
[19]

Automata and rational expression s

Jacques Sakarovitch. Automata and rational expression s. https://arxiv.org/abs/1502.03573, 2015

2015 arXiv
[20]

POSIX regular exp ression parsing with derivatives

Martin Sulzmann and Kenny Zhuo Ming Lu. POSIX regular exp ression parsing with derivatives. In Proc. of FLOPS’14, pages 203–220. Springer, 2014

2014
[21]

Derivative-base d diagnosis of regular expression ambiguity

Martin Sulzmann and Kenny Zhuo Ming Lu. Derivative-base d diagnosis of regular expression ambiguity. Int. J. Found. Comput. Sci. , 28(5):543–562, 2017

2017
[22]

Derivatives and par tial derivatives for regular shuﬄe expressions

Martin Sulzmann and Peter Thiemann. Derivatives and par tial derivatives for regular shuﬄe expressions. J. Comput. Syst. Sci. , 104:323–341, 2019

2019
[23]

Derivatives for enhanced regular expre ssions

Peter Thiemann. Derivatives for enhanced regular expre ssions. In Proc. of CIAA’16, pages 285–297. Springer, 2016. 18 A Proofs A.1 Proof of Proposition 17 Proof. For non-overlapping equations there can be at most one v such that E ⊢ v :R. Suppose E ⊢ v :R whereR ≈x1·R1+· · ·+x...

2016

Pith tools

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

[1] [1]

Implementation of state elimi nation using heuris- tics

Jae-Hee Ahn and Yo-Sub Han. Implementation of state elimi nation using heuris- tics. In Proc. of CIAA’09, pages 178–187. Springer, 2009

work page 2009

[2] [2]

Enumera tion and generation with a string automata representation

Marco Almeida, Nelma Moreira, and Rog´ erio Reis. Enumera tion and generation with a string automata representation. Theoretical Computer Science, 387(2):93 – 102, 2007. Descriptional Complexity of Formal Systems

work page 2007

[3] [3]

Dean N. Arden. Delayed-logic and ﬁnite-state machines. I n 2nd Annual Symposium on Switching Circuit Theory and Logical Design, Detroit, Mi chigan, USA, October 17-20, 1961 , pages 133–151, 1961

work page 1961

[4] [4]

Claus Brabrand and Jakob G. Thomsen. Typed and unambiguou s pattern match- ing on strings using regular expressions. In Proc. of PPDP’10 , pages 243–254. ACM, 2010

work page 2010

[5] [5]

Brzozowski

Janusz A. Brzozowski. Derivatives of regular expression s. J. ACM , 11(4):481–494, 1964. 17

work page 1964

[6] [6]

Brzozowski and Edward J

Janusz A. Brzozowski and Edward J. McCluskey. Signal ﬂow g raph techniques for sequential circuit state diagrams. IEEE Trans. Electronic Computers, 12(2):67–76, 1963

work page 1963

[7] [7]

A general frame- work for the derivation of regular expressions

Pascal Caron, Jean-Marc Champarnaud, and Ludovic Mignot . A general frame- work for the derivation of regular expressions. RAIRO - Theor. Inf. and Applic. , 48(3):281–305, 2014

work page 2014

[8] [8]

Approximation to the smallest regular expression for a given regular language

Manuel Delgado and Jos´ e Morais. Approximation to the smallest regular expression for a given regular language. In Proc. of CIAA’04, pages 312–314. Springer, 2004

work page 2004