Abstract

In previous work I have studied a functional calculus which defines only polynomial time functions while still allowing for nested structural recursive definitions. It was shown that all functions computable in polynomial time and simultaneously linear space are representable in the system. An exact characterisation of the expressive power remained open although Aehlig and Schwichtenberg managed to define all of PTIME in an extension of the language.

I will show in this talk that a non-size increasing function (|f(x)|<=|x|) is representable in the original system iff it is computable in polynomial time, thus in particular characteristic functions of problems in P are representable. A noteworthy point is that polynomials themselves are not representable.

I will also show that the definable functions in an extension of the system with general recursion are precisely those which are computable in polynomial space together with an unbounded stack or equivalently in time O(exp(p(n))) for some polynomial p(n).

One direction of this proof involves a novel encoding of linear (use-once) functions as argument-result pairs with nondeterminism: when constructing a function one guesses an argument and computes the corresponding result. To apply a function one checks whether the actual argument equals the previously guessed one and in this case returns the precomputed result. Otherwise an error results.