{"id":"097c2133-ad03-405f-9d0f-4520b04e2383","arxiv_id":"2507.15316","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A language is 2detLIN if and only if it has a finite, complete, crossing-free prefix-suffix classification.","lead":"This paper characterizes the formal languages accepted by deterministic two-headed automata that read from both ends, using equivalence classes of prefix-suffix pairs. It generalizes the classical Myhill-Nerode theorem from regular languages to the larger class 2detLIN.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Reverse direction of Theorem 1 uses an ill-defined transition rule: one state/letter pair can be forced to two different next states by different presus in the same BC class.","rationale":"The reader's weakest assumption was the omitted proof of Claim 2 in the forward direction. That is a real gap, but a short argument using Lemma 1 appears to establish Claim 2: for two crossing presus sharing outer prefix u1 and suffix v2, the state after the common outer shell would have to move both heads on the remaining middle, contradicting Proposition 1. So the forward direction is likely repairable. The more serious defect I found is in the reverse direction: the transition rule is not well-defined, because language-equivalent presus in one class can have different 'next head' behavior after the same left step. The explicit unary even-length BC is complete, finite, and crossing-free, yet forces both q_odd and p_odd as destinations for the same δ(q_even,a,λ). This does not disprove the theorem, but it invalidates the constructive proof as written. Since the reader already recommended conditional acceptance, my finding reinforces that recommendation: the condition should include fixing the reverse construction, not just supplying the missing proof of Claim 2. I therefore keep the reader's verdict unchanged.","tokens_in":17215,"tokens_out":37912,"duration_ms":404835,"concrete_test":"Formalize the unary BC defined above and run the transition rule from the reverse proof of Theorem 1 on state q_even and letter a. If the rule yields both q_odd and p_odd, the proof's 'exactly one transition' claim fails. Then test a repair: fix a canonical representative per class, e.g., the shortest presu, and check whether the resulting automaton is deterministic and accepts L for every complete crossing-free BC; if not, the characterization itself needs an additional condition.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reverse direction of Theorem 1 in Section 3 defines δ(q_i,a,λ) existentially: q_j is chosen if some (u,v)∈C_i gives (ua,v)∈C_j and (uaa,v) appears, while p_j is chosen if some (u,v)∈C_i gives (ua,v)∈C_j and (ua,av) appears. The text asserts Claims 3–4 make exactly one choice, but this is false. Let T={a}, L={a^{2n}}. Define a complete BC with classes by parity of total length and one representative per word a^N, using split lengths 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. The suffix length N−s(N) is nondecreasing (0,0,0,0,0,0,1,1,...), so the BC has no crossing pairs; it has finite index 2. In C_even, (λ,λ) and (a^4,λ) are both left-type. For letter a: via (λ,λ), the rule gives δ(q_even,a,λ)=q_odd because (a,λ)∈C_odd and (aa,λ) appears. Via (a^4,λ), the rule gives δ(q_even,a,λ)=p_odd because (a^5,λ)∈C_odd and (a^5,a) appears. The same transition is forced to two states, so the constructed object is not deterministic. Claims 3 and 4 hold in this example; they constrain each presu individually, not the consistency of different presus in one class. The theorem may still be true, since the even-length language is regular and hence in 2detLIN, but the constructive proof of the if-direction is invalid as written and needs a canonical representative or an extra compatibility condition.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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}.","tokens_in":17528,"tokens_out":17678,"duration_ms":187923,"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":[{"comment":"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":"Section 3, Claim 2"},{"comment":"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.","section":"Section 3, reverse direction of Theorem 1"}],"minor_comments":[{"comment":"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":"Example 3"},{"comment":"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).","section":"Section 2"},{"comment":"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.","section":"General"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a workshop-style paper with page-limit omissions, but the version under review is being treated as a journal submission. The most serious issue is the reverse-construction flaw in Theorem 1, which is substantive and requires either a strengthened BC condition or a different construction. The theorem may well be true, and the direction of repair is reasonably clear, so I recommend major revision rather than rejection. The heavy reliance on the author's own prior work is not problematic in itself, but the novelty relative to [19,29,34] should be stated more explicitly in a revised introduction."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the presu equivalence and border classification framework is a real extension of Myhill-Nerode to two-headed automata, and the forward direction (automaton to BC) is plausible, but the reverse construction in Theorem 1 is broken in a way that goes beyond missing proofs. The stress-test example is correct: for the even-length unary language {a^{2n}}, define a complete BC with classes by parity, split lengths s(0)=0, ..., s(5)=5, s(6)=5, and s(N)=N−1 for N≥7. The BC is complete, finite-index (2 classes), and has no crossing pairs. The presus (λ,λ) and (a^4,λ) both lie in the even class. For letter a, the paper's rule gives δ(q_even,a,λ)=q_odd via (λ,λ), because (a,λ)∈C_odd and (aa,λ) appears. It also gives δ(q_even,a,λ)=p_odd via (a^4,λ), because (a^5,λ)∈C_odd and (a^5,a) appears. Same state, same letter, two different next states. Claims 3 and 4 hold in this example—they constrain each presu individually, not the consistency of different presus in one class. So the constructed object is not deterministic, and the proof of the if-direction is invalid as written.  What is genuinely good: the idea of using prefix-suffix pairs and imposing completeness and crossing-freeness is new; no prior Myhill-Nerode characterization for 2detLIN exists. Algorithm 1's construction of a BC from an automaton is coherent and illustrative. The non-membership proof for a^n b^n c^n is a nice application. The paper is honest about omitted proofs, and the self-citations are heavy but do not feed the main result.  Soft spots beyond the reverse construction: Claim 2, which asserts the constructed pseudo-BC has no crossing pairs, is stated without proof. The Introduction admits this, but it is load-bearing for the forward direction. The transition construction is dense and the 'uaa' conditions look corrupted in places. Still, the forward direction reads as plausible.  The theorem may be true—the example language is regular, so it is not a counterexample to the statement—but the proof as written does not establish it. A fix likely requires an extra compatibility condition on BCs ensuring all presus in one class agree on which head moves next, or a canonical representative per class. This is a significant gap, not a typo.  I would send this to a serious referee because the idea is new and probably salvageable, but the referee should focus on the reverse construction and require either a corrected proof or a modified theorem. I would not cite it in its current form. For a reading group, it is a maybe—good for discussing what counts as a load-bearing gap.","headline":"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.","tokens_in":876,"tokens_out":2057,"would_cite":false,"duration_ms":64382,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q70"],"pacs":[],"model":"deepseek-v4-flash","headline":"A language is 2detLIN exactly when its prefix-suffix pairs admit a complete, finite, crossing-free classification.","keywords":["2detLIN","deterministic linear automata","Myhill-Nerode theorem","prefix-suffix pairs","border classification","crossing pairs","Watson-Crick automata","linear languages"],"falsifier":"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.","tokens_in":16950,"feed_emoji":"🧬","tokens_out":11035,"duration_ms":107984,"temperature":0.7,"pith_summary":"The paper offers an if-and-only-if structural characterization of the language class 2detLIN, the languages accepted by deterministic automata with two reading heads that start at the two ends of the input and work toward each other. The characterization parallels the classical Myhill-Nerode theorem for regular languages, but instead of classifying prefixes alone, it classifies prefix-suffix pairs (called presus): two pairs are equivalent when inserting the same middle word into each yields the same membership in the language. A language is in 2detLIN exactly when it admits a complete, finite-index classification of presus with no crossing pairs. If correct, this gives a purely language-theoretic way to recognize 2detLIN languages and to construct accepting two-head automata, and it opens the door to a descriptional complexity measure for this class.","feed_headline":"Finite crossing-free classes characterize 2detLIN","feed_subtitle":"A language is 2detLIN exactly when its prefix-suffix pairs admit a complete, crossing-free, finite classification.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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)."],"supporting_citations":[{"why":"The classical Myhill-Nerode theorem that characterizes regular languages by finitely many prefix equivalence classes, the template this paper adapts.","marker":"[15]"},{"why":"Nerode's companion result, also cited for the Myhill-Nerode characterization, establishing the minimal automaton's state count.","marker":"[33]"},{"why":"Defines linear automata as two-head automata recognizing linear languages, the model class under study.","marker":"[14]"},{"why":"Introduces the terminology and basic results for linear automata with two heads used throughout the paper.","marker":"[28]"},{"why":"Establishes that deterministic sensing 5'->3' Watson-Crick automata accept exactly 2detLIN and that all k-rated linear languages lie in this class, underpinning the paper's examples and the fixed-rated analysis.","marker":"[19]"},{"why":"Shows the full hierarchy of deterministic sensing 5'->3' Watson-Crick automata within 2detLIN, providing the class's structural background.","marker":"[29]"},{"why":"Proves that the 1-limited variant of sensing 5'->3' Watson-Crick automata has the same accepting power, justifying the simplified transition model used throughout.","marker":"[31]"}],"fun_headline_variants":["Myhill-Nerode style finite classes capture 2detLIN","Prefix-suffix equivalence classes pin down 2detLIN","No crossing pairs: finite classes define 2detLIN","Two-head automata get Myhill-Nerode via crossing-free classes","Complete crossing-free finite index exactly 2detLIN"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Myhill-Nerode style finite classes capture 2detLIN","Prefix-suffix equivalence classes pin down 2detLIN","No crossing pairs: finite classes define 2detLIN","Two-head automata get Myhill-Nerode via crossing-free classes","Complete crossing-free finite index exactly 2detLIN"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000482,"raw_usage":{"total_tokens":2399,"prompt_tokens":980,"completion_tokens":1419,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":596,"completion_tokens_details":{"reasoning_tokens":1334}},"tokens_in":596,"tokens_out":1419,"duration_ms":10596,"temperature":1.0,"reasoning_tokens":1334,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T15:37:06.114360+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Myhill (1957): Finite automata and the representation of events","cited_arxiv_id":null,"evidence_quote":"The classical Myhill-Nerode theorem that characterizes regular languages by finitely many prefix equivalence classes, the template this paper adapts."},{"cited_title":"Nerode (1958): Linear automaton transformations","cited_arxiv_id":null,"evidence_quote":"Nerode's companion result, also cited for the Myhill-Nerode characterization, establishing the minimal automaton's state count."},{"cited_title":"In Cliff B","cited_arxiv_id":null,"evidence_quote":"Defines linear automata as two-head automata recognizing linear languages, the model class under study."},{"cited_title":"RAIRO Theor","cited_arxiv_id":null,"evidence_quote":"Introduces the terminology and basic results for linear automata with two heads used throughout the paper."},{"cited_title":"Journal of Logic and Computation 23(4), pp","cited_arxiv_id":null,"evidence_quote":"Establishes that deterministic sensing 5'->3' Watson-Crick automata accept exactly 2detLIN and that all k-rated linear languages lie in this class, underpinning the paper's examples and the fixed-rated analysis."}],"review_version":1}