Type-two Iteration with Bounded Query Revision

TL;DR

This paper introduces new bounded iteration methods in applied lambda-calculi for higher-type poly-time computability, showing their equivalence to known limited recursion schemes.

Contribution

It defines bounded iteration forms in a type-two setting and proves their equivalence to the recursor of Cook and Urquhart for poly-time functions.

Findings

Bounded iterators are equivalent to Cobham's limited recursion.

New iteration forms restrict function application to control complexity.

Results extend understanding of higher-type poly-time computation.

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.

Equations

$$\mathsf{lmin}(\mathbf{c},\mathbf{b}):=\{\begin{array}{ll}\mathbf{c}& \text{ if }|\mathbf{c}|<|\mathbf{b}|\\ \mathbf{b}& \text{otherwise.}\end{array}$$

$$\tau ={\tau }_1\to {\tau }_2\to \cdots \to {\tau }_k\to 0$$

$$F(X_1)(X_2)\dots (X_k)=F(X_1,\dots ,X_k).$$

$${\mathcal{V}}_{\phi }(T)(F,F_1,\dots ,F_k):={\mathcal{V}}_{{\phi }^{\prime }}(S)(F_1,\dots ,F_k),$$

$${\mathcal{V}}_{\phi }(T)(F_1,\dots ,F_k)={\mathcal{V}}_{\phi }(S)({\mathcal{V}}_{\phi }(R)(F_1,\dots ,F_k)).\square$$

$$\mathcal{R}(\phi ,\psi ,\mathbf{a},ϵ):=\mathbf{a}\text{and}\mathcal{R}(\phi ,\psi ,\mathbf{a},\mathbf{c}i):=\mathsf{lmin}(\phi (\mathbf{c}i,\mathbf{t}),\psi (\mathbf{c}i)),\text{where}\mathbf{t}=\mathcal{R}(\phi ,\psi ,\mathbf{a},\mathbf{c}).$$

$${\mathcal{R}}_0(\phi ,\mathbf{b},\mathbf{a},\mathbf{c}):=\mathcal{R}(\phi ,\lambda \mathbf{d}.\mathbf{b},\mathbf{a},\mathbf{c}).$$

$$\mathsf{max}(\psi ,\mathbf{c}i):=\{\begin{array}{ll}\psi (\mathbf{c}i)& \text{ if }\mathsf{lmin}(\mathsf{max}(\psi ,\mathbf{c}),\psi (\mathbf{c}i))=\mathsf{max}(\psi ,\mathbf{c})\\ \mathsf{max}(\psi ,\mathbf{c})& \text{ otherwise.}\end{array}$$

$$\mathcal{R}(\phi ,\psi ,\mathbf{a},\mathbf{c})={\mathcal{R}}_0(\lambda \mathbf{d}.\lambda \mathbf{t}.\mathsf{lmin}(\phi (\mathbf{d},\mathbf{t}),\psi (\mathbf{d})),0\mathsf{max}(\psi ,\mathbf{c}),\mathbf{a},\mathbf{c}),$$

$$\mathsf{argmax}(\psi ,\mathbf{c})={\mathcal{R}}_0(\lambda \mathbf{d}.\lambda \mathbf{t}.A(\psi ,\mathbf{d},\mathbf{t}),\mathbf{c},ϵ,\mathbf{c})$$

$$\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},\mathbf{c}):=(\lambda \mathbf{t}.\mathsf{lmin}(\phi (\mathbf{t}),\mathbf{b}){)}^{|\mathbf{c}|}(\mathsf{lmin}(\mathbf{a},\mathbf{b})).$$

$${\mathcal{I}}^{\prime }(\phi ,\mathbf{b},\mathbf{a},\mathbf{c}):=(\lambda \mathbf{t}.\phi (\mathsf{lmin}(\mathbf{t},\mathbf{b})){)}^{|\mathbf{c}|}(\mathbf{a}).$$

$$\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})$$

$${\mathcal{I}}^{\prime }(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})$$

$$\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})$$

$$=\mathsf{lmin}({\mathcal{I}}^{\prime }(\phi ,\mathbf{b},\mathbf{a},\mathbf{c}),\mathbf{b})$$

$${\mathcal{I}}^{\prime }(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})$$

$$=\phi (\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},{\mathbf{c}}^{\prime })).$$

$$\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})=\mathcal{R}(\lambda \mathbf{d}.\lambda \mathbf{t}.\phi (\mathbf{t}),\lambda \mathbf{d}.\mathbf{b},\mathsf{lmin}(\mathbf{a},\mathbf{b}),\mathbf{c}),$$

$$\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},ϵ):=\mathsf{lmin}(\mathbf{a},\mathbf{b})\text{and}\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},\mathbf{c}i):=\mathsf{lmin}(\phi (\mathbf{t}),\mathbf{b}),\text{where}t=\mathcal{I}(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})$$

$${\mathcal{R}}_0^{\prime }(\phi ,\mathbf{a},\mathbf{b},ϵ):=\mathsf{lmin}(\mathbf{a},\mathbf{b})\text{and}{\mathcal{R}}_0^{\prime }(\phi ,\mathbf{a},\mathbf{b},\mathbf{c}i):=\mathsf{lmin}(\phi (\mathbf{c}i,\mathbf{t}),\mathbf{b}),\text{where}\mathbf{t}={\mathcal{R}}_0^{\prime }(\phi ,\mathbf{a},\mathbf{b},\mathbf{c}).$$

$$\Phi (\phi ,\mathbf{b},\mathbf{c}):=\lambda ⟨\mathbf{u},\mathbf{v}⟩.⟨\mathbf{u}0,\mathsf{lmin}(\phi ({\mathbf{c}}^{\le |\mathbf{u}|+1},\mathbf{v}),\mathbf{b})⟩.$$

$$\mathcal{I}(\Phi (\phi ,\mathbf{b},\mathbf{c}),⟨0^{|\mathbf{c}|},\mathbf{b}⟩,⟨ϵ,\mathbf{a}⟩,{\mathbf{c}}^{\prime })=⟨0^{|{\mathbf{c}}^{\prime }|},{\mathcal{R}}_0^{\prime }(\phi ,\mathbf{b},\mathbf{a},{\mathbf{c}}^{\prime })⟩$$

$${\mathcal{R}}_0^{\prime }(\phi ,\mathbf{b},\mathbf{a},\mathbf{c})={\pi }_2(\mathcal{I}(\Phi (\phi ,\mathbf{b},\mathbf{c}),⟨0^{|\mathbf{c}|},\mathbf{b}⟩,⟨ϵ,\mathbf{a}⟩,\mathbf{c})),$$

$$\mathcal{I}(\Phi (\phi ,\mathbf{b},\mathbf{c}),⟨0^{|\mathbf{c}|},\mathbf{b}⟩,⟨ϵ,\mathbf{a}⟩,{\mathbf{c}}^{\prime }i)$$

