Two Decreasing Measures for Simply Typed λ-Terms

PABLO BARENBAUM; CRISTIAN SOTTILE

Roma

Conferencia; 8th International Conference on Formal Structures for Computation and Deduction; 2023

Universidad de Roma

This paper defines two decreasing measures for terms of the simply typed λ-calculus, called the W-measure and the Tm -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 λ m -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 W-measure maps each λ-term to a natural number, and it is obtained by evaluating the term in the λ m -calculus and counting the number of remaining wrappers. The Tm -measure maps each λ-term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree.