A BRICS Mini-Course
May 25-28, 1999
Lectures by
Julia Lawall, jll@cs.brandeis.edu
Department of Computer Science, Brandeis University, Waltham, Massachusetts 02254
Harry Mairson, mairson@cs.brandeis.edu
Department of Computer Science, Brandeis University, Waltham, Massachusetts 02254
In foundational research some two decades ago, Jean-Jacques Lévy attempted to formalize what an ``optimally efficient'' reduction strategy of the lambda calculus would look like, encompassing correctness (reductions always derive existent normal forms) and optimality (maximal sharing of similar redexes). These dual features can be thought of roughly as a synthesis of the correctness of call-by-name, with the efficiency of call-by-value.
Around 1990, John Lamping invented a graph-based implementation that realized Lévy's specification, by introducing a technology for sharing evaluation contexts as well as values. His invention was very similar to Jean-Yves Girard's proofnets for multiplicative-exponential linear logic; subsequently Georges Gonthier showed how a mundane version of Girard's ``geometry of interaction'' could give a semantics to Lamping's graphs. Further, Gonthier's formulation was very similar to that of games for linear logic, with application to full abstraction.
In this minicourse, we will introduce optimal graph reduction for lambda calculus, paying particular attention to implementations of sharing. We will discuss as well the semantics of this graph reduction, and how implementations of sharing can be extended to implement graph reduction for languages with explicit control, especially Filinski's symmetric lambda calculus, and Parigot's lambda-mu calculus. Finally, we discuss the inherent complexity of the parallel beta step, the operation that is at the heart of optimal graph reduction.
Julia Lawall is a Research Associate in Computer Science at Brandeis University. She received her Ph.D. in Computer Science from Indiana University in 1994, and has also held teaching and research positions at Oberlin College and IRISA/Rennes. Her research focuses on optimal reduction, continuations, and partial evaluation.
Harry Mairson is Professor of Computer Science at Brandeis University. He received his Ph.D. in Computer Science from Stanford University in 1984. Before coming to Brandeis, he worked at INRIA and Oxford as a research associate. His recent research has applied his original training in algorithms, data structures, and lower bounds to complexity-theoretic questions concerning programming languages, including database query languages, type systems, and optimal graph reduction.
Building on intuitions derived from the familiar graph implementation of call-by-need reduction, we show how to construct an implementation of the lambda calculus that is optimal, in the sense of Lévy. The implementation is inspired by the proof nets of linear logic. Indeed, there are many such implementations, of which we present two, based on the call-by-name and call-by-value encodings of intuitionistic logic into linear logic, respectively. Because the resulting graphs are proof nets, they can be simplified using standard, but non-optimal, reduction rules. We conclude by showing how to implement these rules locally, avoiding any unnecessary duplication of computation.
Context semantics is a kind of rarified flow analysis, in which the traversal of a static graph is directed by a global state (the ``context'') that records the history of the path. In essence, contexts are detailed codings of moves in a ``readback game'' played between an Opponent who wants to know the Bohm tree of a sharing graph, and the Player who has a copy of the graph. The connections with game semantics, full abstraction theorems, and linear logic will be clarified, as will be the relation of the semantics to Girard's ``geometry of interaction'', Hilbert spaces, etc.
We begin with the context semantics of a trivial lambda calculus, where each variable occurs at most once. (This restriction is commensurate with multiplicative linear logic, but without exponentials.) In this simplified venue, we consider the semantics of lambda (par) and apply (times) nodes, but can ignore the semantics of sharing nodes, which are not needed. We show that graph reduction preserves the semantics exactly, and that contexts code paths in the Bohm tree. The restriction of contexts to these paths yields a ``semantics of accessible paths'', equivalent to the codings of moves in a game.
Next, we introduce the context semantics of the ``croissant'' and ``bracket'' operators that control sharing. Again, the semantics is preserved by reduction. We compare notions of ``global'' versus ``local'' graph reduction, and show how global reductions do not preserve the semantics, but in a precise sense preserve the idea of accessible paths.
We have seen that the proof nets of linear logic can be used as the basis of an optimal implementation of the lambda calculus. Linear logic does not make asymmetric distinctions between inputs and outputs, suggesting that a similar strategy can be used to implement optimal reduction of a language with first-class control operators. The essential problem in implementing such a language is to encode continuations so that they can be duplicated incrementally, without destroying optimality. Our solution is derived from a surprisingly simple transformation on graphs of continuation-passing style terms.
As an application of this technique, we show how to achieve optimal reduction of the lambda calculus extended with Scheme's call/cc operator. The result is an implementation of call/cc that is independent of evaluation order. We can apply the same approach to any language whose control operators can be encoded in the pure lambda calculus using a continuation-passing style translation. In particular, we will consider Parigot's lambda-mu calculus and Filinski's symmetric lambda calculus.
Optimal graph reduction introduces an implementation of ``parallel beta reduction'', but at what computational cost? While parallel beta reduction is nominally implemented by one graph step, many ``sharing reductions'' may be needed prior to that single graph step.
We present the theorem of Asperti and Mairson that the cost of a parallel beta step cannot be bounded by any Kalmar-elementary recursive function. A key insight is that any simply-typed lambda term can be reduced to normal form in a polynomial number of parallel beta steps, by using eta-expansion to bound the effect of sharing nodes. The result follows from Statman's theorem that deciding equivalence of typed terms is not elementary recursive.
The theorem gives a lower bound on the work that must be done by any technology that implements Lévy's notion of optimal reduction. In the case of graph reduction, we give an algorithmic analysis of sharing node interactions, emphasizing the phenomena of ``superposition'' and of ``higher order sharing'', appealing to analogies with quantum mechanics and SIMD-parallelism.
Even though this result seems to be a very negative one, it isn't. We will try to explain why.