Least upper bounds on the size of confluence and Church-Rosser diagrams in term rewriting and \(\lambda\)-calculus. (English) Zbl 1354.68143

Ketema, Jeroen; Simonsen, Jakob Grue

ACM Trans. Comput. Log. 14, No. 4, Article No. 31, 28 p. (2013).

Summary: We study confluence and the Church-Rosser property in term rewriting and \({\lambda}\)-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\rightarrow {}^\ast s' {}^\ast \leftarrow t'\) expressed as a function:
\hsize – for confluence a function \(\text{vs}_R(m,n)\) where the valleys are for peaks \(t {}^\ast\leftarrow s \rightarrow {}^\ast t'\) with \(s\) of size at most \(m\) and the reductions of maximum length \(n\), and
\hsize – for the Church-Rosser property a function \(\text{cvs}_R(m,n)\) where the valleys are for conversions \(t \leftrightarrow {}^\ast t'\) with \(t\) and \(t\)’ of size at most \(m\) and the conversion of maximum length \(n\).
For confluent Term Rewriting Systems (TRSs), we prove that \(\text{vs}_R\) is a total computable function, and for linear such systems that \(\text{cvs}_R\) is a total computable function. Conversely, we show that every total computable function is the lower bound on the functions \(\text{vs}_R(m,n)\) and \(\text{cvs}_R(m,n)\) for some TRS \(R\): In particular, we show that for every total computable function \(\varphi: \mathbb N \to \mathbb N\) there is a TRS \(R\) with a single term \(s\) such that \(\text{vs}_R(| s|,n)\geq \varphi(n)\) and \(\text{cvs}_R(n,n)\geq \varphi(n)\) for all \(n\). For orthogonal TRSs \(R\) we prove that there is a constant \(k\) such that: (a) \(\text{vs}_R(m,n)\) is bounded from above by a function exponential in \(k\) and (b) \(\text{cvs}_R(m,n)\) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy. Similarly, for \({\lambda}\)-calculus, we show that \(\text{vs}_R(m,n)\) is bounded from above by a function in the fourth level of the Grzegorczyk hierarchy.

Reviewer: Reviewer (Berlin)

MSC:

68Q42	Grammars and rewriting systems
03B40	Combinatory logic and lambda calculus
03D20	Recursive functions and relations, subrecursive hierarchies

Keywords:

Church-Rosser property; term rewriting; confluence; lambda calculus; upper bounds; computable function; Grzegorczyk hierarchy