A syntactical analysis of non-size-increasing polynomial time computation

TL;DR

This paper proves that functions definable in a specific affine linear typed lambda-calculus with iteration are polynomial time computable, providing explicit bounds for their computational complexity.

Contribution

It offers a syntactical proof establishing polynomial time computability for functions in a particular lambda-calculus, with explicit bounds that are easy to compute.

Findings

All functions definable in the calculus are polynomial time computable.

Explicit polynomial bounds for these functions are provided.

The proof is syntactical and constructive.

Abstract

A syntactical proof is given that all functions definable in a certain affine linear typed lambda-calculus with iteration in all types are polynomial time computable. The proof provides explicit polynomial bounds that can easily be calculated.