{"id":"dc01c23f-53e0-48cd-af17-565147dbee4b","arxiv_id":"1908.03551","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper defines reordering derivatives that build automata for trace closures of regular languages, proving finiteness for star-connected expressions and for languages with finite uniform scattering rank.","lead":"New derivative operations for regular expressions compute automata for trace closures, where independent letters may commute. For star-connected expressions, or when a new uniform scattering rank is finite, these automata are finite and exact.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Star-connected uniform-rank theorem rests on Lemma 71, whose inductive proof is too compressed to be load-bearing; an exhaustive search can test it.","rationale":"The reader's weakest_assumption identifies Lemma 71 and Prop. 72, and my reading agrees: this is the least secure load-bearing point. I have not found a concrete counterexample, and the lemma may well be true, but the paper's proof of it is a sketch that does not verify the preservation of the induction invariant in the critical block-moving case. Because the entire star-connected-to-uniform-rank direction rests on this lemma, and because the final theorem is only as solid as that step, a conditional acceptance is appropriate: accept the paper provided Lemma 71 is verified by an independent check (e.g., exhaustive search or machine-checked proof). I do not see an internal inconsistency, so REJECT or UNVERDICTED would be too strong; the concern is about proof completeness, not about the plausibility of the central construction.","tokens_in":28629,"tokens_out":49006,"duration_ms":498181,"concrete_test":"Write an exhaustive checker for Lemma 71: enumerate all irreflexive symmetric independence relations I on alphabets of size ≤4, all sequences z1,...,zn of nonempty connected words of total length ≤8, all words w=uv with w∼I z1...zn, and all permutations of z1...zn; verify that some permutation satisfies properties (1) and (2) of Lemma 71. If a counterexample is found, Prop. 72's E*-case is false and the star-connected implication breaks. If no counterexample is found, the remaining risk is the unproved induction step; then formalize the critical block-move argument in a proof assistant such as Isabelle/HOL to check that the invariant really is preserved for all smaller prefixes.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim (Cor. 77 + Prop. 81) is that the N-truncated refined Antimirov automaton is finite and accepts the trace closure whenever JEK has finite uniform scattering rank. The paper's main source of such a rank for its flagship class, star-connected expressions, is Prop. 72, whose E*-case depends on Lemma 71. Lemma 71 asserts that any sequence of nonempty connected words trace-equivalent to w=uv can be permuted so that, for every prefix split of u, no word lying completely in the suffix immediately precedes a word lying completely in the prefix. The proof is an induction on u, but the critical case is only sketched: a block z'_m...z'_l is moved in front of z'_k...z'_{m-1}, and the claim that the new permutation preserves property (2) for all smaller prefixes is asserted without a detailed argument. If Lemma 71 fails, the degree bound for E* does not follow, and with it Prop. 72, the application of Cor. 77 to star-connected regexps, and the advertised 'finite without quotienting' result for star-connected expressions all lose their foundation. The surrounding proof also shows signs of fragility: the counting in Prop. 72 seems to justify a bound roughly |Σ|N+|Σ| rather than (|Σ|+1)N as written, so the proof needs repair even if the statement survives.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper generalizes Brzozowski and Antimirov derivative constructions from regular word languages to trace closures of regular languages. It defines reordering derivatives, both deterministic (Brzozowski-style) and nondeterministic (Antimirov-style), and shows that for star-connected expressions the resulting automata are finite after suitable quotienting. It then introduces a refined Antimirov derivative whose states are lists of regular expressions, together with a new measure, the uniform scattering rank of a language. The central claim is that if a regular expression E has finite uniform scattering rank at most N, then the N-truncated refined Antimirov automaton is finite without quotienting and still accepts the trace closure of JEK; moreover, star-connected languages are shown to have finite uniform rank, so the truncation theorem applies to the flagship class. The paper includes many detailed proofs, worked examples, and a useful comparison with Hashiguchi's scattering rank and with prior work by Ochmański and Klunder et al.","tokens_in":28792,"tokens_out":8897,"duration_ms":99075,"significance":"If the technical results hold, this is a substantive contribution to the theory of trace closures of regular languages and to derivative-based automata constructions. The refined Antimirov automaton with truncation is a genuinely new construction, and the uniform scattering rank is a natural strengthening of Hashiguchi's rank that is tailor-made for a cleaner finiteness theorem without quotienting. The paper is self-contained in its main development, carefully cites external results (Ochmański's characterization, Hashiguchi's rank theorem, Klunder et al.'s rank result), and provides explicit examples that illustrate both the constructions and the necessity of uniformity. The full version also supplies proofs for many propositions that were only sketched in the conference version, which increases its value as a reference. The main caveat is that the proof of the star case for uniform rank rests on a combinatorial permutation lemma whose proof is currently too compressed, and the numerical bound in that proof appears to be miscalculated; these issues affect the proof of Proposition 72 and hence part of the advertised application to star-connected expressions.","major_comments":[{"comment":"The proof of Lemma 71 is not complete in the critical case. After constructing the new permutation by moving z'_m,...,z'_l in front of z'_k,...,z'_{m-1}, the paper asserts that this 'ensures that the new permutation σ'' has property 2 also for all prefixes u' up to u'=u', but no argument is given for why the new decompositions satisfy the required independence conditions or why the universal quantification over u1,...,un and v1,...,vn is preserved. This is not a cosmetic omission: Lemma 71 is the only tool that produces the permutation used in the star case of Proposition 72. Without a rigorous proof of this lemma, the uniform-rank bound for L* does not follow, and with it the application of Corollary 77 to star-connected expressions loses its foundation. The authors should either supply a complete induction or replace this lemma by a fully proved alternative argument.","section":"§5.2, Lemma 71"},{"comment":"The final bound in Proposition 72 is not supported by the preceding estimates. The proof obtains at most |Σ|N from the two-colored z_i and at most |Σ| from the intervening single-colored sequences, which yields a total of at most |Σ|N + |Σ|, not (|Σ|+1)N. The inequality |Σ|N+|Σ| ≤ (|Σ|+1)N fails whenever N < |Σ|, and no such relation is established in the proof. Since Proposition 72 is the statement that star-connected languages have finite uniform rank, the proof should be repaired by either correcting the bound to a quantity that is actually derived (e.g., (|Σ|+1)N+|Σ|) or by giving a sharper accounting that does yield (|Σ|+1)N. This is load-bearing because the exact constant is not essential for the finiteness application, but the current proof does not establish the stated result.","section":"§5.2, Proposition 72"}],"minor_comments":[{"comment":"The proof says 'We only look at the case E*' and omits the union and concatenation cases. These cases are straightforward and are essentially covered by the argument already given in Proposition 68, but for a full-version proof of a central theorem it would be better to state them explicitly or to provide the rank bounds for them.","section":"§5.2, Proposition 72"},{"comment":"The sentence 'Altogether the degree of u ◁z◦⊿v is thus at most (|Σ|+1)N' uses the wrong relation symbol; it should be 'u ∼◁ z◦ ⊿∼ v' (or the appropriate degree-bounded variant), matching the notation used in the rest of the proof.","section":"§5.2, final paragraph"},{"comment":"The proof of Lemma 71 contains the typo 'infrontofof' and the phrase 'has property 2' is used ambiguously; consider defining the permutation as a bijection on indices rather than as a reordered sequence of words, which would make the induction easier to follow.","section":"§5.2, Lemma 71"},{"comment":"There are small typos: 'Hachiguchi' should be 'Hashiguchi' in the proof of Theorem 51, and 'langugage' should be 'language' in the statement of Theorem 52.","section":"§3.4, Theorem 51 and Theorem 52"},{"comment":"The condition '|Γ, Δ|<N' in the first rule of ⇒I_N is easy to misread as the sum of the lengths of the lists Γ and Δ; since Γ and Δ are lists, it would be clearer to write '|Γ|+|Δ|<N' or to say explicitly that the length of the concatenated list is at most N.","section":"§6.1, Definition 73"}],"recommendation":"major_revision","confidential_remarks":"This is a solid and original paper whose main constructions and statements are likely correct, but the combinatorial core of the star-connected uniform-rank theorem is not yet presented with enough rigor. The proof of Lemma 71 needs either a full induction or a replacement argument, and the bound in Proposition 72 needs a corrected derivation. These are fixable within the manuscript's scope, so I recommend major revision rather than rejection. The refereeing process should ask for the complete proof of Lemma 71 and a careful check of the counting in Proposition 72 before the paper is accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis paper deserves a careful read. It generalizes the Brzozowski and Antimirov derivative constructions to trace closures of regular languages, introduces a uniform scattering rank, and shows that a truncated refined Antimirov automaton is finite and accepts the trace closure when the rank is bounded. The constructions are natural and the finiteness theorems are genuinely new. The paper is well-structured, the examples are helpful, and most induction proofs are detailed enough to check by hand.\n\nThe strongest part is the refined Antimirov derivative with lists of regexps and the truncation theorem (Cor. 77 + Prop. 81). The counterexample separating scattering rank from uniform rank (Prop. 67) is crisp and illuminating. I also like the clean use of Ochmański, Hashiguchi, and Klunder et al. as black boxes; the citation pattern is appropriate.\n\nNow the soft spots. Lemma 71 is load-bearing for Proposition 72, which says star-connected languages have finite uniform rank. The proof of Lemma 71 is too compressed. In the critical case it moves a block of words and asserts that the new permutation preserves the required property for all smaller prefixes, giving only a single sentence of justification. This is exactly the kind of combinatorial claim that can hide a subtle failure. The stress-test note is right: this needs a fuller proof, or a machine-checked version, before the paper's main advertised result rests on it.\n\nSecond, the counting in Proposition 72 appears to give a bound of |Σ|N + |Σ|, not (|Σ|+1)N as stated. If I am reading correctly, the final bound is misstated. The existence of a finite uniform rank still follows, so the theorem survives, but the paper states a specific bound and should correct it.\n\nThird, a smaller point: the full version says it includes proofs of the most important propositions, but some are still compressed (Lemmas 70 and 71, and several cases in Prop. 74's proof are only sketched). For a pure mathematics paper this is acceptable, but the reader cannot verify every step without significant effort.\n\nOverall, this is serious work, the central idea is novel, and I think it deserves rigorous refereeing. I recommend acceptance conditional on the authors expanding the proof of Lemma 71 and correcting the bound in Prop. 72. Even if Lemma 71 is fixed, this is a meaningful contribution to trace theory and derivative-based automata constructions.\n\nBring it to reading group if your group works on syntactic automata constructions or trace theory. I would cite it in that context.","headline":"A genuinely new and useful extension of derivative-based automata constructions to trace closures, but the main star-connected result rests on an under-proved combinatorial lemma and a likely misstated bound.","tokens_in":29399,"tokens_out":2526,"would_cite":true,"duration_ms":27785,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that the classical derivative-based automaton constructions extend to trace closures of regular languages, and that a bounded variant is finite and exact whenever the language has finite uniform scattering rank.","keywords":["regular languages","trace closures","language derivatives","reordering derivatives","scattering rank","uniform scattering rank","star-connected expressions","finite automata"],"falsifier":"A concrete refutation would be a star-connected expression E and a word w=uv in its trace closure such that every witness word z in JEK scatters u into more than (|Σ|+1)N blocks, where N is the uniform scattering rank of JEK. A brute-force search over small independence alphabets and connected languages L, comparing minimal scattering block counts for words of [L*]I against the paper's bound, would settle whether Lemma 71's permutation claim always holds.","tokens_in":28322,"feed_emoji":"🔀","tokens_out":11527,"duration_ms":108717,"temperature":0.7,"pith_summary":"Words that differ only by swapping adjacent independent letters are observations of the same concurrent behaviour; the trace closure of a language adds all such equivalent words. The paper extends the two classical syntactic derivative constructions for regular expressions to these trace closures, yielding deterministic and nondeterministic automata for the closure. Because trace closures are generally not regular, those automata are generally infinite; the paper shows that for star-connected expressions suitable quotients are finite. The central result is that a bounded, refined version of the partial-derivative automaton—states are lists of at most N+1 expressions—is finite without any quotienting and accepts the full trace closure exactly when the underlying language has uniform scattering rank at most N. This matters because it gives a finite automata-theoretic handle on non-regular trace languages.","feed_headline":"Scattering-rank cutoff yields finite exact automata for trace closures","feed_subtitle":"A truncated derivative automaton accepts full trace closures without quotienting, once scattering rank is bounded.","key_machinery":"The load-bearing device is the pair: (i) the I-reordering concatenation u·_I v, which interleaves independent letters while keeping dependent order, and the associated reordering derivatives; and (ii) the uniform scattering rank of a language, which bounds by N the number of blocks into which the prefix u of any split w=uv needs to be scattered inside some witness z for w in the closure. The refined partial-derivative construction turns this block bound into a syntactic bound: its states are nonempty lists of at most N+1 regular expressions, one per block, and the derivation rules update the list only when the block count allows. The truncation theorem says that the bounded list automaton is exactly the finite automaton promised: lists cannot grow beyond N+1, and the uniform-rank hypothesis guarantees that no accepted word ever needs a longer list.","core_discovery":"The paper's central claim is that trace closures of regular languages admit syntactic reordering derivatives that behave like the classical ones, and that a carefully truncated automaton can be both finite and exact. The reordering derivative along a word u removes not just an ordinary prefix but a scattered occurrence of u from a witness word: for a language L, the reordering derivative DI_u L collects suffixes v such that some word equivalent to uv lies in L with the u-part scattered in at most N blocks. The refined construction tracks the blocks individually as a list of expressions. The main theorem states that if JEK has uniform scattering rank at most N, then the N-truncated refined automaton accepts exactly the trace closure JEKI, and its state set is finite with no quotienting by syntactic equations; moreover every star-connected language has finite uniform scattering rank, so the construction applies to all regular closed languages.","pith_inferences":["I would expect the uniform-rank bound for starred expressions—(|Σ|+1)N—to translate directly into a state-count bound for the truncated automaton, making the construction a practical way to decide membership in the trace closure when a rank bound is known, even though the closure itself may be non-regular.","The paper's observation that the derivative rules use independence only in one direction suggests a testable extension: the same list-based construction may work for semi-commutations, but the loss of symmetry would likely break the permutation lemma that supplies the rank bound.","A natural next probe is whether languages with finite scattering rank but no uniform rank can ever be accepted by some bounded-list automaton with a cleverer acceptance condition; the paper's example suggests the answer is no, but it does not prove that."],"forward_implications":["For every regular expression whose language has uniform scattering rank at most N, the N-truncated refined automaton is a finite NFA accepting the trace closure exactly, with no quotienting by syntactic equations.","Because every star-connected language has finite uniform scattering rank, every regular trace-closed language—which is exactly the closure of a star-connected language—has a finite truncated automaton for some bound N.","When the independence relation is empty, the reordering derivative constructions reduce to the classical derivative constructions, so the result is a genuine generalization of the standard pipeline rather than a separate construction.","For languages without uniform scattering rank, no truncation level is exact: the paper's example of a language with rank 2 but no uniform rank shows that every N-truncated automaton rejects some word of the closure."],"supporting_citations":[{"why":"introduces the syntactic deterministic derivative of regular expressions that the reordering derivative generalizes.","marker":"[7]"},{"why":"introduces the partial-derivative relation that the refined list-valued construction generalizes.","marker":"[3]"},{"why":"introduces scattering rank, the notion the paper strengthens to uniform scattering rank.","marker":"[9]"},{"why":"proves star-connected languages have scattering rank, the result refined here to uniform rank.","marker":"[12]"},{"why":"establishes that regular closed languages are exactly trace closures of star-connected languages, motivating the star-connected case.","marker":"[18]"},{"why":"supplies the handbook formulations of the rank and star-connectedness results used as background lemmas.","marker":"[19]"}],"fun_headline_variants":["Finite exact automata for trace closures via scattering-rank cutoff","Truncated reordering derivatives yield finite, exact trace-closure automata","Scattering rank bounds automaton size without quotienting","Star-connected languages get finite automata from reordering derivatives","No quotienting: truncated derivative automaton accepts exact trace closures"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof that every star-connected language has finite uniform scattering rank depends on a combinatorial lemma (Lemma 71) asserting that the connected pieces of a witness word can always be permuted so that no piece belonging entirely to the suffix immediately follows a piece belonging entirely to the prefix; if that lemma fails, the whole star-connected case collapses.","fun_headline_variants_meta":{"raw":{"variants":["Finite exact automata for trace closures via scattering-rank cutoff","Truncated reordering derivatives yield finite, exact trace-closure automata","Scattering rank bounds automaton size without quotienting","Star-connected languages get finite automata from reordering derivatives","No quotienting: truncated derivative automaton accepts exact trace closures"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000212,"raw_usage":{"total_tokens":1409,"prompt_tokens":928,"completion_tokens":481,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":544,"completion_tokens_details":{"reasoning_tokens":395}},"tokens_in":544,"tokens_out":481,"duration_ms":5104,"temperature":1.0,"reasoning_tokens":395,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:09:16.994615+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete refutation would be a star-connected expression E and a word w=uv in its trace closure such that every witness word z in JEK scatters u into more than (|Σ|+1)N blocks, where N is the uniform scattering rank of JEK. A brute-force search over small independence alphabets and connected languages L, comparing minimal scattering block counts for words of [L*]I against the paper's bound, would settle whether Lemma 71's permutation claim always holds.","supporting_citations":[{"cited_title":"Recognizable closures and submonoids of free partially commutative monoids","cited_arxiv_id":null,"evidence_quote":"introduces scattering rank, the notion the paper strengthens to uniform scattering rank."},{"cited_title":"On star-connected flat languages","cited_arxiv_id":null,"evidence_quote":"proves star-connected languages have scattering rank, the result refined here to uniform rank."},{"cited_title":"Regular behaviour of concurrent systems","cited_arxiv_id":null,"evidence_quote":"establishes that regular closed languages are exactly trace closures of star-connected languages, motivating the star-connected case."},{"cited_title":"Recognizable trace languages","cited_arxiv_id":null,"evidence_quote":"supplies the handbook formulations of the rank and star-connectedness results used as background lemmas."}],"review_version":1}