Document Open Access Logo

α-Avoidance

Authors Samuel Frontull , Georg Moser , Vincent van Oostrom

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2023.22.pdf
  • Filesize: 1.15 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
Keywords
  • λ-calculus
  • variable capture
  • α-conversion
  • developments
  • safe λ-calculus
  • undecidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

When substitutions and bindings interact, there is a risk of undesired side effects if the substitution is applied naïvely. The λ-calculus captures this phenomenon concretely, as β-reduction may require the renaming of bound variables to avoid variable capture. In this paper we introduce α-paths as an estimation for α-avoidance, roughly expressing that α-conversions are not required to prevent variable capture. These paths provide a novel method to analyse and predict the potential need for α in different calculi. In particular, we show how α-path characterises α-avoidance for several sub-calculi of the λ-calculus like (i) developments, (ii) affine/linear λ-calculi, (iii) the weak λ-calculus, (iv) μ-unfolding and (iv) finally the safe λ-calculus. Furthermore, we study the unavoidability of α-conversions in untyped and simply-typed λ-calculi and prove undecidability of the need of α-conversions for (leftmost-outermost reductions) in the untyped λ-calculus. To ease the work with α-paths, we have implemented the method and the tool is publicly available.

Cite As Get BibTex

Samuel Frontull, Georg Moser, and Vincent van Oostrom. α-Avoidance. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.22

Author Details

Samuel Frontull
  • Universität Innsbruck, Austria
Georg Moser
  • Universität Innsbruck, Austria
Vincent van Oostrom
  • Barendrecht, The Netherlands

Supplementary Materials

References

  1. Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2):159-267, 1993. URL: https://doi.org/10.1006/inco.1993.1044.
  2. Andrea Asperti, Vincent Danos, Cosimo Laneve, and Laurent Regnier. Paths in the lambda-calculus. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994, pages 426-436. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/LICS.1994.316048.
  3. Andrea Asperti and Stefano Guerrini. The optimal implementation of functional programming languages, volume 45 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1998. Google Scholar
  4. Andrea Asperti and Cosimo Laneve. Paths, computations and labels in the λ-calculus. Theoretical Computer Science, 142(2):277-297, 1995. URL: https://doi.org/10.1016/0304-3975(94)00279-7.
  5. Thibaut Balabonski. Weak optimality, and the meaning of sharing. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500606.
  6. Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2nd revised edition, 1984. URL: https://doi.org/10.2307/2274112.
  7. Henk P. Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. Google Scholar
  8. Tomasz Blanc, Jean-Jacques Lévy, and Luc Maranget. Sharing in the Weak Lambda-Calculus. In Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 70-87. Springer, 2005. URL: https://doi.org/10.1007/11601548_7.
  9. William Blum. The Safe Lambda Calculus. PhD thesis, Oxford University, UK, 2009. Google Scholar
  10. William Blum and C.-H. Luke Ong. The Safe Lambda Calculus. In TLCA, pages 39-53, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  11. William Blum and C.-H. Luke Ong. The safe lambda calculus. Logical Methods in Computer Science, Volume 5, Issue 1, February 2009. URL: https://doi.org/10.48550/arXiv.0901.2399.
  12. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 75(5):381-392, 1972. Proc. 19th International Conference on Automated Deduction. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  13. Felice Cardone and J. Roger Hindley. Lambda-Calculus and Combinators in the 20th Century. In Logic from Russell to Church, 2009. URL: https://doi.org/10.1016/S1874-5857(09)70018-4.
  14. Alonzo Church and John Barkley Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39:472-482, 1936. URL: https://doi.org/10.1090/S0002-9947-1936-1501858-0.
  15. Haskell B. Curry. Combinatory Logic. Amsterdam: North-Holland Pub. Co., 1958. Google Scholar
  16. Werner Damm. The IO- and OI-hierarchies. Theoretical Computer Science, 20(2):95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
  17. Jörg Endrullis, Clemens Grabmayer, Jan Willem Klop, and Vincent van Oostrom. On equal μ-terms. Theoretical Computer Science, 412(28):3175-3202, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.011.
  18. Samuel Frontull. Alpha Avoidance. Master’s thesis, University of Innsbruck, 2021. Google Scholar
  19. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Proc. 14th LICS, pages 214-224, 1999. URL: https://doi.org/10.1109/LICS.1999.782617.
  20. J. Roger Hindley. Reductions of Residuals are Finite. Transactions of the American Mathematical Society, 240:345-361, 1978. URL: https://doi.org/10.2307/1998825.
  21. J. Roger Hindley. BCK-Combinators and Linear lambda-Terms have Types. Theoretical Computer Science, 64(1):97-105, 1989. URL: https://doi.org/10.1016/0304-3975(89)90100-X.
  22. Martin Hyland. A simple proof of the Church-Rosser theorem. Oxford University, UK, 1973. Google Scholar
  23. Bart Jacobs. Semantics of lambda-I and of other substructure lambda calculi. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, pages 195-208, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0037107.
  24. Jan W. Klop. Combinatory reduction systems. PhD thesis, Rijksuniversiteit Utrecht, 1980. Google Scholar
  25. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  26. Clemens Kupke, Johannes Marti, and Yde Venema. Size measures and alphabetic equivalence in the μ-calculus. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 18:1-18:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533339.
  27. Harry G. Mairson. Linear lambda calculus and PTIME-completeness. Journal of Functional Programming, 14(6):623-633, 2004. URL: https://doi.org/10.1017/S0956796804005131.
  28. Jolie G. de Miranda. Structures generated by higher-order grammars and the safety constraint. PhD thesis, University of Oxford, UK, 2006. Google Scholar
  29. Maxwell H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of mathematics, 43(2):223-243, 1942. URL: https://doi.org/10.2307/1968867.
  30. Vincent van Oostrom and Roel de Vrijer. Four equivalent equivalences of reductions. Electronic Notes in Theoretical Computer Science, 70(6):21-61, 2002. WRS 2002, 2nd International Workshop on Reduction Strategies in Rewriting and Programming - Final Proceedings (FLoC Satellite Event). URL: https://doi.org/10.1016/S1571-0661(04)80599-1.
  31. Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice Hall, January 1987. Google Scholar
  32. Emil L. Post. A variant of a recursively unsolvable problem. Bulletin of the American Mathematical Society, 52(4):264-268, 1946. URL: https://doi.org/10.2307/2267252.
  33. John Barkley Rosser. Review: H. B. Curry, A New Proof of the Church-Rosser Theorem. Journal of Symbolic Logic, 21(4):377-378, 1956. Google Scholar
  34. David E. Schroer. The Church-Rosser Theorem. PhD thesis, Cornell University, 1965. Google Scholar
  35. Rick Statman. On the complexity of alpha conversion. The Journal of Symbolic Logic, 72(4):1197-1203, 2007. URL: https://doi.org/10.2178/jsl/1203350781.
  36. Terese. Term rewriting systems. Cambridge University Press, 2003. Google Scholar
  37. Christopher P. Wadsworth. Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, University of Oxford, 1971. Google Scholar
  38. Noam Zeilberger. Linear lambda terms as invariants of rooted trivalent maps. Journal of Functional Programming, 26:e21, 2016. URL: https://doi.org/10.1017/S095679681600023X.
  39. Naim Çağman and J. Roger Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198(1-2):239-247, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00250-8.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact