Formalizzazioni del Teorema di Church-Rosser in Agda

In this thesis we present and explore the various concepts in computer-assisted formalizations of the Church-Rosser theorem for β-reduction in the untyped λ-calculus. Using the dependently-typed programming language and proof assistant Agda, we expose four different proof approaches for this theorem along with their complete formalization. The proofs we considered reutilize and exploit the potentiality of an existing infrastructure presented by Wadler et al. (2019) in the book "Programming Language Foundations in Agda", where they implement λ-calculus and substitutions using de Bruijn indices and the σ-calculus by Abadi et al. (1991). The above-mentioned authors also present a confluence proof for β-reduction, employing the classic Tait and Martin-Löf method with parallel reduction. After presenting this proof, we firstly expose a small improvement of this development using Takahashi translation to prove the diamond lemma for parallel reduction, as described in Takahashi (1995). We then present the main contribution of the thesis, which is a complete formalization of the confluence of β-reduction with the methods recently developed by Komori et al. (2014). The refinements they present do not employ parallel reduction, and instead focus on an iterated Takahashi translation. This method allows them to obtain an even simpler proof of confluence which also sharpens and quantifies the previous results. Finally, we show that some of the theorems introduced in this last proof can be used to directly formalize another approach presented by Nagele et al. (2016) in Isabelle/HOL, where the confluence of β-reduction is derived through the use of the so-called Z-property due to Dehornoy et al. (2008).