More Church–Rosser Proofs

Research paper by Tobias Nipkow

Indexed on: 01 Jan '01Published on: 01 Jan '01Published in: Journal of Automated Reasoning


The proofs of the Church–Rosser theorems for β, η, and β ∪ η reduction in untyped λ-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For β-reduction, both the standard proof and Takahashi's are given and compared. All proofs are based on a general theory of commutating relations that supports an almost geometric style of reasoning about confluence diagrams.