Document Open Access Logo

Two Decreasing Measures for Simply Typed λ-Terms

Authors Pablo Barenbaum, Cristian Sottile

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.11.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Author Details

Pablo Barenbaum
  • ICC, Universidad de Buenos Aires, Argentina
  • Universidad Nacional de Quilmes (CONICET), Buenos Aires, Argentina
Cristian Sottile
  • ICC, Universidad de Buenos Aires (CONICET), Argentina
  • Universidad Nacional de Quilmes, Buenos Aires, Argentina

Funding

This work was partially supported by project grants PICT-2021-I-A-00090, PICT-2021-I-INVI-00602, PIP 11220200100368CO, PICT 2019-1272, PUNQ 2218/22, and PUNQ 2219/22.

Acknowledgements

To Giulio Manzonetto for fruitful discussions that led to the development of this work. To Eduardo Bonelli and the anonymous reviewers for feedback on earlier versions of this paper. The second author would like to thank his advisors Alejandro Díaz-Caro and Pablo E. Martínez López.

Cite AsGet BibTex

Pablo Barenbaum and Cristian Sottile. Two Decreasing Measures for Simply Typed λ-Terms. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.11

Abstract

This paper defines two decreasing measures for terms of the simply typed λ-calculus, called the 𝒲-measure and the 𝒯^{𝐦}-measure. A decreasing measure is a function that maps each typable λ-term to an element of a well-founded ordering, in such a way that contracting any β-redex decreases the value of the function, entailing strong normalization. Both measures are defined constructively, relying on an auxiliary calculus, a non-erasing variant of the λ-calculus. In this system, dubbed the λ^{𝐦}-calculus, each β-step creates a "wrapper" containing a copy of the argument that cannot be erased and cannot interact with the context in any other way. Both measures rely crucially on the observation, known to Turing and Prawitz, that contracting a redex cannot create redexes of higher degree, where the degree of a redex is defined as the height of the type of its λ-abstraction. The 𝒲-measure maps each λ-term to a natural number, and it is obtained by evaluating the term in the λ^{𝐦}-calculus and counting the number of remaining wrappers. The 𝒯^{𝐦}-measure maps each λ-term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Lambda calculus
Keywords
  • Lambda Calculus
  • Rewriting
  • Termination
  • Strong Normalization
  • Simple Types

Metrics

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

References

  1. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, pages 381-395, 2010. Google Scholar
  2. Pablo Barenbaum and Eduardo Bonelli. Optimality and the linear substitution calculus. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, pages 9:1-9:16, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.9.
  3. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103. Elsevier, 1984. Google Scholar
  4. Henk P. Barendregt and Giulio Manzonetto. Turing’s contributions to lambda calculus. In B. Cooper and J. van Leeuwen, editors, Alan Turing - His Work and Impact, pages 139-143. Elsevier, 2013. Google Scholar
  5. TCLA Editorial Board. TLCA list of open problems. http://tlca.di.unito.it/opltlca/, 2006.
  6. Thierry Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184-191, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.015.
  7. René David. Normalization without reducibility. Ann. Pure Appl. Log., 107(1-3):121-130, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00030-0.
  8. Philippe de Groote. The conservation theorem revisited. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 163-178. Springer, 1993. URL: https://doi.org/10.1007/BFb0037105.
  9. Roel de Vrijer. A direct proof of the finite developments theorem. The Journal of symbolic logic, 50(2):339-343, 1985. Google Scholar
  10. Roel de Vrijer. Exactly estimating functionals and strong normalization. In Indagationes Mathematicae (Proceedings), volume 90, pages 479-493. North-Holland, 1987. Google Scholar
  11. Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. Open problems in rewriting. In International Conference on Rewriting Techniques and Applications, pages 445-456. Springer, 1991. Google Scholar
  12. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979. Google Scholar
  13. Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. Abstracting models of strong normalization for classical calculi. J. Log. Algebraic Methods Program., 111:100512, 2020. URL: https://doi.org/10.1016/j.jlamp.2019.100512.
  14. Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky. Clocked lambda calculus. Math. Struct. Comput. Sci., 27(5):782-806, 2017. URL: https://doi.org/10.1017/S0960129515000389.
  15. Robin O. Gandy. An early proof of normalization by A.M. Turing. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 453-455. Academic Press, 1980. Google Scholar
  16. Robin O. Gandy. Proofs of strong normalization. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457-477. Academic Press, 1980. Google Scholar
  17. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris 7, 1972. Google Scholar
  18. Felix Joachimski and Ralph Matthes. Short proofs of normalization for the simply- typed lambda-calculus, permutative conversions and Gödel’s T. Arch. Math. Log., 42(1):59-87, 2003. URL: https://doi.org/10.1007/s00153-002-0156-9.
  19. Zurab Khasidashvili, Mizuhito Ogawa, and Vincent van Oostrom. Uniform normalisation beyond orthogonality. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings, volume 2051 of Lecture Notes in Computer Science, pages 122-136. Springer, 2001. URL: https://doi.org/10.1007/3-540-45127-7_11.
  20. Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, Utrecht University, 1980. Google Scholar
  21. Robert Pieter Nederpelt Lazarom. Strong normalization in a typed lambda calculus with lambda structured types. PhD thesis, TU Eindhoven, 1973. Google Scholar
  22. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université de Paris 7, 1978. Google Scholar
  23. Ralph Loader. Notes on simply typed lambda calculus. Technical Report ECS-LFCS-98-381, University of Edinburgh, 1998. Google Scholar
  24. Paul-André Melliès. Axiomatic rewriting theory I: A diagrammatic standardization theorem. 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 554-638. Springer, 2005. URL: https://doi.org/10.1007/11601548_23.
  25. Peter Møller Neergaard and Morten Heine Sørensen. Conservation and uniform normalization in lambda calculi with erasing reductions. Inf. Comput., 178(1):149-179, 2002. URL: https://doi.org/10.1006/inco.2002.3153.
  26. Tobias Nipkow. Higher-order critical pairs. In Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pages 342-343. IEEE Computer Society, 1991. Google Scholar
  27. Jan von Plato. Gentzen’s proof of normalization for natural deduction. Bulletin of Symbolic Logic, 14(2):240-257, 2008. Google Scholar
  28. Dag Prawitz. Natural deduction: a proof-theoretical study. PhD thesis, Almqvist & Wiksell, 1965. Google Scholar
  29. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism, volume 149. Elsevier, 2006. Google Scholar
  30. William W. Tait. A realizability interpretation of the theory of species. In Rohit Parikh, editor, Logic Colloquium, pages 240-251, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. Google Scholar
  31. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact