Encoding Strategies in the Lambda Calculus with Interaction Nets | SpringerLink
Skip to main content
Springer Nature Link
Log in

Encoding Strategies in the Lambda Calculus with Interaction Nets

  • Conference paper
Implementation and Application of Functional Languages (IFL 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4015))

Included in the following conference series:

  • 321 Accesses

Abstract

Interaction nets are a graphical paradigm of computation based on graph rewriting. They have proven to be both useful and enlightening in the encoding of linear logic and the λ-calculus. This paper offers new techniques for the theory of interaction nets, with applications to the encoding of specific strategies in the λ-calculus. In particular we show how to recover the usual call-by-value and call-by-name reduction strategies from general encodings.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abramsky, S.: Computational Interpretations of Linear Logic. Theoretical Comput. Sci. 111, 3–57 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  2. Fernández, M., Mackie, I.: Interaction nets and term rewriting systems. Theoretical Computer Science 190(1), 3–39 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  3. Fernández, M., Mackie, I.: A calculus for interaction nets. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 170–187. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Fernández, M., Mackie, I.: Packing interaction nets: Applications to linear logic and the lambda calculus. In: Frias, M., Heintz, J. (eds.) Proceedings of the 5th Argentinian Workshop of Theoretical Computer Science (WAIT 2001), Anales JAIIO, vol. 30, pp. 91–107 (September 2001)

    Google Scholar 

  6. Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50(1), 1–102 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Google Scholar 

  10. Lafont, Y.: From proof nets to interaction nets. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol. 222, pp. 225–247. Cambridge University Press, Cambridge (1995)

    Chapter  Google Scholar 

  11. Lafont, Y.: Interaction combinators. Information and Computation 137(1), 69–101 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  12. 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)

    Google Scholar 

  13. Lévy, J.-J.: Réductions Correctes et Optimales dans le Lambda-Calcul. Thèse d’état, Université Paris VII (January 1978)

    Google Scholar 

  14. Lippi, S.: λ-calculus left reduction with interaction nets. Mathematical Structures in Computer Science 12(6) (2002)

    Google Scholar 

  15. Lippi, S.: Théorie et pratique des réseaux d’interaction. PhD thesis, Université de la Méditerranée (June 2002)

    Google Scholar 

  16. Mackie, I.: The Geometry of Implementation. PhD thesis, Department of Computing, Imperial College of Science, Technology and Medicine (September 1994)

    Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. Mackie, I.: Interaction nets for linear logic. Theoretical Computer Science 247(1), 83–140 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  19. Mackie, I.: Efficient λ-evaluation with interaction nets. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 155–169. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. Mackie, I., Pinto, J.S.: Encoding linear logic with interaction combinators. Information and Computation 176(2), 153–186 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  21. Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice Hall International, Englewood Cliffs (1987)

    MATH  Google Scholar 

  22. Pinto, J.S.: Parallel Implementation with Linear Logic. PhD thesis, École Polytechnique (February 2001)

    Google Scholar 

  23. Pinto, J.S.: Weak reduction and garbage collection in interaction nets. In: Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain (2003)

    Google Scholar 

  24. Plasmeijer, R., Eekelen, M.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Reading (1993)

    MATH  Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. Sinot, F.-R.: Token-passing nets: Call-by-need for free. Electronic Notes in Theoretical Computer Science 135(5), 129–139 (2006)

    Article  Google Scholar 

  27. Wadsworth, C.P.: Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, Oxford University (1971)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, King’s College London, Strand, London, WC2R 2LS, UK

    Ian Mackie

  2. CNRS & École Polytechnique, LIX (UMR 7161), 91128 Cedex, Palaiseau, France

    Ian Mackie

Authors
  1. Ian Mackie
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Trinity College Dublin, Ireland

    Andrew Butterfield

  2. University of Lübeck, Germany

    Clemens Grelck

  3. Institute of Computer Science, University of Kiel, 24098, Kiel, Germany

    Frank Huch

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mackie, I. (2006). Encoding Strategies in the Lambda Calculus with Interaction Nets. In: Butterfield, A., Grelck, C., Huch, F. (eds) Implementation and Application of Functional Languages. IFL 2005. Lecture Notes in Computer Science, vol 4015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11964681_2

Download citation

  • DOI: https://doi.org/10.1007/11964681_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69174-7

  • Online ISBN: 978-3-540-69175-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation