{"id":"887d9177-a259-49e5-b1d5-f3f00af0e1f8","arxiv_id":"1908.04923","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"For any fixed k, iterators that stop after k length or lookahead revisions are lambda-P equivalent to the Cook-Urquhart recursor over type-one polynomial-time functions.","lead":"This paper introduces new iteration schemas for higher-type polynomial-time computation, where the number of times a function oracle may return growing answers is fixed to a constant. It proves that for any such constant, the generated computable functionals coincide with those of the Cook-Urquhart recursor for basic feasible functionals.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 2.3's final step (R0 ≼ I) is wrong as written: the H-function uses |t|>1 to detect the initial value, which fails when |a|>|b|>1.","rationale":"The reader's verdict identified the background theory as the weakest assumption and noted presentation defects in Lemmas 3.2 and 4.1, but did not flag a concrete failure in Lemma 2.3. My stress-test found a more specific and load-bearing flaw: the proof that the Cook–Urquhart recursor R is P-reducible to the bounded iterator I (Lemma 2.3) contains an incorrect final construction for handling an unbounded initial value. The equality claimed for R0 in terms of R'_0 via the helper H fails for a natural instantiation, as shown by the counterexample in the attack. This matters because Lemma 2.3 is the bridge between the new iterators and Mehlhorn's basic feasible functionals: Theorem 4.3 states I ≡_λP I_k ≡_λP I'_k ≡_λP I', and without I ≡_λP R the connection to Cook–Urquhart recursor is broken. Moreover, Lemma 3.4 explicitly appeals to Lemma 2.3 to justify U ≼_λP I, so the proof of I_k ≼_λP I inherits the gap. The issue is likely repairable by carrying an explicit step/first-call flag in the encoded tuple, and the underlying mathematical claim may well be true; hence the appropriate verdict is CONDITIONAL rather than REJECT. The reader's weakest_assumption about the type-one background is reasonable but not the single most acute point; the internal construction error in Lemma 2.3 is more directly falsifiable and more immediately threatening to the written proof.","tokens_in":13184,"tokens_out":22983,"duration_ms":212072,"concrete_test":"Check the claimed equality of Lemma 2.3 with a='000', b='00', c='0', and ϕ(d,t)='1' if d='0' and |t|=3, else '0'. Compute both sides: R0(ϕ,a,b,c) should be '1', while R'_0(λt.λd.H(ϕ,d,t,a), a, b, c) evaluates to '0', showing the H construction is invalid. For a positive test, re-prove R0 ≼ I by encoding the recursion step count in the tuple (e.g., keeping the number of processed digits in the first component) and verify the simulated value equals R0 for all a,b,c; if no such modified construction is provided, the reduction remains unverified.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The most load-bearing defect is in the proof of Lemma 2.3 (R ≡_λP I), specifically the last paragraph where R0 is expressed through R'_0. To undo the initial truncation lmin(a,b), the authors define H(ϕ,d,t,a) = ϕ(d,t) if |t|>1, else ϕ(d,a), and claim R0(ϕ,a,b,c) = R'_0(λt.λd.H(ϕ,d,t,a), a, b, c) for nonempty c. The intended idea is that the first recursive call should use the original value a, not the truncated value lmin(a,b). But the test |t|>1 does not identify the initial call: when |a|>|b| and |b|>1, the initial value of R'_0 is b, which also satisfies |t|>1, so H returns ϕ(d,b) instead of ϕ(d,a). Concrete counterexample: a='000', b='00', c='0', and ϕ(d,t)='1' if d='0' and |t|=3, else '0'. Then R0(ϕ,a,b,c) = lmin(ϕ(0,a),b) = lmin('1','00') = '1', while R'_0 with H computes u0 = lmin(a,b) = '00' (length 2), H(ϕ,0,u0,a) = ϕ(0,'00') = '0', and the result is lmin('0','00') = '0'. The claimed equality fails. Since Lemma 2.3 is used in Lemma 3.4 to reduce the bounded universal quantifier U to I (and underpins Theorem 4.3's connection to the Cook–Urquhart recursor), the central equivalence is not established as written. This is a gap in the construction rather than a refutation of the theorem—a flag or step-count in the encoding would likely repair it—but the written proof is incorrect for arbitrary a,b.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines type-two iteration operators with bounded query revision: the k-revision iterator I_k and the k-lookahead iterator I'_k, generalizing the bounded iterator I and the Cook-Urquhart recursor R. The main result (Theorem 4.3) asserts that for every fixed k, I, Ik, I'_k, and I' are all mutually P-equivalent, hence each generates the basic feasible functionals of Mehlhorn over a background of type-one polynomial-time functions. The proof proceeds by explicit lambda-term reductions in the applied lambda-calculus λ(P), with a series of lemmas relating R, R0, I, I', and the revision iterators. The paper also discusses efficient implementations of these iterators via tail-recursion elimination and control operators.","tokens_in":13496,"tokens_out":6479,"duration_ms":57973,"significance":"If the theorem holds, the paper provides a machine-independent, syntax-based characterization of type-two feasibility through iteration schemes that restrict the number of query-size revisions, complementing the OTM-based classes SPT and MPT from earlier work by the same authors. The reductions are constructive and the paper introduces reusable programming idioms for higher-type feasible computation. The central equivalence is a natural and valuable result. However, the written proof contains a load-bearing gap in Lemma 2.3 and an unclear proof in Lemma 3.2, so the main theorem is not rigorously established as written.","major_comments":[{"comment":"The reduction R0 ≼ R'_0 is not proved correctly. The function H(ϕ,d,t,a) chooses between ϕ(d,t) and ϕ(d,a) based on whether |t| > 1, intending to recover the original initial value a when the predecessor truncates it to lmin(a,b). This test fails when |a| > |b| > 1: the first recursive value of R'_0 is b, which has length greater than 1, so H returns ϕ(d,b) instead of ϕ(d,a). Concretely, take a='000', b='00', c='0', and ϕ(d,t) returning '1' if d='0' and |t|=3, else '0'. Then the true value R0(ϕ,b,a,c) is '1', but the proposed encoding gives '0'. Since Lemma 2.3 underpins Lemma 3.4 and Theorem 4.3, this is a real gap. A flag indicating the first call, or a step counter based on the prefix of c, would likely repair the construction, but the proof as written is incorrect for arbitrary a and b.","section":"Lemma 2.3, final paragraph"},{"comment":"The proof of the additivity property for k-revision iteration is garbled. The case distinction is unclear: after defining ℓ as the first index from which the values stabilize under k revisions, the proof refers to 'the strings φℓ!k(a),...,φn!k(a) are still all equal' while also discussing a j where φ(φj!k(a)) ≠ φℓ+1!k(a). The notation mixes φ^ℓ_k(a) and φ^ℓ!k(a), and the conclusion 'φ^m!1(φℓ!k(a)) = φ(φℓ!k(a)) = φ^{ℓ+m}!(k+1)(a) for any m' does not follow from the assumptions as stated. Since this lemma is the key inductive step in proving Ik+1 ≼ I, the proof must be rewritten carefully.","section":"Lemma 3.2, proof of (*)"},{"comment":"The proof contains an unbound variable b: the text writes 'the evaluation of Ik(φ, a, b, c ≫ 1)', but the iterator Ik takes three arguments, not four. More importantly, the claim that I'_k(φ,a,c) = φ(Ik(φ,a,c≫1)) is argued informally by asserting that lookahead revisions correspond exactly to preceding length revisions. A rigorous proof would need to track the exact point at which each type of revision occurs and handle the boundary case where the (k+1)-st length revision and the (k+1)-st lookahead revision occur at the same or shifted steps. As written, the argument is too sketchy to verify.","section":"Lemma 4.1, proof"}],"minor_comments":[{"comment":"The argument order of R0 changes between the statement of Lemma 2.1 (R0(φ,b,a,c)) and the last paragraph of Lemma 2.3 (R0(φ,a,b,c)). This inconsistency should be fixed.","section":"Lemma 2.3, last paragraph"},{"comment":"There are several typos and missing spaces: 'F or givenφ' in Lemma 3.2, 'F or k≥ 1' in Lemma 3.4, 'bounded quanitification' in Section 3, 'correpsonds' in Section 5, and inconsistent use of 'ℓ' and 'l' in Lemma 3.2.","section":"Throughout"},{"comment":"The definition of G(φ,t1,b) and G(φ,t0,b) uses t0 and t1 to denote strings ending in 0 and 1, but this convention is not stated in the proof. It should be clarified for readability.","section":"Lemma 3.1, proof"},{"comment":"The definition of truncation writes 'c_{\\le |b|}' with a subscript that is not typeset clearly; the intended meaning is the initial segment of c of length |b|, which should be stated in words.","section":"Section 1.1"}],"recommendation":"major_revision","confidential_remarks":"The paper is a short proceedings-style manuscript (EPTCS 298). The main result is plausible and valuable, but the written proofs of Lemmas 2.3 and 3.2 need substantive repair; the gap in Lemma 2.3 is demonstrably load-bearing. For a journal version, the authors should expand the proofs, fix the H-function encoding with a proper flag or step counter, rewrite Lemma 3.2, and clean up the unbound variable in Lemma 4.1. I would be willing to review a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version: the paper introduces genuinely new families of iteration operators (I_k, I'_k) that bound length/lookahead revision and claims they are all lambda-P equivalent to the Cook-Urquhart recursor. The definitions are natural and the proof idiom—tupling with length-monotone projections—is worth stealing. But the proof as written has a real gap in the reduction from R to the bounded iterator I, and the main equivalence is not established in the text.\n\nThe problem is in the final paragraph of Lemma 2.3. To recover the untruncated initial value a, the authors define H(φ,d,t,a) = φ(d,t) if |t|>1 else φ(d,a), and claim R0(φ,a,b,c) = R'_0(λt.λd.H(φ,d,t,a), a, b, c). The test |t|>1 is supposed to detect the first call, but it doesn't. Take a='000', b='00', c='0', and φ(d,t) = '1' if d='0' and |t|=3, else '0'. The left side is lmin(φ('0',a),b) = '1'. On the right, the initial value is lmin(a,b)='00', so the first step applies H with t='00', which has length 2, so H returns φ('0','00')='0', and the result is '0'. The equality fails. This isn't a cosmetic typo; the construction genuinely mishandles initial values of length greater than one. A flag or step counter should repair it, but as written the proof is wrong.\n\nLemma 2.3 is load-bearing: it's used in Lemma 3.4 to reduce bounded universal search to I and feeds Theorem 4.3. So the central equivalence is conditional on a fix. The paper also has smaller issues: Lemma 3.2's case analysis is garbled, and Lemma 4.1 uses an unbound variable b. The R0 argument order swaps between Lemma 2.1 and 2.3, which likely contributed to the mistake.\n\nOn the plus side, the paper is honest about its assumptions, cites its own prior work appropriately, and identifies a useful link between SPT/MPT and syntactic iteration. If the gap is patched, this is a solid implicit-complexity contribution. As it stands, I'd be careful about citing the equivalence theorem without checking a repair.\n\nI'd send it to a serious referee—the main claim is likely correct and worth the effort—but I'd expect a revision with the proof fixed. For a reading group, maybe; the operators are interesting, but the discussion would be mostly about the bug.","headline":"Useful new iterator families, but the proof of the central equivalence has a real gap in Lemma 2.3 that makes the main theorem unproven as written.","tokens_in":14141,"tokens_out":8451,"would_cite":false,"duration_ms":76465,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03D15","03B40","03D65","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"Iteration with only a constant number of allowed size increases generates all of type-two polynomial time.","keywords":["type-two polynomial time","bounded iteration","length revision","lookahead revision","lambda definability","basic feasible functionals","recursion on notation","implicit computational complexity"],"falsifier":"Find a type-two functional definable with one more allowed revision but not with $k$, under the same base functions; the additivity lemma says none exists, so any concrete witness would refute Theorem 4.3. A more targeted check is to instantiate Lemma 3.2 with a length-doubling function $\\phi(a) = aa$ and verify the stated equality on small inputs; a single mismatch would show the reduction chain is unsound.","tokens_in":12889,"feed_emoji":"🔁","tokens_out":7979,"duration_ms":75798,"temperature":0.7,"pith_summary":"The paper shows that several superficially different iteration schemes are all exactly as powerful as the standard bounded recursor for type-two polynomial time. It works in a simply typed lambda calculus equipped with all first-order polynomial-time functions and compares operators by mutual definability. The new schemes let iteration run for the length of an input string but interrupt or continue depending on how often the step function returns a value longer than any earlier value ('length revisions') or is applied to an argument longer than any earlier argument ('lookahead revisions'). For every fixed constant bound $k$, both kinds of revision-bounded iteration are $P$-equivalent to ordinary bounded iteration, hence generate the same class of functionals: the basic feasible functionals, the standard class of feasible type-two functionals. The point of caring is that the bound becomes intrinsic to the iteration rule rather than an externally imposed length bound.","feed_headline":"A constant number of size increases still yields full type-two poly-time","feed_subtitle":"Length revisions and lookahead revisions define the same functionals as the bounded recursor.","key_machinery":"The central object is the bounded iterator $I(\\phi,b,a,c) = (\\lambda t.\\mathrm{lmin}(\\phi(t),b))^{|c|}(\\mathrm{lmin}(a,b))$, which truncates every intermediate value to the length bound $b$. The revision iterators $I_k$ and $I'_k$ replace that explicit bound by a fixed count of length revisions or lookahead revisions, so they are really families of operators indexed by $k$. The proof machinery has two load-bearing parts: a tupling encoding that carries the recursion parameter $c$ through the iteration as a counter, and a bounded-search functional $M$ that finds the first index where the iteration becomes constant, enabling the reduction from $k+1$ revisions to $k$ revisions plus one final application.","core_discovery":"The central claim is Theorem 4.3: for every $k \\geq 0$, the bounded iterator $I$, the $k$-revision iterator $I_k$, the $k$-lookahead iterator $I'_k$, and the argument-bounded iterator $I'$ are pairwise equivalent under $\\lambda$-definability over the type-one polynomial-time functions. The proof chains the equivalences $R \\equiv I$, $I_k \\preceq I$ by induction on $k$, $I'_k \\preceq I_k$, and $I' \\preceq I'_k$. In plain terms, allowing a fixed number of size increases during iteration does not enlarge the class of type-two functionals one can define: the standard explicit bound can always be simulated, and conversely the revision rules can be enforced by a bounded iterator.","pith_inferences":["Treating $k$ as a resource rather than a definability parameter, the construction suggests the translation overhead grows with $k$; a finer measure under which the revision hierarchy is strict may therefore exist, though the paper does not establish one.","The dynamic 'no more than $k$ revisions' check resembles a runtime exception: the paper's re-entrant recursion sketch suggests control operators such as catch/throw could implement the iterators more efficiently and connect them to existing sequentiality results.","The link to non-size-increasing computation indicates a possible static typing discipline, e.g. an affine or linear type system, that internalises the revision bound and makes the restriction syntactic rather than dynamic.","The reduction's main tools—length comparisons, tupling, and bounded search—are type-one only, so a plausible extension is to adapt the equivalence to higher-type iteration; the collapse may survive, but the encodings would need new infrastructure."],"forward_implications":["For any fixed $k$, allowing one more revision does not enlarge the definable class; all the $I_k$ collapse into the basic feasible functionals.","Every functional definable with bounded revisions inherits the oracle-machine characterization of type-two feasibility, so it runs in time bounded by a second-order polynomial.","The equivalence supplies syntax-level, intrinsic formulations of type-two feasible computation that need no external upper bound on intermediate sizes.","The constant $k$ still controls the cost of the translation: implementing $I_{k+1}$ from $I_k$ inserts a bounded search at each step, so larger $k$ yields more concise definitions without changing expressive power."],"supporting_citations":[{"why":"Supplies the simply typed lambda calculus $\\lambda(P)$ and the recursor $R$ that serves as the baseline for all equivalences.","marker":"[6]"},{"why":"Introduces limited recursion on notation, the first-order scheme whose second-order generalisation the paper's operators capture.","marker":"[3]"},{"why":"Defines the original class of type-two polynomial-time functionals (basic feasible functionals) that all the equivalent operators generate.","marker":"[14]"},{"why":"Establishes that definability in the lambda calculus with $R$ coincides with the basic feasible functionals, grounding the equivalence claim.","marker":"[11]"},{"why":"Introduces length and lookahead revisions in the oracle-machine setting, which the paper transfers to iteration schemes.","marker":"[10]"},{"why":"Gives the oracle Turing machine characterization of type-two feasibility used to motivate why each $I_k$ is basic feasible.","marker":"[9]"}],"fun_headline_variants":["Bounded lookahead iterations keep full poly-time power","Constant size bumps don't change type-two expressivity","Fixed query revision count matches bounded recursor","Capping size increases preserves type-two poly-time","Lookahead and length revisions: same poly-time class"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole construction lives in a lambda calculus that already contains constants for every first-order polynomial-time function, with length-monotone tupling; if that base class were weakened, the specific encodings in the reductions could fail.","fun_headline_variants_meta":{"raw":{"variants":["Bounded lookahead iterations keep full poly-time power","Constant size bumps don't change type-two expressivity","Fixed query revision count matches bounded recursor","Capping size increases preserves type-two poly-time","Lookahead and length revisions: same poly-time class"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00106,"raw_usage":{"total_tokens":4398,"prompt_tokens":845,"completion_tokens":3553,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":461,"completion_tokens_details":{"reasoning_tokens":3478}},"tokens_in":461,"tokens_out":3553,"duration_ms":23714,"temperature":1.0,"reasoning_tokens":3478,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:28:56.286980+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a type-two functional definable with one more allowed revision but not with $k$, under the same base functions; the additivity lemma says none exists, so any concrete witness would refute Theorem 4.3. A more targeted check is to instantiate Lemma 3.2 with a length-doubling function $\\phi(a) = aa$ and verify the stated equality on small inputs; a single mismatch would show the reduction chain is unsound.","supporting_citations":[{"cited_title":"Cook & A","cited_arxiv_id":null,"evidence_quote":"Supplies the simply typed lambda calculus $\\lambda(P)$ and the recursor $R$ that serves as the baseline for all equivalences."},{"cited_title":"Cobham (1965): The intrinsic computational difficulty of functions","cited_arxiv_id":null,"evidence_quote":"Introduces limited recursion on notation, the first-order scheme whose second-order generalisation the paper's operators capture."},{"cited_title":"Mehlhorn (1976): Polynomial and abstract subrecursive classes","cited_arxiv_id":null,"evidence_quote":"Defines the original class of type-two polynomial-time functionals (basic feasible functionals) that all the equivalent operators generate."},{"cited_title":"Kapron (1991): Feasible Computation in Higher Types","cited_arxiv_id":null,"evidence_quote":"Establishes that definability in the lambda calculus with $R$ coincides with the basic feasible functionals, grounding the equivalence claim."},{"cited_title":"Kapron & S.A","cited_arxiv_id":null,"evidence_quote":"Gives the oracle Turing machine characterization of type-two feasibility used to motivate why each $I_k$ is basic feasible."}],"review_version":1}