Hostname: page-component-6bf8c574d5-956mj Total loading time: 0 Render date: 2025-02-21T06:29:04.441Z Has data issue: false hasContentIssue false

A simple proof of the undecidability of strong normalisation

Published online by Cambridge University Press:  04 March 2003

PAWEŁ URZYCZYN
Affiliation:
Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland Email: urzy@mimuw.edu.pl
Rights & Permissions [Opens in a new window]

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
Copyright
© 2003 Cambridge University Press