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

Klaus Aehlig, Helmut Schwichtenberg

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 pro…