Closed reduction: explicit substitutions without $\alpha$-conversion

Abstract

Starting from the $\lambda$-calculus with names, we develop a family of calculi with explicit substitutions that overcome the usual syntactical problems of substitution. The key idea is that only closed substitutions can be moved through certain constructs. This gives a weak form of reduction, called closed reduction, which is rich enough to capture both the call-by-value and call-by-name evaluation strategies in the $\lambda$-calculus. Moreover, since substitutions can move through abstractions and reductions are allowed under abstractions (if certain conditions hold), closed reduction naturally provides an efficient notion of reduction with a high degree of sharing and low overheads. We present a family of abstract machines for closed reduction. Our benchmarks show that closed reduction performs better than all standard weak strategies, and its low overheads make it more efficient than optimal reduction in many cases.