Pith. sign in

REVIEW 2 major objections 5 minor 25 references

Reordering Derivatives of Trace Closures of Regular Languages (Full Version)

T0 review · 2 major / 5 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 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.

desk verdict 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. read the letter →

arxiv 1908.03551 v1 pith:ZPT5UBOR submitted 2019-08-09 cs.FL

Hendrik Maarand , Tarmo Uustalu This is my paper · ORCID
classification cs.FL
keywords regularlanguagestraceclosureslanguagederivativesreorderingscatteringrankuniformstar-connectedexpressionsfiniteautomata
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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

Reading between the lines

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

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

Referee Report

2 major / 5 minor

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.

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 (2)
  1. [§5.2, Lemma 71] 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.
  2. [§5.2, Proposition 72] 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.
minor comments (5)
  1. [§5.2, Proposition 72] 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.
  2. [§5.2, final paragraph] 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.
  3. [§5.2, Lemma 71] 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.
  4. [§3.4, Theorem 51 and Theorem 52] 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.
  5. [§6.1, Definition 73] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the uniform-rank and truncated-automaton results are derived internally from new definitions and lemmas, while external citations and the single self-citation are not load-bearing inputs.

full rationale

The paper's main derivation chain is self-contained. Corollary 77 is not circular: the uniform scattering rank (Definition 65) is a semantic condition on words in [L]I, while the N-truncated refined Antimirov automaton (Definition 73 and Proposition 81) is defined independently by length-bounded lists of regexps and nullable-endpoint acceptance. The implication (a)=>(b) in Corollary 77 is a direct application of the uniform-rank definition, and (b)=>(c) is proved by the separate syntactic completeness lemma Proposition 76, which replays the induction of Proposition 74 rather than assuming the conclusion. Proposition 72, showing that star-connected languages have finite uniform scattering rank, is proved by its own induction using Lemmas 70 and 71; although the induction in Lemma 71 is compressed, a terse proof is a correctness or completeness concern, not a circular reduction, and the lemma does not assume Proposition 72. The only self-citation, the conference version [14], is explicitly identified as the earlier version of this same full paper and is not used to justify any load-bearing step. External results such as Ochmański's characterization, Hashiguchi's rank theorem, and Klunder et al.'s rank bound are cited as established background; the new finiteness and exactness claims are proved from the paper's own Lemmas 56-58, Proposition 60, and Definition 79. No fitted parameter is renamed as a prediction, and no ansatz is imported from the authors' prior work. The distinction between rank and uniform rank, including the counterexample in Proposition 67, shows that the new notion is not merely a renamed classical concept. Accordingly, no circular step is present, and the appropriate score is 0.

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

The paper introduces no fitted parameters. Its axioms are standard mathematical background (Kleene algebra equations, classical theorems of Ochmański, Hashiguchi, and Klunder et al.) plus the standard domain assumption about independence alphabets. The newly introduced mathematical notions, uniform scattering rank and refined derivatives, serve as internal tools rather than unexplained postulates; their validity is supported by the proofs in the paper.

assumptions (3)
  • domain assumption The independence alphabet is finite, and the independence relation I is irreflexive and symmetric.
    Standard definition of Mazurkiewicz trace alphabets; used throughout Sections 3 to 6.
  • standard math Established results by Ochmański [18], Hashiguchi [9], and Klunder et al. [12] hold.
    Used as external theorems in Sections 4.4, 5.1, and 5.2: regular closed languages are closures of star-connected languages; rank implies regular trace closure; star-connected languages have rank. The paper does not re-prove these but relies on them.
  • standard math Standard Kleene algebra equations (idempotence of +, zero laws for 0, unitality, F*F* = F*) are admissible for quotienting automata and for the syntactic equivalence .=
    Used throughout Section 4 to justify quotienting and to simplify expressions; these equations are classical and used for the Brzozowski derivative quotient.
invented entities (2)
  • uniform scattering rank
    purpose: A stronger variant of Hashiguchi's scattering rank, used to prove finiteness of the truncated refined Antimirov automaton and to characterize when truncation still accepts the full trace closure.
    New mathematical definition introduced in Section 5.1. It has no external empirical handle, but it is internally used to state and prove Theorems 77 and 81, and is shown to be finite for star-connected languages.
  • refined Antimirov I-reordering parts-of-derivatives
    purpose: A list-based syntactic derivative relation that yields the refined automaton whose states are lists of regexps.
    New syntactic construction defined inductively in Section 6.1. It is a mathematical tool, not an empirical postulate; its correctness is established by the paper's propositions (74 to 77).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Reordering Derivatives of Trace Closures of Regular Languages (Full Version)." pith.science (2026). https://pith.science/paper/ZPT5UBOR

