Type-two Iteration with Bounded Query Revision

Bruce M. Kapron (University of Victoria); Florian Steinberg (INRIA Saclay)

REVIEW 3 major objections 4 minor 16 references

Type-two Iteration with Bounded Query Revision

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Iteration with only a constant number of allowed size increases generates all of type-two polynomial time.

desk verdict 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. read the letter →

arxiv 1908.04923 v1 pith:CBLUENE3 submitted 2019-08-14 cs.CC cs.LOcs.PL

Bruce M. Kapron (University of Victoria) , Florian Steinberg (INRIA Saclay) This is my paper · ORCID

classification cs.CCcs.LOcs.PL MSC 03D1503B4003D6568Q15

keywords type-twopolynomialtimeboundediterationlengthrevisionlookaheadlambdadefinabilitybasicfeasiblefunctionalsrecursiononnotationimplicitcomputationalcomplexity

topics P versus NP

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

The 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.

Lemma 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.

On 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.

I'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.

Referee Report

3 major / 4 minor

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.

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 (3)

[Lemma 2.3, final paragraph] 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.
[Lemma 3.2, proof of (*)] 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.
[Lemma 4.1, proof] 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.

minor comments (4)

[Lemma 2.3, last paragraph] 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.
[Throughout] There are several typos and missing spaces: 'F or givenφ' in Lemma 3.2, 'F or k≥ 1' in Lemma 3.4, 'bounded quanitiﬁcation' in Section 3, 'correpsonds' in Section 5, and inconsistent use of 'ℓ' and 'l' in Lemma 3.2.
[Lemma 3.1, proof] 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 1.1] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the central equivalences are proved by explicit lambda-term reductions; self-citations are background and not load-bearing.

full rationale

The paper's reduction chain is constructive throughout. Lemma 2.1 proves R ≡ R0 by explicitly defining max and argmax from R0 and then expressing R from R0. Lemma 2.2 gives a simultaneous induction showing I ≡ I'. Lemma 2.3 proves R ≡ I by writing I as a substitution instance of R and constructing R0 (via R'0) from I using the pairing-based functional Φ; the final H-function step is a construction intended to recover the initial value, not an assumption of the equivalence. Lemma 3.4 proves Ik ≼ I by induction, implementing the needed bounded quantification and bounded search U and M by explicit definitions from R and I; it uses the induction hypothesis that Ik is already reducible to I, which is not circular. Lemmas 4.1 and 4.2 relate the lookahead versions to the length-revision versions by explicit identities. The only self-citations, e.g. [9], [10], [11] and [12], provide background characterizations (SPT/MPT, Cook–Urquhart = Mehlhorn) and motivation; they are not used in place of the new proofs, and none of the novel reduction claims is assumed in its own proof. A separate technical gap may exist in the final paragraph of Lemma 2.3, where the condition |t|>1 may fail to identify the initial call when |a|>|b|>1, but this is a correctness defect in the written proof, not a circular reduction: the paper is trying to construct R0 from I, not deriving I from the theorem it claims. Therefore the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No numerical data or fitted parameters appear in this paper; k is a theorem parameter rather than a fitted value. The main assumptions are the standard Cook-Urquhart background (all type-one poly-time functions as constants), length-monotone tupling, and polynomial-time conditionals. No physical or extraneous entities are postulated; the new iterators are explicit definitions in the existing calculus.

assumptions (4)

domain assumption All type-1 polynomial-time functions are available as constant symbols in lambda(P).
Section 1.1 and 1.2; the reducibility relation is defined relative to this constant set, and every reduction in the paper uses these constants.
domain assumption Length-monotone, injective tupling with projections and initial-segment extraction are available as polynomial-time operations.
Section 1.1; Lemma 2.3's encoding of the recursor by the bounded iterator depends on these properties.
domain assumption Polynomial-time conditional and definition by cases are available.
Section 1.1; used in definitions of A, H, N, G and in the iterator I'' in Lemma 4.2.
standard math Standard lambda calculus beta-eta conversion preserves denotational values.
Section 1.2; this justifies treating terms up to beta-eta equivalence when representing functionals.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Type-two Iteration with Bounded Query Revision." pith.science (2026). https://pith.science/paper/CBLUENE3

@misc{pith2026190804923,
  author       = {Pith},
  title        = {Pith review of: Type-two Iteration with Bounded Query Revision},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CBLUENE3}},
  note         = {Machine review of arXiv:1908.04923}
}

