BRICS · Contents · Programme · References · Prerequisites · Participants · Lecture Notes · Registration

Explicit Substitution

A BRICS Mini-Course
October 27, 1996

Lectures by
Kristoffer Høgsbro Rose


Course Contents

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.

Programme

Sunday October 27, 1996, 10:15-11:00 in Auditorium D4

1. Explicit Substitution Rules

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).

Sunday October 27, 1996, 11:15-12:00 in Auditorium D4

2. Explicit Binding

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.

Sunday October 27, 1996, 12:15-13:00 in Auditorium D4

3. Explicit Addresses

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.

Sunday October 27, 1996, 15:15-16:00 in Auditorium D4

4. Strategies and Abstract Machines

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.

Sunday October 27, 1996, 16:15-17:00 in Auditorium D4

5. Generalising to Higher-Order Rewriting

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.

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy, Explicit substitutions, Journal of Functional Programming, 1(4): 375-416, 1991.
  2. H. Barendregt, The lambda calculus: its syntax and semantics (revised edition), North-Holland, 1984.
  3. Z.-E.-A. Benaissa, K. H. Rose, and P. Lescanne, Modeling sharing and recursion for weak reduction strategies using explicit substitution, in H. Kuchen and D. Swierstra (editors), 8th PLILP-Symposium on Programming Language Implementation and Logic Programming, Aachen, Germany, pp. 393-407, September 1996.
  4. R. Bloo and K. H. Rose, Combinatory reduction systems with explicit substitution that preserve strong normalisation, in H. Ganzinger (editor), 7th RTA-International Conference on Rewriting Techniques and Applications, Rutgers University, New Jersey, pp. 169-183, July 1996.
  5. R. Bloo and K. H. Rose, Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, in CSN '95-Computer Science in the Netherlands, Koninklijke Jaarbeurs, Utrecht, pp. 62-72, November 1995.
  6. P.-A. Melliès, Typed lambda-calculi with explicit substitution may not terminate, in M. Dezani, editor, 2nd TLCA-International Conference on Typed Lambda Calculi and Applications, Edinburgh, Scotland, LNCS 902, pp. 328-334, 1995.

    Prerequisites

    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).

    Participants

    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

    Lecture Notes

    BRICS-LS-96-3

    Registration

    Please send an E-mail message to \href{mailto:krisrose@brics.dk}{krisrose@brics.dk} if you wish to participate. There is no fee.