$$=\mathsf{lmin}(⟨0^{|{\mathbf{c}}^{\prime }|}0,\mathsf{lmin}(\phi ({\mathbf{c}}^{\le |{\mathbf{c}}^{\prime }|+1},{\mathcal{R}}_0^{\prime }(\phi ,\mathbf{b},\mathbf{a},{\mathbf{c}}^{\prime })),\mathbf{b})⟩,⟨0^{|\mathbf{c}|},\mathbf{b}⟩)$$

$$=\mathsf{lmin}(⟨0^{|{\mathbf{c}}^{\prime }i|},\mathsf{lmin}(\phi ({\mathbf{c}}^{\prime }i,{\mathcal{R}}_0^{\prime }(\phi ,\mathbf{b},\mathbf{a},{\mathbf{c}}^{\prime })),\mathbf{b})⟩,⟨0^{|\mathbf{c}|},\mathbf{b}⟩)$$

$$=\mathsf{lmin}(⟨0^{|{\mathbf{c}}^{\prime }i|},{\mathcal{R}}_0^{\prime }(\phi ,\mathbf{b},\mathbf{a},{\mathbf{c}}^{\prime }i))⟩,⟨0^{|\mathbf{c}|},\mathbf{b}⟩)$$

$$=⟨0^{|{\mathbf{c}}^{\prime }i|},{\mathcal{R}}_0^{\prime }(\phi ,\mathbf{b},\mathbf{a},{\mathbf{c}}^{\prime }i))⟩$$

