REVIEW 2 major objections 3 minor 39 references
A Myhill-Nerode Type Characterization of 2detLIN Languages
T0 review · 2 major / 3 minor · reviewed 2026-08-06 · deepseek-v4-flash
Pith's one-line read A language is 2detLIN exactly when its prefix-suffix pairs admit a complete, finite, crossing-free classification.
desk verdict A new Myhill-Nerode-style framework for 2detLIN, but the reverse construction's transition rule is ill-defined: the stress-test example correctly shows one state/letter pair forced to two next states by different presus in the same class. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the border classification (BC), a partition of prefix-suffix pairs into language-equivalence classes. Two extra conditions make the BC match 2detLIN: completeness (each input word is split by exactly one pair in the classification) and the absence of crossing pairs (no two pairs whose prefixes and suffixes interleave in a crossing pattern). The BC acts as a finite description of the automaton's state behavior: each class can be realized by one or two states, with the choice of state recording which reading head moves next. The no-crossing condition is what forces the two heads' behaviors to be consistent across all pairs in a class.
What would settle it
Run Algorithm 1 on a complete deterministic linear automaton that accepts a known 2detLIN language with irregular head-step order, and search the generated pseudo-BC for two presus (u1,v1) and (u2,v2) with u1 a proper prefix of u2 and v2 a proper suffix of v1. If any such crossing pair appears, Claim 2 is false and Theorem 1's forward direction fails; conversely, if no implementation over a large test suite ever produces one, that would support the claim but not prove it.
Extended reading notes
Core claim
The paper's central claim is Theorem 1: a language L is in 2detLIN if and only if there exists a complete border classification (BC) for L with finite index that contains no crossing pairs. Here a BC partitions prefix-suffix pairs into equivalence classes under the relation u1 w v1 ∈ L ⇔ u2 w v2 ∈ L for all middle words w; completeness means every word w is represented by exactly one pair (u,v) with w = uv; and crossing pairs would be pairs (u1,v1), (u2,v2) with u1 a proper prefix of u2 and v2 a proper suffix of v1. The proof is constructive in both directions. Given a complete deterministic linear automaton, Algorithm 1 builds a pseudo-BC by breadth-first exploration of reachable states, and the paper claims (without proof in this version) that this pseudo-BC is crossing-free. Conversely, given a complete crossing-free BC, the paper constructs a deterministic linear automaton with at most two states per class, one for each possible next-moving head, and shows it accepts exactly L.
Load-bearing premise
The forward direction of Theorem 1 rests on the paper's Claim 2, which states that the pseudo-BC generated by Algorithm 1 from any complete deterministic linear automaton never contains crossing pairs; the claim is asserted but not proved in this version, and if it fails, the 'only if' half of the characterization collapses.
Editorial extensions
If this is right
- If Theorem 1 holds, membership in 2detLIN can be certified by giving a finite complete crossing-free BC, a purely combinatorial object independent of any particular automaton.
- The same BC yields, by the constructive proof, a complete deterministic linear automaton with at most two states per class, giving a normal form for 2detLIN acceptors.
- For every k-rated linear language (k a nonnegative rational), the BC can be chosen so that the same head always moves for all pairs in a class; for regular languages (k=0) this recovers exactly the classical Myhill-Nerode characterization (Corollary 1).
- The complement of a 2detLIN language is again 2detLIN, because the same equivalence classes serve both languages, only the accepting states change (Proposition 3).
- Languages outside 2detLIN, such as {a^n b^n c^n}, can be proven non-members by showing that no complete finite crossing-free BC can exist (Example 5).
Reading between the lines
- The BC index is not a language invariant: a single 2detLIN language can have many different complete crossing-free BCs, so unlike the regular case there may be no canonical minimal BC; a descriptional complexity measure would need to account for the choice of head-step order.
- The crossing-free condition is reminiscent of non-crossing partitions in combinatorics; it may connect 2detLIN to laminar family structures, and one could test whether BCs of a 2detLIN language always correspond to non-crossing collections of intervals on the word positions.
- Because every regular language is k-rated for any positive rational k, the same regular language admits infinitely many different BCs under Theorem 3; exploring which k minimizes the number of classes could yield an alternative state-count measure for regular languages, as the paper's discussion suggests.
- One could implement Algorithm 1 on a broad set of deterministic linear automata (including non-fixed-rated ones) to test Claim 2 computationally; regardless of outcome, this would clarify whether the unproved crossing-freeness claim is true or needs a restricted hypothesis.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a Myhill-Nerode-type characterization of the class 2detLIN, the languages accepted by deterministic two-headed linear automata. It defines prefix-suffix pairs (called presus) and their equivalence with respect to a language L, and calls a collection of equivalence classes a border classification (BC). Two additional conditions are introduced: completeness, meaning that for every word w the BC contains exactly one presu (u,v) with w=uv, and absence of crossing pairs, meaning that no two presus have the pattern (u1,v1), (u2,v2) with u1 a proper prefix of u2 and v2 a proper suffix of v1. Theorem 1 states that L is in 2detLIN if and only if there is a complete BC with finite index for L that has no crossing pairs. The forward direction is proved by Algorithm 1, which builds a pseudo-BC from a complete deterministic linear automaton; the reverse direction constructs a deterministic linear automaton with two states per equivalence class from a given BC. The paper includes several examples, a discussion of k-rated linear languages, a complement-closure observation, and a non-membership proof for {a^n b^n c^n}.
Significance. If the characterization were established with complete proofs, it would be a genuinely useful structural analogue of the Myhill-Nerode theorem for a nontrivial superclass of the regular languages, with potential consequences for a descriptional-complexity measure for 2detLIN. The paper's concrete algorithmic construction, the worked examples, and the complement-closure observation in Proposition 3 are valuable and give the claimed result a clear intuitive content. However, the two central proof obligations are not discharged in the submitted text: the non-crossing property in the forward direction is asserted without proof, and the reverse transition construction is not well-defined as written. The main theorem is therefore currently unproven, although the underlying idea appears plausible and likely repairable.
major comments (2)
- [Section 3, Claim 2] Claim 2, which states that the pseudo-BC produced by Algorithm 1 from any complete deterministic linear automaton contains no crossing pairs, is load-bearing for the forward direction of Theorem 1, but it is stated with no proof. The text only says that the pseudo-BC is complete and then moves on. Lemma 3 and Claim 1 are likewise asserted without proof. Since the paper explicitly says that some proofs are omitted because of page limits, a journal version must supply these arguments; in particular, Claim 2 needs a real proof, for example by showing that the family of prefix-suffix pairs occurring in computations of a deterministic linear automaton has a laminar or non-crossing structure.
- [Section 3, reverse direction of Theorem 1] The transition rule in the construction from a BC to a deterministic linear automaton is not well-defined. The conditions defining δ(q_i,a,λ) and δ(p_i,λ,a) are existential over presus in the class C_i, and different presus in the same class can force different target states for the same input letter. Concretely, let T={a}, L={a^{2n}}, and consider the complete BC with two classes determined by parity of N, where each word a^N is represented by the single presu (a^{s(N)}, a^{N-s(N)}) with s(0)=0, s(1)=1, s(2)=2, s(3)=3, s(4)=4, s(5)=5, s(6)=5, and s(N)=N−1 for N≥7. This BC has finite index 2, is complete, and has no crossing pairs. In C_even, the presu (λ,λ) gives (a,λ)∈C_odd and (aa,λ) appears, so the rule forces δ(q_even,a,λ)=q_odd. But the presu (a^4,λ)∈C_even gives (a^5,λ)∈C_odd and (a^5,a) appears, so the same rule forces δ(q_even,a,λ)=p_odd. Thus one configuration is assigned two different next states, and the constructed object is not a deterministic linear automaton. Claims 3 and 4 constrain each presu individually and do not prevent conflicts between different presus in one class. The if-direction of Theorem 1 therefore needs either a canonical representative inside each class or an additional compatibility condition; the proof as written is invalid.
minor comments (3)
- [Example 3] The BC defined for L={1^n 0^{3n}} does not appear to be complete as written: for the word 10, none of the listed sets contains (1,0), (10,λ), or (λ,10). Please verify the definition of C6 or adjust the example.
- [Section 2] The notation in Propositions 1 and 2, where δ(q,a,b)=∅ is glossed as 'ab∈T, i.e., one of a and b is a letter, the other is λ', is confusing. It would be clearer to define the transition relation explicitly on (T×{λ}) ∪ ({λ}×T).
- [General] There are several typographical and notational inconsistencies: 'removed form the set' should be 'removed from the set'; the abstract has 'abbr eviated'; and Algorithm 1 uses Σ for the input alphabet while the surrounding text uses T.
Circularity Check
No circularity: the BC characterization is a construction-based iff theorem; self-citations are background only.
full rationale
The main claim (Theorem 1) is a two-direction construction: Algorithm 1 builds a complete pseudo-BC from a complete deterministic linear automaton, and the converse builds a deterministic linear automaton from a complete, finite-index, crossing-free BC. There is no fitted parameter being renamed as a prediction, and no defining quantity is exported as a derived result. The equivalence classes of presus are defined from the language L, exactly as in the classical Myhill-Nerode theorem, so using L in the definition of the BC is the intended characterization mechanism, not circularity. The paper's heavy self-citation (e.g., [19], [29]) is confined to background facts about 2detLIN, k-rated linear languages, and Watson-Crick automata; these facts are not premises of the main iff proof. The admitted omission of some proofs, including Claim 2 that Algorithm 1 produces no crossing pairs, is a completeness/correctness limitation rather than a circular step: the claim is a combinatorial property of the constructed pseudo-BC and is not assumed as the theorem's conclusion. The skeptical observation about the reverse direction's transition rule being possibly non-deterministic for different presus in the same class is a correctness objection, not a self-referential reduction; even if the constructive proof is flawed, the alleged flaw does not make the theorem's statement equivalent to its inputs. Accordingly, no circular step can be exhibited with a quote-and-reduction, and the appropriate finding is no significant circularity.
Assumptions & free parameters
assumptions (4)
- domain assumption The class 2detLIN is exactly the class accepted by 1-limited deterministic linear automata, and these are equivalent to deterministic sensing 5' to 3' Watson-Crick finite automata.
- domain assumption Every deterministic linear automaton can be made complete (total transition function) by adding a sink state without changing the accepted language.
- standard math The classical Myhill-Nerode theorem for regular languages.
- domain assumption All states of an automaton can be assumed reachable without affecting the language.
Cite this review
Pith. "Pith review of A Myhill-Nerode Type Characterization of 2detLIN Languages." pith.science (2026). https://pith.science/paper/RA77JOVB
@misc{pith2026250715316,
author = {Pith},
title = {Pith review of: A Myhill-Nerode Type Characterization of 2detLIN Languages},
year = {2026},
howpublished = {\url{https://pith.science/paper/RA77JOVB}},
note = {Machine review of arXiv:2507.15316}
}
read the original abstract
Linear automata are automata with two reading heads starting from the two extremes of the input, are equivalent to 5' -> 3' Watson-Crick (WK) finite automata. The heads read the input in opposite directions and the computation finishes when the heads meet. These automata accept the class LIN of linear languages. The deterministic counterpart of these models, on the one hand, is less expressive, as only a proper subset of LIN, the class 2detLIN is accepted; and on the other hand, they are also equivalent in the sense of the class of the accepted languages. Now, based on these automata models, we characterize the class of 2detLIN languages with a Myhill-Nerode type of equivalence classes. However, as these automata may do the computation of both the prefix and the suffix of the input, we use prefix-suffix pairs in our classes. Additionally, it is proven that finitely many classes in the characterization match with the 2detLIN languages, but we have some constraints on the used prefix-suffix pairs, i.e., the characterization should have the property to be complete and it must not have any crossing pairs.
Reference graph
Works this paper leans on
-
[1]
V . Amar & Gianfranco R. Putzolu (1964): On a Family of Linear Grammars. Inf. Control. 7(3), pp. 283–291, doi:10.1016/S0019-9958(64)90294-3
-
[2]
V . Amar & Gianfranco R. Putzolu (1965): Generalizations of Regular Events . Inf. Control. 8(1), pp. 56–63, doi:10.1016/S0019-9958(65)90275-5
-
[3]
¨Omer Egecioglu, L´ aszl´ o Heged¨ us & Benedek Nagy (2010):Stateless multicounter 5 ′ → 3′ W atson-Crick automata. In: Fifth International Conference on Bio-Inspired Computing : Theories and Applications, BIC- TA 2010, University of Hunan, Liverpool Hope University, Li verpool, United Kingdom / Changsha, China, September 8-10 and September 23-26, 2010 , ...
-
[4]
¨Omer Egecioglu, L´ aszl´ o Heged¨ us & Benedek Nagy (2011): Hierarchies of Stateless Multicounter 5′ → 3′ Watson-Crick Automata Languages . Fundam. Informaticae 110(1-4), pp. 111–123, doi: 10.3233/ FI-2011-531
work page 2011
-
[5]
Rudolf Freund, Gheorghe P˘ aun, Grzegorz Rozenberg & Arto Salomaa (1997): W atson-Crick finite automata. In Harvey Rubin & David Harlan Wood, editors: DNA Based Computers, Proceedings of a DIMACS Work- shop, Philadelphia, Pennsylvania, USA, June 23-25, 1997 , DIMACS Series in Discrete Mathematics and Theoretical Computer Science 48, DIMACS/AMS, pp. 297–327...
-
[6]
Y uan Gao, Kai Salomaa & Sheng Y u (2010): Transition Complexity of Incomplete DF As. In Ian McQuillan & Giovanni Pighizzini, editors: Proceedings Twelfth Annual Workshop on Descriptional Comp lexity of Formal Systems, DCFS 2010, Saskatoon, Canada, 8-10th Augus t 2010 , EPTCS 31, pp. 99–109, doi: 10. 4204/EPTCS.31.12
work page 2010
-
[7]
L´ aszl´ o Heged¨ us, Benedek Nagy &¨Omer Egecioglu (2012): Stateless multicounter 5′ → 3′ Watson-Crick automata: the deterministic case . Nat. Comput. 11(3), pp. 361–368, doi: 10.1007/S11047-011-9290-9
-
[8]
John E. Hopcroft & Jeffrey D. Ullman (1979): Introduction to Automata Theory, Languages and Computa- tion. Addison Wesley. Available at https://api.semanticscholar.org/CorpusID:31901407
work page 1979
Show all 39 references
-
[9]
Acta Univ
G´ eza Horv´ ath & Benedek Nagy (2010): Pumping lemmas for linear and nonlinear context-free languages . Acta Univ. Sapientiae Informatica 2(2), pp. 194–209, doi: 10. 48550/arXiv.1012.0023. Available at https://acta.sapientia.ro/en/series/ informatica/publications/informatica-...
-
[10]
Ondrej Kl´ ıma & Libor Pol´ ak (2011):On Biautomata . In Rudolf Freund, Markus Holzer, Carlo Mereghetti, Friedrich Otto & Beatrice Palano, editors: Third Workshop on Non-Classical Models for Automata and Applications - NCMA 2011, Milan, Italy, July 18 - July 19, 201 1. Proceed...
2011
-
[11]
Acta Informatica 59(5), pp
Radim Kocman, Zbynek Krivka, Alexander Meduna & Benede k Nagy (2022): A jumping 5′ → 3′ Watson- Crick finite automata model . Acta Informatica 59(5), pp. 557–584, doi: 10.1007/S00236-021-00413-X
2022 doi
-
[12]
Peter Leupold & Benedek Nagy (2009): 5’ → 3’ W atson-Crick Automata with Several Runs. In Henning Bor- dihn, Rudolf Freund, Markus Holzer, Martin Kutrib & Friedri ch Otto, editors: Workshop on Non-Classical Models for Automata and Applications - NCMA 2009, Wroclaw, P oland, Au...
2009
-
[13]
Peter Leupold & Benedek Nagy (2010): 5 ′ → 3′ Watson-Crick Automata With Several Runs . Fundam. Informaticae 104(1-2), pp. 71–91, doi: 10.3233/FI-2010-336
2010 doi
-
[14]
In Cliff B
Roussanka Loukanova (2007): Linear Context Free Languages . In Cliff B. Jones, Zhiming Liu & Jim Woodcock, editors: Theoretical Aspects of Computing - ICTAC 2007, 4th Internat ional Colloquium, Macau, China, September 26-28, 2007, Proceedings , Lecture Notes in Computer Scienc...
2007 doi
-
[15]
Myhill (1957): Finite automata and the representation of events
J. Myhill (1957): Finite automata and the representation of events . W ADDTR-57-624, pp. 112–137. Benedek Nagy 87
1957
-
[16]
In Max H
Benedek Nagy (2008): On 5′ → 3′ Sensing W atson-Crick Finite Automata. In Max H. Garzon & Hao Y an, editors: DNA Computing, 13th International Meeting on DNA Computing , DNA13, Memphis, TN, USA, June 4-8, 2007, Revised Selected Papers , Lecture Notes in Computer Science 4848, ...
2008 doi
-
[17]
In: Mathematical Theory and Computational Practice, CiE 2009, Abstract Book let, Heidelberg, Germany, pp
Benedek Nagy (2009): On a hierarchy of 5′ → 3′ sensing WK finite automata languages . In: Mathematical Theory and Computational Practice, CiE 2009, Abstract Book let, Heidelberg, Germany, pp. 266–275
2009
-
[18]
Triangle 8, pp
Benedek Nagy (2012): A class of 2-head finite automata for linear languages . Triangle 8, pp. 89–99
2012
-
[19]
Journal of Logic and Computation 23(4), pp
Benedek Nagy (2013): On a hierarchy of 5′ → 3′ sensing Watson–Crick finite automata languages . Journal of Logic and Computation 23(4), pp. 855–872, doi: 10.1093/logcom/exr049. arXiv:https://academic. oup.com/logcom/article-pdf/23/4/855/2775832/exr049.pdf
2013 doi
-
[20]
Benedek Nagy (2019): Union-Freeness, Deterministic Union-Freeness and Union- Complexity. In Michal Hospod´ ar, Galina Jir´ askov´ a & Stavros Konstantinidis, editors: Descriptional Complexity of Formal Systems - 21st IFIP WG 1.02 International Conference, DCFS 2019, Koˇsice, S...
2019 doi
-
[21]
Benedek Nagy (2020): 5 ′ → 3′ Watson-Crick pushdown automata. Inf. Sci. 537, pp. 452–466, doi: 10.1016/ J.INS.2020.06.031
2020
-
[22]
Benedek Nagy (2021): State-deterministic 5′ → 3′ Watson-Crick automata . Nat. Comput. 20(4), pp. 725– 737, doi:10.1007/S11047-021-09865-Z
2021 doi
-
[23]
Benedek Nagy (2022): Operational union-complexity . Inf. Comput. 284, p. 104692, doi: 10.1016/J.IC. 2021.104692
2022
-
[24]
Benedek Nagy (2022): Quasi-deterministic 5′ → 3′ Watson-Crick Automata . In Henning Bordihn, G´ eza Horv´ ath & Gy¨ orgy V aszil, editors:Proceedings 12th International Workshop on Non-Classical Models of Automata and Applications, NCMA 2022, Debrecen, Hungary, A ugust 26-27, ...
2022 doi
-
[25]
Annales Mathematicae et Informaticae 58, pp
Benedek Nagy (2023): On language classes accepted by stateless 5′ → 3′ Watson-Crick finite automata . Annales Mathematicae et Informaticae 58, pp. 110–120, doi: 10.33039/ami.2023.08.004
2023 doi
-
[26]
Benedek Nagy (2024): 5 ′ → 3′ Watson-Crick Automata accepting Necklaces . In Florin Manea & Giovanni Pighizzini, editors: Proceedings 14th International Workshop on Non-Classical Models of Automata and Applications (NCMA 2024), NCMA 2024, G¨ ottingen, Germany,12-13 August 2024...
2024 doi
-
[27]
RAIRO Theor
Benedek Nagy & Zita Kov´ acs (2021): On deterministic 1-limited 5′ → 3′ sensing W atson-Crick finite-state transducers. RAIRO Theor. Informatics Appl. 55, pp. 1–18, doi: 10.1051/ITA/2021007
2021
-
[28]
RAIRO Theor
Benedek Nagy & Friedrich Otto (2020): Linear automata with translucent letters and linear contex t-free trace languages. RAIRO Theor. Informatics Appl. 54, p. 3, doi: 10.1051/ITA/2020002
2020
-
[29]
Acta Inf
Benedek Nagy & Shaghayegh Parchami (2021): On deterministic sensing 5′ → 3′ W atson–Crick finite au- tomata: a full hierarchy in 2detLIN . Acta Inf. 58(3), p. 153–175, doi: 10.1007/s00236-019-00362-6
2021 doi
-
[30]
Benedek Nagy & Shaghayegh Parchami (2022): 5 ′ → 3′ Watson-Crick automata languages-without sensing parameter. Nat. Comput. 21(4), pp. 679–691, doi: 10.1007/S11047-021-09869-9
2022 doi
-
[31]
Benedek Nagy, Shaghayegh Parchami & Hamid Mir Mohammad Sadeghi (2017): A New Sensing 5′ → 3′ W atson-Crick Automata Concept. In Erzs´ ebet Csuhaj-V arj´ u, P´ al D¨ om¨ osi & Gy¨ orgy V aszil, editors: Proceed- ings 15th International Conference on Automata and Formal L anguag...
2017 doi
-
[32]
Benedek Nagy & Walaa Y asin (2025): On some Classes of Reversible 2-head Automata. In Nelma Moreira & Luca Prigioniero, editors: Proceedings 15th International Workshop on Non-Classical Models of Automata and Applications (NCMA 2025), NCMA 2025, Loughborough, UK, 21-22 July 20...
2025 doi
-
[33]
Nerode (1958): Linear automaton transformations
A. Nerode (1958): Linear automaton transformations . Proc. Amer. Math. Soc. 9, pp. 541–544, doi: 10. 1090/S0002-9939-1958-0135681-9
1958
-
[34]
Shaghayegh Parchami & Benedek Nagy (2018): Deterministic Sensing 5′ → 3′ Watson-Crick Automata Without Sensing Parameter . In Susan Stepney & Sergey V erlan, editors: Unconventional Computation and Natural Computation - 17th International Conference, U CNC 2018, Fontainebleau,...
2018
-
[35]
Texts in Theoretical Computer Science
Gheorghe P˘ aun, Grzegorz Rozenberg & Arto Salomaa (199 8): DNA Computing - New Computing Paradigms. Texts in Theoretical Computer Science. An EA TCS Series, Springer, Heidelberg, doi:10.1007/ 978-3-662-03563-4
-
[36]
Springer, doi: 10.1007/ 978-3-642-59126-6
Grzegorz Rozenberg & Arto Salomaa (1997): Handbook of F ormal Languages . Springer, doi: 10.1007/ 978-3-642-59126-6
1997
-
[37]
Kai Salomaa (2007): Descriptional Complexity of Nondeterministic Finite Auto mata. In Tero Harju, Juhani Karhum¨ aki & Arto Lepist¨ o, editors:Developments in Language Theory, 11th International Conference, DLT 2007, Turku, Finland, July 3-6, 2007, Proceedings , Lecture Notes ...
2007 doi
-
[38]
Semenov (1974): Regularity of languages k-linear for various k
A.L. Semenov (1974): Regularity of languages k-linear for various k . Dokl. Akad. Nauk SSSR 215(2), pp. 278–281
1974
-
[39]
Sempere & Pedro Garc´ ıa (1994):A Characterization of Even Linear Languages and its Applica tion to the Learning Problem
Jos´ e M. Sempere & Pedro Garc´ ıa (1994):A Characterization of Even Linear Languages and its Applica tion to the Learning Problem . In Rafael C. Carrasco & Jos´ e Oncina, editors: Grammatical Inference and Appli- cations, Second International Colloquium, ICGI-94, Alica nte, S...
1994 doi
Reviewed August 6, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.