read the original abstract

Motivated by recent results of Kapron and Steinberg (LICS 2018) we introduce new forms of iteration on length in the setting of applied lambda-calculi for higher-type poly-time computability. In particular, in a type-two setting, we consider functionals which capture iteration on input length which bound interaction with the type-one input parameter, by restricting to a constant either the number of times the function parameter may return a value of increasing size, or the number of times the function parameter may be applied to an argument of increasing size. We prove that for any constant bound, the iterators obtained are equivalent, with respect to lambda-definability over type-one poly-time functions, to the recursor of Cook and Urquhart which captures Cobham's notion of limited recursion on notation in this setting.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references · 13 canonical work pages

[1]

Cook (1992): A New Recursion-Theoretic Characterization of the Polytime Functions

Stephen Bellantoni & Stephen A. Cook (1992): A New Recursion-Theoretic Characterization of the Polytime Functions. Computational Complexity 2, pp. 97–110, doi:10.1007/BF01201998

doi:10.1007/bf01201998 1992
[2]

Cartwright, P .L

R. Cartwright, P .L. Curien & M. Felleisen (1994): Fully Abstract Semantics for Observably Sequential Lan- guages. Information and Computation 111(2), pp. 297 – 401, doi:10.1006/inco.1994.1047

work page arXiv 1994
[3]

Cobham (1965): The intrinsic computational difﬁculty of functions

A. Cobham (1965): The intrinsic computational difﬁculty of functions . In Y ehoshua Bar-Hillel, editor:Logic, Methodology and Philosophy of Science: Proc. 1964 Intl. Con gress (Studies in Logic and the Foundations of Mathematics), North-Holland Publishing, pp. 24–30

work page 1965
[4]

Cook (1992): Computability and complexity of higher type functions

S.A. Cook (1992): Computability and complexity of higher type functions . In: Logic from com- puter science (Berkeley, CA, 1989) , Math. Sci. Res. Inst. Publ. 21, Springer, New Y ork, pp. 51–72, doi:10.1007/978-1-4612-2822-6 3

work page doi:10.1007/978-1-4612-2822-6 1992
[5]

Cook & B.M

S.A. Cook & B.M. Kapron (1990): Characterizations of the basic feasible functionals of ﬁni te type . In: Feasible mathematics (Ithaca, NY, 1989) , Progr. Comput. Sci. Appl. Logic 9, Birkh¨ auser, pp. 71–96, doi:10.1007/978-1-4612-3466-1 5

work page doi:10.1007/978-1-4612-3466-1 1990
[6]

Cook & A

S.A. Cook & A. Urquhart (1993): Functional interpretations of feasibly constructive arit hmetic. Ann. Pure Appl. Logic 63(2), pp. 103–200, doi:10.1016/0168-0072(93)90044-E

work page doi:10.1016/0168-0072(93)90044-e 1993
[7]

Martin Hofmann (2003): Linear types and non-size-increasing polynomial time comp utation. Inf. Comput. 183(1), pp. 57–85, doi:10.1016/S0890-5401(03)00009-9

work page doi:10.1016/s0890-5401(03)00009-9 2003
[8]

Ignjatovic & A

A. Ignjatovic & A. Sharma (2004): Some applications of logic to feasibility in higher types . ACM TOCL 5(2), pp. 332–350, doi:10.1145/976706.976713

work page arXiv 2004

Show all 16 references

[9]

Kapron & S.A

B.M. Kapron & S.A. Cook (1996): A new characterization of type- 2 feasibility. SIAM J. Comput. 25(1), pp. 117–132, doi:10.1137/S0097539794263452

1996 doi
[10]

Kapron & F

B.M. Kapron & F. Steinberg (2018): Type-two polynomial-time and restricted lookahead . In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Sc ience (Oxford, UK), 2018 , ACM, New Y ork, pp. 579–598, doi:10.1145/3209108.3209124

2018
[11]

Kapron (1991): Feasible Computation in Higher Types

Bruce M. Kapron (1991): Feasible Computation in Higher Types . Technical Report 249/91, Computer Sci- ence Department, University of Toronto

1991
[12]

In: 2nd International Conference on Formal Structures for Comp utation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK , pp