$$H(\phi ,\mathbf{d},\mathbf{t},\mathbf{a})=\{\begin{array}{ll}\phi (\mathbf{d},\mathbf{t})& \text{ if ∣t∣>1;}\\ \phi (\mathbf{d},\mathbf{a})& \text{ otherwise,}\end{array}.$$

$$\mathcal{R}_{0}(\varphi,\mathbf{a},\mathbf{b},\mathbf{c})=\left\{\begin{array}[]{ll}\mathbf{a}&\text{if $\mathbf{c}=\epsilon$;}\\ \mathcal{R}_{0}^{\prime}(\lambda\mathbf{t}.\lambda\mathbf{d}.H(\varphi,\mathbf{d},\mathbf{t},\mathbf{a}),\mathbf{a},\mathbf{b},\mathbf{c})&\text{otherwise}\end{array}\right.$$

$${\phi }_{!k}^n(\mathbf{a}):=\underset{\text{ℓ times}}{\underbrace{\phi (\phi (\dots \phi }}(\mathbf{a})\dots ))$$

$${\mathcal{I}}_k(\phi ,\mathbf{a},\mathbf{c}):={\phi }_{!k}^{|\mathbf{c}|}(\mathbf{a})$$

$$G(\varphi,\mathbf{t}\mathtt{1},\mathbf{b}):=\mathbf{t}\mathtt{1}\quad\quad\quad\quad G(\varphi,\mathbf{t}\mathtt{0},\mathbf{b}):=\left\{\begin{array}[]{ll}\varphi(\mathbf{t})\mathtt{0}&\text{if $|\varphi(\mathbf{t})|\leq|\mathbf{b}|$;}\\ \mathbf{t}\mathtt{1}&\text{otherwise.}\end{array}\right.$$

Full text

1 Introduction

Recursion on notation is a fundamental tool for syntactic characterizations of feasible computation, in particular capturing the notion of bounding the number of steps of a computation in terms of input size. However, as a constraint, it is too weak on its own to capture feasibility as characterized by polynomial time computability. A well-known example is the following: consider a function $\varphi$, mapping binary strings to binary strings, which for any input string $\mathbf{a}$ returns the string concatenated with itself: $\varphi(\mathbf{a})=\mathbf{a}\mathbf{a}$. The function $\varphi$ should clearly be accepted as feasible, but recursion on notation allows the definition of a new function which, on input $\mathbf{b}$ of length $n$ returns $\varphi^{n}(\texttt{0})$, which is a string of length $2^{n}$. To capture feasibility through a recursion scheme, further restrictions are required to prevent this kind of exponential blowup. Indeed, Cobham, in perhaps one of the earliest works mentioning polynomial-time computability, gives a characterization using a scheme of limited recursion on notation [4]. Here, definition of a new function through recursion on functions already known to be from the class is allowed only in case the length of the resulting function may be a priori bounded by the length of a function already known to be in the class. Cobham’s approach is a canonical example of explicit bounding. It is also possible to formulate forms of limited recursion with implicit bounding and recover the same class of polynomial time functions [14, 2].

It is possible to consider feasibility in the type-two setting, which allows computation with respect to an arbitrary function oracle. The original definition of type-two polynomial time was given by Mehlhorn using a straightforward generalization of Cobham’s scheme [15]. Just like the polynomial time functions, this class of functionals allows for a number of different characterizations and is accepted as capturing feasibility at type level two appropriately: Cook and Urquhart gave a formulation of Mehlhorn’s class, and in fact generalized it to all finite types by use of an applied typed lambda calculus with constant symbols for a collection of basic type-one poly-time functions, as well as a recursor $\mathcal{R}$, which captures Mehlhorn’s scheme as a type-two functional [7]. Kapron and Cook showed that Mehlhorn’s class may be characterized in terms of oracle Turing machines ($\mathsf{OTM}$s) whose run-time is bounded by a second-order polynomial [10]. Both of these characterizations have lead to a multitude of applications and further characterizations.

The content of this paper is inspired by a recent description of Mehlhorn’s class given by Kapron and Steinberg [11]. For this it is instructive to think of an analogue of unrestricted recursion on notation in the $\mathsf{OTM}$ setting. Informally, this corresponds to Cook’s notion of oracle polynomial time ($\mathsf{OPT}$) [5], which bounds the running time of $\mathsf{OTM}$s by a polynomial in the size of the input and the largest answer returned by any call to the oracle. Here, a higher time consumption can be justified by an increasing chain of oracle return values and in particular it is possible to recover the example above within $\mathsf{OPT}$. To force feasibility, Kapron and Steinberg use restrictions of $\mathsf{OPT}$ based on query-size revisions. They considered two forms of revision: a length revision occurs when a query to the oracle returns an answer with size larger than the size of the input or the answer to any previous query, a lookahead revision occurs when the size of a query provided to the oracle is larger than the size of any previous such query. Strong polynomial time ($\mathsf{SPT}$) allows only a constant number of length revisions, while moderate polynomial time ($\mathsf{MPT}$) allows only a constant number of lookahead revisions. Kapron and Steinberg prove that both of the classes $\mathsf{SPT}$ and $\mathsf{MPT}$ give proper subsets of Mehlhorn’s class even when restricted to the functionals of the type that they are meant to capture, but that Mehlhorn’s class can be recovered from each of the classes by closing under $\lambda$-abstraction and application. It should be noted that length revisions and $\mathsf{SPT}$ make an earlier apparent in a somewhat different setting in work of Kawamura and Steinberg [13].

The outline of this paper is as follows: In the first section we describe the setting. Namely we work in a simply typed lambda-calculus with constant symbols for all type-1 polynomial-time computable functions. This is identical to the setting Cook and Urquhart chose for their characterization of higher-order polynomial time through the recursor $\mathcal{R}$ and means that we reason about higher-order complexity modulo the availability of the full strength of a first-order bounded recursion scheme. The paper starts from the observation that the bounded recursor $\mathcal{R}$ is meant to model Mehlhorn’s scheme, which is strictly more expressive than the first order scheme that is already available through the constants. Clearly $\mathcal{R}$ adds something, as the class of functionals expressible without its presence has been classified by Seth and is considerably restricted in its access of the oracle [17]. Thus, one may ask for functionals that are less expressive and still generate the same class given the context. Section 2 weakens $\mathcal{R}$ in two steps by first simplifying the way in which the bounding is done and afterwards by restricting the data that is available to the step-function. This leaves us with a functional $\mathcal{I}$ that no longer captures bounded recursion but is better understood as doing bounded iteration.

Section 3 starts involving the ideas of length revisions: Inspired by the definitions of the classes $\mathsf{SPT}$ and $\mathsf{MPT}$ we change the way in which iteration is bounded. The new conditions intuitively provide more freedom than the direct bounding the iterator $\mathcal{I}$ uses and do so in a way that is somewhat orthogonal to how Cook and Urquhart’s original recursor $\mathcal{R}$ did more complicated bounding. We are lead to consider a family of operators $\mathcal{I}_{k}$ where the condition that is imposed becomes less restrictive as $k$ grows. Over the chosen background theory, all of the operators $\mathcal{I}_{k}$ as well as $\mathcal{R}$ and $\mathcal{I}$ are of equal expressive power. However, the parameter $k$ is tightly connected to runtime-bounds for $\mathcal{I}_{k}$ in the $\mathsf{OTM}$ setting, and the use of higher values should allow expressing some functionals that feature more complicated interaction with the oracle more concisely. The proof that all considered operators are equivalent additionally covers a similarly defined family of iterators based on the idea of lookahead revisions that is introduced in Section 4. The final section specifies an efficient generation scheme for the values of the new iterators.

Kapron and Steinberg define the classes $\mathsf{SPT}$ and $\mathsf{MPT}$ using the $\mathsf{OTM}$ framework which is bound to a specific machine model. This paper transfers the notions of length and lookahead revisions to the machine independent setting of iteration schemes, where the number of iterations is determined by the length of a specified input parameter (which is a string over some finite alphabet). Our proofs introduce some interesting and useful idioms for programming in this setting.

1.1 Preliminaries

Let $\Sigma$ denote a finite alphabet that contains symbols 0 and 1, and $\Sigma^{*}$ the set of finite strings over $\Sigma$. The empty string is denoted $\epsilon$, and arbitrary elements of $\Sigma^{*}$ are denoted $\mathbf{a},\mathbf{b},\mathbf{c},\dots$. We attempt to bind names of string variables to their meanings as far as possible: $\mathbf{a}$ is associated with initial values, $\mathbf{b}$ with size-bounds $\mathbf{c}$ with values that a recursion or iteration is carried out over and $\mathbf{t}$ the previous values in a recursion or iteration. For $\mathbf{a}\in\Sigma^{*}$ let $|\mathbf{a}|$ to denote the length of $\mathbf{a}$ and $a_{i}$ its digits, i.e., $\mathbf{a}=a_{1}\dots a_{|\mathbf{a}|}$. We write $\mathbf{b}\subseteq\mathbf{a}$ to indicate that $\mathbf{b}$ is an initial segment of $\mathbf{a}$. We assume that we have symbols for all type-1 poly-time functions, for instance:

• •

Truncation: The 2-ary function sending $\mathbf{b}$ and $\mathbf{c}=c_{1}c_{2}\dots c_{|\mathbf{c}|}$, to $\mathbf{c}^{\leq|\mathbf{b}|}:=c_{1}\dots c_{|\mathbf{b}|}$, if $|\mathbf{b}|\leq|\mathbf{c}|$ and $\mathbf{c}$ otherwise. Note that always $\mathbf{c}^{\leq|\mathbf{b}|}\subseteq\mathbf{c}$ and $\mathbf{c}^{\leq|\varepsilon|}=\varepsilon$. For $\mathbf{c}^{\leq|\mathbf{c}|-1}$ we use the shorthand $\mathbf{c}\gg 1$.

• •

Tupling and projection functions $\langle\cdot,\ldots,\cdot\rangle$ and $\pi_{i}$, such that tupling is monotone with respect to length in each argument. Namely if $|\mathbf{a}_{i}|=|\mathbf{b}_{i}|$ for all $i$ apart from $k$, then $|\mathbf{a}_{k}|\leq|\mathbf{b}_{k}|$ if and only if $|\langle\mathbf{a}_{1},\dots,\mathbf{a}_{n}\rangle|\leq|\langle\mathbf{b}_{1},\dots,\mathbf{b}_{n}\rangle|$.

• •

Length minimum: We adopt the convention used by Cook and Urquart, i.e.

[TABLE]

We also use definition by cases extensively, relying on the fact that there is a polynomial-time conditional and avoid over-use of $\lambda$-abstractions via explicit function definition. Tupling functions that satisfy the demands above exist and are 1-1, but not bijective. In spite of this we still write $\lambda\langle\mathbf{a}_{1},\dots,\mathbf{a}_{k}\rangle.t[\mathbf{a}_{1},\dots,\mathbf{a}_{k}]$ as short hand for $\lambda\mathbf{b}.t[\pi_{1}\mathbf{b},\ldots,\pi_{k}\mathbf{b}]$. This is all done for the sake of readability.

1.2 $\lambda$-Definability

The treatment of the typed $\lambda$-calculus here follows that used by Cook and Urquart for their characterization of Mehlhorn’s class [7]. The set of types is defined inductively as follows:

• •

0 is a type

• •

$(\sigma\rightarrow\tau)$ is a type, if $\sigma$ and $\tau$ are types.

The set $Fn(\tau)$ of functionals of type $\tau$ is defined by induction on $\tau$:

• •

$Fn(0)=\Sigma^{*}$

• •

$Fn(\sigma\rightarrow\tau)=\{F|F:Fn(\sigma)\rightarrow Fn(\tau)\}$.

It is not hard to show that each type $\tau$ has a unique normal form

[TABLE]

where the missing parentheses are put in with association to the right. Hence a functional $F$ of type $\tau$ is considered in a natural way as a function of variables $X_{1},\ldots,X_{k}$, with $X_{i}$ ranging over $Fn(\tau_{i})$, and returning a natural number value:

[TABLE]

The level of a type is defined inductively: The level of type 0 is 0, and the level of the type $\tau$ written in the above normal form is 1 + the maximum of the levels of $\tau_{1},\ldots,\tau_{k}$. This paper is mostly only concerned with functionals of type level smaller or equal two.

Let $\mathbf{X}$ be a class of functionals. The set of $\lambda$-terms over $\mathbf{X}$, denoted $\lambda(\mathbf{X})$ is defined as follows:

• •

For each type $\sigma$ there are infinitely many variables $X^{\sigma},Y^{\sigma},Z^{\sigma},\ldots$ of type $\sigma$, and each such variable is a term of type $\sigma$.

• •

For each functional $F$ (of type $\sigma$) in $\mathbf{X}$ there is a term $F^{\sigma}$ of type $\sigma$.

• •

If $T$ is a term of type $\tau$ and $X$ is a variable of type $\sigma$, then $(\lambda X.T)$ is a term of type $(\sigma\rightarrow\tau)$ (an abstraction).

• •

If $S$ is a term of type $(\sigma\rightarrow\tau)$ and $T$ is a term of type $\sigma$, then $(ST)$ is a term of type $\tau$ (an application).

For readability, we write $S(T)$ for $(ST)$; we also write $S(T_{1},\ldots,T_{k})$ for $(\ldots((ST_{1})T_{2})\ldots T_{k})$, and $\lambda X_{1}\ldots\lambda X_{k}.T$ for $(\lambda X_{1}.(\lambda X_{2}.(\ldots(\lambda X_{k}.T)\ldots)))$.

The set of free variables of a lambda term can be defined inductively and are those that are not bound by a lambda abstraction. A term is called closed, if it has no free variables. In a natural way each closed $\lambda$-term $T$ of type $\tau$ represents a functional in $Fn(\tau)$. This correspondence is demonstrated in the standard way, by showing that a mapping of variables to functionals with corresponding type can be extended to a mapping of terms to functionals with corresponding type.

An assignment is a mapping $\varphi$ taking variables to functionals with corresponding type. Suppose $\varphi$ is an assignment and $T$ a $\lambda$-term over $\mathbf{X}$. The value $\mathcal{V}_{\varphi}(T)$ of $T$ with respect to $\varphi$ is defined by induction on $T$ as follows.

When $T$ is a variable, $\mathcal{V}_{\varphi}(T)$ is $\varphi(T)$. If $T=F^{\sigma}$ is a constant symbol for some $F\in\mathbf{X}$, then $\mathcal{V}_{\varphi}(T)=F$.

Suppose that $\tau=\tau_{1}\rightarrow\ldots\rightarrow\tau_{k}\rightarrow 0$. When $T$ has the form $\lambda X^{\sigma}.S^{\tau}$, $F$ is a type $\sigma$ functional and $F_{i}$ are type $\tau_{i}$ functionals, then

[TABLE]

where $\varphi^{\prime}(X^{\sigma})=F$, but $\varphi^{\prime}$ is otherwise identical to $\varphi$. When $T$ has the form $S^{\sigma\rightarrow\tau}R^{\sigma}$,

[TABLE]

It is not hard to show that if $T,S$ are terms such that $T$ is a $\beta$ or $\eta$ redex and $S$ is its contractum, then for all $\varphi$, $\mathcal{V}_{\varphi}(T)=\mathcal{V}_{\varphi}(S)$. A functional $F$ is represented by a term $T$ relative to an assignment $\varphi$ if $F=\mathcal{V}_{\varphi}(T)$.

Our goal in this paper is to prove the equivalence, with respect to $\lambda$-representability in the presence of poly-time type-1 functions, of type-2 functionals capturing different forms of recursion on notation. To this end we have the following definitions.

Definition 1.1**.**

Let $\mathsf{P}$ be the class of (type-1) poly-time functions, and $F,G$ be functionals. We say that $F$ is $\mathsf{P}$-reducible to $G$, denoted $F\preceq_{\lambda\mathsf{P}}G$ if $F$ is representable by a term of $\lambda(\mathsf{P}\cup\{G\})$, and that $F$ is $\mathsf{P}$-equivalent to $G$, denoted $F\equiv_{\lambda\mathsf{P}}G$, if $F\preceq_{\lambda\mathsf{P}}G$ and $G\preceq_{\lambda\mathsf{P}}F$.

We regularly use that $\mathsf{P}$-reducibility is a transitive relation, which is easily verified. We refer to the class of functionals representable by a term from $\lambda(\mathsf{P}\cup\{G\})$ as the class of functionals generated by $G$. Clearly two functionals are $\mathsf{P}$-equivalent if and only if they generate the same classes of functionals.

2 The Cook-Urquhart recursor and bounded iteration

Our starting point is the recursor that Cook and Urquart use to characterize a class of higher-order polynomial-time functionals [7]. This recursor is patterned on the scheme of limited recursion on notation introduced by Cobham [4] and its second-order variant, introduced by Mehlhorn [15]. In [12] it is proved that the type-two functionals definable in the Cook-Urquhart system coincide with Mehlhorn’s class. The recursor is defined as follows:

[TABLE]

Here, the length minimum $\mathsf{lmin}$ returns its left argument if it has strictly smaller length and the right argument otherwise as defined in the preliminaries. The schemes used by Cobham and Mehlhorn feature explicit external bounding that captures almost directly the notion of bounding by a polynomial (in the first-order setting we could easily use a scheme with explicit bounding by polynomials in the argument size, and as shown by [9] this may be extended to the second-order setting as well). In the Cook-Urquart recursor, this limiting is realized via an additional type-1 input $\psi$. Our first observation is that the limiting may instead be realized through a type-0 input.

Lemma 2.1** ($\mathcal{R}\equiv_{\lambda\mathsf{P}}\mathcal{R}_{0}$).**

The Cook-Urquart recursor and its restriction to constant bounding functions generate the same class of functionals. More specifically $\mathcal{R}$ is $\mathsf{P}$-equivalent to the functional

[TABLE]

Proof.

From the definition of $\mathcal{R}_{0}$ it is immediate that $\mathcal{R}_{0}\preceq_{\lambda\mathsf{P}}\mathcal{R}$. To see that also $\mathcal{R}\preceq_{\lambda\mathsf{P}}\mathcal{R}_{0}$ argue that it suffices to show that $\mathsf{max}\preceq_{\lambda\mathsf{P}}\mathcal{R}_{0}$, where $\mathsf{max}$ is the functional that maximizes return values of a function over the initial segments of a string, i.e. is recursively defined via $\mathsf{max}(\psi,\epsilon):=\psi(\epsilon)$ and

[TABLE]

Indeed, once this is proven $\mathcal{R}\preceq_{\lambda\mathsf{P}}\mathcal{R}_{0}$ follows from the equality

[TABLE]

where the second argument is the maximum with an additional digit added to make sure it is always strictly bigger than any value of $\psi$ on an initial segement of $\mathbf{c}$. This equality can be proven by an induction where the crucial point in the induction step is that the outer of the nested minima always chooses its left argument as value.

To see that the length maximization functional is definable using $\mathcal{R}_{0}$, note that the $\mathsf{argmax}$ functional, which returns the smallest initial segment where a given input-function assumes its maximum, can be defined from $\mathcal{R}_{0}$ via

[TABLE]

where $A(\psi,\mathbf{d},\mathbf{t})=\mathbf{d}$ if $\mathsf{lmin}(\psi(\mathbf{t}),\psi(\mathbf{d}))\neq\psi(\mathbf{t})$ and $\mathbf{t}$ otherwise. Since $\mathsf{max}(\psi,\mathbf{c})=\psi(\mathsf{argmax}(\psi,\mathbf{c}))$, it follows that $\mathsf{max}$ can be expressed and thus that $\mathcal{R}\preceq_{\lambda\mathsf{P}}\mathcal{R}_{0}$. ∎

As a further simplification of $\mathcal{R}$, it is possible to eliminate the reference to the current value of the recursion parameter at each step, that is, to replace a functional capturing a form primitive recursion on notation with one that captures functional iteration. This is known as a folklore result, but to the best of our knowledge does not appear explicitly in any previous work in this setting. The most similar characterization we are aware of is one based on typed loop-programs and appeared in [6]. In the case of primitive recursion, the equivalence with iteration was first explictly proved in [16].

For a function $\varphi\colon\Sigma^{*}\to\Sigma^{*}$ let the $n$-fold iteration $\varphi^{n}$ be inductively defined by $\varphi^{0}(\mathbf{a}):=\mathbf{a}$ and $\varphi^{n+1}(\mathbf{a}):=\varphi(\varphi^{n}(\mathbf{a}))$. An unbounded iterator would be a functional that takes $n,\mathbf{a}$ and $\varphi$ as inputs and returns $\varphi^{n}(\mathbf{a})$. Recall from the introduction, that there are polynomial-time computable $\varphi$ such that the function $\lambda\mathbf{a}.\lambda\mathbf{b}.\varphi^{|\mathbf{b}|}(\mathbf{a})$ exhibits exponential growth and is in particular not polynomial time computable. Thus, to capture the class of feasible functionals, the considered iterator needs to be bounded. We define the bounded iterator $\mathcal{I}$ by

[TABLE]

That is: $\mathcal{I}$ performs $|\mathbf{c}|$ iterations of the input function $\varphi$ on starting value $\mathsf{lmin}(\mathbf{a},\mathbf{b})$, truncating the resulting value after each iteration to be no longer than the bound $\mathbf{b}$.

Before we go on to prove the bounded iterator equivalent to the Cook-Urquart recursor, let us briefly discuss the choices we have taken in bounding. First off, it is easy to see that whether or not the starting value is truncated is irrelevant up to $\mathsf{P}$-equivalence. Furthermore, the definition of $\mathcal{I}$ is such that the bounding is done after $\varphi$ is applied. Another possibility would be to consider an iterator where the bounding is done on the argument side of $\varphi$, i.e. before its application. We give a short proof that the resulting iterator is equivalent.

Lemma 2.2**.**

($\mathcal{I}\equiv_{\lambda\mathsf{P}}\mathcal{I}^{\prime}$) Output-bounded iteration generates the same class of functionals as argument-bounded iteration. More specifically $\mathcal{I}$ is $\mathsf{P}$-equivalent to the functional

[TABLE]

Proof.

We prove that for all $\varphi,\mathbf{b},\mathbf{a},\mathbf{c}$,

[TABLE]

We prove () and (**) simultaneously by induction on $|\mathbf{c}|$. The case when $|\mathbf{c}|=0$ is clear, so suppose () and (**) hold for all $\mathbf{c}^{\prime}$ with $|\mathbf{c}^{\prime}|=k\geq 1$. Consider $\mathbf{c}$ with $|\mathbf{c}|=k+1$, say $\mathbf{c}=\mathbf{c^{\prime}}i$ where $|\mathbf{c}^{\prime}|=k$. Then

[TABLE]

and

[TABLE]

∎

We end the section with the proof that the bounded iterator, and its modification from the preceding lemma, generate the basic feasible functionals. That is, that they generate the same class of functionals as the Cook-Urquart recursor.

Lemma 2.3** ($\mathcal{R}\equiv_{\lambda\mathsf{P}}\mathcal{I}$).**

The Cook-Urquart recursor and the bounded iterator are $\mathsf{P}$-equivalent.

Proof.

The first implication, namely that $\mathcal{I}\preceq_{\lambda\mathsf{P}}\mathcal{R}$, follows from the equality

[TABLE]

that can be proven through a simple induction.

For the converse note that, by Lemma 2.1 the recursor is equivalent to its version $\mathcal{R}_{0}$ where the bounding is done via a constant instead of a function. Thus it suffices to prove that $\mathcal{R}_{0}\preceq_{\lambda\mathsf{P}}\mathcal{I}$. Furthermore note how close the expanded definition of the iterator is to the definition of $\mathcal{R}_{0}$:

[TABLE]

The main difference is that for the recursor the step function $\varphi$ is additionally given access to the value of the recursion parameter $\mathbf{c}$. We postpone the discussion of how to accomodate the additional bounding of the initial value to the end of the proof and show that the operator $\mathcal{R}_{0}^{\prime}$ defined by

[TABLE]

can be expressed by using the bounded iterator. To achieve this define

[TABLE]

In the above $\varphi$ has the type of a functional input of the recursor $\mathcal{R}_{0}^{\prime}$ and $\Phi(\varphi,\mathbf{b},\mathbf{c})$ has the type of a functional input for the bounded iterator for fixed $\varphi$, $\mathbf{b}$ and $\mathbf{c}$. We claim that for any $\mathbf{c}$, and $\mathbf{c}^{\prime}\subseteq\mathbf{c}$,

[TABLE]

and so, in particular

[TABLE]

which proves the $\mathsf{P}$-reducibility of $\mathcal{R}_{0}^{\prime}$ to $\mathcal{I}$. The equality (* ‣ 2) can be verified by fixing $\mathbf{c}$, an proving the following statement by induction on $\mathbf{c}^{\prime}$: if $\mathbf{c}^{\prime}\subseteq\mathbf{c}$, then (* ‣ 2) holds for $\mathbf{c}^{\prime}$. The base case of this induction follows from the properties we demanded the pairing functions to have. Next suppose that the assertion is true for $\mathbf{c}^{\prime}$. If $\mathbf{c}^{\prime}i\subseteq\mathbf{c}$, then it is also the case that $\mathbf{c}^{\prime}\subseteq\mathbf{c}$, and the induction hypothesis implies that (* ‣ 2) holds for $\mathbf{c}^{\prime}$. But then

[TABLE]

Where the last equality uses the properties of the tupling functions again and the fact that $\mathcal{R}_{0}^{\prime}(\varphi,\mathbf{b},\mathbf{a},\mathbf{c^{\prime}}i)$ is either strictly shorter than $\mathbf{b}$ or equal to $\mathbf{b}$.

Finally, to change the initial value, define $H$ as follows:

[TABLE]

then

[TABLE]

and thus we obtain that $\mathcal{R}_{0}\preceq_{\lambda\mathsf{P}}\mathcal{R}_{0}^{\prime}\preceq_{\lambda\mathsf{P}}\mathcal{I}$ and with the fact $\mathcal{R}\preceq_{\lambda\mathsf{P}}\mathcal{R}_{0}$ from Lemma 2.1 also the desired $\mathsf{P}$-reducibility $\mathcal{R}\preceq_{\lambda\mathsf{P}}\mathcal{I}$. ∎

3 Iteration with Constant Length Revision

Both the Cook-Urquart recursor $\mathcal{R}$ as well as the bounded iterator $\mathcal{I}$ require an absolute bound on the size of intermediate value encountered during a recursion. Specifying such a bound a priori can be cumbersome and this section provides an alternative way of bounding an iteration that is inspired by the classes $\mathsf{SPT}$ and $\mathsf{MPT}$ we considered in earlier work [13, 11]. The elementary notion used in the definition of $\mathsf{SPT}$ is that of a length revision. In an $\mathsf{OTM}$ computation a length revision is encountered whenever the answer to an oracle query is longer than any previous response. This notion of a length revision can easily be translated to the realm of recursion schemes: in a recursive definition a length revision happens when the return value of the step function is bigger than any of the values returned earlier. In particular, define

[TABLE]

where $\ell\leq n$ is maximum such that the sequence of applications contains no more than $k$ length revisions, that is an application $\varphi(\mathbf{t})$ where $|\varphi(\mathbf{t})|$ exceeds $|\mathbf{a}|$ and $|\varphi(\mathbf{t}^{\prime})|$ for any previous call. In particular, when $k=0$, this means that no calls return a value that exceeds $|\mathbf{a}|$. For $k\geq 0$, the $k$-revision iterator $\mathcal{I}_{k}$ is the functional defined by

[TABLE]

Superficially, this definition is similar to that of the bounded iterator $\mathcal{I}$ from the last section. The functional $\mathcal{I}_{k}$ iterates a function where the iteration is bounded by $k$ just like the bounded iterator does for each fixed bounding argument $\mathbf{b}$. The essential difference is that $k$ is a statically fixed parameter, i.e., $\mathcal{I}_{k}$ constitutes a family of iterators. Our goal is to show that for each fixed $k$ the operator $\mathcal{I}_{k}$ is $\mathsf{P}$-equivalent to the bounded iterator $\mathcal{I}$ (Theorem 4.3 below).

Without restrictions on $k$, neither of the reducibilities required to prove that $\mathcal{I}_{k}\equiv_{\lambda\mathsf{P}}\mathcal{I}$ are obvious. However, the claim that $\mathcal{I}_{k}\preceq_{\lambda\mathsf{P}}\mathcal{I}$ should appear reasonable given the $\mathsf{OTM}$-based characterization of the basic feasible functionals [10]. As proven in the last section, $\mathcal{I}$ is $\mathsf{P}$-equivalent to $\mathcal{R}$ and thus it is enough to check that $\mathcal{I}_{k}$ is a basic feasible functional, i.e., that $\mathcal{I}_{k}$ is computable by an $\mathsf{OTM}$ whose run-time is bounded by a second-order polynomial. This may be done in a straightforward way, but it is important to note that the complexity of the bounding polynomial (in terms of the depth of calls to the function input, rather than the degree) increases with $k$. In particular, while $\mathcal{I}_{k}$ is $\mathsf{P}$-equivalent to $\mathcal{I}$ for every $k$, the revision parameter $k$ provides a finer delineation of expressive power.

Without an appeal to the $\mathsf{OTM}$-based characterization, showing the $\mathsf{P}$-equivalence of $\mathcal{I}_{k}$ and $\mathcal{I}$ becomes more of a challenge, although the case for $\mathcal{I}_{0}$ is relatively straightforward:

Lemma 3.1** ($\mathcal{I}_{0}\preceq_{\lambda\mathsf{P}}\mathcal{I}$).**

The [math]-revision iterator is $\mathsf{P}$-reducible to the bounded iterator.

Proof.

The main hurdle is to account for the difference in how the violation of the bound is realized: $\mathcal{I}_{0}$ defaults to the previous value in the iteration while $\mathcal{I}$ defaults to the value it is given as bound. Set

[TABLE]

Then $\mathcal{I}_{0}(\varphi,\mathbf{a},\mathbf{c})$ can be obtained from $\mathcal{I}(\lambda\mathbf{t}.G(\varphi,\mathbf{t},\mathbf{a}),\mathbf{a},\mathbf{a}\mathtt{0},\mathbf{c})$ by simply dropping the last bit. Since the definition of $G$ only uses type-1 polynomial time operations and application, the $\mathsf{P}$-reducibility follows. ∎

Note that for unrestricted iteration it holds that $\varphi^{n}(\varphi^{n^{\prime}}(\mathbf{a}))=\varphi^{n+n^{\prime}}(\mathbf{a})$. The following observation points out a similar additivity property for $\varphi^{n}_{!k}$ and is the starting point for recursively constructing $\mathsf{P}$-reductions of $\mathcal{I}_{k}$ to $\mathcal{I}$:

Lemma 3.2**.**

For given $\varphi$, $\mathbf{a}$ and numbers $k$ and $n$ set

[TABLE]

then $\ell\leq n$ and it holds that

[TABLE]

Proof.

Since $n$ always fulfills the condition in the minimization, it follows that $\ell\leq n$. To prove $(*)$ we first note that the minimization condition may be satisfied in two different ways. It may be the case that $\varphi$ gives the same return value on all of the strings $\varphi_{!k}^{\ell}(\mathbf{a}),\dots,\varphi_{!k}^{n-1}(\mathbf{a})$. In this case there will be no further length revisions, and so $\varphi^{n-\ell}_{!1}(\varphi^{\ell}_{!k}(\mathbf{a}))=\varphi^{n-\ell}(\varphi^{\ell}_{!k}(\mathbf{a}))=\varphi^{n}_{!(k+1)}(\mathbf{a})$. Thus suppose that it is not the case that $\varphi$ is constant on these strings and let $j$ be such that $\ell\leq j\leq n-1$ and $\varphi(\varphi^{j}_{!k}(\mathbf{a}))\neq\varphi^{\ell+1}_{!k}(\mathbf{a})$. By definition of $\ell$, the strings $\varphi_{!k}^{\ell}(\mathbf{a}),\ldots,\varphi_{!k}^{n}(\mathbf{a})$ are still all equal. Then $\varphi(\varphi^{j}_{!k}(\mathbf{a}))=\varphi(\varphi^{l}_{!k}(\mathbf{a}))$ and $\varphi(\varphi^{l}_{!k}(\mathbf{a}))$ and $\varphi^{l+1}_{!k}(\mathbf{a})$ can only be different if the $(\ell+1)$-st call to $\varphi$ triggers the $(k+1)$-st length revision. Thus, in this case $\varphi_{!1}^{m}(\varphi^{\ell}_{k}(\mathbf{a}))=\varphi(\varphi^{\ell}_{!k}(\mathbf{a}))=\varphi^{\ell+m}_{!(k+1)}(\mathbf{a})$ for any $m$ and in particular $(*)$ must hold. ∎

In fact, the above proof proves the following slightly stronger statement.

Corollary 3.3**.**

The equality in the last Lemma may be replaced by $\varphi^{n}_{!(k+1)}(\mathbf{a})=\varphi^{n-\ell-1}_{!0}(\varphi(\varphi^{\ell}_{!k}(\mathbf{a})))$.

This allows us to establish the following.

Lemma 3.4** ($\mathcal{I}_{k}\preceq_{\lambda\mathsf{P}}\mathcal{I}$).**

For $k\geq 1$, the $k$-revision iterator is $\mathsf{P}$-reducible to the bounded iterator.

Proof.

We proceed by induction on $k$. The case of $k=0$ has been taken care of in Lemma 3.1. Suppose that the Lemma holds for $k$. We must now define $\mathcal{I}_{k+1}$ using $\mathcal{I}$. By Lemma 3.2 it is sufficient to show that there exists a function that on inputs $\varphi$, $\mathbf{a}$, $k$ and $n$ returns the value $\ell$ and is $\mathsf{P}$-reducible to $\mathcal{I}$. First note that the condition $\varphi^{i}_{k}(\mathbf{a})=\varphi^{j}_{k}(\mathbf{a})$ can be checked by a function from $\lambda(\mathsf{P}\cup\{\mathcal{I}_{k}\})\subseteq\lambda(\mathsf{P}\cup\{\mathcal{I}\})$, where the inclusion follows by the induction hypothesis. Now all that remains is to use $\mathcal{I}$ to characterize the bounded quantification and search used to define $\ell$ in Corollary 3.3. Define the following functionals:

[TABLE]

We first show that $U\preceq_{\lambda\mathsf{P}}\mathcal{R}$ and appeal to Lemma 2.3 to see that it is $\mathsf{P}$-reducible to $\mathcal{I}$. Define

[TABLE]

Then $U(\psi,\mathbf{a},\mathbf{c})=\mathcal{R}(\lambda\mathbf{t}.\lambda\mathbf{d}.V(\psi,\mathbf{a},\mathbf{t},\mathbf{d}),\lambda\mathbf{d}.\mathtt{0},\epsilon,\mathbf{c})$. Since the definition of $V$ only uses polynomial-time computable type-1 functions and application we conclude $U\preceq_{\lambda\mathsf{P}}\mathcal{R}$. To show that $M\preceq_{\lambda\mathsf{P}}\mathcal{I}$, first define

[TABLE]

and define

[TABLE]

Then $M(\psi,\mathbf{a},\mathbf{c})=\mathbf{m}=\mathcal{I}(\lambda\mathbf{t}.N(\psi,\mathbf{a},\mathbf{t}),A(\psi,\mathbf{a}),\mathbf{c}\mathtt{0},\mathbf{c})\gg 1$. In particular, if $\mathbf{m}$ ends in $\mathtt{0}$, then $\mathbf{m}=\mathtt{0}^{j+1}$ and if it ends in $\mathtt{1}$ then $\mathbf{m}=\mathtt{0}^{|\mathbf{c}|+1}\mathtt{1}$. ∎

4 Iteration with Constant Lookahead Revision

Moving to lookahead revision, the definition is similar. Consider the following variant of function iteration

[TABLE]

where $\ell\leq n$ is maximum such that the sequence of applications contains no more than $k$ lookahead revisions, that is an application $\varphi(\mathbf{t})$ where $|\mathbf{t}|$ exceeds $|\mathbf{t}^{\prime}|$ for any previous call $|\varphi(\mathbf{t}^{\prime})|$. Note that we have not included the initial call $\varphi(\mathbf{a})$ as a lookahead revision (choosing to do so would not change any results below.) Then, for $k\geq 0$, the $k$-lookahead revision iterator $\mathcal{I}^{\prime}_{k}$ is the functional such that

[TABLE]

We now consider the relative power of $\mathcal{I}^{\prime}_{k}$.

Lemma 4.1**.**

For any $k\geq 0$, $\mathcal{I}^{\prime}_{k}\preceq_{\lambda\mathsf{P}}\mathcal{I}_{k}$.

Proof.

We claim that $\mathcal{I}^{\prime}_{k}(\varphi,\mathbf{a},\mathbf{c})=\varphi(\mathcal{I}_{k}(\varphi,\mathbf{a},\mathbf{c}\gg 1))$. This is clear in the case that there are no more than $k$ length revisions in the evaluation of $\mathcal{I}_{k}(\varphi,\mathbf{a},\mathbf{b},\mathbf{c}\gg 1)$, as any lookahead revision corresponds exactly to a preceding length revision, and so $\mathcal{I}^{\prime}_{k}(\varphi,\mathbf{a},\mathbf{c})=\varphi^{|\mathbf{c}|}(\mathbf{a})=\varphi(\mathcal{I}_{k}(\varphi,\mathbf{a},\mathbf{c}\gg 1))$. Otherwise suppose that $\mathcal{I}_{k}(\varphi,\mathbf{a},\mathbf{b},\mathbf{c}\gg 1)=\varphi^{\ell}(\mathbf{a})$, which means in particular that $\ell$ is the minimum value less than $|\mathbf{c}|$ such that evaluating $\varphi^{\ell+1}(\mathbf{a})$ results in $k+1$ length revisions. But then $\ell$ is the minimum value less than $|\mathbf{c}|$ such that $\varphi^{\ell+2}(\mathbf{a})$ results in $k+1$ length revisions. But this means $\mathcal{I}^{\prime}_{k}(\varphi,\mathbf{a},\mathbf{c})=\varphi^{\ell+1}(\mathbf{a})=\varphi(\mathcal{I}_{k}(\varphi,\mathbf{a},\mathbf{c}\gg 1))$. ∎

Lemma 4.2**.**

For any $k\geq 0$, $\mathcal{I}^{\prime}\preceq_{\lambda\mathsf{P}}\mathcal{I}^{\prime}_{k}$.

Proof.

Unfortunately, the situation is a little less straightforward than we might hope, as $\mathcal{I}^{\prime}$ and $\mathcal{I}^{\prime}_{k}$ differ slightly in the way they do bounding. $\mathcal{I}^{\prime}_{k}$ expects queries to be bounded in length by previous queries while $\mathcal{I}^{\prime}$ uses an explicit bound $\mathbf{b}$. Define $\psi$ as follows:

[TABLE]

Claim. For all $\mathbf{a},\mathbf{b},\mathbf{c}$, $\mathcal{I}^{\prime}_{k}(\lambda\mathbf{t}.\psi(\mathbf{t},\mathbf{a},\mathbf{b}),\mathbf{b}\mathtt{0},\mathtt{0}\mathbf{c})=\mathsf{lmin}(\mathcal{I}^{\prime}(\varphi,\mathbf{a},\mathbf{b},\mathbf{c}),\mathbf{b})\mathtt{1}$

To prove this claim, first note the in the iteration on the left, the first call to $\psi$ is $\mathbf{b}\mathtt{0}$, of length $|\mathbf{b}|+1$. All subsequent calls are clearly bounded by $|\mathbf{b}|+1$. So there will be no lookahead revisions in this iteration and it remains to prove equality without consideration of the lookahead bound $k$. We use induction on $\mathbf{c}$. When $\mathbf{c}=\epsilon$,

[TABLE]

Now assume that the claim holds for $\mathbf{c}$. Then

[TABLE]

Now define $\mathcal{I}^{\prime\prime}$ as follows:

[TABLE]

First note that $\mathcal{I}^{\prime\prime}\preceq_{\lambda P}\mathcal{I}^{\prime}_{k}$, as definition by cases is a poly-time operation. When $\mathbf{c}=\epsilon$, $\mathcal{I}^{\prime\prime}(\varphi,\mathbf{a},\mathbf{b},\mathbf{c})=\mathbf{a}=\mathcal{I}^{\prime}(\varphi,\mathbf{a},\mathbf{b},\mathbf{c})$. Otherwise, by the claim,

[TABLE]

so that

[TABLE]

∎

Putting everything together, we have a characterization which is the main result of this paper.

Theorem 4.3**.**

For every $k\geq 0$, $\mathcal{I}\equiv_{\lambda\mathsf{P}}\mathcal{I}_{k}\equiv_{\lambda\mathsf{P}}\mathcal{I}^{\prime}_{k}\equiv_{\lambda\mathsf{P}}\mathcal{I}^{\prime}$.

5 More efficient approaches

The implementation of $\mathcal{I}_{k}$ by $\mathcal{I}$ given in Lemma 3.4 requires considerable overhead, involving a bounded quanitification and bounded search at each step. An implementation which directly follows this definition is poly-time, but is needlessly complex. The following observation (which in this setting correpsonds to tail-recursion elimination) will simplify things considerably. In particular, we note an alternate characterization of $\varphi^{n}$: $\varphi^{0}(\mathbf{a})=\mathbf{a}$ and $\varphi^{n+1}(\mathbf{a})=\varphi^{n}(\varphi(\mathbf{a}))$. This leads to the following characterization of $\varphi^{n}_{!k}$.

Lemma 5.1**.**

For all $n,k\geq 0$ we have

[TABLE]

Proof.

We prove by induction on $k$ that the claim holds for all $n$. When $k=0$, iteration stops (absolutely) if $|\varphi(\mathbf{a})|>|\mathbf{a}|$, otherwise it proceeds to the next step. Now assume for $k$ that the claim holds for all $n$. We show that for $k+1$ it holds for all $n$, by induction on $n$. When $n=0$ this is immediate. Assume that it holds for $n$, and consider $\varphi^{n+1}_{!(k+1)}(\mathbf{a})$. Clearly, if $|\varphi(\mathbf{a})|\leq|\mathbf{a}|$, no length revision occurs on the first call, and so $k+1$ are still available for the remaining $n$ calls. Otherwise, only $k$ length revisions are available for the remaining calls. ∎

We also note that, implicit in the proof of Lemma 3.4, is an implementation which is also efficient – in particular, if we “unwind” the induction, we are eventually left relying only on $\mathcal{I}_{0}$. As described in [11], §4.3, we can implement the resulting definition using a form of “re-entrant” recursion. We may view the violation of the length-revision bound as triggering an exception, which may then be caught by an exception handler which re-starts the recursion at the point after the offending oracle call has taken place.

6 Conclusions and Future Work

We have provided a new linguistic characterization of the higher-order polynomial time via iteration schemes that restrict the number of times a step function, presented as an oracle, may return an answer or be presented an input which in length exceeds all previous answers (resp. queries). The characterization and the methods used to prove it lead to a number of questions and potential directions for future research.

The characterization provided in this paper could be termed intrinsic, in that no external bounding is present in the iteration schemes $\mathcal{I}_{k}$ and $\mathcal{I}^{\prime}_{k}$. The condition itself, however, appears to depend on the dynamics of a particular computation. On its face it is not a structural/syntactic restriction, as is usual in implicit computational complexity. This suggests two directions for further research. The first is to investigate the possibility of statically deriving bounds on query revision. The second is to investigate distinctions on how computational resources are bounded as suggested by this and related work, for example intrinsic versus extrinsic, dynamic versus static, and feasibly constructive versus non-feasibly constructive (an example of non-feasibly constructive bounding would be the second-order polynomials of [10]). A related observation is that iteration with bounded query revision appears to be a generalization of non-size-increasing computation [8]. This apparent connection merits further investigation.

In §5 above, we begin to explore the interplay between familiar programming techiques from the implemenation of functional programming languages (e.g, tail-recursion elimination) with respect to the efficient implementation of our iteration schemes. We have also noted that the introduction on control primitives (e.g., catch and throw) may be relevant to the characterization of complexity classes in this setting. We note that such control operators have been shown in [3] to be relevant to the general characterization of sequential higher-order computation. Here we only scratch the surface. Further investigation of these and related techniques in the context of linguistic characterizations of computational complexity could prove fruitful.

As noted at several points in our development, there are issues of finer-grained complexity that arise from our translations. This gives rise to natural questions on the efficiency, or syntactic complexity, of translations, which bear further investigation.

Finally, while we have drawn an analogy between $\mathsf{OTM}$s with bounded query revision (as introduced in [11]) and certain recursion schemes, we have not investigated just how closely related they are. While the equivalences proved in [11] and in this paper imply an equivalence for all the models, a direct proof would be very interesting in furthering our understanding of poly-time $\mathsf{OTM}$s. It would be very rewarding if a simplified proof of the equivalence of [10] could be obtained in this setting.