  This paper defines two decreasing measures for terms of the simply typed
lambda-calculus, called the W-measure and the Tm-measure. A decreasing measure
is a function that maps each typable lambda-term to an element of a
well-founded ordering, in such a way that contracting any beta-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 lambda-calculus. In this system, dubbed the m-calculus, each beta-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 lambda-abstraction. The W-measure maps each
lambda-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 lambda-term to a structure of nested multisets, where the nesting
depth is proportional to the maximum redex degree.
