Skip to main content


eCommons@Cornell

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: http://hdl.handle.net/1813/14402
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.
URI: http://hdl.handle.net/1813/14402
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