Maribel Fernández

Explicit Substitutions without Alpha-Conversion

Starting from the lambda-calculus with names I will describe a family of calculi with explicit substitutions which overcome the usual syntactical problems (alpha-conversion). The key idea is that only closed substitutions are propagated through abstractions. This "closed reduction" strategy is weak, but rich enough to capture both call-by-value and call-by-name evaluations, and it permits certain reductions under abstractions thus offering more sharing. We have developed a name-free syntax, using director strings, which we used to define a family of abstract machines for closed reduction. Our experimental results confirm that, for large combinator-based terms, closed reduction out-performs standard evaluators and its low overheads make it more efficient than optimal reduction in many cases. I will also describe a generalisation of director strings to model arbitrary beta-reductions, and two abstract machines for strong reduction which inherit the efficiency of the weak evaluator.

This is joint work with Ian Mackie and François-Régis Sinot.