A BRICS Mini-Course
October 27, 1996
Lectures by
Kristoffer Høgsbro Rose
The mini-course is five 45-minute lectures that can be attended by everyone; the situation the day before the Verification '96 autumn school makes combination possible.
The basics of making the lambda-calculus operational by defining substitution as a stepwise primitive operation. We discuss the problems this presents, in particular the danger of introducing too many steps such that, for example, simply typed terms are no longer normalising: we show how one proves that an explicit substitution calculus has PSN (preserves strong normalisation of beta-reduction).
In recent years a large number of ``explicit substitution calculi'' have been proposed that only vary in the representation of variable binding: lambda\upsilon, lambda\chi, lambdas, lambdat, and lambdax. We show that these calculi all have essentially the same reductions, in particular the renaming overhead is negligible with respect to normalisation.
One of the most intriguing problems in using lambda calculus as a computational model is how to capture memory. We discuss one technique for doing this, an address oracle based on the so-called lambda-graph rewriting of Wadsworth. It turns out that the techniques combine well with explicit substitution to form computational models that can be used to measure not only time but also space behaviour of lambda-reduction.
We explain how explicit substitution provides a technique for separating the issues of primitives and reduction strategies, and show how an explicit substitution calculus equipped with a strategy can be used to derive an abstract machine. We exploit the techniques of all the previous chapters to give formally understandable justifications for the techniques used for sharing, recursion, and parallelism, in ``real'' implementations of functional programming languages.
We explain how explicit substitution can be used to facilitate reasoning about higher-order rewriting, both by translating higher-order rewrite systems into explicit substitution as well as defining higher-order rewriting through explicit substitution. A few additional complications are encountered when modeling addresses which lead to the notion of explicit recursion.
Knowledge of lambda-calculus [2] as well as some knowledge of the most basic rewriting techniques is assumed (the lecture notes include a summary of the notions and notations actually used).
Olivier Danvy <danvy@brics.dk>
Stefan Dziembowski <stefand@mimuw.edu.pl>
Andy Gordon <adg@cl.cam.ac.uk>
Hanne Gottliebsen <hago@daimi.au.dk>
Øystein Haugen <oystein.haugen@nr.no>
Philipp Heuberger <pheuberg@ra.abo.fi>
Thomas Hildebrandt <hilde@brics.dk>
Marcin Jurdzinski <mju@mimuw.edu.pl>
Søren B. Lassen <thales@brics.dk>
Karoline Malmkjær <karoline@stibo.dk>
Randy Pollack <rap@dcs.ed.ac.uk>
Kim Sunesen <ksunesen@brics.dk>
Svend Haugaard Sørensen <shs@daimi.aau>.dk