Hostname: page-component-74656f9884-j7cmm Total loading time: 0 Render date: 2026-11-07T14:43:34.861Z Has data issue: false hasContentIssue false

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

Published online by Cambridge University Press:  14 March 2005

M. FERNÁNDEZ
Affiliation:
Department of Computer Science, King's College London Strand, London, WC2R 2LS U.K. Email: maribel@dcs.kcl.ac.uk, ian@dcs.kcl.ac.uk, francois@dcs.kcl.ac.uk
I. MACKIE
Affiliation:
Department of Computer Science, King's College London Strand, London, WC2R 2LS U.K. Email: maribel@dcs.kcl.ac.uk, ian@dcs.kcl.ac.uk, francois@dcs.kcl.ac.uk
F-R. SINOT
Affiliation:
Department of Computer Science, King's College London Strand, London, WC2R 2LS U.K. Email: maribel@dcs.kcl.ac.uk, ian@dcs.kcl.ac.uk, francois@dcs.kcl.ac.uk LIX, École Polytechnique, 91128 Palaiseau cedex, France
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Information

Type
Paper
Copyright
2005 Cambridge University Press