{"id":"e7265308-af48-481e-9852-7feee626fa11","arxiv_id":"1908.03710","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A formal framework based on bijective parse-tree coercions shows that non-overlapping regular equations, including those from DFAs and subtraction, yield unambiguous solutions.","lead":"This paper gives a precise, coercion-based account of solving regular expression equations with Arden's Lemma, and uses it to show that certain equation shapes yield unambiguous regular expressions. It also provides direct algebraic methods for subtracting, shuffling, and intersecting two regular expressions without building automata.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 25 rests on omitted bijective coercions for normalization rules E2–E5; if any of these is not a bijection or word-preserving, the unambiguity-transfer argument collapses.","rationale":"The central claim is Theorem 25: non-overlapping regular equations produce unambiguous solutions. The proof mechanism is a bijection between parse trees of the original equations and parse trees of the final expressions, built from coercions for the Arden step, normalization steps, and substitution steps. I examined the Arden coercion in Lemma 19 and the E1 coercion/inverse in Lemma 20: both appear to be genuine bijections. The coercions for E2–E5 are plausible to define (reassociation, commutativity, and distribution) and likely work, but they are not present in the paper, so the theorem is not actually demonstrated. I could not construct a counterexample to Theorem 25 by testing simple DFAs and their equation solutions, which makes me think the claim itself is likely true. The load-bearing risk is the incomplete proof of Lemma 20, compounded by the weak one-sided definition of bijective in Definition 18 and the restricted hole grammar for E6. The reader's CONDITIONAL verdict is therefore appropriate: the unambiguity theorem should be accepted only once the missing coercions and their bijectivity are supplied. No change to the reader's verdict is needed.","tokens_in":17693,"tokens_out":34859,"duration_ms":386372,"concrete_test":"Formalize Lemma 20 in a proof assistant (e.g., Coq or Lean): define parse trees, the equivalence rules (E1)–(E7), and explicit coercions for rules (E2)–(E5) and for congruence contexts (E6), and prove for each coercion f and its stated inverse g that f(g x) = x, g(f y) = y, and |f t| = |t| for all parse trees. A lighter check is to implement these coercions in the Haskell repository and run exhaustive property tests on parse trees up to a bounded depth for each rule. If all two-sided inverse and word-preservation laws are proved, the gap is closed; if any coercion fails, Theorem 25 collapses.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 25 depends on Lemma 20: every equivalence step in normalization must be realized by a bijective parse-tree coercion that preserves flattening. The proof only defines the coercion for rule (E1); for (E2)–(E5) it says 'can be defined similarly. Details are omitted for brevity,' and congruence/transitivity for (E6)–(E7) is only sketched. If any of these coercions is not bijective, or if normalization cannot be carried out with such coercions, then the unique parse tree of a non-overlapping equation maps to one parse tree of the solution, but other parse trees of the solution could exist outside the image, so the conclusion 'unambiguous' does not follow. The formal definition of bijective coercion in Definition 18 is also one-sided: it only requires g(v)⇓u whenever f(u)⇓v, which does not ensure the surjectivity/right-inverse needed to rule out extra parse trees in the solution. Additionally, the hole grammar for rule (E6) is stated only for sum contexts ([] | β[]+β | β+β[]), while the normalization argument in the proof of Theorem 11 appears to require congruence inside product contexts such as r·[]; if the intended grammar is broader, that needs to be stated. These are load-bearing presentation gaps, not a demonstrated counterexample.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":17926,"tokens_out":11108,"duration_ms":117923,"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":[{"comment":"","section":"Section 4, Lemma 20"},{"comment":"","section":"Section 4, Definition 18"},{"comment":"","section":"Section 3, Definition 9 and proof of Theorem 11"},{"comment":"","section":"Section 6.3, Theorem 40"}],"minor_comments":[{"comment":"","section":"Section 3, proof of Theorem 11"},{"comment":"","section":"Section 4, Proposition 14"},{"comment":"","section":"Section 3, Definition 10"}],"recommendation":"major_revision","confidential_remarks":"The paper is not fatally flawed: the overall approach appears sound, and the missing coercions and the one-sided bijectivity definition are repairable within the manuscript's scope. However, the central unambiguity theorem currently depends on explicitly omitted proof details plus a concrete error in the one exhibited inverse, so I cannot recommend acceptance in the present form. I would be willing to review a revised version that supplies the coercions for rules (E2)--(E5), fixes the definition of bijectivity, and clarifies the congruence rule (E6)."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nThe 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.\n\nThe 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.\n\nThe 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.\n\nBottom 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.","headline":"Solid paper with a genuinely new unambiguity result, but Theorem 25 rests on omitted coercions that must be supplied before the proof is complete.","tokens_in":18445,"tokens_out":4829,"would_cite":true,"duration_ms":47947,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45"],"pacs":[],"model":"deepseek-v4-flash","headline":"Solving regular equations by bijective parse-tree coercions makes unambiguous equation systems yield unambiguous regular expressions, covering DFA conversion and subtraction.","keywords":["regular equations","regular expressions","parse trees","unambiguity","derivatives of regular expressions","subtraction of regular languages","shuffle of regular languages","coercions"],"falsifier":"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.","tokens_in":17445,"feed_emoji":"🧮","tokens_out":11313,"duration_ms":108512,"temperature":0.7,"pith_summary":"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.","feed_headline":"DFA-to-regex output is unambiguous via parse-tree coercions","feed_subtitle":"A bijective parse-tree calculus yields unambiguous regexes for DFA conversion and subtraction.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the fixpoint equivalence used in each elimination step.","marker":"[3]"},{"why":"Defines ambiguity as two distinct parse trees for the same word, the property the main theorem rules out.","marker":"[4]"},{"why":"Supplies derivatives and the expansion theorem used to build the equation sets for DFA conversion, subtraction, and shuffle.","marker":"[5]"},{"why":"Gives the view of expressions as types and parse trees as values on which the coercion calculus is built.","marker":"[9]"},{"why":"Provides the coinductive bisimulation technique used to prove correctness of subtraction and shuffle.","marker":"[17]"}],"fun_headline_variants":["Bijective parse-tree coercions give unambiguous regex for DFA","Solving regular equations via invertible parse-tree maps","DFA-to-regex without ambiguity via parse-tree coercions","Parse-tree algebra makes regular equation solutions unambiguous","Direct algebraic solving yields unambiguous regex from DFA conversion"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Bijective parse-tree coercions give unambiguous regex for DFA","Solving regular equations via invertible parse-tree maps","DFA-to-regex without ambiguity via parse-tree coercions","Parse-tree algebra makes regular equation solutions unambiguous","Direct algebraic solving yields unambiguous regex from DFA conversion"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001082,"raw_usage":{"total_tokens":4489,"prompt_tokens":874,"completion_tokens":3615,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":490,"completion_tokens_details":{"reasoning_tokens":3538}},"tokens_in":490,"tokens_out":3615,"duration_ms":28005,"temperature":1.0,"reasoning_tokens":3538,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:06:20.272883+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the fixpoint equivalence used in each elimination step."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines ambiguity as two distinct parse trees for the same word, the property the main theorem rules out."},{"cited_title":"Brzozowski","cited_arxiv_id":null,"evidence_quote":"Supplies derivatives and the expansion theorem used to build the equation sets for DFA conversion, subtraction, and shuffle."},{"cited_title":"Greedy regular expressio n matching","cited_arxiv_id":null,"evidence_quote":"Gives the view of expressions as types and parse trees as values on which the coercion calculus is built."},{"cited_title":"Bonsangue, and Jan J","cited_arxiv_id":null,"evidence_quote":"Provides the coinductive bisimulation technique used to prove correctness of subtraction and shuffle."}],"review_version":1}