Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus

We study the Church-Rosser property—which is also known as confluence—in term rewriting and λ-calculus. Given a system R and a peak t ←* s →* t′ in R, we are interested in the length of the reductions in the smallest corresponding valley t →* s′ ←* t′ as a function vs R (m, n) of the size m of s and the maximum length n of the reductions in the peak. For confluent term rewriting systems (TRSs), we prove the (expected) result that vs R (m, n) is a computable function. Conversely, for every total computable function ϕ(n) there is a TRS with a single term s such that vs R ( ∣ s ∣ , n) ≥ ϕ(n) for all n. In contrast, for orthogonal term rewriting systems R we prove that there is a constant k such that vs R (m, n) is bounded from above by a function exponential in k and independent of the size of s. For λ-calculus, we show that vs R (m,n) is bounded from above by a function contained in the fourth level of the Grzegorczyk hierarchy.