Church-Rosser Made Easy
Author
Kozen, Dexter
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.
Sponsorship
National Science Foundation CCF-0635028
Date Issued
2010-02-05T21:27:36Z
Keywords
Type
article