Abstract
Fine-grained reformulation of the lambda calculus is expected to solve several difficulties with the notion of substitutions—definition, implementation and cost properties. However, previous attempts including those using explicit substitutions and those using Interaction Nets were not ideally simple when it came to the encoding of the pure (as opposed to weak) lambda calculus. This paper presents a novel, fine-grained, and highly asynchronous encoding of the pure lambda calculus using LMNtal, a hierarchical graph rewriting language, and discusses its properties. The major strength of the encoding is that it is significantly simpler than previous encodings, making it promising as an alternative formulation, rather than just the encoding, of the pure lambda calculus. The membrane construct of LMNtal plays an essential role in encoding colored tokens and operations on them. The encoding has been tested using the publicly available LMNtal implementation.
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.
References
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit Substitutions. Journal of Functional Programming 1(4), 375–416 (1991)
Bloo, R., Geuvers, H.: Explicit Substitution: on the Edge of Strong Normalization. Theoretical Computer Science 211(1–2), 375–395 (1999)
Berry, G., Boudol, G.: The Chemical Abstract Machine. In: Proc. POPL 1990, pp. 81–94. ACM, New York (1990)
Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence Properties of Weak and Strong Calculi of Explicit Substitutions. J. ACM 43(2), 362–397 (1996)
Fernández, M., Mackie, I., Sinot, F.-R.: Closed Reduction: Explicit Substitutions without α-conversion. Mathematical Structures in Computer Science 15(2), 343–381 (2005)
Lafont, Y.: Interaction Nets. In: Proc. POPL 1990, pp. 95–108. ACM, New York (1990)
Lamping, J.: An Algorithm for Optimal Lambda-Calculus Reductions. In: Proc. POPL 1990, pp. 16–30. ACM, New York (1990)
Lang, F.: Modèles de la β-réduction pour les implantations. Ph.D. Thesis, Ècole Normale Supérieure de Lyon (1998)
Mackie, I.: YALE: Yet Another Lambda Evaluator Based on Interaction Nets. In: Proc. ICFP 1998, pp. 117–128. ACM, New York (1998)
Mackie, I.: Efficient λ-Evaluation with Interaction Nets. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 155–169. Springer, Heidelberg (2004)
Melliès, P.-A.: Typed λ -Calculi with Explicit Substitutions May Not Terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328–334. Springer, Heidelberg (1995)
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)
Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs (1987)
Ueda, K., Kato, N.: LMNtal: a Language Model with Links and Membranes. In: Mauri, G., Păun, G., Jesús Pérez-Jímenez, M., Rozenberg, G., Salomaa, A. (eds.) WMC 2004. LNCS, vol. 3365, pp. 110–125. Springer, Heidelberg (2005)
Ueda, K.: Encoding Distributed Process Calculi into LMNtal. Electronic Notes in Theoretical Computer Science 209, 187–200 (2008)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ueda, K. (2008). Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)