Type-two Iteration with Bounded Query Revision

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

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.

In Thomas Seiller and Steffen Jost: Proceedings Third Joint Workshop on Developments in Implicit Computational complExity and Foundational & Practical Aspects of Resource Analysis (DICE-FOPARA 2019), Prague, Czech Republic, 6.4.2019 - 7.4.2019, Electronic Proceedings in Theoretical Computer Science 298, pp. 61–73.
Published: 14th August 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.298.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org