No CrossRef data available.
Article contents
A simple proof of the undecidability of strong normalisation
Published online by Cambridge University Press: 04 March 2003
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.
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.
- Type
- Research Article
- Information
- Copyright
- © 2003 Cambridge University Press