[Prev][Next][Index][Thread]
Lower bounds on optimal evaluation
To the Types forum:
We thought the following recent result was interesting enough that it
warranted an announcement in the Types forum. A paper on the subject
is being written as you are reading this, and will be available
shortly from the WWW page http://www.cs.brandeis.edu/~mairson. We do
not think that the result spells the end of the "optimal evaluation"
enterprise, but without doubt, the theorem motivates the need for an
"optimal reevaluation."
Yours sincerely,
Andrea Asperti
University of Bologna
asperti@cs.unibo.it
Harry Mairson
Brandeis University
mairson@cs.brandeis.edu
-----------------------------------------------------------------------
Parallel beta reduction is not elementary recursive
-----------------------------------------------------------------------
We analyze the inherent complexity of implementing L\'evy's notion of
{\em optimal evaluation} for the $\lambda$-calculus, where similar
redexes are contracted in one step via so-called {\em parallel
$\beta$-reduction.} Optimal evaluation was finally realized by
Lamping, who introduced a beautiful graph reduction technology for
sharing {\em evaluation contexts} dual to the sharing of {\em values}.
His pioneering insights have been modified and improved in subsequent
implementations of optimal reduction.
We prove that the cost of parallel $\beta$-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(2^n)$, $O(2^{2^n})$,
$O(2^{2^{2^n}})$, or in general, $O(f(n))$ where $f(n)$ is any fixed
stack of 2s with an $n$ on top.
A key insight, essential to the establishment of this nonelementary
lower bound, is that by a straightforward rewriting based on
$\eta$-expansion, any simply-typed $\lambda$-term can be reduced to
normal form in a number of parallel $\beta$-steps that is only linear
in the length of the explicitly-typed term. The result follows from
Statman's theorem that deciding equivalence of typed $\lambda$-terms
is not elementary recursive.
The main theorem gives a lower bound on the work that must be done by
{\em any} technology that implements L\'evy's notion of optimal
reduction. However, in the significant case of Lamping's solution, we
make some important remarks addressing {\em how} work done by
$\beta$-reduction is translated into equivalent work carried out by
his bookkeeping nodes. In particular, we identify the computational
paradigms of {\em superposition} of values and of {\em higher-order
sharing}, appealing to compelling analogies with quantum mechanics and
SIMD-parallelism.