Church–Rosser Made Easy

Issue title: From Mathematical Beauty to the Truth of Nature: to Jerzy Tiuryn on his 60th Birthday

Article type: Research Article

Authors: Kozen, Dexter

Affiliations: Department of Computer Science, Cornell University, Ithaca, New York 14853-7501, USA. kozen@cs.cornell.edu

Note: [] Address for correspondence: Department of Computer Science, Cornell University, Ithaca, New York 14853-7501, USA

Abstract: The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus.

Keywords: lambda-calculus, confluence, Church–Rosser theorem

DOI: 10.3233/FI-2010-322

Journal: Fundamenta Informaticae, vol. 103, no. 1-4, pp. 129-136, 2010