Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus

TY - JOUR

T1 - Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus

AU - Ketema, Jeroen

AU - Simonsen, Jakob Grue

PY - 2013/11

Y1 - 2013/11

N2 - We study confluence and the Church-Rosser property in term rewriting and λ-calculus with explicit bounds on term sizes and reduction lengths. Given a system R, we are interested in the lengths of the reductions in the smallest valleys t →* s′ *← t′ expressed as a function: -for confluence a function vsR(m, n) where the valleys are for peaks t *← s →* t′ with s of size at most m and the reductions of maximum length n, and -for the Church-Rosser property a function cvsR(m, n) where the valleys are for conversions t ↔* t′ with t and t′ of size at most mand the conversion of maximum length n. For confluent Term Rewriting Systems (TRSs), we prove that vsR is a total computable function, and for linear such systems that cvsR is a total computable function. Conversely, we show that every total computable function is the lower bound on the functions vsR(m, n) and cvsR(m, n) for some TRS R: In particular, we show that for every total computable function φ : N -→ N there is a TRS R with a single term s such that vsR(|s|, n) ≥ φ(n) and cvsR(n, n) ≥ φ(n) for all n. For orthogonal TRSs R we prove that there is a constant k such that: (a) vsR(m, n) is bounded from above by a function exponential in k and (b) cvsR(m, n) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy. Similarly, for λ-calculus, we show that vsR(m, n) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy.

AB - We study confluence and the Church-Rosser property in term rewriting and λ-calculus with explicit bounds on term sizes and reduction lengths. Given a system R, we are interested in the lengths of the reductions in the smallest valleys t →* s′ *← t′ expressed as a function: -for confluence a function vsR(m, n) where the valleys are for peaks t *← s →* t′ with s of size at most m and the reductions of maximum length n, and -for the Church-Rosser property a function cvsR(m, n) where the valleys are for conversions t ↔* t′ with t and t′ of size at most mand the conversion of maximum length n. For confluent Term Rewriting Systems (TRSs), we prove that vsR is a total computable function, and for linear such systems that cvsR is a total computable function. Conversely, we show that every total computable function is the lower bound on the functions vsR(m, n) and cvsR(m, n) for some TRS R: In particular, we show that for every total computable function φ : N -→ N there is a TRS R with a single term s such that vsR(|s|, n) ≥ φ(n) and cvsR(n, n) ≥ φ(n) for all n. For orthogonal TRSs R we prove that there is a constant k such that: (a) vsR(m, n) is bounded from above by a function exponential in k and (b) cvsR(m, n) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy. Similarly, for λ-calculus, we show that vsR(m, n) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy.

KW - Church-Rosser property, Term rewriting, confluence, lambda calculus, upper bounds

U2 - 10.1145/2528934

DO - 10.1145/2528934

M3 - Journal article

SN - 1529-3785

VL - 14

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 4

M1 - 31

ER -