×

More Church-Rosser proofs (in Isabelle/HOL). (English) Zbl 0958.03011

Summary: The proofs of the Church-Rosser theorems for \(\beta\), \(\eta\), and \(\beta\cup \eta\) reduction in untyped \(\lambda\)-calculus are formalized in Isabelle/HOL, an implementation of higher order logic in the generic theorem prover Isabelle. For \(\beta\)-reduction, both the standard proof and Takahashi’s are given and compared. All proofs are based on a general theory of commuting relations that supports an almost geometric style of reasoning about confluence diagrams.

MSC:

03B35 Mechanization of proofs and logical operations
03B40 Combinatory logic and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI