|
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
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
