Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments \(\mu (f)\subseteq \{1,\ldots ,k\}\) of k-ary function symbols f only. Terms which cannot be further rewritten in this way are called \(\mu \)-normal forms. For left-linear term rewriting systems (TRSs), the so-called normalization via\(\mu \)-normalization procedure provides a systematic way to obtain normal forms by the stepwise computation and combination of intermediate \(\mu \)-normal forms. In this paper, we show how to obtain bounds on the derivational complexity of computations using this procedure by using bounds on the derivational complexity of context-sensitive rewriting. Two main applications are envisaged: Normalization via \(\mu \)-normalization can be used with non-terminating TRSs where the procedure still terminates; on the other hand, it can be used to improve on bounds of derivational complexity of terminating TRSs as it discards many rewritings.
Notes
Partially supported by the EU (FEDER), and projects RTI2018-094403-B-C32 and PROMETEO/2019/098.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
In term rewriting [5] and rewriting-based languages, including lazy functional languages like Haskell [19], the normal form t of expressions s is often achieved by first obtaining a head-normal formu, i.e., a term which does not rewrite to a redex (i.e., there is no rule \(\ell \rightarrow r\) such that \(u\rightarrow ^*\sigma (\ell )\) for some substitution \(\sigma \)). Therefore, such a term u has a stable root symbol f which cannot be changed by further rewritings. Thus, we can write \(u=f(s_1,\ldots ,s_k)\) for some terms \(s_1,\ldots ,s_k\) and recursively continue the normalization process starting from \(s_1,\ldots ,s_k\) to obtain normal forms \(t_1,\ldots ,t_k\) which are then used to finally return \(t=f(t_1,\ldots ,t_k)\). This procedure, though, has an important drawback: It is undecidable whether shas (or uis) a head-normal form [44, Section 8]. In context-sensitive rewriting (CSR [40]), the normalization via\(\mu \)-normalization procedure ([40, Section 9.3], \(\textit{N} \mu \textit{N}\) in the following) plays a similar role and can be used in programming languages like CafeOBJ [20], Maude [11] or OBJ [24], which permit the use of syntactic replacement restrictions à la CSR as follows. Each k-ary symbol f of the signature is given replacement restrictions by means of a replacement map \(\mu \) which defines a subset \(\mu (f)\subseteq \{1,\ldots ,k\}\) of (active) arguments of f which can be rewritten; rewriting is forbidden on arguments \(i\notin \mu (f)\) (often called frozen). Such a restriction is top-down propagated to the structure of terms s so that we distinguish between active and frozen positions of subterms, with the topmost position always active. In CSR only subterms at active positions can be rewritten (denoted \(s\hookrightarrow _{}t\)).
Example 1
(Running example I) Consider the following variant \(\mathcal{R}\) of a TRS in [40, Example 8.20]:
with \(\mu ({\mathsf {f}})=\mu ({\mathsf {h}})=\varnothing \) and \(\mu ({\mathsf {g}})=\{1\}\). We have \(\underline{{\mathsf {a}}}\hookrightarrow \underline{{\mathsf {h}}({\mathsf {a}})}\hookrightarrow {\mathsf {b}}\). However, \({\mathsf {h}}(\underline{{\mathsf {a}}})\not \hookrightarrow {\mathsf {h}}({\mathsf {h}}({\mathsf {a}}))\), as subterm \({\mathsf {a}}\) is not active in \({\mathsf {h}}({\mathsf {a}})\).
Advertisement
Terms which cannot be further rewritten using CSR are called \(\mu \)-normal forms. In general, they can contain reducible terms, i.e., they are not normal forms.
Example 2
(Running example II) Consider \(\mathcal{R}=\{{\mathsf {app}}({\mathsf {app}}(x,y),z) \rightarrow {\mathsf {app}}(x,{\mathsf {app}}(y,z))\}\) [46, Example 1] together with \(\mu ({\mathsf {app}})=\{1\}\). We have
where u is a \(\mu \)-normal form which is not a normal form.
In \(\textit{N} \mu \textit{N}\), \(\mu \)-normal forms play the role of head-normal forms: In order to obtain the normal form t of a term s, we first obtain a \(\mu \)-normal form u of s and then jump into the maximal (in size) frozen subterms of u, which are below the so-called maximal replacing context\( MRC ^\mu (u)\) of u, to continue the normalization. This is sketched in Fig. 1. The good point of \(\mu \)-normal forms is that they are decidable (see [40, Sect. 6]).
Fig. 1
Normalization via \(\mu \)-normalization
×
Remark 1
(Normalization via\(\mu \)-normalization inMaude) Since replacement maps can be used in Maude (see [40, Section 4.3]), an implementation of \(\textit{N} \mu \textit{N}\) in Full Maude [11, Chapter 18] wyas developed in [16]. In [41, Sect. 10.2] an implementation using Maude’s strategy language [17, 54] is described, see
The study of the length of rewriting computations (i.e., the number of rewriting steps) can be understood as an efficiency measure regarding the ‘time’ they take. Given a terminating TRS \(\mathcal{R}\) and a term s, the derivational height of s (written \(\mathsf {dh}(s,\rightarrow )\)) is defined as the maximum length of rewriting sequences \(s=s_1\rightarrow s_2\rightarrow \cdots \rightarrow s_m\) starting from s. Then, the derivational complexity, \(\mathsf {dc}_\mathcal{R}(n)\), of \(\mathcal{R}\) is the maximum derivational height of terms s of size |s| at most n, i.e., \(|s|\le n\). After Hofbauer and Lautemann’s pioneering work [33], the use of termination proofs to obtain bounds on \(\mathsf {dc}_\mathcal{R}(n)\) has been investigated by several authors focusing on the use of polynomials [7‐9, 51], matrices [18, 46, 48, 58], recursive path orderings [10, 32, 59], dependency pairs [29, 45], etc. Also, a number of tools have been developed to automatically (try to) obtain derivational complexity bounds for TRSs, see [23] and the references therein.
1.1 Contributions of the Paper
In this paper, we investigate derivational complexity of CSR and derivational complexity of \(\textit{N} \mu \textit{N}\), also in connection with derivational complexity of rewriting. It is obvious that CSR can be used to avoid reductions. Furthermore, under some assumptions it is able to simulate rewriting computations and compute normal forms (see [40, Section 5.2]). In this case, CSR can be used to put bounds on the length of normalizing sequences when CSR can be taken as a rewriting strategy.
Example 3
(Running Example III) Consider the following TRS \(\mathcal{R}\) [4, Example 3.23]:
As discussed in [4], \(\mathcal{R}\) cannot be proved terminating by using a simplification ordering [14], in particular polynomial interpretations over the naturals or (variants of) recursive path orderings. Matrix interpretations also fail to prove \(\mathcal{R}\) terminating. When using AProVE [22] to obtain derivational complexity bounds for \(\mathcal{R}\), a linear lower bound is given, but no upper bound is provided (reported as \(\mathtt{BOUNDS(n^1, INF)}\)). However, when considering \(\mu ({\mathsf {f}})=\mu ({\mathsf {s}})=\{1\}\), it is possible to prove that CSR suffices to compute any normal form of terms s. Furthermore, we show that the length of context-sensitive computations is bounded by O(n), see Example 19.
The ability of CSR to ‘reinforce’ termination can be used to guarantee that CSR or \(\textit{N} \mu \textit{N}\) terminates even if \(\mathcal{R}\) is non-terminating. Thus, we can investigate derivational complexity for such non-terminating TRSs.
Example 4
Although \(\mathcal{R}\) in Example 1 is not terminating (due to rule (1)), it is normalizing (i.e., every term has a normal form) and for all ground terms tCSR is able to obtain the normal form of t (see Example 10 and Corollary 1). Also, CSR terminates for all terms (see Example 14), and we actually obtain a constant bound O(1) on the derivational complexity of CSR.
In some cases, though, CSR is not able to directly obtain normal forms and often stops yielding a \(\mu \)-normal form (see Example 2). In this case, \(\textit{N} \mu \textit{N}\) can be used to approximate derivational complexity of terminating TRSs by using derivational complexity of CSR, often obtaining ‘improved’ complexity bounds.
Example 5
(Running example IV) Consider the TRS \(\mathcal{R}\) in [55, Example 8]:
Steinbach proved \(\mathcal{R}\) polynomially terminating1 by using a polynomial interpretation with quadratic polynomials (see Example 11). According to [33], a doubly exponential bound \(2^{2^{O(n)}}\) would be given on \(\mathsf {dc}_\mathcal{R}(n)\). If the replacement map \(\mu (\wedge )=\{2\}\) and \(\mu (f)=\{1,\ldots ,ar(f)\}\) for any other symbol f is used, we can improve it (for \(\textit{N} \mu \textit{N}\)) to \(2^{O(n^2)}\) (Example 39).
After some general preliminaries in Sect. 2 and a brief summary of context-sensitive rewriting in Sect. 3, Sect. 4 provides the technical definitions on derivational complexity. Section 5 summarizes the bounds obtained from several termination techniques. Section 6 introduces derivational complexity of CSR and provides some results which permit the obtention of bounds on derivational complexity of CSR. Section 7 defines normalization via \(\mu \)-normalization. Section 8 introduces an extension of CSR called layeredCSR (LCSR). Then, \(\textit{N} \mu \textit{N}\) is formulated as normalization using LCSR. A sufficient criterion for proving termination of \(\textit{N} \mu \textit{N}\) for non-terminating TRSs is also given. Section 9 defines computational complexity of \(\textit{N} \mu \textit{N}\) as the derivational complexity of LCSR. Section 10 discusses how to obtain bounds on derivational complexity of \(\textit{N} \mu \textit{N}\). Section 11 shows how to obtain bounds on derivational complexity of \(\textit{N} \mu \textit{N}\) from bounds on derivational complexity of CSR. Section 12 discusses some related work. Section 13 concludes.
2 Preliminaries
This section collects some definitions and notations about term rewriting. More details and missing notions can be found in [5, 50, 57]. In the following, \(\mathcal{P}(A)\) denotes the power set of a set A. The cardinality of a finite set A is denoted as |A|.
Given a binary relation \(\mathsf {R}\subseteq A\times A\) on a set A, we often write \(a\,\mathsf {R}\,b\) instead of \((a,b)\in \mathsf {R}\). Given two relations \(\mathsf {R},\mathsf {R}'\subseteq A\times A\), their composition is defined by \(\mathsf {R}\circ \mathsf {R}'=\{(a,b)\in A\times A\mid (\exists c)\, a\,\mathsf {R}\,c\,\wedge \, c\,\mathsf {R}'\,b\}\). Also, for all \(n\in \mathbb {N}\), the n-fold composition \(\mathsf {R}^n\) of \(\mathsf {R}\) is defined by \(\mathsf {R}^0=\{(x,x)\mid x\in A\}\) and \(\mathsf {R}^{n}=\mathsf {R}\circ \mathsf {R}^{n-1}\) if \(n>0\). The transitive closure of \(\mathsf {R}\) is denoted by \(\mathsf {R}^+\), and its reflexive and transitive closure by \(\mathsf {R}^*\). The relation \(\mathsf {R}\) is finitely branching if for all \(a\in A\), the set \(\{a\,\mathsf {R}\,b\mid b\in A\}\) of direct successors of a is finite. An element \(a\in A\) is irreducible (or an \(\mathsf {R}\)-normal form), if there exists no b such that \(a\,\mathsf {R}\,b\); we say that b is an \(\mathsf {R}\)-normal form of a (written \(a\,\mathsf {R}^!\,b\)) if \(a~\mathsf {R}^*b\) and b is an \(\mathsf {R}\)-normal form. We also say that a is \(\mathsf {R}\)-normalizing, and that a has an \(\mathsf {R}\)-normal form. Also, \(\mathsf {R}\) is normalizing if every \(a\in A\) has an \(\mathsf {R}\)-normal form. Given \(a\in A\), if there is no infinite sequence \(a=a_1~\mathsf {R}~a_2~\mathsf {R}~\cdots ~\mathsf {R}~a_n~\mathsf {R}\cdots \), then a is \(\mathsf {R}\)-terminating; \(\mathsf {R}\) is terminating (or well-founded2); if a is \(\mathsf {R}\)-terminating for all \(a\in A\). We say that \(\mathsf {R}\) is confluent if, for every \(a,b,c\in A\), whenever \(a~\mathsf {R}^*b\) and \(a~\mathsf {R}^*c\), there exists \(d\in A\) such that \(b~\mathsf {R}^*d\) and \(c~\mathsf {R}^*d\).
Throughout the paper, \({\mathcal{X}}\) denotes a countable set of variables and \({\mathcal{F}}\) denotes a signature, i.e., a set of function symbols \(f,g \ldots \), each having a fixed arity ar(f). The set of terms built from \({\mathcal{F}}\) and \({\mathcal{X}}\) is \({{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\). The set of variables in a term t is denoted \(\mathcal{V}ar(t)\). Let \(\Box \notin {\mathcal{F}}\cup {\mathcal{X}}\) be a special constant symbol. A context is a term in \({\mathcal{T}({\mathcal{F}}\cup \{\Box \},{\mathcal{X}})}\). If \(C[,\ldots ,]\) is a context with n occurrences of \(\Box \), then \(C[t_1,\ldots ,t_n]\) is the result of replacing the occurrences of \(\Box \) with \(t_1,\ldots ,t_n\) from left to right. A context containing precisely one occurrence of \(\Box \) is denoted by \(C[\,]\). A term is said to be linear if no variable occurs more than once in t. Terms are viewed as labeled trees in the usual way. Positions\(p,q,\ldots \) are sequences of positive natural numbers used to address subterms of t. We denote the empty sequence by \(\Lambda \). Given positions p, q, we denote their concatenation as p.q. Positions are ordered by the standard prefix ordering\(\le \), i.e., \(p\le q\) if \(q=p.p'\) for some position \(p'\). Given a set of positions P, \(minimal_\le (P)\) is the set of minimal positions of P w.r.t. \(\le \). If p is a position, and Q is a set of positions, \(p.Q=\{p.q~|~q\in Q\}\). We denote the empty chain by \(\Lambda \). The set of positions of a term t is \({\mathcal{P}os}(t)\). Positions of non-variable symbols in t are denoted as \({\mathcal{P}os}_{\mathcal{F}}(t)\), and \({\mathcal{P}os}_{\mathcal{X}}(t)\) are the positions of variables. The subterm of t at position p is denoted as \(t|_p\) and \(t[s]_p\) is the term t with the subterm at position p replaced by s. The symbol labeling the root of t is denoted as root(t). Given terms t and s, \({\mathcal{P}os}_s(t)\) denotes the set of positions of the subterm s in t, i.e., \({\mathcal{P}os}_s(t)=\{p\in {\mathcal{P}os}(t)\mid t|_p=s\}\). The depth\(\delta _t\) of a term t is the number of nodes on a branch of the term tree of t of maximal length: \(\delta _t=1\) if t is a variable or a constant; \(\delta _{t}=1+\max \{\delta _{t_1},\ldots ,\delta _{t_k}\}\) if \(t=f(t_1,\ldots ,t_k)\) [57, Definition 2.1.7]. The size of t, i.e., the number of symbols occurring in t is denoted |t|.
A rewrite rule is an ordered pair \((\ell ,r)\), written \(\ell \rightarrow r\), with \(\ell ,r\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\), \(\ell \not \in {\mathcal{X}}\) and \(\mathcal{V}ar(r)\subseteq \mathcal{V}ar(\ell )\). The left-hand side (lhs) of the rule is \(\ell \) and \(r\) is the right-hand side (rhs). A term rewriting system (TRS) is a pair \(\mathcal{R}=({\mathcal{F}}, R)\) where R is a set of rewrite rules. The set of lhs’s of \(\mathcal{R}\) is denoted as \(L(\mathcal{R})\) . An instance \(\sigma (\ell )\) of \(\ell \in L(\mathcal{R})\) by a substitution \(\sigma \) is a redex. The set of redex positions in t is \({\mathcal{P}os}_\mathcal{R}(t)\). A TRS \(\mathcal{R}\) is left-linear if for all \(\ell \in L(\mathcal{R})\), \(\ell \) is a linear term. A rule \(\ell \rightarrow r\) is collapsing if \(r\in {\mathcal{X}}\); it is duplicating if \(|{\mathcal{P}os}_x(\ell )|<|{\mathcal{P}os}_x(r)|\) for some variable x. A TRS \(\mathcal{R}\) is collapsing (resp. duplicating) if it contains a collapsing (resp. duplicating) rule. Given \(\mathcal{R}=({\mathcal{F}},R)\), we consider \({\mathcal{F}}\) as the disjoint union \({\mathcal{F}}={\mathcal{C}}\uplus {\mathcal{D}}\) of symbols \(c\in {\mathcal{C}}\), called constructors and symbols \(f\in {\mathcal{D}}\), called defined functions, where \({\mathcal{D}}=\{root(\ell )~|~\ell \rightarrow r\in R\}\) and \({\mathcal{C}}={\mathcal{F}}-{\mathcal{D}}\). Then, \({\mathcal{T}({\mathcal{C}},{\mathcal{X}})}\) (resp. \({\mathcal{T}({\mathcal{C}})}\)) is the set of (ground) constructor terms.
Given a TRS \(\mathcal{R}\), a term \(s\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) rewrites to t at position p, written \(s{\mathop {\rightarrow }\limits ^{p}}_\mathcal{R}t\) (or just \(s\rightarrow t\)), if \(s|_p=\sigma (\ell )\) and \(t=s[\sigma (r)]_p\), for some rule \(\ell \rightarrow r\) in \(\mathcal{R}\), \(p\in {\mathcal{P}os}(s)\) and substitution \(\sigma \). A TRS \(\mathcal{R}\) is terminating if \(\rightarrow _\mathcal{R}\) is terminating. A term s is a head-normal form (or root-stable) if there is no redex t such that \(s\rightarrow ^*_\mathcal{R}t\). A term is said to be root-normalizing if it has a root-stable reduct. The \(\rightarrow _\mathcal{R}\)-normal forms of \(\mathcal{R}\) are simply called normal forms; \({\mathsf {NF}}_\mathcal{R}\) is the set of normal forms of \(\mathcal{R}\). A term is said to be normalizing if it is \(\rightarrow _\mathcal{R}\)-normalizing. A TRS is normalizing if all terms are.
3 Context-Sensitive Rewriting
In this section, we provide some background on CSR, following [40]. Given a signature \({\mathcal{F}}\), a replacement map is a mapping \(\mu :{\mathcal{F}}\rightarrow \wp (\mathbb {N})\) satisfying that, for all symbols f in \({\mathcal{F}}\), \(\mu (f)\subseteq \{1,\ldots ,ar(f)\}\). The set of replacement maps for the signature \({\mathcal{F}}\) is \({M_{{\mathcal{F}}}}\) (or \({M_{\mathcal{R}}}\) for a TRS \(\mathcal{R}=({\mathcal{F}},R)\)). Replacement maps are compared as follows: \(\mu \sqsubseteq \mu '\) if for all \(f\in {\mathcal{F}},~ \mu (f)\subseteq \mu '(f)\); we often say that \(\mu \) is more restrictive than \(\mu '\). Extreme cases are \({\mu _\bot }\), which disallows replacements in all arguments: \({\mu _\bot }(f)=\varnothing \) for all \(f\in {\mathcal{F}}\), and \({\mu _\top }\), which restricts no replacement: \({\mu _\top }(f)=\{1,\ldots ,k\}\) for all k-ary symbols \(f\in {\mathcal{F}}\). We say that a binary relation \({\mathsf {R}}\) on terms is \(\mu \)-monotonic if for all k-ary symbols f, \(i\in \mu (f)\), and terms \(s_1,\ldots ,s_k,t_i\), if \(s_i\,{\mathsf {R}}\,t_i\), then \(f(s_1,\ldots ,s_i,\ldots ,s_k)\,{\mathsf {R}}\,f(s_1,\ldots ,t_i,\ldots ,s_k)\). The set \({\mathcal{P}os}^\mu (t)\) of \(\mu \)-replacing (oractive) positions of t is:
and \(\overline{{\mathcal{P}os}^\mu }(t)={\mathcal{P}os}(t)- {\mathcal{P}os}^\mu (t)\) is the set of non-\(\mu \)-replacing (or frozen) positions.
Example 6
For \(\mathcal{R}\) and \(\mu \) as in Example 5, Fig. 2 depicts the active and frozen (in gray) positions of \(\ell _{(8)}\) and \(r_{(8)}\).
Fig. 2
Active and frozen (in gray) positions of \(\ell _{(8)}\) and \(r_{(8)}\)
×
×
Given a term t, \(\mathcal{V}ar^\mu (t)\) (resp. ) is the set of variables occurring at active (resp. frozen) positions in t: \(\mathcal{V}ar^\mu (t)=\{x\in \mathcal{V}ar(t)\mid \exists p\in {\mathcal{P}os}^\mu (t),x=t|_p\}\) and . Note that variables in could also be in \(\mathcal{V}ar^\mu (t)\) and vice versa. For instance, \(\mathcal{V}ar^\mu (r_{(10)})=\{x,y\}\) and . Also, we write if t is a frozen subterm of s.
Context-sensitive rewriting (CSR) is the restriction of rewriting obtained when a replacement map \(\mu \) is used to specify the redex positions that can be contracted.
Definition 1
(Context-sensitive rewriting) Let \(\mathcal{R}\) be a TRS, \(\mu \in {M_{\mathcal{R}}}\) and s and t be terms. Then, s\(\mu \)-rewrites to t, written \(s{\mathop {\hookrightarrow }\limits ^{p}}_{\mathcal{R},\mu } t\) (or \(s\hookrightarrow _{\mathcal{R},\mu }t\), \(s\hookrightarrow _{\mu }t\), or even \(s\hookrightarrow _{}t\)), if \(s{\mathop {\rightarrow }\limits ^{p}}_\mathcal{R}t\) and p is active in s (i.e., \(p\in {\mathcal{P}os}^\mu (s)\)). We often use \(\rightarrow _{\not \mu }\) to denote rewriting at frozen positions: \(\rightarrow _{\not \mu }\,=\,\rightarrow -\hookrightarrow _{\mu }\).
If \(\hookrightarrow _{\mathcal{R},\mu }\) is confluent (resp. terminating), we say that \(\mathcal{R}\) is \(\mu \)-confluent (resp. \(\mu \)-terminating). The \(\hookrightarrow _{\mathcal{R},\mu }\)-normal forms are called \(\mu \)-normal forms and \(\mathsf {NF}^\mu _\mathcal{R}\) is the set of \(\mu \)-normal forms of \(\mathcal{R}\). The canonical replacement map\({\mu ^{ can }_\mathcal{R}}\) of a TRS \(\mathcal{R}\) is the most restrictive replacement map\(\mu \)ensuring that the non-variable subterms of the left-hand sides\(\ell \)of the rules\(\ell \rightarrow r\)of\(\mathcal{R}\)are active, i.e., \({\mathcal{P}os}_{\mathcal{F}}(\ell )\subseteq {\mathcal{P}os}^\mu (\ell )\). Given a TRS \(\mathcal{R}\), we let \({ CM _{\mathcal{R}}}=\{\mu \in {M_{\mathcal{R}}}\mid {\mu ^{ can }_\mathcal{R}}\sqsubseteq \mu \}\) be the set of replacement maps that are equal or less restrictive than the canonical replacement map. If \(\mu \in { CM _{\mathcal{R}}}\), we also say that \(\mu \) is a canonical replacement map for \(\mathcal{R}\); if \(\mu \) is exactly \({\mu ^{ can }_\mathcal{R}}\), we will speak about the canonical replacement map of \(\mathcal{R}\).
Example 7
The canonical replacement map \({\mu ^{ can }_\mathcal{R}}\) for \(\mathcal{R}\) in Example 1 is \({\mu _\bot }\). Thus, \(\mu \) in Example 1 is not the canonical replacement map (as \(\mu ({\mathsf {c}})=\{1\}\)), but \(\mu \in { CM _{\mathcal{R}}}\), i.e., it is a canonical replacement map.
For TRSs \(\mathcal{R}\) and canonical replacement maps \(\mu \in { CM _{\mathcal{R}}}\), we often say that \(\hookrightarrow _{\mathcal{R},\mu }\) performs canonical CSR [40, Sect. 5]. Canonical CSR is useful in (head) normalization and infinitary normalization with left-linear TRSs [40, Sect. 9].
4 Derivational Complexity in Term Rewriting
The following definition formalizes the standard notion of derivational complexity. The definition is given for abstract relations \(\mathsf {R}\) rather than TRSs.
Definition 2
(Derivational complexity) Let \(\mathsf {R}\) be a well-founded and finitely branching relation, and t be a term. Then, the derivational height of t is
Obviously, \(\mathsf {dh}(t,\mathsf {R})\), hence \(\mathsf {dc}_\mathsf {R}(n)\), is defined only if \(\mathsf {R}\) is well founded. Requiring that \(\mathsf {R}\) is also finitely branching, though, is often necessary.
Example 8
Consider the terminating TRS \(\mathcal{R}=\{a\rightarrow i\mid i\in \mathbb {N}\}\cup \{i+1\rightarrow i\mid i\in \mathbb {N}\}\). Note that \(\rightarrow _\mathcal{R}\) is not finitely branching. In particular, \(\mathsf {dh}(a,\rightarrow _\mathcal{R})\) is not defined because for all \(n\in \mathbb {N}\), a admits a rewrite sequence \(a\rightarrow n\rightarrow ^*0\) of length \(n+1\).
In this paper, we deal with TRSs \(\mathcal{R}=({\mathcal{F}},R)\) and (subsets of) the rewrite relation \(\rightarrow _\mathcal{R}\). Thus, along the paper we assume \(\rightarrow _\mathcal{R}\) to be finitely branching (thus, \(\hookrightarrow _{\mathcal{R},\mu }\) also is). A sufficient condition making \(\rightarrow _\mathcal{R}\) finitely branching is requiring R to be finite.3 This is often the case in most practical uses.
Notation 1
In the following, when dealing with TRSs \(\mathcal{R}\) and the rewrite relation \(\rightarrow _\mathcal{R}\), we use \(\mathsf {dc}_\mathcal{R}\) instead of \(\mathsf {dc}_{\rightarrow _\mathcal{R}}\).
4.1 Use of Ground Terms in Term Rewriting
For TRSs \(\mathcal{R}=({\mathcal{F}},R)\) whose signature \({\mathcal{F}}\) contains a constant symbol a, we have \({{\mathcal{T}({\mathcal{F}})}}\ne \varnothing \). In this case, by closedness of term rewriting with respect to substitution application (see, e.g., [5, Definition 4.2.2]), every rewrite sequence \(s_1\rightarrow _\mathcal{R}s_2\rightarrow _\mathcal{R}\cdots \rightarrow _\mathcal{R}s_n\) has a corresponding (ground) rewrite sequence \(s'_1\rightarrow _\mathcal{R}s'_2\rightarrow _\mathcal{R}\cdots \rightarrow _\mathcal{R}s'_n\) of the same length which is obtained by replacing, for all \(1\le i\le n\), all variable occurrences in \(s_i\) by a to obtain \(s'_i\). Thus, \(\mathsf {dh}_\mathcal{R}\) remains unchanged if only ground terms are considered, i.e., we have
If \({\mathcal{F}}\) contains no constant symbol, we can add a fresh constant \(\bullet \) to obtain \({\mathcal{F}}^\bullet ={\mathcal{F}}\cup \{\bullet \}\). It is also well known that this does not affect termination of \(\mathcal{R}\) [56]. Given a term \(t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\), a ground term \(t^\bullet \in {\mathcal{T}({\mathcal{F}}^\bullet )}\) is obtained by replacing all variables in t by \(\bullet \). We have the following.
Proposition 1
Let \(\bullet \) be a constant symbol, \(\mathcal{R}=({\mathcal{F}},R)\) be a TRS where \(\bullet \notin {\mathcal{F}}\) and \(\mathcal{R}^\bullet =({\mathcal{F}}^\bullet ,R)\). Then, for all \(n\in \mathbb {N}\), \(\mathsf {dc}_\mathcal{R}(n)=\mathsf {dc}_{\mathcal{R}^\bullet }(n)\).
Proof
Let \(s\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) and \(s=s_1\rightarrow _\mathcal{R}s_2\rightarrow _\mathcal{R}\cdots \rightarrow _\mathcal{R}s_m\) for some terms \(s_1,\ldots ,s_m\). Since rewriting is closed under substitutions, for all \(1\le i\le m\), we can instantiate each variable in \(s_i\) with \(\bullet \) to obtain \(s^\bullet =s^\bullet _1\rightarrow _\mathcal{R}s^\bullet _2\rightarrow _\mathcal{R}\cdots \rightarrow ^\bullet _\mathcal{R}s_m\). Since the rules in \(\mathcal{R}\) and \(\mathcal{R}^\bullet \) coincide, we have \(s^\bullet _1\rightarrow _{\mathcal{R}^\bullet } s^\bullet _2\rightarrow _{\mathcal{R}^\bullet }\cdots \rightarrow ^\bullet _{\mathcal{R}^\bullet } s^\bullet _m\). Hence, \(\mathsf {dh}(s,\rightarrow _\mathcal{R})\le \mathsf {dh}(s^\bullet ,\rightarrow _{\mathcal{R}^\bullet })\). Since the signature of \(\mathcal{R}^\bullet \), i.e., \({\mathcal{F}}^\bullet \), contains a constant symbol \(\bullet \), and for all terms \(t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\), \(|t|=|t^\bullet |\), by using (11), we conclude \(\mathsf {dc}_\mathcal{R}(n)\le \mathsf {dc}_{\mathcal{R}^\bullet }(n)\).
Now let \(s=s_1\rightarrow _{\mathcal{R}^\bullet } s_2\rightarrow _{\mathcal{R}^\bullet }\cdots \rightarrow _{\mathcal{R}^\bullet } s_m\), for some \(s\in {\mathcal{T}({\mathcal{F}}^\bullet ,{\mathcal{X}})}\). Since rules in \(\mathcal{R}\) and \(\mathcal{R}^\bullet \) coincide, we have \(s_1\rightarrow _{\mathcal{R}} s_2\rightarrow _{\mathcal{R}}\cdots \rightarrow _{\mathcal{R}} s_m\). Now replace each occurrence of \(\bullet \) in terms \(s_i\), \(1\le i\le m\) by a variable \(x\in {\mathcal{X}}\) to obtain a term \(s'_i\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\). Since \(\bullet \) does not occur in any rule of \(\mathcal{R}\), we have \(s'_1\rightarrow _\mathcal{R}s'_2\rightarrow _\mathcal{R}\cdots \rightarrow _\mathcal{R}s'_m\). Thus, we have \(\mathsf {dh}(s,\rightarrow _{\mathcal{R}^\bullet })\le \mathsf {dh}(s',\rightarrow _\mathcal{R})\). Since for all terms \(t\in {\mathcal{T}({\mathcal{F}}^\bullet ,{\mathcal{X}})}\), \(|t|=|t'|\), we obtain \(\mathsf {dc}_{\mathcal{R}^\bullet }(n)\le \mathsf {dc}_\mathcal{R}(n)\). Therefore, we obtain \(\mathsf {dc}_\mathcal{R}(n)=\mathsf {dc}_{\mathcal{R}^\bullet }(n)\), as desired.
Remark 2
(Non-empty set of ground terms) Proposition 1 means that, whether the signature \({\mathcal{F}}\) of a TRS \(\mathcal{R}=({\mathcal{F}},R)\) contains constant symbols or not, we can add a fresh constant \(\bullet \) to \({\mathcal{F}}\) without changing the complexity bounds. In the following, it is often important to be able to guarantee that \({{\mathcal{T}({\mathcal{F}})}}\ne \varnothing \) holds, i.e., \({\mathcal{F}}\) contains a constant symbol. Thus, as a kind of preprocessing, we can systematically use \(\mathcal{R}^\bullet =({\mathcal{F}}^\bullet ,R)\) instead of \(\mathcal{R}\).
4.2 Derivational Complexity and Strategies
A non-deterministic one-step rewriting strategy is a function \(\mathsf{S}\) that assigns a non-empty subset \(\mathsf{S}(t)\subseteq {\mathcal{P}os}_\mathcal{R}(t)\) of redexes to every reducible term t [6, 44]. We write \(s\rightarrow _\mathsf{S}t\) if \(s{\mathop {\rightarrow }\limits ^{p}}t\) and \(p\in \mathsf{S}(t)\). A strategy \(\mathsf{S}\) is normalizing if for all normalizing terms t no infinite \(\rightarrow _\mathsf{S}\)-sequence starts from t. The notions and notations in Definition 2 apply to normalizing strategies \(\mathsf{S}\) for normalizing TRSs \(\mathcal{R}\) to yield \(\mathsf {dh}(t,\rightarrow _\mathsf{S})\) for normalizing terms t and \(\mathsf {dc}_{\rightarrow _\mathsf{S}}(n)\) (or just \(\mathsf {dc}_\mathsf{S}(n)\)) as the derivational height and complexity of computations using a strategy \(\mathsf{S}\). Obviously, for terminating TRSs \(\mathcal{R}\) and arbitrary strategies \(\mathsf{S}\),
(Strategies in derivational complexity analysis) There are non-terminating, but normalizing TRSs \(\mathcal{R}\) (where \(\mathsf {dc}_\mathcal{R}\) is not defined) for which a given strategy \(\mathsf{S}\) is still normalizing and \(\mathsf {dc}_\mathsf{S}\) defined. This is a positive aspect of analyzing derivational complexity of strategies. Another aspect is that in real-life programming languages a particular strategy \(\mathsf{S}\) (rather than full rewriting) is implemented and used. In this case, \(\mathsf {dc}_\mathsf{S}\) is a more realistic bound for practical uses than \(\mathsf {dc}_\mathcal{R}\).
Derivational complexity (bounds) for specific rewriting strategies like innermost rewriting (where only redexes not containing other redexes are contracted) have been investigated [29, 49]. The obtained bounds often differ from full rewriting.
Example 9
If computations with \(\mathcal{R}\) in Example 3 are restricted to innermost rewriting, AProVE yields \(\mathtt{BOUNDS(n^1, n^2)}\), i.e., a linear lower bound (displayed as \(\mathtt{n^1}\) in the first argument) and a quadratic upper bound (\(\mathtt{n^2}\) in the second argument), instead of \(\mathtt{BOUNDS(n^1, INF)}\), where a linear lower bound was found but no finite upper bound could be obtained.
Although, in general, CSR is not a rewriting strategy (as it is unable to reduce terms in \(\mu \)-normal form which are not normal forms, see [40, Remark 1.2] for a discussion), in some cases we can rely on the following result to faithfully use bounds on \(\mathsf {dc}_\mu (n)\) as bounds for (a subclass of) normalizing sequences for TRSs.
Theorem 1
[40, Theorem 5.8] Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\). Let s, t be terms such that \({\mathcal{P}os}(t)={\mathcal{P}os}^\mu (t)\). Then, \(s\rightarrow ^*t\) if and only if \(s\hookrightarrow _{\mu }^*t\).
Given a TRS \(\mathcal{R}=({\mathcal{F}},R)\) with \({\mathcal{F}}={\mathcal{C}}\,\uplus \,{\mathcal{D}}\), a defined symbol \(f\in {\mathcal{D}}\) is called completely defined if no ground normal form contains such a symbol; \(\mathcal{R}\) is completely defined if all defined symbols are completely defined. We have the following.
Corollary 1
Let \(\mathcal{R}\) be a completely defined left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that, for all constructor symbols \(c\in {\mathcal{C}}\), \(\mu (c)={\mu _\top }(c)\). Let s and t be terms, with t ground. Then, \(s\rightarrow ^!t\) if and only if \(s\hookrightarrow ^!_{\mu }t\).
Proof
Since \(\mathcal{R}\) is completely defined, t is a constructor term and \({\mathcal{P}os}^\mu (t)={\mathcal{P}os}(t)\). By Theorem 1, the conclusion follows.
Example 10
Note that \(\mathcal{R}\) in Example 1, with defined symbols \({\mathsf {a}}\), \({\mathsf {f}}\), and \({\mathsf {h}}\) is completely defined as there is a rule that applies to the root of any term \({\mathsf {a}}\), \({\mathsf {f}}(t)\) and \({\mathsf {h}}(t)\) for all terms t. Also, it is not difficult to prove, by induction on the structure of the ground normal form t, that \(\mathcal{R}\) in Example 3 is completely defined.
As a consequence of Corollary 1, for left-linear, completely defined TRSs \(\mathcal{R}\) and \(\mu \in { CM _{\mathcal{R}}}\) satisfying \(\mu (c)={\mu _\top }(c)\) for all constructor symbols c, the set of ground normal forms of \(\mathcal{R}\) and the set of ground \(\mu \)-normal forms of \(\mathcal{R}\) coincide. Thus, dealing with ground terms t, CSR can be seen as a (non-deterministic) one-step rewriting strategy given by \(\mathsf{S}_{ CSR }(t)={\mathcal{P}os}^\mu _\mathcal{R}(t)\). It is often the case that \(\mathsf {dc}_{\mathsf{S}_{ CSR }}\) can be used when \(\mathsf {dc}_\mathcal{R}\) is undefined (Example 18), or improves on \(\mathsf {dc}_\mathcal{R}\) as suggested by (12), see Example 19.
Remark 4
(Reinforcing completely definedness?) In view of the previous discussion, one could think of adding rules of the shape \(f(x_1,\ldots ,x_k)\rightarrow \bot \) (where \(\bot \) is a fresh constant symbol) to each defined symbol \(f\in {\mathcal{D}}\) so that \(\mathcal{R}\) becomes completely defined whilst the maximal length of rewriting sequences in such a new TRS \(\mathcal{R}_\bot \) barely changes, i.e., \(\mathsf {dc}_\mathcal{R}\) and \(\mathsf {dc}_{\mathcal{R}_\bot }\) (asymptotically) coincide. However, the set \(\mathsf {NF}_{\mathcal{R}_\bot }\) of normal forms of \(\mathcal{R}_\bot \) would in general lack some normal forms of \(\mathcal{R}\) due to the addition of rules as above. In this situation, the use of Corollary 1 with \(\mathcal{R}_\bot \) to obtain bounds on \(\mathsf {dc}_\mathcal{R}\) using (12) with \(\mathsf{S}_{ CSR }\) based on \(\mathcal{R}_\bot \) and \(\mu \) would be misleading as many \(\mathcal{R}\)-normal forms would not be really approximated using CSR.
5 Termination Proofs and Complexity Bounds
As remarked above, derivational complexity bounds are often obtained from the method to obtain a termination proof. We summarize the ones we use in the paper, namely polynomial and matrix interpretations which are particular cases of the semantic approach to prove termination of rewriting often called termination by interpretation [60] and also [50, Sect. 5.2.1].
5.1 Termination by Interpretation
Given a signature \({\mathcal{F}}\), an \({\mathcal{F}}\)-algebra \(\mathcal{A}\) consists of a set (by abuse, also denoted \(\mathcal{A}\)) together with a mapping \(f^\mathcal{A}:\mathcal{A}^k\rightarrow \mathcal{A}\), for each k-ary symbol \(f\in {\mathcal{F}}\). Terms t are interpreted by induction on their structure by using valuation mappings \(\alpha :{\mathcal{X}}\rightarrow \mathcal{A}\) to give meaning to variables inside as follows: (i) \([\alpha ]_\mathcal{A}(x)=\alpha (x)\) if \(x\in {\mathcal{X}}\) and (ii) \([\alpha ]_\mathcal{A}(f(t_1,\ldots ,t_k))=f^\mathcal{A}([\alpha ]_\mathcal{A}(t_1),\ldots ,[\alpha ]_\mathcal{A}(t_k))\). If \(\mathcal{A}\) is supplied with a well-founded relation \(\succ \) on \(\mathcal{A}\), then \((\mathcal{A},\succ )\) is called a well-founded\({\mathcal{F}}\)-algebra. Mappings \(f^\mathcal{A}\) are often required to be monotone, i.e., for all \(i\in \{1,\ldots ,k\}\) and \(x_1,\ldots ,x_k,y_i\in \mathcal{A}\), if \(x_i\succ y_i\), then \(f^\mathcal{A}(x_1,\ldots ,x_i,\ldots ,x_k)\succ f^\mathcal{A}(x_1,\ldots ,y_i,\ldots ,x_k)\). In this case, \((\mathcal{A},\succ )\) is a monotone well-founded\({\mathcal{F}}\)-algebra. A well-founded monotone algebra \((\mathcal{A},\succ )\) induces a reduction ordering\(\succ _\mathcal{A}\) on terms: \(s\succ _\mathcal{A}t\) iff for all valuations \(\alpha \), \([\alpha ]_\mathcal{A}(s)\succ [\alpha ]_\mathcal{A}(t)\). We say that \((\mathcal{A},\succ )\) is compatible with a TRS \(\mathcal{R}\) if \(\ell \succ _\mathcal{A}r\) for all \(\ell \rightarrow r\in \mathcal{R}\). A TRS is terminating if and only if it admits a compatible non-empty well-founded monotone algebra [60, Proposition 1].
5.1.1 Polynomial Interpretations
The use of polynomials for proving termination of rewriting goes back to Manna and Ness [42] and Lankford [35] (see also [12, 39] and the references therein). In a polynomial interpretation (PI) \(\mathcal{A}\), the domain \(\mathcal{A}\) is an infinite interval of natural or positive real numbers, and the well-founded relation \(\succ \) on \(\mathcal{A}\) is the usual order over the naturals \(>_\mathbb {N}\) (in the first case) or the ordering \(>_\delta \) over the reals in the second case, where \(\delta \) is a positive number and \(x>_\delta y\) if and only if \(x-y\ge \delta \) [39]. Mappings \(f^\mathcal{A}\) are obtained, for each \(x_1,\ldots ,x_k\in \mathcal{A}\) by evaluating a polynomial \(\sum _{\vec {\alpha }\in \mathbb {N}^k}f_{\vec {\alpha }} x^{\vec {\alpha }}\), where, for each tuple \(\vec {\alpha }\) of k natural numbers \(\alpha _1,\ldots ,\alpha _k\in \mathbb {N}\), the coefficient\(f_{\vec {\alpha }}\) is a number multiplying the monomial \(x^{\vec {\alpha }}=x_1^{\alpha _1}\cdots x_k^{\alpha _k}\) of the polynomial.
Remark 5
(Terms as polynomials) Terms t interpreted by using a polynomial interpretation \(\mathcal{A}\) yield polynomials\(t^\mathcal{A}\) obtained by using variable names (ranging now on the domain of the polynomial interpretation) instead of valuation mappings \(\alpha \).
Example 11
(Running example IV—polynomial termination) The TRS \(\mathcal{R}\) in Example 5 is proved terminating by using a reduction ordering \(\succ _\mathcal{A}\) obtained from a polynomial interpretation \(\mathcal{A}\) as follows [55, Example 11]4
The subtraction \(\ell ^\mathcal{A}_{(10)}-r^\mathcal{A}_{(10)}\) of both polynomials yields \(x^2+y^2-xy+3x+y+6=(x-y)^2+xy+3x+y+6\), which is clearly positive for all \(x,y\ge 0\). This proves \(\succ _\mathcal{A}\) compatible with rule (10), i.e., \(\ell _{(10)}\succ _\mathcal{A}r_{(10)}\) holds.
In this paper, we often restrict the attention to interpretations with simply shaped polynomials, like linear polynomials \(f^\mathcal{A}(x_1,\ldots ,x_k)=f_1x_1+\cdots +f_kx_k+f_0\), where \(f_i\ge 1\) for all \(1\le i\le k\) (due to the monotonicity requirements), or even strongly linear polynomials \(f^\mathcal{A}(x_1,\ldots ,x_k)=x_1+\cdots +x_k+f_0\). Also, for simplicity we restrict the attention to polynomials over the naturals, i.e., the interpretation domain is \(\mathbb {N}\), and hence, the polynomial coefficients \(f_i\) are natural numbers as well.
5.1.2 Matrix Interpretations
In matrix interpretations (over the naturals) \(\mathcal{A}\) [18], the interpretation domain is \(\mathbb {N}^d\), the set of tuples (or vectors) \(\mathbf {x}\) of d natural numbers. Mappings \(f^\mathcal{A}\) are expressions \(\sum _{i=1}^kF_ix_i+\mathbf {f}_0\), where \(\mathbf {f}_0\) is a vector of d natural numbers and \(F_1,\ldots ,F_k\) are d-square matrices of natural numbers. Monotonicity of \(f^\mathcal{A}\) is guaranteed if, for all \(1\le i\le k\), the top leftmost entry \((F_i)_{11}\) is positive, i.e., \((F_i)_{11}\ge 1\).
Remark 6
(Terms as affine mappings) As usual, terms t interpreted by using a matrix interpretation \(\mathcal{A}\) yield affine mappings\(t^\mathcal{A}\) which are obtained by just replacing the use of valuation mappings \(\alpha \) by the variable name (ranging now on the domain of the matrix interpretation), i.e., \(x^\mathcal{A}=\mathbf {x}\) and \(f(t_1,\ldots ,t_k)^\mathcal{A}=f^{\mathcal{A}}(t^\mathcal{A}_1,\ldots ,t^\mathcal{A}_k)\).
The following order \(\succ \) is often used (see also[47]): for all \(x_1,\ldots ,x_d,y_1,\ldots ,y_d\in \mathbb {N}\),
$$\begin{aligned} (x_1,\ldots ,x_d)\succ (y_1,\ldots ,y_d)&\text {iff}&x_1>_\mathbb {N}y_1 \text { and } x_i\ge _\mathbb {N}y_i \text { for all}\quad 2\le i\le d \end{aligned}$$
(13)
In a triangular matrix interpretation (TMI), all matrices \(F_i\) are upper triangular and for all k-ary symbols \(f\in {\mathcal{F}}\), \(1\le i\le k\) and \(1\le j\le d\), \((F_i)_{jj}\le 1\) (but \((F_i)_{11}=1\) due to the monotonicity requirement); also, for all \(1\le j\le d\), \(A_{ij}=0\) if \(j>i\).
Remark 7
Matrix interpretations were generalized to admit real entries and interpretation domains which are tuples of non-negative real natural numbers [1]. The ordering \(\succ _\delta \) is used instead of \(>_\mathbb {N}\) for strict comparisons of tuple components in (13). See also [48], which extended TMIs to matrix interpretations over the reals.
5.2 Derivational Complexity Bounds from Termination Proofs
Table 1 summarizes the best (general) upper bounds reported for the different techniques we use in the paper. Except for (arbitrary) matrix interpretations, all considered techniques provide bounds given by elementary functions6.
Table 1
Bounds on \(\mathsf {dc}_\mathcal{R}(n)\) from termination techniques
Bounds obtained from other methods, e.g., lexicographic or multiset orderings [10, 32, 59], Knuth–Bendix orderings [34] or dependency pairs [3, 21], have been analyzed too [33, 45, 46, 48]. In general, they exceed those in Table 1.
Example 12
(Running example IV—complexity bound) For \(\mathcal{R}\) in Example 5, in view of Table 1 and according to the polynomial termination proof in Example 11, the best upper bound we can obtain is doubly exponential, i.e., \(2^{2^{O(n)}}\).
Example 13
(Running example II—termination and complexity bound) Consider the TRS \(\mathcal{R}\) in Example 2. A proof of termination is obtained by using the reduction ordering \(\succ _\mathcal{A}\) induced by the following TMI \(\mathcal{A}\) with domain \(\mathbb {N}^2\) [46, Example 4]:
For the rule \(\ell \rightarrow r\) in \(\mathcal{R}\), we have:
For all \(1\le i\le 2\) and \(x_i,y_i,z_i\in \mathbb {N}\), \(x_1+2x_2+y_1+y_2+z_1+1>x_1+x_2+y_1+y_2+z_1\) for the first component of the obtained vectors, and \(x_2+y_2+z_2+2\ge x_2+y_2+z_2+2\) for the second one. Thus, \(\ell ^\mathcal{A}\succ _\mathcal{A}r^\mathcal{A}\), and \(\mathsf {dc}_\mathcal{R}(n)\in O(n^2)\) (see Table 1).
6 Derivational Complexity of Context-Sensitive Rewriting
According to Definition 2, given a finitely branching TRS \(\mathcal{R}\) and \(\mu \in {M_{\mathcal{R}}}\) such that \(\mathcal{R}\) is \(\mu \)-terminating, the derivational height and derivational complexity of CSR are defined as:
For signatures containing a constant symbol, as for ordinary term rewriting (see Sect. 4.1), since CSR is also closed under substitutions [40, Sect. 4], we can consider ground terms only, i.e., we have:
Following the discussion in Sect. 4.1, we also have the following version of Proposition 1 for CSR (with an analogous proof using the fact that CSR is closed under substitutions).
Proposition 2
Let \(\bullet \) be a constant symbol, \(\mathcal{R}=({\mathcal{F}},R)\) be a TRS where \(\bullet \notin {\mathcal{F}}\), \(\mu \in {M_{\mathcal{R}}}\), and \(\mathcal{R}^\bullet =({\mathcal{F}}^\bullet ,R)\). Then, for all \(n\in \mathbb {N}\), \(\mathsf {dc}_{\mathcal{R},\mu }(n)=\mathsf {dc}_{\mathcal{R}^\bullet ,\mu }(n)\).
In the following, we often use \(\mathsf {dh}_\mu \) and \(\mathsf {dc}_\mu \) (rather than \(\mathsf {dh}_{\mathcal{R},\mu }\) and \(\mathsf {dc}_{\mathcal{R},\mu }\)). Since \(\hookrightarrow _{\mu }\subseteq \rightarrow \) for all \(\mu \in {M_{\mathcal{R}}}\), bounds on \(\mathsf {dc}_\mathcal{R}(n)\) are also bounds on \(\mathsf {dc}_\mu (n)\), i.e.,
Proposition 3
For all terms s and \(n\in \mathbb {N}\), \( \mathsf {dh}_\mu (s)\le \mathsf {dh}(s,\rightarrow _\mathcal{R})\) and \(\mathsf {dc}_\mu (n)\le \mathsf {dc}_\mathcal{R}(n)\).
For left-linear, non-collapsing, and \({\mu _\bot }\)-terminating TRSs \(\mathcal{R}\), if \({\mu _\bot }\) is canonical, then the derivational height of all terms is bounded by the size of \(\mathcal{R}\).
Proposition 4
Let \(\mathcal{R}=({\mathcal{F}},R)\) be a finite, left-linear, non-collapsing TRS such that \(\mu _\bot \in { CM _{\mathcal{R}}}\). If \(\mathcal{R}\) is \({\mu _\bot }\)-terminating, then for all terms s and \(n\in \mathbb {N}\), \(\mathsf {dh}_{\mu _\bot }(s) \le |R|\) and \(\mathsf {dc}_{\mu _\bot }(n)\in O(1)\).
Proof
In the following, for \(\mathcal{R}=({\mathcal{F}},R)\), we let \(R_{ cons }=\{\ell \rightarrow r\in R\mid root (r)\in {\mathcal{C}}_\mathcal{R}\}\) and call them the constructor rules of \(\mathcal{R}\). First, note that, since \({\mu _\bot }\) permits no reduction on the arguments of any function symbol, every \(\mu \)-reduction sequence \(s_1{\mathop {\hookrightarrow }\limits ^{p_1}}_{}s_2{\mathop {\hookrightarrow }\limits ^{p_2}}_{}\cdots {\mathop {\hookrightarrow }\limits ^{p_n}}_{}s_{n+1}\) satisfies \(p_1=\cdots =p_n=\Lambda \). We proceed by induction on the number n of rules in \(\mathcal{R}\). First, note that, since \(\mathcal{R}\) is left-linear and \({\mu _\bot }\in { CM _{\mathcal{R}}}\), all rules in R are of the form \(f(x_1,\ldots ,x_k)\rightarrow r\) where \(x_1,\ldots ,x_k\) are different variables and r is a non-variable term (due to non-collapsingness of \(\mathcal{R}\)). This means that every term \(f(t_1,\ldots ,t_k)\) is \({\mu _\bot }\)-reducible if f is a defined symbol. Therefore, there must be at least one constructor rule\(\ell \rightarrow r\) where \( root (r)\in {\mathcal{C}}_\mathcal{R}\). Otherwise, the application of a rule could always be followed by the application of another rule (at the root position) and \(\mathcal{R}\) would not be \({\mu _\bot }\)-terminating. If \(n=1\), then the only rule in \(\mathcal{R}\) must be a constructor rule. Thus, if \(s\hookrightarrow _{}s'\), then \( root (s')=c\). Since c is a constructor symbol and \({\mu _\bot }(c)=\varnothing \), no further reduction is possible. Thus, \(\mathsf {dh}(s)\le 1\), as desired. If \(n>1\), then consider a \(\mu \)-rewrite sequence \(s=s_1\hookrightarrow _{}\cdots \hookrightarrow _{}s_{n+1}\). If a constructor rule \(\alpha :\ell \rightarrow r\in R_{ cons }\) is used in the sequence, then it can be used only at the end of the sequence, and therefore, the sequence \(s_1\hookrightarrow _{}s_n\) of length \(n-1\) can be obtained using a TRS \(\mathcal{R}'=({\mathcal{F}}',R')\) which is as \(\mathcal{R}\) except the constructor rule, i.e., \(R'=R-\{\alpha \}\). Note that \(\mathcal{R}'\) is left-linear, non-collapsing and \({\mu _\bot }\)-terminating as well. Note also that \({\mathcal{C}}_{\mathcal{R}}\subseteq {\mathcal{C}}_{\mathcal{R}'}\) but \({\mathcal{C}}_{\mathcal{R}'}\) could include \( root (\ell )\), which is defined in \(\mathcal{R}\) but may become constructor in \(\mathcal{R}'\) due to the removal of \(\alpha \). By the induction hypothesis, \(n-1\le |R'|-1\), and hence, \(n\le |R|\) as required. If no constructor rule is used in the sequence, then, again, we can obtain the same sequence using a TRS \(\mathcal{R}'=({\mathcal{F}}',R')\)where \(R'=R-R_{ cons }\). By the induction hypothesis, \(n\le |R'|< |R|\).
Remark 8
(Application to recursive program schemes) A recursive program scheme (RPS [13, 43]) is a TRS consisting of (left-linear) rules \({f(x_1,\ldots ,x_k)\rightarrow r}\), one per defined function symbol \(f\in {\mathcal{D}}\) [57, Definition 3.4.7]. Clearly, \({\mu _\bot }\in { CM _{\mathcal{R}}}\) for all RPSs \(\mathcal{R}\). Note that \(\mathcal{R}\) in Example 1 is an RPS.
6.1 Proving Termination of CSR
Several techniques for proving termination of rewriting have been generalized to CSR [40, Sect. 7.1]. Tools like AProVE and mu-term [28] (which we use in the proofs below) can be used to prove termination of CSR. Termination of CSR is characterized by the \(\mu \)-reduction orderings >, which are \(\mu \)-monotonic, closed under substitutions, and well-founded relations on terms [61]. A TRS is \(\mu \)-terminating if it admits a compatible \(\mu \)-reduction ordering >. This implies
as it is implicit in the proof of [61, Proposition 1]. Also, \(\mu \)-reduction orderings can be obtained from \(\mu \)-monotone, well-founded \({\mathcal{F}}\)-algebras \((\mathcal{A},\succ )\) where mappings \(f^\mathcal{A}\) are required to be \(\mu \)-monotone, i.e., for all \(f\in {\mathcal{F}}\), \(i\in \mu (f)\), and \(x_1,\ldots ,x_k,y_i\in \mathcal{A}\), if \(x_i\succ y_i\), then \(f^\mathcal{A}(x_1,\ldots ,x_i,\ldots ,x_k)\succ f^\mathcal{A}(x_1,\ldots ,y_i,\ldots ,x_k)\) [61, Sect. 3]. The different termination techniques considered in Table 1 (among others) have been adapted to CSR: polynomial orderings in [26, 39]; matrix interpretations in [2].
Remark 9
(Guaranteeing\(\mu \)-monotonicity) In linear polynomial interpretations \(\mathcal{A}\), \(\mu \)-monotonicity is guaranteed if, for all k-ary symbols \(f\in {\mathcal{F}}\) and \(i\in \mu (f)\), the ith coefficient \(f_i\) of the linear polynomial \(f^\mathcal{A}(x_1,\ldots ,x_k)\) satisfies \(f_i\ge 1\). Similarly, dealing with matrix interpretations \(\mathcal{A}\), \(\mu \)-monotonicity is guaranteed if, for all k-ary symbols \(f\in {\mathcal{F}}\) and \(i\in \mu (f)\), the leftmost uppermost entry \((F_i)_{11}\) of the ith matrix \(F_i\) of the affine expression \(f^\mathcal{A}(\mathbf {x}_1,\ldots ,\mathbf {x}_k)\) satisfies \((F_i)_{11}\ge 1\).
6.2 Polynomial Bounds on \(\mathsf {dc}_\mu (n)\) from Matrix and Polynomial Interpretations
In the following result, \(I_d\) is the identity d-square matrix.
Theorem 2
Let \(\mathcal{R}\) be a TRS, \(\mu \in {M_{\mathcal{R}}}\) and let \(\mathcal{A}\) be a \(\mu \)-monotone TMI with domain \(\mathbb {N}^d\) for some \(d\in \mathbb {N}_{>0}\) such that \(\succ _\mathcal{A}\) is compatible with \(\mathcal{R}\).
1.
If for all \(f\in {\mathcal{F}}\), \(f^\mathcal{A}(x_1,\ldots ,x_k)=I_dx_i\) for some \(1\le i\le k\), or \(f^\mathcal{A}(x_1,\ldots ,x_k)=\mathbf {f}\) for some vector \(\mathbf {f}\), then \(\mathsf {dc}_\mu (n)\in O(1)\);
2.
otherwise, \(\mathsf {dc}_\mu (n)\in O(n^d)\).
Proof
We rework the proof of [46, Theorem 6] to make explicit the points which are different for CSR. According to (15), for all \(\mu \)-rewrite sequences \(s\hookrightarrow _{\mathcal{R},\mu }^kt\) of length k we have \([\alpha ]_\mathcal{A}(s)\succ ^k[\alpha ]_\mathcal{A}(t)\), where \(\succ \) is the ordering on tuples in (13). By definition of \(\succ \), this implies \(([\alpha ]_\mathcal{A}(s))_1\ge _\mathbb {N}k+([\alpha ]_\mathcal{A}(t))_1\ge _\mathbb {N}k\), i.e., for all valuations \(\alpha \), the first entry \(([\alpha ]_\mathcal{A}(s))_1\) of the vector interpreting s is an upper bound of the length k of the sequence. In particular, this holds for \(\alpha _0\) defined by \(\alpha _0(x)=\mathbf {0}\) for all \(x\in {\mathcal{X}}\). For all upper triangular matrices \(M\in \mathbb {N}^{d\times d}\) with diagonal entries 0 or 1, and \(p\in \mathbb {N}\), [46, Lemma 5] proves that the entries of \(M^p\) satisfy
This implies that, for all \(1\le i,j\le d\), \((M^p)_{ij}\in O(p^{d-1})\). As noticed in the proof of [46, Theorem 6], whenever terms s are interpreted by using \(\mathcal{A}\), such products of (possibly different) matrices occur in \(s^\mathcal{A}\) in number p at most the depth \(\delta _s\) of s minus one, i.e., \(p\le \delta _s-1\) (for constant or variable terms (of depth 1), no product is required). Of course, \(\delta _s\le |s|\); hence, \(p\le |s|\). Furthermore, the authors observe that the number m of products to be considered as additive components of \([\alpha ]_\mathcal{A}(s)\) is exactly |s|. By considering \(M^0=I_d\) as a ‘degenerate’ product accompanying the vector representing the interpretation of a constant or the valuation of the variable, this is acceptable. Note also that \((I_d)_{ij}\in O(p^{d-1})\) if \(p>0\). Thus, an addition \(\sum _{i=1}^mN_i\mathbf {a}_i\) of \(m=|s|\) vectors \(N_i\mathbf {a}_i\) obtained from products \(N_i\) of at most \(p\le |s|\) matrices each with entries \((N_i)_{qr}\) bounded by \(O(|s|^{d-1})\) is necessary to obtain the interpretation of s in \(\mathcal{A}\) with respect to a given valuation \(\alpha \). Since the addition of \(m=|s|\) values bounded by \(O(|s|^{d-1})\) is bounded by \(O(|s|^d)\), we obtain \(([\alpha ]_\mathcal{A}(s))_1\in O(|s|^d)\) and, since\(([\alpha ]_\mathcal{A}(s))_1\) is an upper bound on the length of any \(\mu \)-derivation starting from s, \(\mathsf {dc}_\mu (n)\in O(n^d)\), which proves item 2.
As for the particular case considered in item 1, where for all \(f\in {\mathcal{F}}\), \(f^\mathcal{A}=I_dx_i\) for some \(1\le i\le k\) or \(f^\mathcal{A}=\mathbf {f}\), note that the interpretation \([\alpha _0]_\mathcal{A}(t)\) of a term t using such kind of interpretation \(\mathcal{A}\) is of the form \([\alpha _0]_\mathcal{A}(t)\le \mathbf {b}\) for some vector \(\mathbf {b}=\max (\{f^\mathcal{A}(\mathbf {0},\ldots ,\mathbf {0})\mid f\in {\mathcal{F}}\}\cup \{\mathbf {0}\})\). Since \(\mathbf {b}\) depends on \(\mathcal{A}\) only, we have \(\mathsf {dh}(s,\hookrightarrow _{})\le \mathbf {b}_1\) for all terms s, and hence, \(\mathsf {dc}_\mu (n)\in O(1)\).
Remark 10
(More bounds based on matrix interpretations) Important improvements on [46, Theorem 6] regarding the use of matrix interpretations to obtain complexity bounds on \(\mathsf {dc}_\mathcal{R}(n)\) are discussed in [48]. We claim that (as Theorem 2(2) does for [46, Theorem 6]) they can be used as they are to obtain bounds on \(\mathsf {dc}_\mu (n)\). The reason is that monotonicity plays no essential role in the proof of such results, which apply to matrix interpretations \(\mathcal{A}\) generating an ordering \(\succ _\mathcal{A}\) which is compatible with the rewrite relation. For \(\rightarrow _\mathcal{R}\) monotonicity would be required on \(\mathcal{A}\) (to guarantee termination, not compatibility!); for \(\hookrightarrow _{\mathcal{R},\mu }\), \(\mu \)-monotonicity would be required instead (to guarantee \(\mu \)-termination now). Bounds obtained from the analysis of matrices in \(\mathcal{A}\) would apply to \(\mathsf {dc}_\mathcal{R}(n)\) or \(\mathsf {dc}_\mu (n)\) without special changes.
For polynomial interpretations, we have the following result, where by a hyperlinear polynomial interpretation \(\mathcal{A}\) we mean a strongly linear interpretation where for all \(f\in {\mathcal{F}}\), \(f^\mathcal{A}=x\) for some \(x\in {\mathcal{X}}\) or \(f^\mathcal{A}\in \mathbb {N}\).
Theorem 3
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). Let \(\mathcal{A}\) be a polynomial interpretation and \(\succ _\mathcal{A}\) be the corresponding \(\mu \)-reduction ordering that is compatible with \(\mathcal{R}\).
1.
If \(\mathcal{A}\) is hyperlinear, then \(\mathsf {dc}_\mu (n)\in O(1)\).
2.
If \(\mathcal{A}\) is strongly linear, then \(\mathsf {dc}_\mu (n)\in O(n)\).
3.
If \(\mathcal{A}\) is linear, then \(\mathsf {dc}_\mu (n)\in 2^{O(n)}\).
The first two items are particular cases of one-dimensional matrix interpretations. The proof of the last two cases is an immediate adaptations of the proofs of [33, Proposition 2.2.1] and [33, Proposition 2.1.2], respectively.
The bounds in Theorem 3 are tight, i.e., they cannot be improved.
Remark 11
Note that matrix interpretations \(\mathcal{A}_M\) satisfying the condition in item 1 of Theorem 2 can always be treated as polynomial interpretations \(\mathcal{A}_P\) as in item 1 of Theorem 3 by just letting \(f^{\mathcal{A}_P}((\mathbf {x}_1)_1,\ldots ,(\mathbf {x}_k)_1)=(f^{\mathcal{A}_M}(\mathbf {x}_1,\ldots ,\mathbf {x}_k))_1\).
Example 14
Consider \(\mathcal{R}\) and \(\mu \) in Example 1. A proof of \(\mu \)-termination for \(\mathcal{R}\) is obtained with the following hyperlinear interpretation
By Theorem 3(1), \(\mathsf {dc}_\mu (n)\in O(1)\).
Example 15
Consider \(\mathcal{R}\) and \(\mu \) in Example 2. A proof of \(\mu \)-termination of \(\mathcal{R}\) is obtained with the strongly linear interpretation \(\mathcal{A}\) where \({\mathsf {app}}^\mathcal{A}(x,y) = x+1\). By Theorem 3(2), \(\mathsf {dc}_\mu (n)\in O(n)\).
Example 16
Consider \(\mathcal{R}\) and \(\mu \) in Example 3. The strongly linear interpretation
proves \(\mathcal{R}\)\(\mu \)-terminating. By Theorem 3(2), \(\mathsf {dc}_\mu (n)\in O(n)\).
Example 17
Consider \(\mathcal{R}\) and \(\mu \) in Example 5. A proof of \(\mu \)-termination of \(\mathcal{R}\) is obtained with the linear interpretation
By Theorem 3(3), \(\mathsf {dc}_\mu (n)\in 2^{O(n)}\).
Remind that TRSs \(\mathcal{R}\) in Examples 1 and 3 are left-linear and completely defined (see Example 10). Thus, they fulfill the conditions in Corollary 1. According to Remark 3, we notice the following.
Example 18
(Running example I—bounds) For \(\mathcal{R}\) and \(\mu \) in Example 1, \(\mathsf {dc}_\mu (n)\in O(1)\) in Example 14 provides a suitable bound on the length of normalization sequences in \(\mathcal{R}\). Note that \(\mathsf {dc}_\mathcal{R}(n)\) is not defined as \(\mathcal{R}\) is not terminating.
Example 19
(Running example III—improved bounds) For \(\mathcal{R}\) and \(\mu \) in Example 3, \(\mathsf {dc}_\mu (n)\in O(n)\) in Example 16 improves on AProVE’s bounds for rewriting and innermost rewriting (Examples 3 and 9).
7 Normalization via \(\mu \)-Normalization
For left-linear TRSs \(\mathcal{R}\) and \(\mu \in { CM _{\mathcal{R}}}\), normalization of terms can be decomposed in the computation of a (possibly empty) initial subsequence of context-sensitive rewriting steps followed of a possibly empty sequence of additional reductions issued on maximal frozen subterms of \(\mu \)-normal forms.
Theorem 4
[40, Theorem 6.8] Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\). Let \(s,t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) such that \(s\rightarrow ^!t\). There exists \(u\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) such that \(s\hookrightarrow ^!_{\mu }u\rightarrow ^!_{\not \mu } t\) and \( MRC ^\mu (u)= MRC ^\mu (t)\).
This is the basis of the iterative normalization via\(\mu \)-normalization (\(\textit{N} \mu \textit{N}\)) process \(\mathtt {norm}_{\mu }\) in [37, Sect. 4], further discussed in [40, Sect. 9.3], see also Fig. 1:
(Deterministic/non-deterministic presentations of\({\mathsf {norm}}_\mu \)) In [37, Figure 1] \({\mathsf {norm}}_\mu (t)\) deterministically returns a (possibly empty) set of termsT, whereas the (simpler) presentation in [40, Sect. 9.3] non-deterministically returns one of the terms in T. For simplicity, the presentation of the above algorithm uses this style. In the sequel, we rather follow the set-theoretic presentation in the technical results.
In order to prepare the analysis of derivational complexity of \(\textit{N} \mu \textit{N}\), we investigate the number of maximal frozen subterms \(s_1,\ldots ,s_n\) in (18) of the \(\mu \)-normal forms u obtained in \(\textit{N} \mu \textit{N}\)’s \(\mu \)-normalization steps (17). Note that \(\textit{N} \mu \textit{N}\) will recursively continue on such terms in (16).
Definition 3
Let \(\mu \) be a replacement map and t be a term. The number of maximal frozen subterms of t, which coincides with the number of holes of its maximal replacing context \( MRC ^\mu (t)\), is denoted as \(\mathsf {nmf}_{\mu }(t)=|{\mathcal{F}r}^{\mu }(t)|=| minimal _\le (\overline{{\mathcal{P}os}^\mu }(t))|\).
Example 20
For \(\mathcal{R}\) and \(\mu \) in Example 5, \(\mathsf {nmf}_{\mu }(\ell _{(8)}) = |{\mathcal{F}r}^{\mu }(\ell _{(8)})| = |\{1\} | = 1\) and \(\mathsf {nmf}_{\mu }(r_{(8)}) = |{\mathcal{F}r}^{\mu }(r_{(8)})| = |\{1.1,2.1\}| = 2\).
Section 7.1 investigates bounds on \(\mathsf {nmf}_{\mu }(t)\) for a given term t. Then, Sect. 7.2 explores how to approximate the number \(\mathsf {nmf}_{\mu }(t)\) of maximal frozen subterms \(s'\) of the \(\mu \)-normal forms t of a given term s.
7.1 The Number of Maximal Frozen Subterms of a Term
Definition 4
(p-adic and p-active signature) Let \({\mathcal{F}}\) be a signature and \(\mu \in {M_{{\mathcal{F}}}}\). Let p be the least natural number such that \(ar(f)\le p\) for all \(f\in {\mathcal{F}}\). Then \({\mathcal{F}}\) is called a p-adic signature. Let p be the least natural number such that \(|\mu (f)|\le p\) for all \(f\in {\mathcal{F}}\). Then, \({\mathcal{F}}\) is called p-active (with respect to \(\mu \)).
We often use monadic and dyadic instead of 1- and 2-adic. In the sequel, given a term t, \({\mathcal{F}}(t)\) is the set of symbols from \({\mathcal{F}}\) occurring in t. We have the following.
Proposition 5
Let \({\mathcal{F}}\) be a signature, \(\mu \in {M_{{\mathcal{F}}}}\), \(t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\), and \({\mathcal{G}}={{\mathcal{F}}( MRC ^\mu (t))}\).
1.
If \({\mathcal{G}}\) is p-adic and 0-active, then \(\mathsf {nmf}_{\mu }(t)=ar( root (t))\le p\).
2.
If for all \(f\in {\mathcal{G}}\), \(\mu (f)={\mu _\top }(f)\), then \(\mathsf {nmf}_{\mu }(t)=0\).
3.
If \({\mathcal{G}}\) is p-adic for some \(p>1\), and 1-active, then \(\mathsf {nmf}_{\mu }(t)\le \frac{p-1}{p}| MRC ^\mu (t)|\).
The first two cases and the last one are trivial. As for the third case, if \(p>1\) and \({\mathcal{G}}\) is 1-active, then since \(|\mu (f)|\le 1\) for all \(f\in {\mathcal{G}}\), each level of the tree associated with t has (at most) a single active position and (at least) a single minimal frozen position. The structure of t allowing for more frozen positions is \(t=f(x_1,\ldots ,x_{i-1},u,x_{i+1},\ldots ,x_p)\) where f is a p-adic symbol with \(\mu (f)=\{i\}\) for some \(1\le i\le p\), \(x_1,\ldots ,x_{i-1},x_{i+1},x_p\) are (non-necessarily distinct) variables, and u is either a variable or a term of the same structure. In this case, each level of the tree below the root adds (at most) \(p-1\) new minimal frozen positions to \({\mathcal{F}r}^{\mu }(t)= minimal (\overline{{\mathcal{P}os}^\mu }(t))\), and therefore, there are
minimal frozen positions in t. We also have \(| MRC ^\mu (t)|=1+(p-1)+| MRC ^\mu (u)|\), i.e., \(| MRC ^\mu (t)|=(\delta _t-1)p+1\). Hence, \(\delta _t-1=\frac{| MRC ^\mu (t)|-1}{p}\) and using (19), we obtain \(\mathsf {nmf}_{\mu }(t)=\frac{| MRC ^\mu (t)|-1}{p}(p-1)\le \frac{p-1}{p}| MRC ^\mu (t)|\).
The following fact is used below.
Proposition 6
Let \(s,t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) be such that \(s=\sigma (t)\) for some substitution \(\sigma \). Let \(\mu \in {M_{\mathcal{R}}}\). Then, \(\mathsf {nmf}_{\mu }(s)=\mathsf {nmf}_{\mu }(t)+ \sum _{x\in \mathcal{V}ar(t)}|{\mathcal{P}os}^\mu _x(t)|\mathsf {nmf}_{\mu }(\sigma (x))\).
Proof
The set of positions in the frontier of s consists of the positions in the frontier of t together with those frozen positions introduced by instances \(\sigma (x)\) of active positions of variables in t.
7.2 The Number of Maximal Frozen Subterms of \(\mu \)-Normal Forms of Terms
In \(\textit{N} \mu \textit{N}\), intermediate \(\mu \)-normal forms t of terms s are obtained, and then, \(\textit{N} \mu \textit{N}\) resumes on maximal frozen subterms of t. In this section, we investigate approximations to the maximum value of \(\mathsf {nmf}_{\mu }(t)\) whenever t is a \(\mu \)-normal form of s.
Definition 5
Let \(\mathcal{R}\) be a finitely branching TRS and \(\mu \in {M_{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\mu \)-terminating. For all terms s, we let \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s) = \max _{s\hookrightarrow ^!_{\mu }t}\mathsf {nmf}_{\mu }(t)\).
In order to use Proposition 5 to obtain bounds on \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\), we need to consider the function symbols occurring in the maximal replacing contexts of \(\mu \)-normal forms of terms. For this purpose, we introduce the following notation:
We can approximate \({\mathcal{F}}^!_{\mu }\) as \({\mathcal{F}}\); however, completely defined symbols can be discarded as they cannot occur in the maximal replacing context of (ground) normal forms. This motivates the restriction to ground terms s in the definition of \({\mathcal{F}}^!_{\mu }\), thus guaranteeing groundness of t. As discussed in Sect. 4.1, if \({{\mathcal{T}({\mathcal{F}})}}=\varnothing \), we just need to add a fresh constant symbol \(\bullet \) to \({\mathcal{F}}\) and deal with \(\mathcal{R}^\bullet \) instead of \(\mathcal{R}\).
Example 21
[Running example V] Consider the following (non-terminating) TRS \(\mathcal{R}\)
$$\begin{aligned}&{\mathsf {f}}({\mathsf {b}},y) \rightarrow y \end{aligned}$$
(21)
$$\begin{aligned}&{\mathsf {f}}({\mathsf {c}}(x),y) \rightarrow y \end{aligned}$$
(22)
together with \(\mu ={\mu ^{ can }_\mathcal{R}}\), i.e., \(\mu ({\mathsf {f}})=\{1\}\) and \(\mu ({\mathsf {c}})=\varnothing \). Since \({\mathsf {a}}\) and \({\mathsf {f}}\) are completely defined (use induction on the structure of ground normal forms) \({\mathcal{F}}^!_{\mu }={\mathcal{C}}=\{{\mathsf {b}},{\mathsf {c}}\}\).
The following result is immediate from Proposition 5.
Corollary 2
Let \(\mathcal{R}=({\mathcal{F}},R)\) be a TRS, \(\mu \in {M_{\mathcal{R}}}\) be such that \({\mathcal{F}}^!_{\mu }\) is p-adic, and s be a ground term. Then,
1.
If \({\mathcal{F}}^!_{\mu }\) is 0-active, then \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le p\).
2.
If for all \(f\in {\mathcal{F}}^!_{\mu }\), \(\mu (f)={\mu _\top }(f)\), then \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)=0\).
Proof
Since s is ground, the \(\mu \)-normalization of s leads to a term t in \({\mathcal{T}({\mathcal{F}}^!_{\mu })}\). Now we apply the first two items of Proposition 5 with \(\mathcal{G}={\mathcal{F}}^!_{\mu }\).
Example 22
For \(\mathcal{R}\) and \(\mu \) in Example 21, \({\mathcal{F}}^!_{\mu }=\{{\mathsf {b}},{\mathsf {c}}\}\). Since \({\mathcal{F}}^!_{\mu }\) is monadic and 0-active, by Corollary 2(1), for all ground terms s, \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le 1\).
Note that, if the size of sdecreases when computing a \(\mu \)-normal form t of s, then \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\) is clearly bounded by |s|. In the following, we investigate this issue.
7.2.1 Size-Decreasing Relations
In this section, we investigate conditions guaranteeing that some relations (in particular the \(\mu \)-normalization relation \(\hookrightarrow ^!_{\mu }\)) are size-decreasing in the following sense:
Definition 6
(Size-decreasing relation) Consider a relation \(\mathsf {R}\) on terms. We say that \(\mathsf {R}\) is size-decreasing if for all terms \(s,t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\), \(s\,\mathsf {R}\,t\) implies \(|s|\ge |t|\).
Clearly, size-decreasingness of \(\mathsf {R}\) implies size-decreasingness of \(\mathsf {R}^+,\mathsf {R}^*, \mathsf {R}^!\) and also size-decreasingness of any subrelation \(\mathsf {R}'\subseteq \mathsf {R}\). The following result is immediate from the notion of size-decreasingness and Proposition 5.
Proposition 7
Let \(\mathcal{R}=({\mathcal{F}},R)\) and \(\mu \in {M_{\mathcal{R}}}\) be such that \({\mathcal{F}}\) is p-adic and \(\hookrightarrow ^!_{\mu }\) is size-decreasing. Let s be a ground term. If \(p>1\) and \({\mathcal{F}}^!_{\mu }\) is 1-active, then (i) \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le \frac{p-1}{p}|s|\). Otherwise, (ii) \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le |s|\).
Proof
By size-decreasingness of \(\hookrightarrow ^!_{\mu }\), \(|s|\ge |t|\) for all \(\mu \)-normal forms t of s. Since s is ground, t is also ground and \(t\in {\mathcal{T}({\mathcal{F}}^!_{\mu })}\). By Proposition 5, with \(\mathcal{G}={\mathcal{F}}^!_{\mu }\), we have, for item (i),
Item (ii) follows due to the fact that \(|s|\ge |t|\) (size-decreasingness of \(\hookrightarrow ^!_{\mu }\)).
In the following, we investigate criteria to guaranteee size-decreasingness of \(\hookrightarrow ^!_{}\).
7.2.2 Size-Decreasing TRSs
Definition 7
(Size-decreasing rules and TRSs) A rule \(\ell \rightarrow r\) satisfying \(|\ell |\ge |r|\) is called size-decreasing. A TRS \(\mathcal{R}\) is size-decreasing if all rules are size-decreasing.
Example 23
The TRS \(\mathcal{R}\) in Example 2 is size-decreasing. The TRSs \(\mathcal{R}\) in Examples 1, 3, 5 and 21 are not size-decreasing.
The following observation is used below: given a term t and a substitution \(\sigma \), \(|\sigma (t)|=|t|+\sum _{x\in \mathcal{V}ar(t)}|{\mathcal{P}os}_x(t)|(|\sigma (x)|-1)\).
Proposition 8
Let s and t be terms and \(\ell \rightarrow r\) be a non-duplicating rule. If \(s\rightarrow _{\ell \rightarrow r}t\), then \(|s|-|t|\ge |\ell |-|r|\).
Proof
Since \(s\rightarrow _{\ell \rightarrow r}t\), we have \(s|_p=\sigma (\ell )\) for some \(p\in {\mathcal{P}os}(s)\) and substitution \(\sigma \) and \(t=s[\sigma (r)]_p\). Therefore, since \(|t|=|s|-|\sigma (\ell )|+|\sigma (r)|\), we have
Since \(|{\mathcal{P}os}_x(\ell )|\ge |{\mathcal{P}os}_x(r)|\) and \(|\sigma (x)|-1\ge 0\), we have \(|s|-|t|\ge |\ell |-|r|\).
Proposition 9
Let \(\mathcal{R}\) be a size-decreasing TRS. Then, \(\rightarrow ^*\) is size-decreasing iff \(\mathcal{R}\) is non-duplicating.
Proof
For the if part, we proceed by induction on the length of the sequence \(s\rightarrow ^*t\), to prove \(|s|\ge |t|\). The base case is immediate. Let \(s\rightarrow s'\rightarrow ^*t\) with \(s|_p=\sigma (\ell )\) and \(s'=s[\sigma (r)]_p\). By Proposition 8, \(|\sigma (\ell )|\ge |\sigma (r)|\); hence, \(|s|\ge |s'|\). By the induction hypothesis, \(|s|\ge |s'|\ge |t|\), i.e., \(\rightarrow ^*\) is size-decreasing. Now, for the only if part, we proceed by contradiction. Assume that both \(\mathcal{R}\) and \(\rightarrow ^*\) are size-decreasing but \(\mathcal{R}\) is duplicating. Then there is a rule \(\ell \rightarrow r\) with \(m=|\ell |-|r|\ge 0\) (by size-decreasingness of \(\mathcal{R}\)) and \(|{\mathcal{P}os}_x(\ell )|<|{\mathcal{P}os}_x(r)|\) for some variable x. Let \(n=|{\mathcal{P}os}_x(r)|-|{\mathcal{P}os}_x(\ell )|>0\). Let t be a term of size \(|t|=k\ge m+2\) and \(\sigma \) be such that \(\sigma (x)=t\) and \(\sigma (y)=y\) for all \(y\ne x\). Let \(s=\sigma (\ell )\) and \(s'=\sigma (r)\). Note that \(s\rightarrow s'\). Now, note that \(|s|=|\ell |+|{\mathcal{P}os}_x(\ell )|(k-1)\) and \(|s'|=|r|+|{\mathcal{P}os}_x(r)|(k-1)\). Hence, \(|s|-|s'|=|\ell |-|r|+(|{\mathcal{P}os}_x(\ell )|-|{\mathcal{P}os}_x(r)|)(k-1)=m-n(k-1)=m-n(m+1)<0\) (because \(n>0\)), i.e., \(\rightarrow ^*\) is not size-decreasing, a contradiction.
Example 24
The TRS \(\mathcal{R}\) in Example 2 is size-decreasing and non-duplicating. By Proposition 9, \(\rightarrow ^*\) (and hence \(\hookrightarrow ^!_{\mu }\), for \(\mu \) in the example) is size-decreasing.
Remark 13
(Limitation) Left-linear and non-duplicating TRSs are linear. Since left-linearity is necessary for \(\textit{N} \mu \textit{N}\) to be sound, this leads to a strong restriction on the TRSs amenable for a complexity treatment that assumes non-duplicatingness.
7.2.3 Weakly Size-Decreasing TRSs
The following definition slightly relaxes size-decreasingness.
Definition 8
(Weak size-decreasingness) A TRS \(\mathcal{R}\) is weakly size-decreasing if for all rules \(\ell \rightarrow r\in \mathcal{R}\) with \(|\ell |<|r|\), there are rules \(\ell _1\rightarrow r_1,\ldots ,\ell _n\rightarrow r_n\in \mathcal{R}\) and substitutions \(\sigma _i\) such that (i) \(r=\sigma _1(\ell _1)\), (ii) for all \(1\le i< n\), \(r_i=\sigma _{i+1}(\ell _{i+1})\) and (iii) \(|r|-|\ell |\le \sum _{i=1}^n|\ell _i|-|r_i|\).
Example 25
The TRS \(\mathcal{R}\) in Example 21 is weakly size-decreasing: both (21) and (22) are size-decreasing, and (i) the right-hand side \(r_{(20)}\) of rule (20) matches \(\ell _{(22)}\) and (ii) \(|r_{(20)}|-|\ell _{(20)}|=3\le 3=|\ell _{(22)}|-|r_{(22)}|\), as required in Definition 8.
For size-decreasing and non-duplicating TRSs, \(\rightarrow ^*\) is size-decreasing (Proposition 9), and hence, \(\hookrightarrow ^*_{}\) and \(\hookrightarrow ^!_{}\) also are. However, in general size-decreasingness of \(\hookrightarrow ^!_{}\) does not imply that of \(\hookrightarrow ^*_{}\). For weak size-decreasingness, we have the following.
Proposition 10
Let \(\mathcal{R}\) be a weakly size-decreasing and non-duplicating TRS and \(\mu \in {M_{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\mu \)-confluent and \(\mu \)-terminating. Then, \(\hookrightarrow ^!_{}\) is size-decreasing.
Proof
Since \(\mathcal{R}\) is \(\mu \)-terminating, there is a \(\mu \)-reduction ordering \(\succ \) on terms such that whenever \(s\hookrightarrow ^+_{} t\), we have \(s\succ t\). We proceed by induction on s using \(\succ \). As for the base case, we consider terms s which are \(\mu \)-normal forms. Thus, \(s=t\). For the induction step, if s is \(\mu \)-reducible, assume \(s\hookrightarrow _{\ell \rightarrow r}s'\hookrightarrow ^!_{}t\), hence \(s\succ s'\) and either \(s'\succ t\) or \(s'=t\). By Proposition 8, \(|s|-|s'|\ge |\ell |-|r|\) and by the induction hypothesis we have \(|s'|\ge |t|\). We consider two cases. (A) If \(\ell \rightarrow r\) is size-decreasing, then \(|\ell |\ge |r|\) and \(|s|\ge |s'|\ge |t|\). (B) If \(\ell \rightarrow r\) is not size-decreasing, then there are rules \(\ell _1\rightarrow r_1,\ldots ,\ell _n\rightarrow r_n\in \mathcal{R}\) for some \(n>0\) and substitutions \(\sigma _i\) such that \(r=\sigma '(\ell _1)\), for all \(1\le i< n\), \(r_i=\sigma _{i+1}(\ell _{i+1})\), and \(|r|-|\ell |\le \sum _{i=1}^n|\ell _i|-|r_i|\). Note that \(\sigma (r)=\sigma (\sigma _1(\ell _1))\), and therefore,
and therefore \(|s|\ge |s''|\). By \(\mu \)-confluence, \(s''\hookrightarrow ^!_{}t\). If \(s''=t\), then \(|s''|\ge |t|\); hence, \(|s|\ge |t|\). Otherwise, \(s\succ s''\succ t\); by the induction hypothesis \(|s|\ge |t|\).
Example 26
Consider \(\mathcal{R}\) and \(\mu \) in Example 21. The following strongly linear polynomial interpretation
proves \(\mathcal{R}\)\(\mu \)-terminating. Also, \(\mathcal{R}\) is \(\mu \)-confluent as there is no critical pair and no active variable in the left-hand side of a rule becomes frozen anywhere else in the rule (LHRV property, see [40, Sect. 8]). By Proposition 10, \(\hookrightarrow ^!_{}\) is size-decreasing.
7.2.4 Beyond Size-Decreasingness
Definition 9
Let \(\mathcal{R}=({\mathcal{F}},R)\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). Given a rule \(\ell \rightarrow r\in \mathcal{R}\), we let \(F(\ell \rightarrow r)=\mathsf {nmf}_{\mu }(r)-\mathsf {nmf}_{\mu }(\ell )\). Then, \(F(\mathcal{R})=\max \{F(\ell \rightarrow r)\mid \ell \rightarrow r\in \mathcal{R}\}\). When no confusion arises, we drop \(\mathcal{R}\) and rather use F instead of \(F(\mathcal{R})\).
Intuitively, \(F(\mathcal{R})\) shows how many maximal frozen subterms can be introduced by the application of a rewrite step with \(\mathcal{R}\). In particular, if \(F(\mathcal{R})<0\) we can think of rules as ‘destroying’ frozen positions.
Therefore, \(F(\mathcal{R})=1\). For \(\mathcal{R}\) and \(\mu \) in Example 2, \(F(\mathcal{R})=-1\).
We have the following:
Proposition 11
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). For all \(\ell \rightarrow r\in \mathcal{R}\), \(\mathsf {nmf}_{\mu }(r)\le F(\mathcal{R})+\mathsf {nmf}_{\mu }(\ell )\).
Proof
By Definition 9, for all \(\ell \rightarrow r\in \mathcal{R}\), we have \(F(\mathcal{R})\ge F(\ell \rightarrow r)\) and \(F(\ell \rightarrow r)+\mathsf {nmf}_{\mu }(\ell )= \mathsf {nmf}_{\mu }(r)\). Hence, \(\mathsf {nmf}_{\mu }(r)\le F(\mathcal{R})+\mathsf {nmf}_{\mu }(\ell )\).
Definition 10
[25, Definition 1] Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). A rule \(\ell \rightarrow r\) is non-\(\mu \)-duplicating iff for all \(x\in \mathcal{V}ar(\ell )\), \(|{\mathcal{P}os}^\mu _x(\ell )|\ge |{\mathcal{P}os}^\mu _x(r)|\). A TRS is called non-\(\mu \)-duplicating if all rules are; otherwise, it is called \(\mu \)-duplicating.
Example 28
The TRS \(\mathcal{R}\) with \(\mu \) in Example 5 is non-\(\mu \)-duplicating:
The following results put bounds on \(\mathsf {nmf}_{\mu }(t)\) whenever t is obtained by \(\mu \)-rewriting a term s. Size-decreasingness is not required, but bounds now depend on (bounds on) the derivational height of CSR.
Proposition 12
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\) be such that \(\mathcal{R}\) is non-\(\mu \)-duplicating. Let \(F=F(\mathcal{R})\) and s, t be terms such that \(s\hookrightarrow ^*_{}t\). Then,
1.
If \(F> 0\), then \(\mathsf {nmf}_{\mu }(t)\le \mathsf {nmf}_{\mu }(s)+ F\mathsf {dh}_\mu (s)\) and \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le \mathsf {nmf}_{\mu }(s)+ F\mathsf {dh}_\mu (s)\).
2.
If \(F\le 0\), then \(\mathsf {nmf}_{\mu }(t)\le \mathsf {nmf}_{\mu }(s)\) and \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le \mathsf {nmf}_{\mu }(s)\).
3.
If \(F<0\), then \(\mathsf {dh}_\mu (s)\le \frac{\mathsf {nmf}_{\mu }(s)}{|F|}\).
Proof
We prove, by induction on the length n of \(s\hookrightarrow ^*_{}t\), that \(\mathsf {nmf}_{\mu }(t)\le \mathsf {nmf}_{\mu }(s)+Fn\). Note that \(n\le \mathsf {dh}_\mu (s)\). If \(n=0\), then \(s=t\) and it is immediate. If \(n>0\), let \(s\hookrightarrow _{}s'\hookrightarrow ^*_{}t\), i.e., there are \(\ell \rightarrow r\in \mathcal{R}\), \(p\in {\mathcal{P}os}^\mu (s)\) and a substitution \(\sigma \) such that \(s|_p=\sigma (\ell )\) and \(s'=s[\sigma (r)]_p\). By Proposition 6,
Now, since \(n\le \mathsf {dh}_\mu (s)\), we have (1) if \(F\ge 0\), then \(\mathsf {nmf}_{\mu }(t)\le \mathsf {nmf}_{\mu }(s)+F\mathsf {dh}_\mu (s)\) and \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(t)\le \mathsf {nmf}_{\mu }(s)+F\mathsf {dh}_\mu (s)\), as desired. In particular, (2) if \(F\le 0\), then \(\mathsf {nmf}_{\mu }(t)\le \mathsf {nmf}_{\mu }(s)\) and \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\le \mathsf {nmf}_{\mu }(s)\). Finally, (3) if \(F<0\), since \(\mathsf {nmf}_{\mu }(t)\ge 0\), it must be \(n|F|\le \mathsf {nmf}_{\mu }(s)\) for all n representing the length of a \(\mu \)-rewrite sequence starting from s. Thus, \(\mathsf {dh}_\mu (s)\le \frac{\mathsf {nmf}_{\mu }(s)}{|F|}\).
In the remainder of the paper, we investigate computational complexity of \(\textit{N} \mu \textit{N}\):
1.
Section 8 recalls and further develops a generalization of CSR called layeredCSR (LCSR [38]) and provides a characterization of \(\textit{N} \mu \textit{N}\) using LCSR.
2.
Section 9 defines computational complexity of \(\textit{N} \mu \textit{N}\) as the derivational complexity of LCSR and investigates derivational height of LCSR.
3.
Section 10 connects derivational complexity of LCSR and derivational complexity of CSR.
4.
Finally, Sect. 11 shows how to obtain bounds on derivational complexity of LCSR from bounds on \(\mathsf {dc}_\mu (n)\).
8 Layered Context-Sensitive Rewriting
In [38], layered normalization of terms was formalized as a reduction relation called layered context-sensitive rewriting.
Definition 11
(Layered Context-Sensitive Rewriting)[38, Definition 1] Let \(\mathcal{R}\) be a TRS, \(\mu \in {M_{\mathcal{R}}}\) and \(s,t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\). We write \(s{\mathop {\hookrightarrow \!\!\!\!\!\rightarrow }\limits ^{p}}_{\mu }t\) (or just \(s\hookrightarrow \!\!\!\!\!\rightarrow _\mu t\), or \(s\hookrightarrow \!\!\!\!\!\rightarrow t\)) if either
1.
\(s{\mathop {\hookrightarrow }\limits ^{p}}_{\mu } t\), or
2.
s is a \(\mu \)-normal form, \(s=C[s_1,\ldots ,s_i,\ldots ,s_n]\), where \(C[,\ldots ,]= MRC ^\mu (t)\), \(t=C[s_1,\ldots ,t_i,\ldots ,s_n]\), \(s_i=s|_q\) for some \(i\in \{1,\ldots ,n\}\) and \(q\in {\mathcal{P}os}(s)\), \(p=q.p'\) for some position \(p'\), and \(s_i{\mathop {\hookrightarrow \!\!\!\!\!\rightarrow }\limits ^{p'}}_{\mu } t_i\).
Example 29
Consider \(\mathcal{R}\), \(\mu \), and the \(\mu \)-normal form u in Example 2. Note that \( MRC ^\mu (u)={\mathsf {app}}(x_1,\Box )\). The normalization sequence with \(\hookrightarrow \!\!\!\!\!\rightarrow \) finishes (5):
In contrast to CSR, where \(\mathsf {NF}_\mathcal{R}\subseteq \mathsf {NF}^\mu _\mathcal{R}\) but, in general, \(\mathsf {NF}^\mu _\mathcal{R}\not \subseteq \mathsf {NF}_\mathcal{R}\) (see Example 2), \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }\)-normal forms are normal forms.
Proposition 13
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). Then, NF\(_{\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }}=\)NF\(_{\mathcal{R}}\).
Proof
Since normal forms are irreducible, \(\mathsf {NF}_{\mathcal{R}}\subseteq \mathsf {NF}_{\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }}\) trivially holds. Now let \(t\in \mathsf {NF}_{\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }}\). By definition of LCSR, \(t\in \mathsf {NF}^\mu _\mathcal{R}\) and if \(t=C[t_1,\ldots ,t_n]\) for \(C[,\ldots ,]= MRC ^\mu (t)\), then \(t_1,\ldots ,t_n\in \mathsf {NF}_{\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }}\). We prove by structural induction that \(t\in \mathsf {NF}_\mathcal{R}\). If t is a constant or a variable, it is obvious. Otherwise, since \(t_1,\ldots ,t_n\in \mathsf {NF}_{\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }}\) and \(C[,\ldots ,]\ne \Box \), by the induction hypothesis \(t_1,\ldots ,t_n\in \mathsf {NF}_\mathcal{R}\). Thus, if t is not a normal form, there must be a position \(p\in {\mathcal{P}os}_{\mathcal{F}}(C[,\ldots ,])\), i.e., \(p\in {\mathcal{P}os}^\mu (t)\) such that \(t|_p\) is a redex. Hence, \(t\not \in \mathsf {NF}^\mu _\mathcal{R}\), a contradiction.
For left-linear TRSs \(\mathcal{R}\) and canonical replacement maps \(\mu \in { CM _{\mathcal{R}}}\), layered CSR sequences can be decomposed into an initial sequence of \(\mu \)-rewriting steps which eventually obtains a \(\mu \)-normal form. After that, the terms in the sequence remain \(\mu \)-normal forms.
Proposition 14
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\). Consider a (finite or infinite) \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-sequence \( t_1\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }t_2\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\cdots \). If \(t_i\) is a \(\mu \)-normal form for some \(i\ge 1\), then there is \(m\ge 1\) such that for all \(1\le j<m\), \(s_j\) is \(\mu \)-reducible and for all \(j\ge m\), \(t_j\) is a \(\mu \)-normal form.
Proof
Let m be such that \(t_m\) is the first \(\mu \)-normal form in the sequence (note that \(m\le i\)). By definition of LCSR, for all j, \(1\le j<m\), \(t_j\) is \(\mu \)-reducible. And for all \(t_j\) with \(j\ge m\), \(t_m\rightarrow ^*t_j\). By [40, Theorem 6.2], \(t_j\) is a \(\mu \)-normal form.
Proposition 14 may fail to hold if left-linearity or \(\mu \in { CM _{\mathcal{R}}}\) is not required.
Let \(\mu ({\mathsf {f}})=\varnothing \). Note that \(\mu \notin { CM _{\mathcal{R}}}\). Although \({\mathsf {f}}({\mathsf {a}})\) is a \(\mu \)-normal form, we have \({\mathsf {f}}(\underline{{\mathsf {a}}})\,\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\,{\mathsf {f}}({\mathsf {c}})\) and \({\mathsf {f}}({\mathsf {c}})\) is not a \(\mu \)-normal form. Now, consider the non-left-linear TRS \(\mathcal{R}'\) and \(\mu '({\mathsf {g}})=\varnothing \). Note that \(\mu '=\mu ^{ can }_\mathcal{R'}\). Although \({\mathsf {g}}({\mathsf {c}},{\mathsf {a}})\) is a \(\mu '\)-normal form, we have \({\mathsf {g}}({\mathsf {c}},\underline{{\mathsf {a}}})\,\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R}',\mu '}\,{\mathsf {g}}({\mathsf {c}},{\mathsf {c}})\) and \({\mathsf {g}}({\mathsf {c}},{\mathsf {c}})\) is not a \(\mu '\)-normal form. Thus, in both cases, the statement claimed in Proposition 14 does not hold.
In the following auxiliary result, which we use later, \( sprefix _t(p)\) is the strict prefix of position p in a term t, i.e., the (possibly empty) list of symbols traversed when going from the root of t to position p (excluding p) [40, Sect. 3]. The result establishes that, for left-linear TRSs and \(\mu \in { CM _{\mathcal{R}}}\) such that \(\mathcal{R}\) is \(\mu \)-terminating, in infinite LCSR sequences there are strict prefixes of arbitrary length which remain unchanged after some point in the sequence.
Proposition 15
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\mu \)-terminating. For all \(t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) starting an infinite \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-sequence \(t=t_1\hookrightarrow \!\!\!\!\!\rightarrow _{\mu } t_2\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\cdots \) and for all \(N\ge 0\), there are \(i\ge 0\) and \(p\in {\mathcal{P}os}(t_i)\) such that \(|p|\ge N\) and for all u such that \(t_i\rightarrow ^*u\), \(p\in {\mathcal{P}os}(u)\) and \( sprefix _{t_i}(p)= sprefix _{u}(p)\).
Proof
By induction on N. If \(N=0\), it is trivial. If \(N>0\), then by Proposition 14, and since \(\mathcal{R}\) is \(\mu \)-terminating, we can assume that there is \(m\ge 1\) such that \(t_i\hookrightarrow t_{i+1}\) for all i, \(1\le i<m\) and \(t_m\in \mathsf {NF}^\mu _\mathcal{R}\). By [40, Theorems 6.2 & 6.3], if \(C[~]= MRC ^\mu (t_m)\), then, for all \(i\ge m\), \(t_i=C[t_{i1},\ldots ,t_{ik}]\in \mathsf {NF}^\mu _\mathcal{R}\) for terms \(t_{ij}\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\). Furthermore, no reduct of \(t_i\) (with this or other rewrite sequence) contains a \(\mu \)-replacing redex. Note that C[ ] is not empty. Therefore, for all \(i\ge m\), \(|t_i|\ge N_1\) where \(N_1=min(\{|p_j|\mid p_j\in {\mathcal{P}os}_\Box (C)\})>0\) is the minimum depth of a hole symbol \(\Box \) in C[ ]. Let \(t_m=C[t_{m1},\ldots ,t_{mk}]\). There is j, \(1\le j\le k\) such that \(t_{mj}\) starts an infinite sequence. Assume that \(t_m|_{p'}=t_{mj}\) for some \(p'\in {\mathcal{P}os}_\Box (C)\). By the induction hypothesis, there is \(n\ge m\) and \(q\in {\mathcal{P}os}(t_{n})\) such that \(|q|\ge N-N_1\) and for all v such that \(t_{n}|_{p'}\rightarrow ^*v\), \(q\in {\mathcal{P}os}(v)\) and \( sprefix _{t_{n}|_{p'}}(q)= sprefix _v(q)\). Now, we let \(p=p'.q\). Note that, since \(t_m\in \mathsf {NF}^\mu _\mathcal{R}\), by [40, Theorem 6.2], \(t_n=C[t_{m1},\ldots ,t_{mj-1},t_n|_{p'},\ldots ,t_{mk}]\in \mathsf {NF}^\mu _\mathcal{R}\) and for all u such that \(t_n\rightarrow ^*u\), we will have \(p\in {\mathcal{P}os}(u)\) and \( sprefix _{t_n}(p)= sprefix _{u}(p)\) as desired.
As a consequence of Proposition 15, terms in infinite \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-sequences steadily increase their depth (and size).
Corollary 3
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\mu \)-terminating. For all \(t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\) starting an infinite \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-sequence \(t=t_1\hookrightarrow \!\!\!\!\!\rightarrow _{\mu } t_2\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\cdots \) and for all \(M,N\ge 0\), there is \(i\ge 0\) such that for all u with \(t_i\rightarrow ^*u\), \({\delta }_{u}\ge M\) and \(|u|\ge N\).
8.1 Normalization via \(\mu \)-Normalization and Layered CSR
We use the following theorem in the proof of the main result in this section which characterizes \(\textit{N} \mu \textit{N}\) as \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-normalization (Theorem 6).
Theorem 5
[38, Theorem 5] Let \(\mathcal{R}=({\mathcal{F}},R)\) be a left-linear TRS, \(\mu \in { CM _{\mathcal{R}}}\), and \(s,t\in {{\mathcal{T}({\mathcal{F}},{\mathcal{X}})}}\). Then, \(s\rightarrow ^!t\) if and only if \(s\,\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }\,t\).
Theorem 5 does not hold for arbitrary reducts (i.e., we cannot change \(\rightarrow ^!\) by \(\rightarrow ^*\) and \(\hookrightarrow \!\!\!\!\!\rightarrow ^!\) by \(\hookrightarrow \!\!\!\!\!\rightarrow ^*\)) [38, Example 4].
Theorem 6
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\). For all terms s, t,
(\(\Rightarrow \)) If \(t\in {\mathsf {norm}}_\mu (s)\), then \(s\rightarrow ^!t\). By Theorem 5, \(t\,\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }\,u\). (\(\Leftarrow \)) If \(s\,\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }\,t\), then, since t is a normal form (hence a \(\mu \)-normal form), by Proposition 14, there is \(m>0\) such that \(s=s_1\hookrightarrow _{\mu }s_2\hookrightarrow _{\mu }\cdots \hookrightarrow _{}s_m\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }t\) with \(s_m\) a normal form and \(s_i\)\(\mu \)-reducible for all \(1\le i<m\). We proceed by induction on the lexicographic combination of \(>_\mathbb {N}\) and \(\rhd \) on pairs of positive natural numbers and terms. For the base case, if \(m=1\), then s is a \(\mu \)-normal form which is either a constant or a variable. By [40, Theorem 5.8], \(s\hookrightarrow ^!_{\mu }t\) and \(\overline{{\mathcal{P}os}^{\mu }}(t)=\varnothing \) (hence \( MRC ^\mu (t)=t\)). Therefore, according to (17) and (18), \({\mathsf {norm}}_\mu (s)=t\). For the induction case, assume that \(m>1\). We consider two cases:
1.
If \(s_2\) is a \(\mu \)-normal form, by [40, Theorem 6.3] we have \(C[,\ldots ,]= MRC ^\mu (s_2)= MRC ^\mu (t)\), and therefore, \(s_2=C[s'_1,\ldots ,s'_n]\) and \(t=C[t_1,\ldots ,t_n]\) for some terms \(s'_1,\ldots ,s'_n,t_1,\ldots ,t_n\), and for all \(1\le i\le n\), \(s'_i\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }t_i\). Since \(C[,\ldots ,]\ne \Box \), by the induction hypothesis, for all \(1\le i\le n\), \(t_i\in {\mathsf {norm}}_\mu (s'_i)\) and according to (17), \(t\in {\mathsf {norm}}_\mu (s_2)\); hence, \(t\in {\mathsf {norm}}_\mu (s)\).
2.
If \(s_2\) is not a \(\mu \)-normal form, then by the induction hypothesis, \(t\in {\mathsf {norm}}_\mu (s_2)\); hence, \(t\in {\mathsf {norm}}_\mu (s)\).
Left-linearity of \(\mathcal{R}\) and \(\mu \in { CM _{\mathcal{R}}}\) are necessary for Theorem 6 to hold.
Example 31
Consider \(\mathcal{R}\) and \(\mu \) in Example 30. We have \({\mathsf {f}}({\mathsf {c}})\in {\mathsf {norm}}_\mu ({\mathsf {f}}({\mathsf {a}}))\), but, since \({\mathsf {f}}({\mathsf {c}})\) is not a normal form, it can be reduced with LCSR. Furthermore, \({{\mathsf {f}}({\mathsf {a}})\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mathcal{R},\mu }{\mathsf {b}}}\), but \(b\notin {\mathsf {norm}}_\mu ({\mathsf {f}}({\mathsf {a}}))\). With \(\mathcal{R}'\) and \(\mu '\) we have \({\mathsf {g}}({\mathsf {c}},{\mathsf {c}})\in {\mathsf {norm}}_\mu ({\mathsf {g}}({\mathsf {c}},{\mathsf {a}}))\), but \({\mathsf {g}}({\mathsf {c}},{\mathsf {c}})\) can be reduced with LCSR. Also, \({\mathsf {g}}({\mathsf {c}},{\mathsf {a}})\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mathcal{R},\mu }{\mathsf {b}}\), but \({\mathsf {b}}\notin {\mathsf {norm}}_\mu ({\mathsf {g}}({\mathsf {c}},{\mathsf {a}}))\).
Theorem 6 enables the use of LCSR in a reduction-based description of \(\textit{N} \mu \textit{N}\) which can be used to define computational complexity of \(\textit{N} \mu \textit{N}\) as derivational complexity of \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\). In order to do this, we need to guarantee that LCSR terminates when used with a CS-TRS \((\mathcal{R},\mu )\). In the following section, we investigate this problem.
8.2 Termination of Layered CSR
We introduce a short notation for termination of \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }\).
Definition 12
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). We say that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating if \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }\) is terminating.
Termination of LCSR provides a sufficient condition for normalization of TRSs:
Proposition 16
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). If \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating, then \(\mathcal{R}\) is normalizing.
Proof
Since \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating, for every term s there is t such that \(s\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }t\). By Proposition 13, t is a normal form, i.e., \(\mathcal{R}\) is normalizing.
Terminating TRSs are \(\widehat{\mu }\)-terminating for all \(\mu \in {M_{\mathcal{R}}}\). And \(\widehat{\mu }\)-terminating TRSs are \(\mu \)-terminating. We also have the following sufficient condition for \(\widehat{\mu }\)-termination.
Theorem 7
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\). If \(\mathcal{R}\) is confluent, normalizing and \(\mu \)-terminating, then \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating.
Proof
If \(\mathcal{R}\) is not \(\widehat{\mu }\)-terminating, there is an infinite \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-sequence \(t=t_1\hookrightarrow \!\!\!\!\!\rightarrow t_2{\hookrightarrow \!\!\!\!\!\rightarrow }\cdots \). Since \(\mathcal{R}\) is normalizing and confluent, t has a single normal form \(\overline{t}\) of size \(N=|\overline{t}|\). By Corollary 3, there is \(i\ge 1\) such that \(|t_i|\ge N+1\). By confluence, \(t_i\rightarrow ^*\overline{t}\) and by Corollary 3, \(|\overline{t}|\ge N+1\), leading to a contradiction.
The following example shows that confluence cannot be dropped from Theorem 7.
Example 32
Consider the non-confluent TRS \(\mathcal{R}=\{{\mathsf {a}}\rightarrow {\mathsf {b}},{\mathsf {a}}\rightarrow {\mathsf {c}}({\mathsf {a}})\}\) [36, Example 39] together with \(\mu ={\mu _\bot }\in { CM _{\mathcal{R}}}\). Although \(\mathcal{R}\) is \(\mu \)-terminating and normalizing, we have the following infinite sequence of LCSR: \(\underline{{\mathsf {a}}}\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }{\mathsf {c}}(\underline{{\mathsf {a}}})\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }{\mathsf {c}}({\mathsf {c}}(\underline{{\mathsf {a}}}))\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\cdots \).
Confluence and normalization of TRSs can often be automatically proved by using available tools, see CoCoWeb [31], for a unified platform of confluence tools, and FORT [52] for normalization (of right-ground TRSs).
Example 33
For \(\mathcal{R}\) and \(\mu \) in Example 21, the \(\mu \)-termination proof in Example 26 is obtained by mu-term7. Confluence is proved by all CoCoWeb tools. Finally, \(\mathcal{R}\) can easily be proved normalizing. Thus, \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating
8.3 Layered CSR as a Rewriting Strategy
In contrast to CSR, \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mathcal{R},\mu }\)-normal forms are normal forms (Proposition 13), and therefore, LCSR always reduces terms which are not normal forms. Thus, LCSR can be seen as a (non-deterministic) one-step rewriting strategy
Now, the following generalization of Theorem 7 is immediate (the proof is analogous to that of Theorem 7).
Theorem 8
Let \(\mathcal{R}\) be a left-linear and confluent TRS, and \(\mu \in { CM _{\mathcal{R}}}\). If \(\mathcal{R}\) is \(\mu \)-terminating, then \(\mathsf{S}_{ LCSR }\) is normalizing.
Theorem 8 formalizes the observation in [40, Sect. 9.3], claiming that \({\mathsf {norm}}_\mu \) is a mapping from terms to terms whenever \(\mathcal{R}\) is left-linear and confluent, and \(\mu \in { CM _{\mathcal{R}}}\) makes \(\mathcal{R}\)\(\mu \)-terminating.
9 Derivational Height of Layered Context-Sensitive Rewriting
Theorem 6 describes \(\textit{N} \mu \textit{N}\) as normalization using LCSR. Thus, we investigate computational complexity of \(\textit{N} \mu \textit{N}\) as the derivational complexity of LCSR:
Definition 13
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating. Let
denote the derivational height and derivational complexity of LCSR, respectively.
In the remainder of the paper, we obtain bounds on \(\mathsf {dc}_{\widehat{\mu }}(n)\) from bounds on \(\mathsf {dc}_{\mu }(n)\). According to Proposition 14, for left-linear TRSs \(\mathcal{R}\) and \(\mu \in { CM _{\mathcal{R}}}\), rewrite sequences in LCSR can be decomposed in a (possibly empty) initial subsequence of context-sensitive rewriting steps followed of a possibly empty sequence of additional reductions issued on \(\mu \)-normal forms. If \(\mathcal{R}\) is \(\mu \)-terminating, then the initial context-sensitive sequence must be finite.
Proposition 17
Let \(\mathcal{R}\) be a terminating, left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\). For all terms t and \(n\in \mathbb {N}\), \(\mathsf {dh}_{\widehat{\mu }}(t) \le \mathsf {dh}(t,\rightarrow _\mathcal{R})\) and \(\mathsf {dc}_{\widehat{\mu }}(n) \le \mathsf {dc}_\mathcal{R}(n)\).
Remark 14
In the following, we use sums (\(\sum \)) and products (\(\prod \)) of numbers indexed by finite but potentially empty collections of indices. As usual, we give values 0 and 1, respectively, to sums and products of empty collections of numbers.
The following result connects \(\mathsf {dh}_\mu \) and \(\mathsf {dh}_{\widehat{\mu }}\) on the basis of the definition of LCSR.
Proposition 18
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating. Then,
Since \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating, it is also \(\mu \)-terminating. By Proposition 14, every maximal normalization sequence \(s=s_1\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }s_2\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\cdots \hookrightarrow \!\!\!\!\!\rightarrow _{\mu }s_n=t\), where t is a normal form, can be written as follows:
for some \(m\ge 1\) such that \(s_m,\ldots ,s_n\) are \(\mu \)-normal forms. Let \(C[,\ldots ,]= MRC ^\mu (s_m)\) a context with p holes. By [40, Theorem 6.3], for all \(m\le i\le n\) we have \(s_i=C[s_{i1},\ldots ,s_{ip}]\) for some terms \(s_{i1},\ldots ,s_{ip}\). In particular, \(t=C[t_1,\ldots ,t_p]\) where \(t_j=s_{nj}\) for all \(1\le j\le p\). Moreover, for all \(1\le j\le p\), \(s_{mj}\,\hookrightarrow \!\!\!\!\!\rightarrow ^!_{\mu }\,t_{j}\). Therefore, \(\mathsf {dh}_{\widehat{\mu }}(s)=n\le m+\sum _{j=1}^p\mathsf {dh}_{\widehat{\mu }}(s_{mj})\). Since \(m\le \mathsf {dh}_\mu (s)\), we obtain
Since there can be several \(\mu \)-normal forms u of s, with different maximal \(\mu \)-replacing contexts \( MRC ^\mu (u)\) with \(\mathsf {nmf}_{\mu }(u)\) holes, from (24) we finally obtain (23).
Note that, in (23), we can replace the different values \(\mathsf {nmf}_{\mu }(u)\) for \(\mu \)-normal forms u of s by \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\) in Definition 5 to remove the big sum in (23):
The advantage is that we can use the bounds on \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\) developed in Sect. 7.2 (Corollary 2 and Proposition 12) to obtain a translation of (25) into a bound on \(\mathsf {dc}_{\widehat{\mu }}(n)\). However, we first have to deal with the maximal frozen subterms occurring in (25). The set of maximal frozen subterms \(s'\) which can be obtained from \(\mu \)-normal forms u of s is:
We have \({\mathcal{F}r}^{\mu }(u_1)=\{1.1\}\) and \(s_1={\mathsf {f}}({\mathsf {g}}({\mathsf {f}}({\mathsf {g}}({\mathsf {f}}(x)))))\) is the maximal frozen subterm in \(u_1\). The outermost\(\mu \)-normalization of s is:
where the maximal frozen subterm of \(u_2\) is \(s_2={\mathsf {f}}({\mathsf {f}}({\mathsf {f}}(x)))\). There also are ‘intermediate’ \(\mu \)-normalization sequences for s:
where the maximal frozen subterms of \(u_3\) and \(u_4\) are \(s_3={\mathsf {f}}({\mathsf {g}}({\mathsf {f}}({\mathsf {f}}(x))))\), and \(s_4={\mathsf {f}}({\mathsf {f}}({\mathsf {g}}({\mathsf {f}}(x))))\), respectively. Thus, \(\mathsf {MFRZ}_{\mu }(s) = \{s_1,s_2,s_3,s_4\}\).
By using the previous notations, Proposition 18 leads to the following:
Theorem 9
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating. Let s be a term. Then,
For non-\(\mu \)-duplicating TRSs, according to Proposition 12, we have
Corollary 4
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is non-\(\mu \)-duplicating and \(\widehat{\mu }\)-terminating, and \(F=F(\mathcal{R})\). Let s be a term. Then,
of length 2. This is the only possible \(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-sequence on t. However, if we make t ground by replacing the variable occurrence of x by a to obtain a term \(t'\) of the same size, we are only able to obtain a shorter sequence
consisting of a single context-sensitive rewriting step due to the fact that \(t'\) is not a \(\mu \)-normal form now.
Thus, it is unclear whether an equality like (11) holds for LCSR.
In particular, Example 35 shows that LCSR is not closed under substitutions, even for left-linear TRSs \(\mathcal{R}\) and \(\mu \in { CM _{\mathcal{R}}}\): We have \(t=f(x,f(\underline{f(a,a)},a)) \hookrightarrow \!\!\!\!\!\rightarrow _{\mu } f(x,f(a,a))=u\), but the instance \(t'\) of t does not\(\hookrightarrow \!\!\!\!\!\rightarrow _{\mu }\)-reduce to the corresponding instance \(u'=f(a,f(a,a))\) of u.
For this reason, in the following we also consider ground terms in the analysis of derivational complexity of LCSR. Accordingly, we introduce the following
Clearly, for all \(n\in \mathbb {N}\), \(\mathsf {gdc}_{\widehat{\mu }}(n)\le \mathsf {dc}_{\widehat{\mu }}(n)\).
10 Derivational Complexity of Normalization via \(\mu \)-Normalization
We can use (26) to obtain bounds on \(\mathsf {dc}_{\widehat{\mu }}(n)\) by replacing (i) \(\mathsf {dh}_{\widehat{\mu }}(s)\) by \(\mathsf {dc}_{\widehat{\mu }}(n)\) for terms s whose size is bounded by n, (ii) \(\mathsf {dh}_\mu (s)\) by \(\mathsf {dc}_\mu (n)\), (iii) \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\) by
to obtain an upper bound on the (maximum) number \(\mathsf {NMF}^{\hookrightarrow ^!_{}}_{\mu }(s)\) of holes in \( MRC ^\mu (u)\) to be considered in each intermediate \(\mu \)-normalization phase of \(\textit{N} \mu \textit{N}\) when applied to terms s of size \(|s|\le n\) to yield a \(\mu \)-normal form u, and (iv) \(\mathsf {dh}_{\widehat{\mu }}(s')\) by \(\mathsf {dc}_{\widehat{\mu }}(n-1)\), thus assuming a decrease of \(|s'|\) with respect to |s| for all \(s'\in \mathsf {MFRZ}_{\mu }(s)\) to obtain
from which an explicit description of \(\mathsf {dc}_{\widehat{\mu }}(n)\) in terms of \(\mathsf {dc}_\mu (n)\) can be obtained. However, Example 34 shows that terms \(s'\) in \(\mathsf {MFRZ}_{\mu }(s)\) can be bigger than s; for instance, \(|s_1|=6>5=|s|\). Thus, in general, terms in \(\mathsf {MFRZ}_{\mu }(s)\) do not decrease in size. Hence, item (iv) in the previous list may fail to be sound.
Definition 14
We say that \(\mathsf {MFRZ}_{\mu }\) is (strictly) size-decreasing if for all terms s and \(s'\in \mathsf {MFRZ}_{\mu }(s)\), \(|s|>|s'|\).
Proposition 19
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\). If \(\hookrightarrow ^!_{}\) is size-decreasing, then \(\mathsf {MFRZ}_{\mu }\) is size-decreasing.
Proof
If \(t'\in \mathsf {MFRZ}_{\mu }(s)\), then there is a term t such that \(s\hookrightarrow ^!_{}t\) and \(t'\) is a frozen (i.e., strict) subterm of t. By size-decreasingness of \(\hookrightarrow ^!_{}\), \(|s|\ge |t|\). Since \(t\rhd t'\), \(|s|>|t'|\).
Example 36
Consider \(\mathcal{R}\) in Example 2 and \(\mu \) in Example 15. As shown in Example 24, \(\hookrightarrow ^!_{\mathcal{R},\mu }\) is size-decreasing. By Proposition 19, \(\mathsf {MFRZ}_{\mu }\) is size-decreasing.
The following alternative result establishes conditions guaranteeing a decrease in the size of frozen subterms obtained at the end of any\(\mu \)-rewrite sequence.
Proposition 20
Let \(\mathcal{R}\) be a TRS and \(\mu \in {M_{\mathcal{R}}}\) be such that, for all \(\ell \rightarrow r\in \mathcal{R}\), \(\overline{Pos^\mu _{\mathcal{F}}}(r)=\varnothing \) and . Then, for all terms s such that \(s\hookrightarrow ^*_{\mu }t\) and frozen subterms \(t'\) of t, and \(|s|>|t'|\). Hence, \(\mathsf {MFRZ}_{\mu }\) is size-decreasing.
Proof
If t contains no frozen subterm, then the conclusion vacuously follows. Thus, assume that t contains a frozen subterm \(t'\), i.e., . We proceed by induction on the length n of the sequence \(s\hookrightarrow ^*_{\mu }t\). If \(n=0\), then \(s=t\), and therefore, . If \(n>0\), then consider \(s\hookrightarrow _{\mu } s'\hookrightarrow ^*_{\mu }t\). We have \(s|_p=\sigma (\ell )\) for some \(p\in {\mathcal{P}os}^\mu (s)\), \(\ell \rightarrow r\in \mathcal{R}\), and substitution \(\sigma \). We also have \(s'=s[\sigma (r)]_p\). By the induction hypothesis, , i.e., there is a position \(q\in \overline{{\mathcal{P}os}^\mu }(s')\) such that \(s'|_q=t'\). If \(q\parallel p\), then \(q\in \overline{{\mathcal{P}os}^\mu }(s)\) and . Otherwise, \(p<q\) and, since \(\overline{{\mathcal{P}os}^\mu _{\mathcal{F}}}(r)=\varnothing \), there is a variable \(x\in \mathcal{V}ar(r)\) such that either (i) \(x\in \mathcal{V}ar^\mu (r)\) and , or (ii) and \(\sigma (x)\unrhd t'\). In the first case (i), we have , and hence, . In the second case (ii), since , we also have . Since frozen positions always are below the root of terms, s can be written \(s=f(s_1,\ldots ,s_k)\) and we have \(s_i\unrhd t'\) for some \(1\le i\le n\), i.e., \(|s|>|s_i|\ge |t'|\).
Example 37
For \(\mathcal{R}\) and \(\mu \) in Example 5, \(\hookrightarrow ^!_{}\) is not size-decreasing. For instance, \(s=\underline{x \wedge (y\vee z)} \hookrightarrow _{(8),\mu } (x\wedge y)\vee (x\wedge z)=t\) and t is a \(\mu \)-normal form, but \(|s|=5<7=|t|\). However, the conditions in Proposition 20 are fulfilled, thus proving \(\mathsf {MFRZ}_{\mu }\) size-decreasing: subterms at frozen positions in right-hand sides of rules are variables; as for frozen variables in left- and right-hand sides,
11 Bounds on \(\mathsf {dc}_{\widehat{\mu }}(n)\)
In this section, we use the previous results to obtain bounds on \(\mathsf {dc}_{\widehat{\mu }}(n)\).
Theorem 10
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating and \(\mathsf {MFRZ}_{\mu }\) is size-decreasing. Then,
The following corollary of Proposition 5 provides some bounds for \(\mathsf {bnmf}_{\mu }(n)\).
Corollary 5
Let \({\mathcal{F}}\) be a p-adic signature and \(\mu \in {M_{{\mathcal{F}}}}\). Then, for all \(n\in \mathbb {N}\),
1.
If \(\mu =\mu _\bot \), then \(\mathsf {bnmf}_{\mu }(n)\le p\).
2.
If \(\mu ={\mu _\top }\), then \(\mathsf {bnmf}_{\mu }(n)=0\).
3.
If \(p>1\), and \({\mathcal{F}}\) is 1-active, then \(\mathsf {bnmf}_{\mu }(n)\le \frac{p-1}{p}n\).
4.
Otherwise, \(\mathsf {bnmf}_{\mu }(n)\le n\).
The following result characterizes some bounds on \(\mathsf {bnmf}_{\mu }(n)\).
Proposition 21
Let \({\mathcal{F}}\) be a p-adic signature and \(\mu \in {M_{{\mathcal{F}}}}\). Then, for all \(n\in \mathbb {N}\),
1.
\(\mathsf {bnmf}_{\mu }(n)=0\) if and only if \(\mu ={\mu _\top }\).
2.
\(\mathsf {bnmf}_{\mu }(n) \le p\) if and only if \(\mu ={\mu _\top }\) or \(\mu (f) = \varnothing \) for all \(f\in {\mathcal{F}}\) with \(ar(f)\ge 2\).
Proof
1.
The if part follows by Corollary 5(2). As for the only if part, we proceed by contradiction. Assume that, for all \(n\in \mathbb {N}\), \(\mathsf {bnmf}_{\mu }(n)=0\) but \(\mu \ne {\mu _\top }\). Then there is a k-ary symbol f with \(k\ge 1\) such that \(\mu (f)\subset \{1,\ldots ,k\}\). Hence, the term \(f(x_1,\ldots ,x_k)\) of size \(k+1\) contains at least a frozen subterm. Hence, \(\mathsf {bnmf}_{\mu }(k+1)\ne 0\), a contradiction.
2.
Regarding the if part, if \(\mu ={\mu _\top }\), then, by Corollary 5(2), we have \(\mathsf {bnmf}_{\mu }(n)=0\le p\). Otherwise, we prove by structural induction on terms t that \(\mathsf {nmf}_{\mu }(t)\le p\). If t is a constant or a variable, then \(\mathsf {nmf}_{\mu }(t)=0\le p\). If \(t=f(t_1,\ldots ,t_k)\) for some symbol \(f\in {\mathcal{F}}\) and \(t_1,\ldots ,t_k\), we consider two cases: (a) If f is a monadic symbol, then \(t=f(t')\) and by the induction hypothesis, \(\mathsf {nmf}_{\mu }(t')\le p\). If \(\mu (f)=\{1\}\), then, by the induction hypothesis, \(\mathsf {nmf}_{\mu }(t)=\mathsf {nmf}_{\mu }(t')\le p\); if \(\mu (f)=\varnothing \), then \(\mathsf {nmf}_{\mu }(t)=1\le p\) (b) If \(ar(f)>1\), then \(\mu (f)=\varnothing \) and \(\mathsf {nmf}_{\mu }(t)=ar(f)\le p\). Thus, for all terms t, \(\mathsf {nmf}_{\mu }(t)\le p\), i.e., \(\mathsf {bnmf}_{\mu }(n)\le p\).
Regarding the only if part, assume that \(\mathsf {bnmf}_{\mu }(n)\le p\), but (c) \(\mu \ne {\mu _\top }\) and (d) \(\mu (f)\ne \varnothing \) for some \(f\in {\mathcal{F}}\) with \(ar(f)\ge 2\). Then, by (d) there is \(g\in {\mathcal{F}}\) with \(ar(g)\ge 2\) and \(|\mu (g)|\ne \varnothing \), i.e., \(i_1\in \mu (g)\) for some \(1\le i_1\le ar(g)\). Let \(i_2\in \{1,\ldots ,ar(g)\}-\{i_1\}\) be another argument index of g. Without loss of generality, we assume \(i_1<i_2\). By (c), there is \(f\in {\mathcal{F}}\) with \(j\notin \mu (f)\) for some \(1\le j\le ar(f)\). Let \(s=f(y_1,\ldots ,y_{i-1},y,y_{i+1},\ldots ,y_{q})\) and
Note that y is frozen in s and x is active in position \(i_1\) of t. Define \(t_0=s\) and for all \(m> 0\)\(t_m=\sigma _m(t)\), where \(\sigma _m(x)=t_{m-1}\). We consider two cases: (A) If \(i_2\in \mu (g)\), then t contains at least two active positions (\(i_1\) and \(i_2\)) and for all \(m\ge 0\), \(t_m\) contains at least \(2^m\) maximal frozen subterms (introduced by the occurrences of variable y in s when distributed in \(t_m\)). (B) If \(i_2\notin \mu (g)\), then for all \(m\ge 0\), \(t_m\) contains at least \(m+1\) maximal frozen subterms. Therefore, for a sufficiently big value of m, we have \(\mathsf {nmf}_{\mu }(t_m)>p\), thus contradicting the bound for \(\mathsf {bnmf}_{\mu }(n)\).
For non-\(\mu \)-duplicating TRSs, we have the following.
Theorem 11
Let \(\mathcal{R}\) be a left-linear TRS and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating and non-\(\mu \)-duplicating, and \(\mathsf {MFRZ}_{\mu }\) is size-decreasing. Let \(F=F(\mathcal{R})\).
1.
If \(F>0\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\le \sum _{i=1}^{n}\left( \prod _{j=i+1}^{n}(\mathsf {bnmf}_{\mu }(j)+F\mathsf {dc}_\mu (j))\right) \mathsf {dc}_\mu (i)\).
2.
If \(F=0\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\le \sum _{i=1}^{n}\left( \prod _{j=i+1}^{n}\mathsf {bnmf}_{\mu }(j)\right) \mathsf {dc}_\mu (i)\).
3.
If \(F<0\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\le \sum _{i=1}^{n}\prod _{j=i+1}^{n}\mathsf {bnmf}_{\mu }(j)\).
Proof
Proceed like in Theorem 10, using Corollary 4 instead of Theorem 9 for the three considered cases.
The following result shows how asymptotic bounds on \(\mathsf {dc}_{\widehat{\mu }}(n)\) and \(\mathsf {gdc}_{\widehat{\mu }}(n)\) are obtained from asymptotic bounds on \(\mathsf {dc}_\mu (n)\). Remind that we assume TRSs \(\mathcal{R}=({\mathcal{F}},R)\) where \({\mathcal{F}}\) contains a constant symbol (see (14) for CSR); use \(\mathcal{R}^\bullet =({\mathcal{F}}^\bullet ,R)\) otherwise, as explained in the previous sections, see Proposition 2. This is important when bounds depend on \({\mathcal{F}}^!_{\mu }\), which is defined assuming the existence of ground terms.
Corollary 6
Let \(\mathcal{R}=({\mathcal{F}},R)\) be a left-linear TRS such that \({{\mathcal{T}({\mathcal{F}})}}\ne \varnothing \) and \(\mu \in { CM _{\mathcal{R}}}\) be such that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating and \(\mathsf {MFRZ}_{\mu }\) is size-decreasing. Let \(\mathsf {dc}_\mu (n)\in O({\mathfrak {f}}(n))\).
1.
If \({\mathcal{F}}^!_{\mu }\) is 0-adic, then \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O({\mathfrak {f}}(n))\).
2.
If for all \(f\in {\mathcal{F}}^!_{\mu }\), \(\mu (f)={\mu _\top }(f)\), then \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O({\mathfrak {f}}(n))\).
3.
If \({\mathcal{F}}^!_{\mu }\) is monadic and 0-active, then \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O(n{\mathfrak {f}}(n))\).
4.
If \({\mathcal{F}}^!_{\mu }\) is p-adic with \(p>1\), then
(a)
If \({\mathcal{F}}^!_{\mu }\) is 0-active, then \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O(p^n{\mathfrak {f}}(n))\)
(b)
If \(\hookrightarrow ^!_{}\) is size-decreasing, then \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O(n^{n}{\mathfrak {f}}(n))\)
5.
If \(\mathcal{R}\) is non-\(\mu \)-duplicating, then let \(\eta _F\in \{-1,0,1\}\) denote the sign of \(F(\mathcal{R})\).
(a)
If \(F(\mathcal{R})>0\), then
i.
if \(\mathsf {bnmf}_{\mu }(n)\le b\) for some \(b\in \mathbb {N}\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\in n({\mathfrak {f}}(n))^n2^{O(n)}\),
if \(\mathsf {bnmf}_{\mu }(n)=0\) for all \(n\in \mathbb {N}\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\in O(({\mathfrak {f}}(n))^{1+\eta _F})\),
ii.
if there is \(b\ge 1\) such that \(\mathsf {bnmf}_{\mu }(n)\le b\) for all \(n\in \mathbb {N}\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\in O(nb^n{\mathfrak {f}}(n))\),
By Theorem 10 and Corollary 2(2), which applies to ground terms, and taking into account (14), \(\mathsf {gdc}_{\widehat{\mu }}(n)\le \mathsf {dc}_\mu (n)\), i.e., \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O({\mathfrak {f}}(n))\).
3.
By Theorem 10 and Corollary 2(1), \(\mathsf {gdc}_{\widehat{\mu }}(n)\le n\mathsf {dc}_\mu (n)\), i.e., \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O(n{\mathfrak {f}}(n))\).
Otherwise, we similarly obtain \(\mathsf {dc}_{\widehat{\mu }}(n)\in O((n{\mathfrak {f}}(n))^n)\).
(b)
By Theorem 11, if \(F=0\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\le \sum _{i=1}^{n}\left( \prod _{j=i+1}^{n}\mathsf {bnmf}_{\mu }(j)\right) \mathsf {dc}_\mu (i)\); if \(F<0\), \(\mathsf {dc}_{\widehat{\mu }}(n)\le \sum _{i=1}^{n}\prod _{j=i+1}^{n}\mathsf {bnmf}_{\mu }(j)\).
As for the first case, (i) \(\mathsf {bnmf}_{\mu }(n)=0\), if \(F=0\), we obtain \(\mathsf {dc}_{\widehat{\mu }}(n)\le \mathsf {dc}_\mu (n)\in O({\mathfrak {f}}(n))\); if \(F<0\), then \(\mathsf {dc}_{\widehat{\mu }}(n)\le \sum _{i=1}^{n}\prod _{j=i+1}^{n}0=1\in O(1)\). Both can be written at once as \(\mathsf {dc}_{\widehat{\mu }}(n)\in O(({\mathfrak {f}}(n))^{1+\eta _F})\). The other cases are similar.
Example 38
(Running example II—bounds) For \(\mathcal{R}\) and \(\mu \) in Example 2, \({\mathcal{F}}\) is 1-active and by Proposition 5, \(\mathsf {bnmf}_{\mu }(n)\le \frac{n}{2}\); \(\mathcal{R}\) is non-\(\mu \)-duplicating (Example 24); and \(F(\mathcal{R})=-1\) (Example 27). The strongly linear interpretation in Example 15 proves \(\mathsf {dc}_\mu (n)\in O(n)\). By Corollary 6(5(b)iii), \(\mathsf {dc}_{\widehat{\mu }}(n)\in O(n^n)\). This bound is worse than the quadratic bound for \(\mathsf {dc}_\mathcal{R}(n)\) obtained in Example 13 (also by AProVE).
Example 39
(Running example IV—improved bounds) For \(\mathcal{R}\) and \(\mu \) in Example 5, \(\mathcal{R}\) is non-\(\mu \)-duplicating (Example 28); \(F(\mathcal{R})=1\) (Example 27); and the linear interpretation in Example 17 proves \(\mathsf {dc}_\mu (n)\in 2^{O(n)}\). By Corollary 6(5(a)ii), there is \(c>0\) such that \(\mathsf {dc}_{\widehat{\mu }}(n)\in O((n 2^{cn})^n)\). Since
we get \(\mathsf {dc}_{\widehat{\mu }}(n)\in 2^{O(n^2)}\), improving on the doubly exponential bound for \(\mathsf {dc}_\mathcal{R}(n)\) obtained from the polynomial interpretation in Example 11 (see Example 12).
Example 40
(Running example V—bounds) For \(\mathcal{R}\) and \(\mu \) in Example 21, \(\mathcal{R}\) is proved \(\mu \)-terminating by using a strongly linear polynomial interpretation (Example 26). By Theorem 3(2), \(\mathsf {dc}_\mu (n)\in O(n)\). Furthermore, \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating (Example 33). Since \({\mathcal{F}}^!_{\mu }=\{{\mathsf {b}},{\mathsf {c}}\}\) is monadic and 0-active (Example 22), by Corollary 6 (3), \(\mathsf {gdc}_{\widehat{\mu }}(n)\in O(n^2)\). Note that \(\mathcal{R}\) is not terminating, and \(\mathsf {dc}_\mathcal{R}(n)\) is undefined.
12 Related Work
As far as we know, this is the first paper explicitly defining and investigating derivational complexity of CSR and \(\textit{N} \mu \textit{N}\). However, Hirokawa and Moser [30] pioneering the use of CSR in complexity analysis by applying CSR to investigate runtime complexity analysis of TRSs [29]. In runtime complexity analysis, all considered initial expressions s are basic terms \(s\in {{\mathcal{T}_b({\mathcal{F}},{\mathcal{X}})}}\), i.e., terms \(s=f(t_1,\ldots ,t_k)\) where \(t_1,\ldots ,t_k\) are constructor terms. Given a terminating TRS, the runtime complexity of basic terms of size at most n is denoted \(\mathsf {rc}_\mathcal{R}(n)\) and bounds on \(\mathsf {rc}_\mathcal{R}(n)\) are obtained from matrix interpretations, among other techniques. Bounds on runtime complexity can be very different from bounds on derivational complexity. For instance, [29, Example 1] shows a TRS whose derivational complexity is exponentially bounded whereas its runtime complexity is proved linear in [30, Example 18]. Hirokawa and Moser show how to define replacement maps \(\mu \) so that the compatibility of the ordering \(\succ _\mathcal{A}\) induced by specific \(\mu \)-monotone matrix interpretations \(\mathcal{A}\) (restricted versions of TMIs, actually) can be used to correctly induce bounds on \(\mathsf {rc}_\mathcal{R}(n)\). As a matter of fact, they were providing the first analysis of runtime complexity of CSR based on matrix interpretations: a \(\mu \)-monotone matrix interpretation \(\mathcal{A}\) whose associated ordering \(\succ _\mathcal{A}\) is compatible with a TRS \(\mathcal{R}\) actually proves \(\mu \)-termination of \(\mathcal{R}\). As discussed in the proofs of our Theorem 2, the validity of the polynomial bounds obtained from matrix interpretations \(\mathcal{A}\) in [30, Sect. 2] does not depend on any monotonicity assumption. Thus, given a replacement map \(\mu \), they actually provide bounds on \(\mathsf {rc}_{\mathcal{R},\mu }(n)=\max \{\mathsf {dh}(s,\hookrightarrow _{\mu })\mid s\in {{\mathcal{T}_b({\mathcal{F}},{\mathcal{X}})}}, |s|\le n \}\), the runtime complexity bound for CSR. Therefore, the results in [30, Sect. 2] can be used to obtain bounds on \(\mathsf {rc}_{\mathcal{R},\mu }(n)\) for arbitrary replacement maps \(\mu \).8
13 Conclusions
We have investigated derivational complexity of CSR, with special emphasis in the analysis of derivational complexity (bounds) for normalization via \(\mu \)-normalization, a normalization procedure based on CSR which has been recently implemented for use in Maude by using its strategy language (see Remark 1). An appropriate definition of derivational complexity for CSR, \(\mathsf {dc}_\mu (n)\), is given in Sect. 6. Some results showing how to obtain bounds on derivational complexity of CSR are given in Proposition 4 (on a purely syntactic basis), and Theorems 2 and 3, for proofs of \(\mu \)-termination based on matrix and polynomial interpretations, respectively. Normalization via \(\mu \)-normalization can be used not only with terminating TRSs but also with \(\mu \)-terminating TRSs for which the procedure is guaranteed to terminate. Section 7 gives a characterization of normalization via \(\mu \)-normalization using layeredCSR, which permits to reuse the standard definition of derivational complexity for abstract reduction relations. Theorem 7 provides a criterion for termination of layered CSR which can be used to prove termination of \(\textit{N} \mu \textit{N}\) to make sense of derivational complexity analysis of non-terminating TRSs. We provide full descriptions of the length \(\mathsf {dh}_{\widehat{\mu }}(s)\) of \(\textit{N} \mu \textit{N}\) computations starting from a term s from the length of the intermediate context-sensitive rewrite sequences (Proposition 18 and Theorem 9). Such a description is used to characterize the derivational complexity \(\mathsf {dc}_{\widehat{\mu }}(n)\) of \(\textit{N} \mu \textit{N}\) when used to evaluate terms of size at most n (Theorems 10 and 11). These results finally yield asymptotic bounds on \(\mathsf {dc}_{\widehat{\mu }}(n)\) and \(\mathsf {gdc}_{\widehat{\mu }}(n)\). In Corollary 6, we show how to obtain them from bounds on \(\mathsf {dc}_\mu (n)\).
Overall, we can benefit from CSR to improve bounds on computational complexity of normalization in different ways. First, dealing with non-terminating but \(\mu \)-terminating and normalizing TRSs,
1.
If CSR can be seen as a rewriting strategy (because \(\mu \)-normal forms and normal forms coincide), then \(\mathsf {dc}_\mu (n)\) can be used instead of the undefined \(\mathsf {dc}_\mathcal{R}(n)\). The running example I (Example 1) illustrates this use.
2.
If \(\mu \)-normal forms are not normal forms, then \(\textit{N} \mu \textit{N}\) can be used to obtain them, provided that \(\mathcal{R}\) is \(\widehat{\mu }\)-terminating, as in running example V (Example 21).
Dealing with terminating TRSs, we can also obtain some advantages:
1.
If \(\mu \)-normal forms and normal forms coincide, then \(\mathsf {dc}_\mu (n)\) can be used instead of \(\mathsf {dc}_\mathcal{R}(n)\). The running example III (Example 3) illustrates this.
2.
Otherwise, we can use \(\textit{N} \mu \textit{N}\) to obtain normal forms. Sometimes \(\mathsf {dc}_{\widehat{\mu }}(n)\) yields better estimations than \(\mathsf {dc}_\mathcal{R}(n)\) (e.g., the running example IV (Example 5). In other cases, no improvement is obtained (e.g., running example II, Example 2).
14 Future work
Extending this research to also consider lower bounds on derivational complexity of CSR and \(\textit{N} \mu \textit{N}\) would be interesting. Also considering runtime complexity of \(\textit{N} \mu \textit{N}\) is interesting. More research would be necessary to remove the size-decreasingness requirement in some of our results as it imposes quite hard requirements on TRSs to obtain explicit asymptotic bounds. The point is evident by comparing, e.g., Theorem 10 with Theorem 9, establishing the (recursive) relationship between derivational length of CSR and \(\textit{N} \mu \textit{N}\), where size-decreasingness is not necessary. This suggests that size-decreasingness is not an intrinsic feature of the description of derivational complexity of \(\textit{N} \mu \textit{N}\). Unfortunately, the attempts to get rid from this restriction failed to date.
Acknowledgements
I thank the referees for their comments and suggestions leading to many improvements in the presentation of the paper. Examples 8 and 35 were suggested by the referees. Also the discussion in Remark 4 was motivated by the questions posed by a referee.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
See [50, Definition 2.1.1] and the paragraph below this definition for a clarifying discussion about the use of ‘well-founded’ and ‘terminating’ in mathematics and computer science.
There are infinite (and terminating) TRSs which are finitely branching. Consider, for instance, the TRS \(\mathcal{R}\) with set of rules \(R=\{i+1\rightarrow i\mid i\in \mathbb {N}\}\).
Steinbach’s interpretation is \([\lnot ](x)=x^2\), \(x[\wedge ]y = xy+x\) and \(x[\vee ]y=x[\supset ]y=x+y+2\) with interpretation domain \(\mathbb {N}_{\ge 3}\). The interpretation in Example 11 is obtained from it by normalizing the intepretation domain to \(\mathbb {N}\) using the translation \(n\mapsto n+3\) [12, Sect. 3.4].
Rather than considering infinitely many valuations of the variables of the rules, we leave the variables as such and then compare the obtained polynomials as usual (see Remark 5).
Actually, mu-term automatically computes a strongly linear interpretation over the rationals as follows: \({\mathsf {a}}^\mathcal{A}=1\), \({\mathsf {b}}^\mathcal{A}=0\), \({\mathsf {c}}^\mathcal{A}(x) = 0\), and \({\mathsf {f}}^\mathcal{A}(x,y) = x+y+\frac{1}{2}\), from which we easily obtain the interpretation over the naturals in Example 26.
Although Hirokawa and Moser were not aware of this, in personal e-mail communication on early July 2020, they agreed with this analysis of their results.
) is the set of variables occurring at active (resp. frozen) positions in t: \(\mathcal{V}ar^\mu (t)=\{x\in \mathcal{V}ar(t)\mid \exists p\in {\mathcal{P}os}^\mu (t),x=t|_p\}\) and
. Note that variables in
could also be in \(\mathcal{V}ar^\mu (t)\) and vice versa. For instance, \(\mathcal{V}ar^\mu (r_{(10)})=\{x,y\}\) and
. Also, we write
if t is a frozen subterm of s.
For instance, for rule (10), we have:5
The subtraction \(\ell ^\mathcal{A}_{(10)}-r^\mathcal{A}_{(10)}\) of both polynomials yields \(x^2+y^2-xy+3x+y+6=(x-y)^2+xy+3x+y+6\), which is clearly positive for all \(x,y\ge 0\). This proves \(\succ _\mathcal{A}\) compatible with rule (10), i.e., \(\ell _{(10)}\succ _\mathcal{A}r_{(10)}\) holds.
For the rule \(\ell \rightarrow r\) in \(\mathcal{R}\), we have:For all \(1\le i\le 2\) and \(x_i,y_i,z_i\in \mathbb {N}\), \(x_1+2x_2+y_1+y_2+z_1+1>x_1+x_2+y_1+y_2+z_1\) for the first component of the obtained vectors, and \(x_2+y_2+z_2+2\ge x_2+y_2+z_2+2\) for the second one. Thus, \(\ell ^\mathcal{A}\succ _\mathcal{A}r^\mathcal{A}\), and \(\mathsf {dc}_\mathcal{R}(n)\in O(n^2)\) (see Table 1).
For signatures containing a constant symbol, as for ordinary term rewriting (see Sect. 4.1), since CSR is also closed under substitutions [40, Sect. 4], we can consider ground terms only, i.e., we have:Following the discussion in Sect. 4.1, we also have the following version of Proposition 1 for CSR (with an analogous proof using the fact that CSR is closed under substitutions).
Since \(|{\mathcal{P}os}_x(\ell )|\ge |{\mathcal{P}os}_x(r)|\) and \(|\sigma (x)|-1\ge 0\), we have \(|s|-|t|\ge |\ell |-|r|\).
proves \(\mathcal{R}\) \(\mu \)-terminating. Also, \(\mathcal{R}\) is \(\mu \)-confluent as there is no critical pair and no active variable in the left-hand side of a rule becomes frozen anywhere else in the rule (LHRV property, see [40, Sect. 8]). By Proposition 10, \(\hookrightarrow ^!_{}\) is size-decreasing.
denote the derivational height and derivational complexity of LCSR, respectively.
. Then, for all terms s such that \(s\hookrightarrow ^*_{\mu }t\) and frozen subterms \(t'\) of t,
and \(|s|>|t'|\). Hence, \(\mathsf {MFRZ}_{\mu }\) is size-decreasing.
. We proceed by induction on the length n of the sequence \(s\hookrightarrow ^*_{\mu }t\). If \(n=0\), then \(s=t\), and therefore,
. If \(n>0\), then consider \(s\hookrightarrow _{\mu } s'\hookrightarrow ^*_{\mu }t\). We have \(s|_p=\sigma (\ell )\) for some \(p\in {\mathcal{P}os}^\mu (s)\), \(\ell \rightarrow r\in \mathcal{R}\), and substitution \(\sigma \). We also have \(s'=s[\sigma (r)]_p\). By the induction hypothesis,
, i.e., there is a position \(q\in \overline{{\mathcal{P}os}^\mu }(s')\) such that \(s'|_q=t'\). If \(q\parallel p\), then \(q\in \overline{{\mathcal{P}os}^\mu }(s)\) and
. Otherwise, \(p<q\) and, since \(\overline{{\mathcal{P}os}^\mu _{\mathcal{F}}}(r)=\varnothing \), there is a variable \(x\in \mathcal{V}ar(r)\) such that either (i) \(x\in \mathcal{V}ar^\mu (r)\) and
, or (ii)
and \(\sigma (x)\unrhd t'\). In the first case (i), we have
, and hence,
. In the second case (ii), since
, we also have
. Since frozen positions always are below the root of terms, s can be written \(s=f(s_1,\ldots ,s_k)\) and we have \(s_i\unrhd t'\) for some \(1\le i\le n\), i.e., \(|s|>|s_i|\ge |t'|\).