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.

翻译：摘要：本文定义了简单类型λ演算中项的两个递减度量，分别称为W-度量和Tm-度量。递减度量是将每个可类型化的λ项映射到良基序中某个元素的函数，使得任何β-归约约简都会减小该函数的值，从而蕴含强规范化性质。两个度量均基于辅助演算（即λ演算的非擦除变体）构造性定义。在该系统（称为m-演算）中，每次β-步都会创建一个"包装器"，其中包含参数副本，该副本既不能被擦除，也不能以其他方式与上下文交互。两个度量关键依赖于图灵和普拉维茨已知的观察：归约约简不能创建更高阶的归约式，其中归约式的阶定义为λ-抽象类型的层级高度。W-度量将每个λ项映射到自然数，通过评估m-演算中的项并统计剩余包装器数量获得。Tm-度量将每个λ项映射到嵌套多重集结构，其嵌套深度与最大归约式阶成比例。