@misc{pith2026190803551,
  author       = {Pith},
  title        = {Pith review of: Reordering Derivatives of Trace Closures of Regular Languages (Full Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZPT5UBOR}},
  note         = {Machine review of arXiv:1908.03551}
}
read the original abstract

We provide syntactic derivative-like operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and Brzozowski automata, suitably quotiented, are finite. We also define a refined version of the Antimirov reordering derivative operation where parts-of-derivatives (states of the automaton) are nonempty lists of regular expressions rather than single regular expressions. We define the uniform scattering rank of a language and show that, for a regexp whose language has finite uniform scattering rank, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing long states, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform scattering rank.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

25 extracted references · 18 canonical work pages

  1. [1]

    Characterizations of the decidability of some problems for regular trace languages

    IJsbrand Jan Aalbersberg and Hendrik Jan Hoogeboom. Characterizations of the decidability of some problems for regular trace languages. Math.\ Syst.\ Theory , 22(1):1--19, 1989. http://dx.doi.org/10.1007/BF02088289 doi:10.1007/BF02088289

    work page doi:10.1007/bf02088289 1989

  2. [2]

    Trace languages defined by regular string languages

    IJsbrand Jan Aalbersberg and Emo Welzl. Trace languages defined by regular string languages. Theor.\ Inf.\ Appl. , 20(2):103--119, 1986. http://dx.doi.org/10.1051/ita/1986200201031 doi:10.1051/ita/1986200201031

    work page arXiv 1986

  3. [3]

    Antimirov

    Valentin M. Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theor.\ Comput.\ Sci. , 155(2):291--319, 1996. http://dx.doi.org/10.1016/0304-3975(95)00182-4 doi:10.1016/0304-3975(95)00182-4

    doi:10.1016/0304-3975(95)00182-4 1996

  4. [4]

    Equivalence and membership problems for regular trace languages

    Alberto Bertoni, Giancarlo Mauri, and Nicoletta Sabadini. Equivalence and membership problems for regular trace languages. In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming: 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings , volume 140 of Lecture Notes in Computer Science , pages 61--71. Springer, 1982...

    work page doi:10.1007/bfb0012757 1982

  5. [5]

    Unambiguous regular trace languages

    Alberto Bertoni, Giancarlo Mauri, and Nicoletta Sabadini. Unambiguous regular trace languages. In Janos Demetrovics, Gyula Katona, and Arto Salomaa, editors, Algebra, Combinatorics, and Logic in Computer Science , volume 42 of Collquia Mathematica Societas J \'a nos Bolyai , pages 113--123. North-Holland, 1986

    work page 1986

  6. [6]

    Partial derivative automaton for regular expressions with shuffle

    Sabine Broda, Ant \' o nio Machiavelo, Nelma Moreira, and Rog \' e rio Reis. Partial derivative automaton for regular expressions with shuffle. In Jeffrey Shallit and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems: 17th International Workshop, DCFS 2015, Waterloo, ON, Canada, June 25-27, 2015, Proceedings , volume 9118 of Lecture N...

    work page doi:10.1007/978-3-319-19225-3_2 2015

  7. [7]

    Brzozowski

    Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM , 11(4):481--494, 1964. http://dx.doi.org/10.1145/321239.321249 doi:10.1145/321239.321249

    arXiv 1964

  8. [8]

    Semi-commutations

    Mireille Clerbout and Michel Latteux. Semi-commutations. Inf. Comput. , 73(1):59--74, 1987. http://dx.doi.org/10.1016/0890-5401(87)90040-X doi:10.1016/0890-5401(87)90040-X

    work page doi:10.1016/0890-5401(87)90040-x 1987

