Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
5th June, 1998: Harry Mairson
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 5th June, 1998: Harry Mairson

Speaker: Harry Mairson, Brandeis University
Title: Parallel Beta Reduction is Not Elementary Recursive
Time: 5th June, 1998, 14:00
Abstract:

We investigate a hybrid procedure-calling protocol known as optimal evaluation, which incorporates the best features of call-by-value and call-by-name: arguments to procedures are evaluated at most once, and only if they are needed. We examine this hybrid scheme as embedded in the lambda-calculus, the programming language enthusiast's tabula rasa. Optimal evaluation was finally realized by Lamping, who introduced a beautiful graph reduction technology for sharing evaluation contexts dual to the sharing of values.

We prove that the cost of parallel beta-reduction -- the "shared procedure call" that is the fundamental operation of optimal reduction -- is not bounded by any Kalmar-elementary recursive function. Not merely do we establish that the parallel beta-step cannot be a unit-cost operation, we demonstrate that the time complexity of implementing a sequence of n parallel beta-steps is not bounded as O(2n), O(22n), O(222n), or in general, O(K(a,n)) where K(a,n) is a fixed stack of a 2s with an n on top.

The main theorem gives a lower bound on the work that must be done by any technology that implements optimal reduction. In the significant case of Lamping's solution, we make some important remarks addressing how work done by beta-reduction is translated into other graph reduction operations. In particular, we identify the computational paradigms of superposition of values and of higher-order sharing, appealing to compelling analogies with quantum mechanics and SIMD-parallelism.

(Joint work with Andrea Asperti, Universita di Bologna, and presented at the ACM POPL (Principles of Programming Languages) conference, January 1998.)