{"id":"535b41e4-5456-4e24-a133-99a35da09843","arxiv_id":"2601.14114","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A deterministic automaton construction produces partial reductions for Kleene algebra with linear hypotheses, yielding completeness and decidability on every expression where it terminates.","lead":"Program equivalence often needs extra facts about specific programs, which plain Kleene algebra cannot use. This paper presents an automaton-based method that turns such facts—of a restricted shape—into a partial reduction, automatically proving more equivalences whenever the construction stops.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Induction in Lemma 3.15 is not justified: the extension from a plain solution yields only an H-solution, so it cannot be re-applied to the next automaton in the chain T0^i(X).","rationale":"I read the paper as attempting to construct partial reductions for KA with a single linear hypothesis e≤w, and the central claim is Theorem 4.10/Corollary 4.11: whenever the iterated automaton construction TH* terminates, rH is a partial reduction, yielding completeness and decidability over its domain. For this claim, the load-bearing condition is that the reduction inequality rH(g) ≤H g holds. The proof of this inequality rests on extending a solution of the original automaton to an H-solution of the patched automaton (Lemma 3.15/4.9). The reader's concern is exactly right: the proof of Lemma 3.15 constructs the extension for one application of T0 but does not supply the plain solution needed for the next iteration. I considered whether this is merely a presentational gap or a substantive one. It is substantive in the written proof: without a generalized statement, the induction is a non sequitur. However, the fix appears straightforward, so I would not call the central result false. No other issue I found is more load-bearing: the one-step language inclusion (Lemma 3.12/4.6), the saturation lemma (4.8), and the use of least H-solutions (Lemma 3.14) are plausible and supported by the appendix. The paper honestly acknowledges termination is not characterized (Section 5, Example 4.12), which is a limitation, not a flaw. Thus the correct verdict remains CONDITIONAL, as the reader concluded.","tokens_in":19396,"tokens_out":13558,"duration_ms":118254,"concrete_test":"Check whether Lemma 3.15 (and its TH analogue, Lemma 4.9) can be restated with 's is an H-solution to X' in the hypothesis. Verify that the proof in Appendix B goes through with '≤H' in place of '≤' wherever the solution property is used; in particular, the final derivation of w·s(x') ≤ s(x_i) becomes w·s(x') ≤H s(x_i). If this generalized lemma holds, the induction over the finite chain is legitimate and the two reduction theorems are recovered. If it fails, construct a finite automaton and hypothesis where one-step extension from an H-solution of X does not produce an H-solution of T0(X); such a counterexample would undermine Theorem 3.16.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Appendix B, Lemma 3.15 proves that a solution s of X can be extended to an H-solution s* of T0(X). The proof then says the result follows by induction over the finite chain X ⊑ T0(X) ⊑ ... ⊑ T0^n(X). This induction is not valid as written: after one step, s* is only an H-solution to T0(X), not a plain solution, while the lemma's hypothesis requires a plain solution to the current automaton. To apply the lemma again at T0(X) one would need a plain solution to T0(X), which is not supplied. The same issue transfers verbatim to Lemma 4.9 for the saturated construction TH, and therefore to Theorem 4.10 and Corollary 4.11, the central conditional completeness/decidability result. Without a repaired iteration, the inequality r0(g) ≤H g (and rH(g) ≤H g) is not established. The gap appears repairable — the proof step 'w·s(x') ≤ s(x_i)' can likely be weakened to '≤H' if the lemma is generalized to H-solutions — but as written the proof is incomplete.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper develops an automaton-based method to construct partial reductions for Kleene algebra with a linear hypothesis e≤w. Given an expression g, one builds a finite automaton, repeatedly patches it (T0) or patches with a w-saturated automaton for e (TH), and if the chain stabilizes finitely, reads off a regular expression r(g). The authors prove that JgK_H ⊆ Jr(g)K and r(g) ≤H g, and use the standard reduction argument to obtain completeness and decidability of KAH on the domain of r. The saturated construction is shown to terminate in cases where the basic one does not, and the method recovers known reduction-based completeness results.","tokens_in":19670,"tokens_out":24119,"duration_ms":227721,"significance":"The partial-reduction viewpoint is a useful and honest relaxation: it gives completeness/decidability for individual expressions even when hypothesis closure is not globally regular. The constructions are algorithmic and the paper provides concrete examples and detailed appendix proofs. If the central preservation lemmas are correctly established, the main theorems are valuable and would meaningfully extend the toolkit for Kleene algebra with hypotheses. The main caveat is that Lemma 3.15 (and the analogous Lemma 4.9) contain a genuine, though apparently local, induction gap; the core ideas look sound and repairable.","major_comments":[{"comment":"The proof says 'we only concern ourselves with one application of T0, and we can re-apply the result to each successive operation of T0.' This induction is not justified. The one-step construction turns a plain solution s of X into an H-solution s* of T0(X). To re-apply the lemma at T0(X), one would need a plain solution of T0(X); no such solution is produced, and s* is generally not plain because the ε-transition equation from x_i to z_i^0 is proved only up to H via e≤w. Thus r0(g) ≤H g in Theorem 3.16 is not established as written. The gap is repairable: state and prove the one-step extension for an arbitrary H-solution (checking all inequalities in KAH), then iterate along the chain.","section":"Appendix B, Lemma 4.9 / Theorem 4.10"},{"comment":"Lemma 4.9 is said to 'largely follow' Lemma 3.15, so it inherits the same induction gap. Since Theorem 4.10 and Corollary 4.11 are the central results for the saturated construction, this is a load-bearing omission. The same repair works: prove a one-step extension from H-solutions to H-solutions for TH, replacing the use of s_{Z_i}(z_i^0) ≡ e by Lemma 4.8's s_{Z^w_i}(z_i^0) ≡H e, and then iterate. As written, the main theorem that rH is a partial reduction, and hence the partial completeness/decidability corollary, is not fully proved.","section":"Appendix B, Lemma 4.9 / Theorem 4.10"}],"minor_comments":[{"comment":"The proof refers to 'Lemma 3.15' for the extension to T*_H(X); this should be Lemma 4.9.","section":"Theorem 4.10 proof"},{"comment":"For TH, the patching condition is stated using l_X(x_i) from the original automaton, but no analogue of Remark 3.8 is given. A brief remark that TH also patches all states simultaneously would prevent confusion.","section":"Definition 4.4"},{"comment":"The induction from the one-step inclusion H(l_X(x)) ⊆ l_{T0(X)}(x) to the iterated statement H*(l_X(x)) ⊆ l_{T*}(x) is only announced. It is routine (apply the one-step property to each automaton in the chain and use monotonicity of H), but spelling it out would make the appendix self-contained.","section":"Lemma 3.12 / Lemma 4.6"}],"recommendation":"major_revision","confidential_remarks":"I think the paper is a solid candidate after a local proof repair. The induction gap is real and affects the central theorem, but the fix is clear and does not require new conceptual machinery. No concern about novelty or citation practice. I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core idea here is good: define partial reductions so you get completeness and decidability on a subdomain even when a total reduction is impossible, and derive them via an automaton patching construction for linear hypotheses e≤w. The saturation variant (TH) is a real improvement over the naive T0, and the examples (ba≤a, ab≤ba) are clear and informative. The paper is honest about where it succeeds and where it fails, and it connects well to the existing total-reduction literature of Doumane et al. and Pous et al. If the proof gap below is fixed, the conditional completeness/decidability results are a solid within-subfield contribution.\n\nThe soft spot is exactly where the reader’s report points. Lemma 3.15 proves that a plain solution of X can be extended to an H-solution of T0(X). The proof then says the finite chain X ⊑ T0(X) ⊑ ... ⊑ T0^n(X) is handled by induction. That induction does not go through as written: after one step you have an H-solution of T0(X), not a plain solution, so you cannot reapply the lemma at T0(X). The appendix repeats the same assertion rather than proving the generalized claim. The issue transfers verbatim to Lemma 4.9 for TH, and therefore to Theorem 4.10 and Corollary 4.11, so the central inequality rH(g) ≤H g is not established as the proof stands. This looks repairable: you should generalize the lemma to take an H-solution and produce an H-solution, weakening the key step w·s(x') ≤ s(xi) to ≤H. But it is currently a real gap in a load-bearing result. The lack of a termination characterization is acknowledged as future work, which is fine; that is a limitation, not an error.\n\nWho is this for? People working on Kleene algebra with hypotheses, completeness, and decidability, and possibly the Rocq tactic community. It deserves a serious referee: the idea is novel, the exposition is good, and the gap is likely fixable without changing the shape of the construction. I would not cite the main theorem yet, but I would probably cite the construction after a repair.\n\nRecommendation: send this to peer review, but tell the authors the proof of Lemma 3.15 / Lemma 4.9 needs to be repaired before the paper can be accepted. This is exactly the kind of preprint a good referee should see.","headline":"Useful construction for partial reductions in KA with linear hypotheses, but the main proof has a repairable induction gap in Lemma 3.15 (and its TH analogue).","tokens_in":20108,"tokens_out":2326,"would_cite":false,"duration_ms":26343,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q70","03B25","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper shows that for a hypothesis of the form e ≤ w in Kleene algebra, an automaton-based saturation construction yields a partial reduction: on expressions where the construction terminates, hypothesis-closed language equivalence matc","keywords":["Kleene algebra","hypotheses","linear hypotheses","partial reductions","automata","completeness","decidability","saturation"],"falsifier":"Run the construction on a concrete case such as H = {ba ≤ a} and expression a, where T_H terminates: check whether the language of the final automaton equals the hypothesis-closed language {b^k a : k ≥ 0}. Any mismatch would refute the reduction claim. More generally, search for a finite terminating T_H output where r_H(g) is not provably ≤_H g, which would expose a failure of the iterated extension lemma.","tokens_in":19290,"feed_emoji":"🤖","tokens_out":3530,"duration_ms":35432,"temperature":0.7,"pith_summary":"The paper attacks a known bottleneck: adding program-specific hypotheses to Kleene algebra (KA) destroys completeness and decidability, and the standard fix—a total reduction—is often impossible because hypothesis closure can turn regular languages non-regular. The authors propose partial reductions instead: maps that only need to work on some expressions. They build such partial reductions automatically for linear hypotheses of the form e ≤ w, using an automaton construction that repeatedly 'patches' an automaton with a copy of an automaton for e. When the construction terminates, it yields an expression whose regular language is exactly the hypothesis-closed language of the original, and the two are provably equal up to the hypothesis. This gives completeness and decidability on the domain of termination, which is wider than what total-reduction methods cover.","feed_headline":"Automaton closure proves more program equivalences in Kleene algebra","feed_subtitle":"When the construction terminates, hypothesis-closed equivalence becomes decidable for those expressions.","key_machinery":"The central mechanism is the 'patching' operation: given an automaton X and a state x, the construction attaches a fresh automaton Z for the expression e, adding an ε-transition from x into Z's start state and ε-transitions from Z's accepting state back to every state reachable from x by reading w. The improved version uses the w-saturated automaton Z^w, which adds initial-state and final-state reset transitions so that loops introduced by the hypothesis do not force infinite re-patching. Iterating this patching, using a Brzozowski-style derivative test to decide which states need patching, yields the chain whose limit is the reduced automaton. The proof that this is a reduction relies on le","core_discovery":"The central claim is that for any linear hypothesis e ≤ w, the automaton construction T_H (patching with the w-saturated automaton for e, iterated to its limit) defines a partial reduction r_H. Concretely, whenever T_H terminates finitely on the automaton of an expression g, two properties hold: the hypothesis-closed language of g is contained in the regular language of r_H(g), and r_H(g) is provably below g in KAH. Consequently, for any two expressions g and h on which r_H is defined, equality of their hypothesis-closed languages implies g ≡_H h, and this equivalence is decidable. If T_H terminates on all expressions, this yields full completeness and decidability for KAH.","pith_inferences":["A clear next step is to characterize exactly when T_H terminates; if that characterization matches a regularity criterion for hypothesis-closed languages, the method would be optimal within its class of hypotheses.","The saturation idea is local to the patched automaton; Example 4.12 suggests a context-sensitive refinement—saturating with respect to the host automaton's paths—might handle hypotheses that currently cause infinite iteration.","The partial-reduction framework could be used as a proof-assistant tactic: a user supplies a linear hypothesis, the tactic runs the automaton construction, and if it terminates, the equivalence question reduces to a decidable regular-language check.","Because the construction yields syntactic reductions, it could help synthesize witnesses: when two expressions are provably equivalent under H, the reduced expressions give an explicit KA proof bridge."],"forward_implications":["For any linear hypothesis where the construction always terminates, KAH becomes complete and decidable for all expressions.","The construction recovers known reductions for contraction hypotheses such as a ≤ aa, giving a uniform explanation for existing completeness results.","For sets of 'independent' hypotheses, the reduction can be applied hypothesis-by-hypothesis, chaining reductions down to plain KA.","The technique lifts to any system that reduces to KA, such as Kleene algebra with tests or NetKAT, potentially extending them with additional linear hypotheses.","The termination domain of r_H precisely identifies a broad class of expressions on which hypothesis-closed equivalence is decidable, even when no total reduction exists."],"fun_headline_variants":["Automaton method proves more program equivalences in Kleene algebra","Partial reductions via automata decide more Kleene algebra equivalences","Automaton construction yields decidable equivalences for linear hypotheses","Mechanical reductions prove more equivalences in Kleene algebra","Automaton-based partial reductions expand provable program equivalences"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The argument assumes that the one-step extension lemma—turning a solution of an automaton into an H-solution of its patched successor—can be applied repeatedly along the infinite chain of patched automata, even when the intermediate automaton already contains patched-in states; the paper only proves the one-step version for plain solutions, and the iterated version is not stated.","fun_headline_variants_meta":{"raw":{"variants":["Automaton method proves more program equivalences in Kleene algebra","Partial reductions via automata decide more Kleene algebra equivalences","Automaton construction yields decidable equivalences for linear hypotheses","Mechanical reductions prove more equivalences in Kleene algebra","Automaton-based partial reductions expand provable program equivalences"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000584,"raw_usage":{"total_tokens":2548,"prompt_tokens":676,"completion_tokens":1872,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":420,"completion_tokens_details":{"reasoning_tokens":1789}},"tokens_in":420,"tokens_out":1872,"duration_ms":13665,"temperature":1.0,"reasoning_tokens":1789,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T09:19:40.021608+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the construction on a concrete case such as H = {ba ≤ a} and expression a, where T_H terminates: check whether the language of the final automaton equals the hypothesis-closed language {b^k a : k ≥ 0}. Any mismatch would refute the reduction claim. More generally, search for a finite terminating T_H output where r_H(g) is not provably ≤_H g, which would expose a failure of the iterated extension lemma.","supporting_citations":[],"review_version":1}