Lambda calculi and linear speedups

www.cs.chalmers.se Abstract. The equational theories at the core of most functional pro-gramming are variations on the standard lambda calculus. The best-known of these is the call-by-value lambda calculus whose core is the value-beta computation rule (λx.M)V → M [V/x] where V is restricted to be a value rather than an arbitrary term. This paper investigates the transformational power of this core theory of functional programming. The main result is that the equational theory of the call-by-value lambda calculus cannot speed up (or slow down) programs by more than a constant factor. The corresponding result also holds for call-by-need but we show that it does not hold for call-by-name: there are programs for which a single beta reduction can change the program’s asymptotic complexity.