Document

# Two Decreasing Measures for Simply Typed λ-Terms

## File

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

## 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 As

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

## 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.
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.
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.
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.
10. Roel de Vrijer. Exactly estimating functionals and strong normalization. In Indagationes Mathematicae (Proceedings), volume 90, pages 479-493. North-Holland, 1987.
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.
12. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979.
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.
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.
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.
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.
21. Robert Pieter Nederpelt Lazarom. Strong normalization in a typed lambda calculus with lambda structured types. PhD thesis, TU Eindhoven, 1973.
22. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université de Paris 7, 1978.
23. Ralph Loader. Notes on simply typed lambda calculus. Technical Report ECS-LFCS-98-381, University of Edinburgh, 1998.
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.
27. Jan von Plato. Gentzen’s proof of normalization for natural deduction. Bulletin of Symbolic Logic, 14(2):240-257, 2008.
28. Dag Prawitz. Natural deduction: a proof-theoretical study. PhD thesis, Almqvist & Wiksell, 1965.
29. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism, volume 149. Elsevier, 2006.
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.
31. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.