Least upper bounds on the size of Church-Rosser diagrams in term rewriting and λ-calculus

TY - GEN

T1 - Least upper bounds on the size of Church-Rosser diagrams in term rewriting and λ-calculus

AU - Ketema, Jeroen

AU - Simonsen, Jakob Grue

N1 - Conference code: 10

PY - 2010

Y1 - 2010

N2 - 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 vsR(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 vsR(m, n) is a computable function. Conversely, for every total computable function φ(n) there is a TRS with a single term s such that vsR(|s|, n) ≥ φ(n) for all n. In contrast, for orthogonal term rewriting systems R we prove that there is a constant k such that vsR(m, n) is bounded from above by a function exponential in k and independent of the size of s. For λ-calculus, we show that vsR(m, n) is bounded from above by a function contained in the fourth level of the Grzegorczyk hierarchy.

AB - 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 vsR(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 vsR(m, n) is a computable function. Conversely, for every total computable function φ(n) there is a TRS with a single term s such that vsR(|s|, n) ≥ φ(n) for all n. In contrast, for orthogonal term rewriting systems R we prove that there is a constant k such that vsR(m, n) is bounded from above by a function exponential in k and independent of the size of s. For λ-calculus, we show that vsR(m, n) is bounded from above by a function contained in the fourth level of the Grzegorczyk hierarchy.

U2 - 10.1007/978-3-642-12251-4_20

DO - 10.1007/978-3-642-12251-4_20

M3 - Article in proceedings

SN - 978-3-642-12250-7

T3 - Lecture notes in computer science

SP - 272

EP - 287

BT - Functional and Logic Programming

A2 - Blume, Matthias

A2 - Kobayashi, Naoki

A2 - Vidal, Germán

PB - Springer

T2 - 10th International Symposium on Functional and Logic Programming

Y2 - 19 April 2010 through 21 April 2010

ER -