Hostname: page-component-599cfd5f84-56l7z Total loading time: 0 Render date: 2025-01-07T07:07:05.575Z Has data issue: false hasContentIssue false
  • English
  • Français

A simple proof of the undecidability of strong normalisation

Published online by Cambridge University Press:  04 March 2003

PAWEŁ URZYCZYN
PAWEŁ URZYCZYN
Affiliation:
Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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
Mathematical Structures in Computer Science , Volume 13 , Issue 1 , February 2003 , pp. 5 - 13
Copyright
© 2003 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)