{"id":"bb186da8-6fd4-4297-9387-fac245bfd6ac","arxiv_id":"1908.04038","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Regular separability and intersection emptiness are independent decision problems: each can be decidable while the other is undecidable, on natural language classes.","lead":"A theory result shows that two basic decision problems about formal languages, checking whether two systems share an execution and checking whether they have a regular certificate of separation, are logically independent. The authors build machine models in which one problem is decidable while the other is undecidable, answering a question raised by a recent pattern of results.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Decidability half of Theorem 4.1 rests on Lemma 4.8, whose Appendix B existential step is circular as printed and omits the padding-elimination transduction; the proof needs repair, though the intended argument is likely sound.","rationale":"The reader identified Appendix B's existential induction as the most fragile part, and I agree that this is the load-bearing point for the first independence direction. However, I view the issue as more than a harmless typo: the existential step as written is circular and omits a necessary padding-elimination transduction. The intended repair is standard and likely correct, so I would not reject the paper, but the manuscript should be corrected before acceptance. The rest of the paper checks out: Lemma 4.5 is correct once 2S is read as {2^n | n in S}, Lemma 4.6 then gives the undecidability reduction, and Section 5's HOPA constructions and reductions are plausible. Thus the appropriate verdict is conditional acceptance pending a clean rewrite of Appendix B's existential case.","tokens_in":17203,"tokens_out":47797,"duration_ms":500123,"concrete_test":"Rewrite the existential step of Appendix B: given a reset VASS for LR' with R' subset N^{1+k}, construct a reset VASS for LR, where R is the projection onto the last k coordinates. Explicitly define the homomorphism that erases the y-track and the rational transduction that deletes the trailing all-padding suffix; compose them and verify the result is exactly LR, then apply Lemma 4.3. As a sanity check, apply the construction to phi(x)=exists y (y+y=x); the resulting reset VASS should accept exactly the reversed binary representations of even numbers (with leading zeros allowed). If this example cannot be handled, Lemma 4.8 and hence the decidability half of Theorem 4.1 are unproven.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The decidability side of Theorem 4.1 depends on Lemma 4.8, which claims every formula of Sigma+_1(N,+,<=,1,pseudoR) defines a pseudo-R relation with an effectively computable reset VASS. The proof is deferred to Appendix B. In the existential case, for phi(x)=exists y phi'(y,x), the text says: 'By induction hypothesis LR in R and since LR' is a homomorphic image of LR, Lemma 4.3 it tells us that LR' belongs effectively to R.' This is circular: the valid induction hypothesis is LR' in R, and LR is a projected image of LR', not the other way around. As printed, the step does not establish that LR is in R. Moreover, even after correcting the direction, projection is not literally a homomorphism of the convolution language: if the eliminated variable y is longer than all remaining coordinates, erasing the y-track leaves a suffix of all-padding columns that is not part of the standard convolution for the projected tuple. One must compose the erasing homomorphism with a rational transduction that deletes trailing all-padding columns, and then invoke closure under rational transductions (Lemma 4.3). This missing step is essential because the relation is pseudo-R only if its exact convolution language LR belongs to R. Since Lemma 4.10 reduces IE(I(pseudoR),I(pseudoR)) to truth in this logic, the decidable-intersection half of Theorem 4.1 rests on this repair. The rest of the paper, including Lemma 4.5 and Section 5, appears sound.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper constructs two pairs of language classes showing that regular separability and intersection emptiness are independent decision problems. In Section 4, the class I(pseudoR), based on incrementing automata with reset-VASS predicates, is shown to have undecidable regular separability but decidable intersection emptiness (Theorem 4.1). In Section 5, the pair (H, I(powerH)) is shown to have decidable regular separability but undecidable intersection emptiness (Theorem 5.2). The proofs combine reductions from the infinity problem for reset VASS, a decidability argument for a positive existential logic over pseudo-R predicates, and a separation characterization for unary languages.","tokens_in":17586,"tokens_out":14780,"duration_ms":138809,"significance":"If the proof gap in Lemma 4.8 is repaired, the result is significant: it refutes the emerging intuition that regular separability and intersection emptiness are equivalent under mild closure assumptions. The constructions are natural, the paper gives explicit reductions and full appendix proofs, and it builds on independent external results (reset VASS boundedness undecidability, higher-order pushdown infinity decidability, context-free intersection undecidability). The main contribution is a family of counterexamples rather than a new algorithmic technique, but the counterexamples are well chosen and the high-level explanation in the conclusion is valuable.","major_comments":[{"comment":"The existential step in the induction is not established as written. The text reads: 'By induction hypothesis LR in R and since LR′ is a homomorphic image of LR, Lemma 4.3 it tells us that LR′ belongs effectively to R.' This applies the induction hypothesis to LR, which is precisely the statement to be proved; the available induction hypothesis is LR′ ∈ R. Moreover, even after correcting the direction, the erasing homomorphism from LR′ to LR is not literally well defined: if the eliminated variable y has a longer binary representation than all remaining variables, erasing the y-track leaves a suffix of all-padding columns that is not part of the standard convolution of the projected tuple. The proof must first apply the erasing homomorphism and then compose with a rational transduction that deletes trailing all-padding columns, and only then invoke closure under rational transductions (Lemma 4.3). Because Lemma 4.8 underpins the decidability half of Theorem 4.1 via Lemma 4.10, this gap is load-bearing and must be repaired.","section":"Appendix B (Lemma 4.8), existential case"}],"minor_comments":[{"comment":"The sentence 'By Lemma 4.4, K1 and K2 are regularly separable if and only if K1 is finite and disjoint from K2' should cite Lemma 4.5, which is the unary separability characterization; Lemma 4.4 states undecidability of the infinity problem for reset VASS.","section":"Lemma 4.6, proof"},{"comment":"The displayed formula defines φ2(y) via ∃x φ_T(x,y) ∧ S2(x), which describes membership in T aS2, but the preceding reduction concerns T aS1 ∩ aS2. Since intersection is symmetric, the resulting formula is correct (up to renaming of variables), but the text should state the direction explicitly and replace the apparent typo 'T aS2\\aS1≠∅' with 'T aS2 ∩ aS1 ≠ ∅'.","section":"Lemma 4.10, final paragraph"},{"comment":"The phrase 'the language {a^x | 2^ℓ < x < 2^{ℓ+1}}⊆S1' is imprecise: the whole interval is not contained in S1 in general. Since 2N denotes the powers of two, the intended statement is that every x in that interval that is not a power of two belongs to S1, which is sufficient for the argument. Please rephrase to avoid ambiguity.","section":"Lemma 4.5, proof"},{"comment":"There is a typo in 'the lanuage TL is accepted': it should be 'language'.","section":"Lemma 3.2, proof"}],"recommendation":"major_revision","confidential_remarks":"The Appendix B gap is the only serious obstacle I see; the intended argument is standard and likely repairable. The main claims are probably correct, and the paper's narrative is clear. I would support acceptance after the proof is fixed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper's main claim holds up: regular separability and intersection emptiness are not mutually reducible in general. The authors construct two new language classes, I(pseudoR) and I(powerH), and prove in Theorems 4.1 and 5.2 that one problem can be decidable while the other is undecidable. This directly refutes the correspondence that the recent literature had observed, and the classes are natural enough that the result feels like a genuine counterexample, not a contrivance.\n\nWhat I like: the high-level arguments are clean and the building blocks (reset VASS, higher-order pushdown automata, rational transductions) are used cleverly. Lemma 4.5, the unary separator characterization, is simple and elegant. The reductions in Section 5 are also well done, and the paper is for the most part clearly written.\n\nThe soft spot is Appendix B, the proof of Lemma 4.8, which is the load-bearing decidability half of Theorem 4.1. As printed, the existential case is wrong. It says 'By induction hypothesis LR in R and since LR' is a homomorphic image of LR…', which reverses the actual direction: the induction hypothesis should give LR' in R, and LR is a projected image of LR'. Worse, the projection is not literally a homomorphism of the convolution language: erasing the eliminated coordinate leaves a suffix of all-padding columns if that word was strictly longest, and those columns must be removed by a rational transduction before closure under homomorphisms applies. The omission of this padding-elimination step is essential, because the definition of pseudo-R relation requires the exact convolution language. Lemma 4.10 then inherits the gap, so the decidability side of Theorem 4.1 depends on this fix.\n\nThat said, the intended argument is obvious and the repair is routine—compose the erasing homomorphism with a transducer that strips trailing padding columns, then invoke Lemma 4.3. I am fairly confident the result is true. There are also minor cross-reference errors (Lemma 4.6 cites Lemma 4.4 instead of 4.5) that should be caught by a careful referee.\n\nThe paper deserves a serious referee and likely acceptance after the appendix is fixed. I would cite it if I worked in this area, and I'd bring it to the reading group. The citation practice looks fine—the self-citations to [14] and [20] are appropriate.\n\nRecommendation: send to peer review; the main theorems are novel and significant, and the flaw is in the writing, not the underlying idea.","headline":"A genuinely new independence result with a broken but repairable appendix proof.","tokens_in":18070,"tokens_out":3631,"would_cite":true,"duration_ms":36301,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","03D05","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"Regular separability and intersection emptiness are independent problems: each can be decidable while the other is undecidable.","keywords":["regular separability","intersection emptiness","decidability","incrementing automata","reset vector addition systems","higher-order pushdown automata","pseudo-R predicates","power-H predicates"],"falsifier":"A reader could test the appendix's critical step by taking a pseudo-$R$ predicate $S$ and applying the proof to the formula $\\exists y\\,(S(y)\\land x=y)$: if the projection relation cannot be realized by a reset VASS—or the construction provably fails—then Lemma 4.8 collapses and with it the decidability of $IE(I(\\mathrm{pseudo}R),I(\\mathrm{pseudo}R))$.","tokens_in":17042,"feed_emoji":"🔀","tokens_out":16801,"duration_ms":150760,"temperature":0.7,"pith_summary":"This paper confronts the question whether regular separability—deciding if a regular language can sit between one input language and another—is just intersection emptiness in disguise. Earlier results on every language class where the question was settled showed the two problems decidable or undecidable together, suggesting a possible reduction. The paper refutes that suggestion by constructing two families of language classes: for incrementing automata whose final-counter predicates come from reset vector addition systems, intersection emptiness is decidable while regular separability is undecidable; for higher-order pushdown languages against incrementing automata with power predicates built from the same class, regular separability is decidable while intersection emptiness is undecidable. A fair reader should take away that the two problems are genuinely different and that no simple transfer from one to the other can exist under mild closure assumptions.","feed_headline":"Separability and intersection emptiness are independent problems","feed_subtitle":"Concrete automata classes show each problem decidable while the other is not, in both directions.","key_machinery":"The arguments run on three machines and one arithmetic logic. Reset vector addition systems (reset VASS) supply the first counterexample: their languages are closed under rational transductions, intersection, and union, emptiness is decidable, but infinity is undecidable. The class $I(\\mathrm{pseudo}R)$ wraps them as predicates: an incrementing automaton reads a word while a counter only increases, and acceptance requires the final counter value to lie in a set $\\nu(L)$ for some reset-VASS language $L$. For these classes, Lemma 4.5 is the load-bearing criterion: for unary languages $a^{S_0}, a^{S_1}$ with $\\mathbb{N}\\setminus 2\\mathbb{N}\\subseteq S_1$, regular separability holds exactly when $S_0$ is finite and disjoint from $S_1$, which turns separability into finiteness. Undecidability of infinity for reset VASS then makes $RS(I(\\mathrm{pseudo}R),I(\\mathrm{pseudo}R))$ undecidable, while a decision procedure for the positive existential arithmetic fragment $\\Sigma^+_1(\\mathbb{N},+,\\le,1,\\mathrm{pseudo}R)$—proved by showing every definable relation is effectively a pseudo-$R$ relation—makes intersection emptiness decidable. In the other direction, higher-order pushdown automata have decidable infinity but undecidable intersection, and Lemma 5.4 shows they can convert binary encodings into unary ones; together with Lemma 5.7 (regular separability is preserved by applying an inverse rational transduction) this yields decidable $RS(H,I(\\mathrm{power}H))$ and undecidable $IE(H,I(\\mathrm{power}H))$.","core_discovery":"The paper's central claim is that regular separability and intersection emptiness are independent decision problems, in the strong sense that neither can be reduced to the other. Concretely, Theorem 4.1 states that $RS(I(\\mathrm{pseudo}R),I(\\mathrm{pseudo}R))$ is undecidable while $IE(I(\\mathrm{pseudo}R),I(\\mathrm{pseudo}R))$ is decidable, where $I(\\mathrm{pseudo}R)$ is the class of languages accepted by incrementing automata whose acceptance predicates are binary encodings $\\nu(L)$ of reset-VASS languages. Theorem 5.2 states the reverse imbalance: $RS(H,I(\\mathrm{power}H))$ is decidable while $IE(H,I(\\mathrm{power}H))$ is undecidable, where $H$ is the class of all higher-order pushdown languages and $\\mathrm{power}H$ stands for predicates of the form $\\mathbb{N}\\setminus 2\\mathbb{N}\\cup\\{2^{\\nu(w)}\\mid w\\in L\\}$ with $L\\in H$. If these theorems are right, the previously observed decidability correspondence between the two problems was an accident of the particular classes studied, not a general law.","pith_inferences":["The same 'distort by encoding into numbers' recipe could be tried on other pairs of classes: take a class with decidable intersection but undecidable infinity and pass to $I(\\mathrm{pseudo}C)$; the paper's reset-VASS instance suggests the dichotomy may reappear, for example with lossy channel systems, which the paper notes could replace reset VASS.","For the reverse direction, the construction is asymmetric and uses power predicates, which the paper itself calls contrived; a natural next target is a single symmetric class $\\mathcal{C}$ with $RS(\\mathcal{C},\\mathcal{C})$ decidable and $IE(\\mathcal{C},\\mathcal{C})$ undecidable, or the mirror image.","Because Lemma 4.5 reduces regular separability to finiteness of a unary language, the hard core of regular separability undecidability may be infinity rather than disjointness; if so, classes with decidable infinity may admit decidable regular separability even when intersection is hard.","A testable extension would be to replace regular separators with other separator classes, such as piecewise testable or context-free languages, in the two constructions; the proofs lean on special properties of regular separators, so the independence result need not transfer."],"forward_implications":["In the class $I(\\mathrm{pseudo}R)$, one can decide whether two languages intersect, yet cannot decide whether a regular certificate separates them; safety verification is therefore strictly easier than regular-certificate synthesis there.","In the pair $(H,I(\\mathrm{power}H))$, one can always decide regular separability, so the obstruction to undecidability is not the existence of a separator but the intersection itself.","No general reduction between the two problems can exist merely because the language classes are full trios with decidable emptiness, since both counterexample families have those properties.","The paper's conclusion that the two problems are fundamentally different implies that any combinatorial characterization of regular separability must be incomparable with intersection emptiness.","The reduction from intersection emptiness to infinite intersection noted in the paper means the infinite-intersection problem is also not a common characterization of regular separability."],"supporting_citations":[{"why":"It supplies the equivalence between closure under rational transductions and closure under homomorphic image, inverse homomorphic image, and intersection with regular languages, which is used to show the constructed classes are full trios.","marker":"[3]"},{"why":"It supplies the decision procedure template for automatic structures that Lemma 4.8 adapts to decide the positive existential arithmetic theory with pseudo-reset-VASS predicates.","marker":"[4]"},{"why":"It supplies the automata recognizing the atomic relations $x+y=z$ and $x=1$ inside the induction proving Lemma 4.8.","marker":"[5]"},{"why":"It provides Lemma 5.7, the fact that regular separability is preserved under inverse rational transductions, which reduces the decidable side of the second counterexample to the unary case.","marker":"[14]"},{"why":"It proves undecidability of boundedness for reset nets, from which Lemma 4.4 derives undecidability of the infinity problem for reset VASS, driving the undecidability of regular separability in the first counterexample.","marker":"[15]"},{"why":"It proves that infinity and unboundedness are decidable for higher-order pushdown languages, which is the key ingredient for decidability of $RS(H,I(\\mathrm{power}H))$.","marker":"[20]"},{"why":"It supplies undecidability of intersection emptiness for context-free languages, which is reduced to $IE(H,I(\\mathrm{power}H))$ to obtain the undecidable side of the second counterexample.","marker":"[21]"},{"why":"It supplies Parikh's theorem, which makes rational transductions over unary languages expressible in the decidable arithmetic fragment used for intersection emptiness in the first counterexample.","marker":"[25]"}],"fun_headline_variants":["No reduction between separability and emptiness","Regular separability and emptiness are independent","Counterexample: one decidable, other not, both ways","Separability vs emptiness: none reduces to other","Independent: regular separability and emptiness"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The decidability of intersection in the first counterexample rests on a formal induction claiming that every positive existential question about the natural numbers with predicates defined by reset vector addition systems can be answered by building another reset system; the appendix's crucial existential step swaps the two relations involved, so that induction is the load-bearing point that must be checked.","fun_headline_variants_meta":{"raw":{"variants":["No reduction between separability and emptiness","Regular separability and emptiness are independent","Counterexample: one decidable, other not, both ways","Separability vs emptiness: none reduces to other","Independent: regular separability and emptiness"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000304,"raw_usage":{"total_tokens":1787,"prompt_tokens":1024,"completion_tokens":763,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":640,"completion_tokens_details":{"reasoning_tokens":695}},"tokens_in":640,"tokens_out":763,"duration_ms":8453,"temperature":1.0,"reasoning_tokens":695,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:55:06.377442+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A reader could test the appendix's critical step by taking a pseudo-$R$ predicate $S$ and applying the proof to the formula $\\exists y\\,(S(y)\\land x=y)$: if the projection relation cannot be realized by a reset VASS—or the construction provably fails—then Lemma 4.8 collapses and with it the decidability of $IE(I(\\mathrm{pseudo}R),I(\\mathrm{pseudo}R))$.","supporting_citations":[{"cited_title":"Transductions and context-free languages","cited_arxiv_id":null,"evidence_quote":"It supplies the equivalence between closure under rational transductions and closure under homomorphic image, inverse homomorphic image, and intersection with regular languages, which is used to show the constructed classes are full trios."},{"cited_title":"Automatic structures","cited_arxiv_id":null,"evidence_quote":"It supplies the decision procedure template for automatic structures that Lemma 4.8 adapts to decide the positive existential arithmetic theory with pseudo-reset-VASS predicates."},{"cited_title":"Finite presentations of infinite structures: Automata and interpretations","cited_arxiv_id":null,"evidence_quote":"It supplies the automata recognizing the atomic relations $x+y=z$ and $x=1$ inside the induction proving Lemma 4.8."},{"cited_title":"An approach to regular separability in vector addition systems","cited_arxiv_id":null,"evidence_quote":"It provides Lemma 5.7, the fact that regular separability is preserved under inverse rational transductions, which reduces the decidable side of the second counterexample to the unary case."},{"cited_title":"Reset nets between decidability and undecidability","cited_arxiv_id":null,"evidence_quote":"It proves undecidability of boundedness for reset nets, from which Lemma 4.4 derives undecidability of the infinity problem for reset VASS, driving the undecidability of regular separability in the first counterexample."},{"cited_title":"Luke Ong","cited_arxiv_id":null,"evidence_quote":"It proves that infinity and unboundedness are decidable for higher-order pushdown languages, which is the key ingredient for decidability of $RS(H,I(\\mathrm{power}H))$."},{"cited_title":"Context-free languages and turing machine computations","cited_arxiv_id":null,"evidence_quote":"It supplies undecidability of intersection emptiness for context-free languages, which is reduced to $IE(H,I(\\mathrm{power}H))$ to obtain the undecidable side of the second counterexample."},{"cited_title":"On context-free languages","cited_arxiv_id":null,"evidence_quote":"It supplies Parikh's theorem, which makes rational transductions over unary languages expressible in the decidable arithmetic fragment used for intersection emptiness in the first counterexample."}],"review_version":1}