2026-07-22T04:54:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17995 2024-03-06T11:00:49Z ddc:004 open_access

Two Decreasing Measures for Simply Typed λ-Terms Barenbaum, Pablo Sottile, Cristian Lambda Calculus Rewriting Termination Strong Normalization Simple Types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pablo Barenbaum and Cristian Sottile 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.11 urn:nbn:de:0030-drops-179956 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.11 eng https://creativecommons.org/licenses/by/4.0/legalcode