Akitoshi Kawamura & Florian Steinberg (2017): Polynomial Running Times for Polynomial-Time Oracle Machines. In: 2nd International Conference on Formal Structures for Comp utation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK , pp. 23:1–23:18, doi:10.4230/LIPIcs.FSC...

2017 doi
[13]

In: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (Am sterdam, The Netherlands), 1991 , IEEE Computer Society, pp

Daniel Leivant (1991): A F oundational Delineation of Computational Feasiblity . In: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (Am sterdam, The Netherlands), 1991 , IEEE Computer Society, pp. 2–11, doi:10.1109/LICS.1991.15162 5

1991
[14]

Mehlhorn (1976): Polynomial and abstract subrecursive classes

K. Mehlhorn (1976): Polynomial and abstract subrecursive classes . J. Comp. Sys. Sci. 12(2), pp. 147–178, doi:10.1016/S0022-0000(76)80035-9

1976 doi
[15]

Robinson (1947): Primitive recursive functions

Raphael M. Robinson (1947): Primitive recursive functions . Bull. Amer. Math. Soc. 53(10), pp. 925–942, doi:10.1090/S0002-9904-1947-08911-4

1947 doi
[16]

In: Eighth Annual IEEE Symposium on Logic in Computer Science (Montreal, PQ, 1993) , IEEE Comput

Anil Seth (1993): Some desirable conditions for feasible functionals of type 2. In: Eighth Annual IEEE Symposium on Logic in Computer Science (Montreal, PQ, 1993) , IEEE Comput. Soc. Press, Los Alamitos, CA, pp. 320–331, doi:10.1109/LICS.1993.287576

1993

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Cook (1992): A New Recursion-Theoretic Characterization of the Polytime Functions

Stephen Bellantoni & Stephen A. Cook (1992): A New Recursion-Theoretic Characterization of the Polytime Functions. Computational Complexity 2, pp. 97–110, doi:10.1007/BF01201998

doi:10.1007/bf01201998 1992

[2] [2]

Cartwright, P .L

R. Cartwright, P .L. Curien & M. Felleisen (1994): Fully Abstract Semantics for Observably Sequential Lan- guages. Information and Computation 111(2), pp. 297 – 401, doi:10.1006/inco.1994.1047

work page arXiv 1994

[3] [3]

Cobham (1965): The intrinsic computational difﬁculty of functions

A. Cobham (1965): The intrinsic computational difﬁculty of functions . In Y ehoshua Bar-Hillel, editor:Logic, Methodology and Philosophy of Science: Proc. 1964 Intl. Con gress (Studies in Logic and the Foundations of Mathematics), North-Holland Publishing, pp. 24–30

work page 1965

[4] [4]

Cook (1992): Computability and complexity of higher type functions

S.A. Cook (1992): Computability and complexity of higher type functions . In: Logic from com- puter science (Berkeley, CA, 1989) , Math. Sci. Res. Inst. Publ. 21, Springer, New Y ork, pp. 51–72, doi:10.1007/978-1-4612-2822-6 3

work page doi:10.1007/978-1-4612-2822-6 1992

[5] [5]

Cook & B.M

S.A. Cook & B.M. Kapron (1990): Characterizations of the basic feasible functionals of ﬁni te type . In: Feasible mathematics (Ithaca, NY, 1989) , Progr. Comput. Sci. Appl. Logic 9, Birkh¨ auser, pp. 71–96, doi:10.1007/978-1-4612-3466-1 5

work page doi:10.1007/978-1-4612-3466-1 1990

[6] [6]

Cook & A

S.A. Cook & A. Urquhart (1993): Functional interpretations of feasibly constructive arit hmetic. Ann. Pure Appl. Logic 63(2), pp. 103–200, doi:10.1016/0168-0072(93)90044-E

work page doi:10.1016/0168-0072(93)90044-e 1993

[7] [7]

Martin Hofmann (2003): Linear types and non-size-increasing polynomial time comp utation. Inf. Comput. 183(1), pp. 57–85, doi:10.1016/S0890-5401(03)00009-9

work page doi:10.1016/s0890-5401(03)00009-9 2003

[8] [8]

Ignjatovic & A

A. Ignjatovic & A. Sharma (2004): Some applications of logic to feasibility in higher types . ACM TOCL 5(2), pp. 332–350, doi:10.1145/976706.976713

work page arXiv 2004