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

## Key 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.