Show all 25 references
  1. [9]

    Recognizable closures and submonoids of free partially commutative monoids

    Kosaburo Hashiguchi. Recognizable closures and submonoids of free partially commutative monoids. Theor.\ Comput.\ Sci. , 86(2):233--241, 1991. http://dx.doi.org/10.1016/0304-3975(91)90019-X doi:10.1016/0304-3975(91)90019-X

    1991 doi

  2. [10]

    Concurrent K leene algebra and its foundations

    Tony Hoare, Bernhard M \" o ller, Georg Struth, and Ian Wehrman. Concurrent K leene algebra and its foundations. J.\ Log.\ Algebr.\ Program. , 80(6):266--296, 2011. http://dx.doi.org/10.1016/j.jlap.2011.04.005 doi:10.1016/j.jlap.2011.04.005

    2011 doi

  3. [11]

    Stephen C. Kleene. Representation of events in nerve sets and finite automata. In Claude E. Shannon and John McCarthy, editors, Automata Studies , volume 34 of Annals of Mathematics Studies , pages 3--42. Princeton University Press, 1956

    1956

  4. [12]

    On star-connected flat languages

    Barbara Klunder, Edward Ochma \'n ski, and Krystyna Stawikowska. On star-connected flat languages. Fund.\ Inf. , 67(1--3):93--105, 2005. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi67-1-3-08

    2005

  5. [13]

    A completeness theorem for K leene algebras and the algebra of regular events

    Dexter Kozen. A completeness theorem for K leene algebras and the algebra of regular events. Inf.\ Comput. , 110(2):366--390, 1994. http://dx.doi.org/10.1006/inco.1994.1037 doi:10.1006/inco.1994.1037

    1994

  6. [14]

    Reordering derivatives of trace closures of regular languages

    Hendrik Maarand and Tarmo Uustalu. Reordering derivatives of trace closures of regular languages. In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27--30, 2019, Amsterdam, The Netherlands , volume 140 of Lei...

    2019 doi

  7. [15]

    Concurrent program schemes and their interpretations

    Antoni Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB-78, University of Aarhus, 1978. http://dx.doi.org/10.7146/dpb.v6i78.7691 doi:10.7146/dpb.v6i78.7691

    1978 doi

  8. [16]

    Introduction to trace theory

    Antoni Mazurkiewicz. Introduction to trace theory. In Volker Diekert, editor, The Book of Traces , pages 3--41. World Scientific, 1995. http://dx.doi.org/10.1142/9789814261456_0001 doi:10.1142/9789814261456_0001

    1995 doi

  9. [17]

    J. D. McKnight. K leene quotient theorems. Pac.\ J.\ Math. , 14(4):1343--1352, 1964. http://dx.doi.org/10.2140/pjm.1964.14.1343 doi:10.2140/pjm.1964.14.1343

    1964 doi

  10. [18]

    Regular behaviour of concurrent systems

    Edward Ochma \'n ski. Regular behaviour of concurrent systems. Bull.\ EATCS , 27:56--67, 1985

    1985

  11. [19]

    Recognizable trace languages

    Edward Ochma \'n ski. Recognizable trace languages. In Volker Diekert, editor, The Book of Traces , pages 167--204. World Scientific, 1995. http://dx.doi.org/10.1142/9789814261456_0006 doi:10.1142/9789814261456_0006

    1995 doi

  12. [20]

    Rabin and Dana S

    Michael O. Rabin and Dana S. Scott. Finite automata and their decision problems. IBM J.\ Res.\ Devel. , 3(2):114--125, 1959. http://dx.doi.org/10.1147/rd.32.0114 doi:10.1147/rd.32.0114

    1959 doi

  13. [21]

    On regular trace languages

    Jacques Sakarovitch. On regular trace languages. Theor. Comput. Sci. , 52:59--75, 1987. http://dx.doi.org/10.1016/0304-3975(87)90080-6 doi:10.1016/0304-3975(87)90080-6

    1987 doi

  14. [22]

    The "last" decision problem for rational trace languages

    Jacques Sakarovitch. The "last" decision problem for rational trace languages. In Imre Simon, editor, LATIN '92, 1st Latin American Symposium on Theoretical Informatics, S \ a o Paulo, Brazil, April 6-10, 1992, Proceedings , volume 583 of Lecture Notes in Computer Science , pa...

    1992 doi

  15. [23]

    Derivatives for regular shuffle expressions

    Martin Sulzmann and Peter Thiemann. Derivatives for regular shuffle expressions. In Adrian - Horia Dediu, Enrico Formenti, Carlos Mart \' n - Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications: 9th International Conference, LATA 2015, Nice, France,...

    2015 doi

  16. [24]

    Notes on finite asynchronous automata

    Wies aw Zielonka. Notes on finite asynchronous automata. Theor.\ Inf.\ Appl. , 21(2):99--135, 1987. http://dx.doi.org/10.1051/ita/1987210200991 doi:10.1051/ita/1987210200991

    1987

  17. [25]

    Asynchronous automata

    Wies aw Zielonka. Asynchronous automata. In Volker Diekert, editor, The Book of Traces , pages 205--247. World Scientific, 1995. http://dx.doi.org/10.1142/9789814261456_0007 doi:10.1142/9789814261456_0007

    1995 doi

Pith tools

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