An Induction Measure on A-terms and Its Applications
Hongwei Xi · 1996
A useful induction measure on A-terms is presented here. Combining leftmost reduction with subterm reduction, we introduce a new notion called W-reduction for untyped A-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 Ti-normalisability, which is essentially a bridge linking W-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 AK-calculus, and the strong normalisation theorem for simply typed A-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, the proof is also quite perspicacious. Finally, we give a brief comparison between W-reduction and other methods such as perpetual strategies. We claim ^-reduction is a clean presentation of many similar ideas mentioned in the literature.