The Church-Rosser Theorem and Analysis of Reduction Length (Proof theory and proving)

Abstract

The Church-Rosser theorem in the type-free $lambda$-calculus is well investigated both for $beta$-equality and $beta$-reduction. We provide a new proof of the theorem for $beta$-equality simply with Takahashi's translation. Based on this, we analyze quantitative properties of witnesses of the Church-Rosser theorem by using the notion of parallel reduction. In particular, upper bounds for reduction sequences on the theorem are obtained as the fourth level of the Grzegorczyk hierarchy, i.e., non-elementary recursive functions. Moreover, the proof method developed here can be applied to other reduction systems such as $lambda$-calculus with $beta eta$-reduction, Girard's system $Gamma$, Gödel's system mathrm{T}, combinatory logic, and Pure Type Systems as well.