Kozen, Dexter Church-Rosser made easy. (English) Zbl 1231.03012 Fundam. Inform. 103, No. 1-4, 129-136 (2010). 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 Keywords:lambda-calculus; confluence; Church-Rosser theorem PDFBibTeX XMLCite \textit{D. Kozen}, Fundam. Inform. 103, No. 1--4, 129--136 (2010; Zbl 1231.03012) Full Text: DOI