On Upper Bounds on the Church-Rosser Theorem

TL;DR

This paper presents a new proof of the Church-Rosser theorem for beta-equality in the lambda-calculus using Takahashi's translation, establishing upper bounds within the Grzegorczyk hierarchy.

Contribution

It introduces a novel proof avoiding parallel reductions and derives explicit upper bounds for reduction sequences.

Findings

Proof of the Church-Rosser theorem without parallel reductions

Upper bounds on reduction sequences at the fourth level of the Grzegorczyk hierarchy

Application of Takahashi's translation to lambda-calculus

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 with no use of parallel reductions, but simply with Takahashi's translation (Gross-Knuth strategy). Based on this, upper bounds for reduction sequences on the theorem are obtained as the fourth level of the Grzegorczyk hierarchy.