An induction measure on λ-terms and its applications

Abstract: "A useful induction measure on [lambda]-terms is presented here. Combining leftmost reduction with subterm reduction, we introduce a new notion called H-reduction for untyped [lambda]-calculus. Since a subterm reduction is only performed on a term when it is in an empty context, the H-reduction is really a relation in a more rigorous sense. We then prove the equivalence between strong normalisability and H-normalisability, which is essentially a bridge linking H-reduction to various strong normalisation problems. Exploiting the new notion, we present some simplified proofs for several fundamental theorems such as finiteness of developments, the conservation theorem for [lambda]K-calculus, and the strong normalisation theorem for simply typed [lambda]-calculus. Also a simplified proof of the characterisation theorem on perpetual redexes in [BK82] is included. Compared with other proofs in the literature, all presented proofs are quite concise and straightforward. In the case of the conservation therorem [sic], the proof is also quite perspicacious. Finally, we give a brief comparison between H-reduction and other methods such as perpetual strategies. We claim H-reduction is a clean presentation of many similar ideas mentioned in the literature."