Abstract
We present a name free λ-calculus with explicit substitutions based on a generalized notion of director strings: we annotate a term with information about how each substitution should be propagated through the term. 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 derive the closed reduction strategy (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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. In Proc. of the 22nd ACM Symposium on Principles of Programming Languages (POPL’95), pages 233–246. ACM Press, 1995.
A. Asperti, C. Giovanetti, and A. Naletto. The bologna optimal higher-order machine. Journal of Functional Programming, 6(6):763–810, 1996.
U. Berger, M. Eberl, and H. Schwichtenberg. Normalization by evaluation, 1998.
P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, 1996.
N. G. de Bruijn. Lambda calculus notation with nameless dummies. Indagationes Mathematicae, 34:381–392, 1972.
M. Fernández and I. Mackie. Closed reductions in the λ-calculus. In J. Flum and M. Rodríguez-Artalejo, editors, Proc. of Computer Science Logic (CSL’99), number 1683 in Lecture Notes in Computer Sciences. Springer, 1999.
M. Fernández and I. Mackie. Director strings and explicit substitutions. WESTAPP’01, Utrecht, 2001.
G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In Conference Record of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992.
T. Hardin, L. Maranget, and B. Pagano. Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming, 8(2):131–176, 1998.
J. Kennaway and M. Sleep. Director strings as combinators. ACM Transactions on Programming Languages and Systems, 10(4):602–626, 1988.
J. Lamping. An algorithm for optimal lambda calculus reductions. In Proc. 17th ACM Symposium on Principles of Programmining Languages, 1990.
F. Lang. Modèles de la β-réduction pour les implantations. PhD thesis, École Normale Supérieure de Lyon, 1998.
F.-R. Sinot. Calculs avec chaînes directrices: Implémentation efficace du λ-calcul, 2002. Master’s Thesis (Mémoire de DEA), École Normale Supérieure, http://www.dcs.kcl.ac.uk/pg/francois/DEA/.
N. Yoshida. Optimal reduction in weak lambda-calculus with shared environments. Journal of Computer Software, 11(6):3–18, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sinot, FR., Fernández, M., Mackie, I. (2003). Efficient Reductions with Director Strings. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive