Lambda-calculus with director strings

We present a name free λ-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 β-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 λ-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.