The Algebra of Church-Rosser

The focus of the thesis is the algebraization of the proof of Church–Rosser theorem, a fundamental result in the theory of the λ-calculus. Various proofs of this theorem have been proposed over time, ranging from fully syntactic approaches to more abstract methods. Among these, the most renowned is the one by Tait and Martin-Löf proof using so-called parallel reduction. In this work, we give an algebraic account, and also a generalisation, of Tait and Martin-Löf techniques. We do so employing Term Relation Algebras, extensions of relation algebras axiomatising relations over syntactic structures. Within such algebras, we formalise the confluence technique by Tait and Martin-Löf, without resting, however, on any term syntax. This result is a general algebraic technique readily applicable to a wide array of languages.