Applicative Control and Computational Complexity

Abstract

We establish a tight correspondence between three major complexity classes and simple syntactic restrictions on applicative programs in the simply typed lambda calculus with a recurrence operator. The syntactic restrictions considered are: recurrence arguments cannot be passed as computed values (“input-driven terms”), abstracted higher-order variables can appear at most once (“solitary terms”), and abstracted variables cannot be eventually nested (“separated terms”).

We show that the functions over word algebras represented by inputdriven terms are precisely the poly-time functions (a result akin to [8] (Chapter 24.2)). When input-driven recurrence is permitted over all finite types, the elementary functions are obtained (a result akin to [1]). When terms are further restricted to solitary ones, even recurrence in all finite type yields only the poly-time functions. Finally, separated terms generate exactly the poly-space functions.

The interest in the approach discussed here lies in its simplicity: the complexity characterizations are based on restricted use of standard applicative constructs, rather than a syntactic overlay as in ramified recurrence [3], [12], [15], [7], [21]. However, approaches based on ramified recurrence are more powerful than simple syntactic control, as well as more conceptually and methodologically coherent. Thus, the two approaches are complementary and of independent interest.