# zbMATH — the first resource for mathematics

Least upper bounds on the size of confluence and Church-Rosser diagrams in term rewriting and $$\lambda$$-calculus. (English) Zbl 1354.68143
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
Full Text: