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 -