View Related Documents

Abstract

We present a name free lambda-calculus with explicit substitutions, based on a generalised notion of director strings. Terms are annotated with information – directors – that indicate how substitutions should be propagated. We first present a calculus where we can simulate arbitrary beta-reduction steps, and then simplify the rules to model the evaluation of functional programs (reduction to weak head normal form). We also show that we can define the closed reduction strategy. This is a weak strategy which, in contrast with standard weak strategies, allows certain reductions to take place inside lambda-abstractions thus offering more sharing. Our experimental results confirm that, for large combinator-based terms, our weak evaluation strategies out-perform standard evaluators. Moreover, we derive two abstract machines for strong reduction which inherit the efficiency of the weak evaluators.

Keywords  lambda-Calculus - Explicit Substitutions - Director Strings - Strategies

Projet Logical, Pôle Commun de Recherche en Informatique du plateau de Saclay, CNRS, École Polytechnique, INRIA, Université Paris-Sud.

Fulltext Preview

Image of the first page of the fulltext document