Abstract
Closed reduction is a very efficient reduction strategy for the lambda calculus, which is explained using a simple form of explicit substitutions. This paper introduces this strategy, and gives an implementation as a system of interaction nets. We obtain one of the most efficient implementations of this kind to date.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asperti, A., Giovannetti, C., Naletto, A.: The bologna optimal higher-order machine. Journal of Functional Programming 6(6), 763–810 (1996)
Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol. 45. Cambridge University Press, Cambridge (1998)
Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, 2nd edn. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland Publishing Company, Amsterdam (1984) (revised edition)
Fernández, M., Mackie, I.: Closed reductions in the λ-calculus. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 220–234. Springer, Heidelberg (1999)
Fernández, M., Mackie, I., Sinot, F.-R.: Closed reduction: explicit substitutions without alpha conversion. Mathematical Structures in Computer Science 15(2), 343–381 (2005)
Girard, J.-Y.: Geometry of interaction 1: Interpretation of System F. In: Ferro, R., Bonotto, C., Valentini, S., Zanardo, A. (eds.) Logic Colloquium 1988. Studies in Logic and the Foundations of Mathematics, vol. 127, pp. 221–260. North Holland Publishing Company, Amsterdam (1989)
Gonthier, G., Abadi, M., Lévy, J.-J.: The geometry of optimal lambda reduction. In: Proceedings of the 19th ACM Symposium on Principles of Programming Languages (POPL 1992), pp. 15–26. ACM Press, New York (1992)
Gonthier, G., Abadi, M., Lévy, J.-J.: Linear logic without boxes. In: Proceedings of the 7th IEEE Symposium on Logic in Computer Science (LICS 1992), pp. 223–234. IEEE Press, Los Alamitos (1992)
Lafont, Y.: Interaction nets. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL 1990), pp. 95–108. ACM Press, New York (1990)
Lamping, J.: An algorithm for optimal lambda calculus reduction. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL 1990), pp. 16–30. ACM Press, New York (1990)
Lévy, J.-J.: Optimal reductions in the lambda calculus. In: Hindley, J.P., Seldin, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 159–191. Academic Press, London (1980)
Lippi, S.: λ-calculus left reduction with interaction nets. Mathematical Structures in Computer Science 12(6) (2002)
Mackie, I.: The Geometry of Implementation. PhD thesis, Department of Computing, Imperial College of Science, Technology and Medicine (September 1994)
Mackie, I.: YALE: Yet another lambda evaluator based on interaction nets. In: Proceedings of the 3rd International Conference on Functional Programming (ICFP 1998), pp. 117–128. ACM Press, New York (1998)
Mackie, I.: Interaction nets for linear logic. Theoretical Computer Science 247(1), 83–140 (2000)
Mackie, I.: Efficient λ-evaluation with interaction nets. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 155–169. Springer, Heidelberg (2004)
Mackie, I., Pinto, J.S.: Encoding linear logic with interaction combinators. Information and Computation 176(2), 153–186 (2002)
Pinto, J.S.: Weak reduction and garbage collection in interaction nets. Electronic Notes in Theoretical Computer Science 84(4), 625–640 (2003)
Sinot, F.-R.: Call-by-name and call-by-value as token-passing interaction nets. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 386–400. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mackie, I. (2011). An Interaction Net Implementation of Closed Reduction. In: Scholz, SB., Chitil, O. (eds) Implementation and Application of Functional Languages. IFL 2008. Lecture Notes in Computer Science, vol 5836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24452-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-24452-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24451-3
Online ISBN: 978-3-642-24452-0
eBook Packages: Computer ScienceComputer Science (R0)