A simple proof of the undecidability of strong normalisation
Paweł Urzyczyn · Mathematical Structures in Computer Science · 2003
The purpose of this note is to give a methodologically simple proof of the undecidability of strong normalisation 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 normalizable or has no normal form. Intersection types are used for the strong normalization argument.