×

Church-Rosser made easy. (English) Zbl 1231.03012

Summary: The Church-Rosser theorem states that the \(\lambda\)-calculus is confluent under \(\beta\)-reductions. The standard proof of this result is due to Tait and Martin-Löf. 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.

MSC:

03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI