A simple proof of the undecidability of strong normalization

摘要

The purpose of this note is to give a methodologically simple proof of the undecidability of strong normalization in the pure lambda calculus. For this we show how to represent an arbitrary partial recursive function by a term whose application to any Church numeral is either strongly normalization or has no normal form. Intersection types are used for the strong normalization argument.