Skip to main content


eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Church-Rosser Made Easy
Authors: Kozen, Dexter
Keywords: lambda-calculus
Church-Rosser theorem
Issue Date: 5-Feb-2010
Abstract: The Church-Rosser theorem states that the lambda-calculus is confluent under alpha- and beta-reductions. The standard proof of this result is due to Tait and Martin-Loef. 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 beta-eta-calculus.
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
ChurchRosser.pdfMain article291.4 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us