Church-Rosser Made Easy
MetadataShow full item record
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.
lambda-calculus; Church-Rosser theorem