Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In this paper we present the new confluence tool CoLL for left-linear term rewrite systems (TRSs). The tool has two distinctive features. One is use of Jouannaud and Kirchner’s theorem for the Church-Rosser modulo property. Our tool supports rewriting modulo associativity and/or commutativity rules. Another notable feature is that confluence is proved by commutation criteria only. By using Hindley’s Commutation Theorem [1] confluence is proved via commutation of subsystems of an input TRS. In addition to them, CoLL implements a simple transformation technique that eliminates redundant rewrite rules.

The remaining part of the paper is organized as follows: In Sect. 3 we discuss how to use the Church-Rosser modulo theorem for associativity and/or commutativity rules. Commutation criteria and decomposition techniques supported in the tool are described in Sect. 4. In Sect. 5 we report experimental results to assess effectiveness of the presented techniques and the tool. The final section describes related work and concluding remarks. The tool is available at:

http://www.jaist.ac.jp/project/saigawa/coll/

2 Preliminaries

We assume familiarity of term rewriting and unification theory [2]. We recall here only some notions for rewriting and rewriting modulo. We consider terms built from a signature \(\mathcal {F}\) and a set \(\mathcal {V}\) of variables. We write \(s \mathrel {{\vartriangleright }}t\) if t is a proper subterm of s.

Commutation. Let \(\mathcal {R}\) and \(\mathcal {S}\) be TRSs. We say that \(\mathcal {R}\) and \(\mathcal {S}\) commute if . Confluence of \(\mathcal {R}\) is equivalent to self-commutation of \(\mathcal {R}\), i.e., commutation of \(\mathcal {R}\) and \(\mathcal {R}\). The relation \(\rightarrow _\mathcal {S}^* \cdot \rightarrow _\mathcal {R}^{} \cdot \rightarrow _\mathcal {S}^*\) is called the relative step of \(\mathcal {R}\) over \(\mathcal {S}\), and denoted by \(\rightarrow _{\mathcal {R}/\mathcal {S}}\). We say that \(\mathcal {R}/\mathcal {S}\) is terminating if \(\rightarrow _{\mathcal {R}/\mathcal {S}}\) is terminating.

Multi-steps. The multi-step of a TRS \(\mathcal {R}\) is inductively defined on terms as follows:

  1. 1.

    for all \(x \in \mathcal {V}\),

  2. 2.

    if for all \(1 \leqslant i \leqslant n\), and

  3. 3.

    if \(\ell \rightarrow r \in \mathcal {R}\) and \(\sigma \) and \(\tau \) are substitutions that for all variables x.

Rewriting Modulo. Let \(\mathcal {R}\) and \(\mathcal {E}\) be TRSs. The rewrite step \(\rightarrow _{\mathcal {R},\mathcal {E}}\) of \(\mathcal {R}\) modulo theory \(\mathcal {E}\) is defined as follows: \(s \rightarrow _{\mathcal {R},\mathcal {E}} t\) if If \(s|_p \leftrightarrow ^*_\mathcal {E}\ell \sigma \) and \(t = s[r\sigma ]_p\) for some position \(p \in \mathcal {P}\mathsf {os}_\mathcal {F}(s)\), rule \(\ell \rightarrow r \in \mathcal {R}\), and substitution \(\sigma \). The relation \(\rightarrow _{\mathcal {R},\mathcal {E}}\) is Church-Rosser modulo \(\mathcal {E}\), denoted by \(\mathsf {CR}(\mathcal {R},\mathcal {E})\), if . Let \(\mathcal {F}_{\mathsf {A}}\), \(\mathcal {F}_{\mathsf {C}}\), and \(\mathcal {F}_{\mathsf {AC}}\) be pairwise disjoint sets of binary function symbols. We define the three theories \({\mathsf {A}}\) (associativity), \({\mathsf {C}}\) (commutativity), and \({\mathsf {AC}}\) as:

$$\begin{aligned} {\mathsf {A}}&= \{ f(f(x,y),z) \rightarrow f(x,f(y,z)),~ f(x,f(y,z)) \rightarrow f(f(x,y),z) \mid f \in \mathcal {F}_{\mathsf {A}}\} \\ {\mathsf {C}}&= \{ f(x,y) \rightarrow f(y,x) \mid f \in \mathcal {F}_{\mathsf {C}}\} \\ {\mathsf {AC}}&= \{ f(f(x,y),z) \rightarrow f(x,f(y,z)),~ f(x,y) \rightarrow f(y,x) \mid f \in \mathcal {F}_{\mathsf {AC}}\} \end{aligned}$$

Critical Pairs. Conditions for confluence are often based on the notion of critical pairs. We denote by \(\mathcal {U}_\mathcal {E}(s \approx t)\) a fixed complete set of \(\mathcal {E}\)-unifiers for terms s and t. Let \(\ell _1 \rightarrow r_1\) be a rule in a TRS \(\mathcal {R}\) and \(\ell _2 \rightarrow r_2\) a variant of a rule in a TRS \(\mathcal {S}\) with \(\mathcal {V}\mathsf {ar}(\ell _1) \cap \mathcal {V}\mathsf {ar}(\ell _2) = \varnothing \). When \(p \in \mathcal {P}\mathsf {os}_\mathcal {F}(\ell _2)\) and \(\sigma \in \mathcal {U}_\mathcal {E}(\ell _1 \approx \ell _2|_p)\), the pair \((\ell _2\sigma [r_1\sigma ]_p, r_2\sigma )\) is called an \(\mathcal {E}\) -extended critical pair (or simply \(\mathcal {E}\) -critical pair) of \(\mathcal {R}\) on \(\mathcal {S}\), and written \(\ell _2\sigma [r_1\sigma ]_p \mathrel {{\mathrel {{_{\mathcal {R},\mathcal {E}}}{\leftarrow }}}{\rtimes }{\rightarrow _{\mathcal {S}}}} r_2\sigma \).

3 Confluence via Church-Rosser Modulo

In this section we explain how the next theorem by Jouannaud and Kirchner [3] is used for confluence analysis. Especially, we discuss how to deal with associativity and/or commutativity rules.

Theorem 1

Let \(\mathcal {R}\) and \(\mathcal {E}\) be TRSs that \(\mathcal {R}/\mathcal {E}\) is terminating and \(\mathrel {{\vartriangleright }}\cdot \leftrightarrow _\mathcal {E}^*\) is well-founded. Then, .   \(\Box \)

We use the next left-linear TRS \(\mathcal {R}_1\) to illustrate problems that arise when employing Theorem 1:

$$\begin{aligned} 1:\mathsf {0} + x&\rightarrow x \qquad 2:x + (y + z) \rightarrow (x + y) + z \qquad 3:(x + y) + z \rightarrow x + (y + z) \end{aligned}$$

Let \(\mathcal {F}_{\mathsf {A}}= \{ {+} \}\). We may assume \({\mathsf {A}}= \{2,3\}\). An idea here is proving \(\mathsf {CR}(\{1\},{\mathsf {A}})\) to conclude confluence of \(\mathcal {R}_1\). The next trivial lemma validates this idea. We call a TRS \(\mathcal {E}\) reversible if holds.

Lemma 2

Suppose \(\mathcal {E}\) is reversible. If \(\mathsf {CR}(\mathcal {R},\mathcal {E})\) then \(\mathcal {R}\cup \mathcal {E}\) is confluent.   \(\Box \)

Reversibility of \({\mathsf {A}}\) and well-foundedness of \(\mathrel {{\vartriangleright }}\cdot \leftrightarrow _{\{2,3\}}^*\) are trivial. Termination of \(\{1\}/{\mathsf {A}}\) can be shown by AC-RPO [4]. Therefore, it remains to test joinability of extended critical pairs to apply Theorem 1.

3.1 Associative Unification

How to compute \({\mathsf {A}}\)-critical pairs? Plotkin [5] introduced a procedure that enumerates a minimal complete set of \({\mathsf {A}}\)-unifiers. It is well-known that a minimal complete set need not to be finite, and thus the procedure may not terminate. In fact there is a one-rule TRS that admits infinitely many \({\mathsf {A}}\)-critical pairs. Probably this is one of main reasons that existing confluence tools do not support Theorem 1 for associativity theory. However, as observed in [6], a minimal complete set resulting from the procedure is finite whenever an input equality is a pair of linear terms that share no variables. Therefore, for every left-linear TRS one can safely use Plotkin’s procedure to compute their \({\mathsf {A}}\)-critical pairs.

We present a simple variant of Plotkin’s procedure [5, 7] specialized for our setting. Let S and T be sets of substitutions. We abbreviate the set \(\{\sigma \tau \mid \sigma \in S ~ and ~ \tau \in T\}\) to ST. Given a term t, we write \(t{\downarrow }_{{\mathsf {A}}'}\) for the normal form of t with respect to \({\mathsf {A}}'\). Here \({\mathsf {A}}'\) stands for the confluent and terminating TRS \(\{ f(f(x, y), z) \rightarrow f(x, f(y, z)) \mid f \in \mathcal {F}_{\mathsf {A}}\}\).

Definition 3

Let s and t be terms. The function \(\langle s \approx t \rangle \) is inductively defined as follows:

$$\begin{aligned} \langle s \approx t \rangle = {\left\{ \begin{array}{ll} \{ \{ s \mapsto t \} \} &{} \textit{if} \ s \in \mathcal {V}\\ \{ \{ t \mapsto s \} \} &{} \textit{if} \ s \notin \mathcal {V}\ \textit{and} \ t \in \mathcal {V}\\ A_1 \cdots A_n \cup A_{s,t} \cup A_{t,s} &{} \textit{if} \ s = f({s_1},\dots ,{s_{n}}) \ \textit{and} \ t = f({t_1},\dots ,{t_{n}})\\ \varnothing &{} \textit{otherwise} \end{array}\right. } \end{aligned}$$

where,

$$\begin{aligned} A_i&= \langle s_i \approx t_i \rangle , \qquad A_{s,t} = {\left\{ \begin{array}{ll} \{ \{ s_1 \mapsto f(t_1, s_1) \} \} \langle s \approx t_2 \rangle &{} \text {if (*)}\\ \varnothing &{} \text {otherwise} \end{array}\right. } \end{aligned}$$

and \((*)\) stands for \(s = f(s_1,s_2)\), \(t = f(t_1,t_2)\), \(f \in \mathcal {F}_{\mathsf {A}}\), and \(s_1 \in \mathcal {V}\).

Theorem 4

Let s and t be linear terms with \(\mathcal {V}\mathsf {ar}(s) \cap \mathcal {V}\mathsf {ar}(t) = \varnothing \). The set \(\langle s{\downarrow }_{{\mathsf {A}}'} \approx t{\downarrow }_{{\mathsf {A}}'} \rangle \) is a finite complete set of their \({\mathsf {A}}\)-unifiers.   \(\Box \)

We illustrate the use of the theorem. Let \(s = \mathsf {0} + x\), \(t = (x' + y') + z'\), and \(\mathcal {F}_{\mathsf {A}}= \{ {+} \}\). A complete set of \({\mathsf {A}}\)-unifiers for the terms is computed as follows:

$$\begin{aligned} \langle s{\downarrow }_{{\mathsf {A}}'} \approx t{\downarrow }_{{\mathsf {A}}'} \rangle&= \langle \mathsf {0} + x \approx x' + (y' + z') \rangle \\&= \bigl (\langle \mathsf {0} \approx x' \rangle \langle x \approx y' + z' \rangle \bigr ) \,\cup \, \bigl (\{ \{ x' \mapsto \mathsf {0}+x' \} \} \langle x'+(y'+z') \approx x \rangle \bigr )\\&= \bigl \{ \{ x' \mapsto \mathsf {0}, x \mapsto y' + z' \},~ \{ x' \mapsto \mathsf {0} + x', x \mapsto x' + (y' + z') \} \bigr \} \end{aligned}$$

This set induces the \({\mathsf {A}}\)-critical pairs:

$$\begin{aligned} y' + z' \quad&{\mathrel {{_{\{1\},{\mathsf {A}}}}{\leftarrow }}}\rtimes {\rightarrow _{\{3\}}}~~ \mathsf {0} + (y' + z')\\ x' + (y' + z') \quad&{\mathrel {{_{\{1\},{\mathsf {A}}}}{\leftarrow }}}\rtimes {\rightarrow _{\{3\}}}~~ (\mathsf {0} + x') + (y' + z') \end{aligned}$$

Both of the right-hand sides reduce to the corresponding left-hand sides by the rewriting modulo step \(\rightarrow _{\{1\},{\mathsf {A}}}\). What about the other critical pairs?

3.2 Coherence

Consider the \({\mathsf {A}}\)-critical pair:

$$\begin{aligned} x + z \quad {\mathrel {{_{\{1\},{\mathsf {A}}}}{\leftarrow }}}{\rtimes }{\rightarrow _{\{2\}}}\,\,\,(x + \mathsf {0}) + z \end{aligned}$$

Contrary to our intention, \((x + \mathsf {0}) + z \rightarrow _{\{1\},{\mathsf {A}}} x + z\) does not hold, and thus \(\mathsf {CR}(\{1\},{\mathsf {A}})\) is refuted by Theorem 1. This undesired incapability of rewriting modulo is known as the coherence problem [3, 8].

Definition 5

A pair \((\mathcal {R},\mathcal {E})\) is strongly coherent if \({\leftrightarrow _\mathcal {E}^* \cdot \rightarrow _{\mathcal {R},\mathcal {E}}} \subseteq {\rightarrow _{\mathcal {R},\mathcal {E}} \cdot \leftrightarrow _\mathcal {E}^*}\).

Lemma 6

Suppose \(\mathcal {E}\) is reversible and \((\mathcal {R},\mathcal {E})\) is strongly coherent. If \(\mathsf {CR}(\mathcal {R},\mathcal {E})\) then \(\mathcal {R}\cup \mathcal {E}\) is confluent, and vice versa.   \(\Box \)

While the strong coherence property always holds for rewriting modulo \({\mathsf {C}}\), rewriting modulo \({\mathsf {A}}\) and \({\mathsf {AC}}\) rarely satisfy the property. This can be overcome by extending a rewrite system. Since an extension for \({\mathsf {AC}}\) is known [3, 8], here we consider an \({\mathsf {A}}\)-extension of a TRS.

Definition 7

Let \(\mathcal {R}\) be a TRS. The \({\mathsf {A}}\) -extended TRS \(\mathsf {Ext}_{\mathsf {A}}(\mathcal {R})\) consists of

$$\begin{aligned} \ell&\rightarrow r \qquad f(\ell ,x) \rightarrow f(r,x)&f(x,f(\ell ,y)) \rightarrow f(x,f(r,y)) \\&\quad \qquad \quad f(x,\ell ) \rightarrow f(x,r) \end{aligned}$$

for all rules \(\ell \rightarrow r \in \mathcal {R}\) with \(f = \mathrm {root}(\ell ) \in \mathcal {F}_A\). Here x and y are fresh variables not in \(\ell \).

Lemma 8

The pair \((\mathsf {Ext}_{\mathsf {A}}(\mathcal {R}), {\mathsf {A}})\) is strongly coherent and \({\rightarrow _{\mathsf {Ext}_{\mathsf {A}}(\mathcal {R})}} = {\rightarrow _\mathcal {R}}\).

Proof

From the inclusion \({\rightarrow _{\mathsf {A}}\cdot \rightarrow _{\mathsf {Ext}_{\mathsf {A}}(\mathcal {R}),{\mathsf {A}}}} \subseteq {\rightarrow _{\mathsf {Ext}_{\mathsf {A}}(\mathcal {R}),{\mathsf {A}}} \cdot \rightarrow _{\mathsf {A}}^*}\) the first claim follows. Since \(\rightarrow _\mathcal {R}\) is closed under contexts, the second claim is trivial.   \(\Box \)

The TRS \(\mathsf {Ext}_{\mathsf {A}}(\{1\})\) consists of the four rules:

$$\begin{aligned} \mathsf {0} + x&\rightarrow x&w + (\mathsf {0} + x)&\rightarrow w + x \\ (\mathsf {0} + x) + y&\rightarrow x + y&w + ((\mathsf {0} + x) + y)&\rightarrow w + (x + y) \end{aligned}$$

As the extended TRS contains all original rules, we have again the previous \({\mathsf {A}}\)-critical pair:

$$\begin{aligned} x + z \quad {\mathrel {{_{\{1\},{\mathsf {A}}}}{\leftarrow }}}{\rtimes }{\rightarrow _{\{2\}}}\,\,\, (x + \mathsf {0}) + z \end{aligned}$$

Since \((x + \mathsf {0}) + z \rightarrow _{\mathsf {Ext}_{\mathsf {A}}(\{1\}),{\mathsf {A}}} x + z\) holds, the pair is joinable. Similarly, one can verify that all other \({\mathsf {A}}\)-critical pairs are joinable. Therefore, \(\mathsf {CR}(\mathsf {Ext}_{\mathsf {A}}(\{1\}),{\mathsf {A}})\) is concluded by Theorem 1. Finally, confluence of \(\mathcal {R}_1\) is established.

3.3 Commutative Unification

Commutative unification also benefits from left-linearity. We define \(\mathcal {U}_\mathcal {E}^{\mathsf {C}}(s \approx t)\) as .

Lemma 9

Suppose \({\mathsf {C}}\) and \(\mathcal {E}\cup \mathcal {E}^{-1}\) commute. If \(\mathcal {V}\mathsf {ar}(s) \cap \mathcal {V}\mathsf {ar}(t) = \varnothing \) and s is linear then \(\mathcal {U}_\mathcal {E}^{\mathsf {C}}(s \approx t)\) is a complete set of \({\mathsf {C}}\cup \mathcal {E}\)-unifiers for s and t.

Proof

Since it is trivial that \(\mathcal {U}_\mathcal {E}^{\mathsf {C}}(s \approx t)\) consists of \(\mathcal {E}\cup {\mathsf {C}}\)-unifiers, we only show completeness of the set. Let \(s\sigma \leftrightarrow _{{\mathsf {C}}\cup \mathcal {E}}^* t\sigma \). One can show by using induction, commutation, and the reversibility of \({\mathsf {C}}\). Thus, for some u. Since holds, . Due to the linearity of s there are \(s'\) and \(\sigma '\) such that \(u = s'\sigma '\), , and for all variables x. We define the substitution \(\mu \) as follows:

$$\begin{aligned} \mu = \{ x \mapsto x\sigma \mid x \in \mathcal {V}\mathsf {ar}(s) \} \cup \{ x \mapsto x\sigma ' \mid x \in \mathcal {V}\mathsf {ar}(t) \} \end{aligned}$$

Since s and t share no variables, \(\mu \) is well-defined. By the definition we obtain \(s'\mu \leftrightarrow _\mathcal {E}^* t\mu \).   \(\Box \)

Since \({\mathsf {A}}\) and \({\mathsf {C}}\) are left-linear TRSs that share no function symbols, their commutation can be proved (by using e.g. Theorem 11 in the next section). So Lemma 9 gives a way to compute \({\mathsf {A}}\cup {\mathsf {C}}\)-critical pairs.

Example 10

Consider the left-linear TRS \(\mathcal {R}_2\) with \(\mathcal {F}_{\mathsf {A}}= \{ {*} \}\) and \(\mathcal {F}_{\mathsf {C}}= \{ \mathsf {eq} \}\):

$$\begin{aligned} \begin{array}{l@{\qquad }l@{\quad }l} 1:\mathsf {eq}(\mathsf {a}, \mathsf {a}) \rightarrow \mathsf {T} &{} 3:\mathsf {eq}(\mathsf {a} * x, y * \mathsf {a}) \rightarrow \mathsf {eq}(x, y) &{} 5:(x * y) * z \rightarrow x * (y * z)\\ 2:\mathsf {eq}(\mathsf {a}, x * y) \rightarrow \mathsf {F} &{} 4:\mathsf {eq}(x, y) \rightarrow \mathsf {eq}(y,x) &{} 6:x * (y * z) \rightarrow (x * y) * z \end{array}\end{aligned}$$

Let \(\mathcal {R}= \{1,2,3\}\) and \(\mathcal {E}= \{4,5,6\}\). Note that \(\mathcal {E}= {\mathsf {C}}\cup {\mathsf {A}}\). It is sufficient to show \(\mathsf {CR}(\mathsf {Ext}_{\mathsf {A}}(\mathcal {R}), \mathcal {E})\). We can use AC-RPO to prove termination of \(\mathcal {R}/\mathcal {E}\), which is equivalent to that of \(\mathsf {Ext}_{\mathsf {A}}(\mathcal {R})/\mathcal {E}\) due to the identity in Lemma 6. Let \(s = \mathsf {eq}(\mathsf {a} * x, y * \mathsf {a})\) and \(t = \mathsf {eq}(\mathsf {a} * x', y' * \mathsf {a})\). A complete set of their \({\mathsf {A}}\cup {\mathsf {C}}\)-unifiers is:

$$\begin{aligned} \mathcal {U}_{\mathsf {A}}^{\mathsf {C}}(s \approx t)&= \langle s \approx t \rangle \cup \langle \mathsf {eq}(y * \mathsf {a}, \mathsf {a} * x) \approx \mathsf {eq}(\mathsf {a} * x', y' * \mathsf {a}) \rangle \\&= \left\{ \begin{array}{llll} \{ x \mapsto x',~ &{} y \mapsto y' \}, \\ \{ x \mapsto \mathsf {a},~ &{} y \mapsto \mathsf {a},~ &{} x' \mapsto \mathsf {a},~ &{} y' \mapsto \mathsf {a} \} \\ \{ x \mapsto y' * \mathsf {a},~ &{} y \mapsto \mathsf {a} * y,~ &{} x' \mapsto y * \mathsf {a},~ &{} y' \mapsto \mathsf {a} * y' \} \\ \end{array} \right\} \end{aligned}$$

In this way we can compute complete sets to induce the set of all \(\mathcal {E}\)-critical pairs. Since all pairs are joinable, \(\mathsf {CR}(\mathcal {R},\mathcal {E})\) is concluded.

4 Commutation

4.1 Commutation Criteria

Our tool employs three commutation criteria. The first commutation criterion is the development closedness theorem [9–12].

Theorem 11

(Development Closedness). Left-linear TRSs \(\mathcal {R}\) and \(\mathcal {S}\) commute if the inclusions and hold.   \(\Box \)

The second criterion is the commutation version of the confluence criterion based on rule labeling with weight function [13, 14].

Definition 12

A weight function w is a function from \(\mathcal {F}\) to \(\mathbb {N}\). The weight w(C) of a context C is defined as follows:

$$\begin{aligned} w(C) = {\left\{ \begin{array}{ll} 0 &{} \text {if} \ C = \Box \\ w(f) + w(C') &{} \text {if} \ C = f(t_1,\ldots ,C',\ldots ,t_n) \ \textit{with a context} \ C' \\ \end{array}\right. } \end{aligned}$$

The weight is admissible for a TRS \(\mathcal {R}\) if

$$\begin{aligned} \{ w(C) \mid C[x] = \ell \} \geqslant ^{\mathrm {mul}}\{ w(C) \mid C[x] = r \} \end{aligned}$$

holds for all \(\ell \rightarrow r \in \mathcal {R}\) and \(x \in \mathcal {V}\mathsf {ar}(r)\). Here \(\geqslant ^{\mathrm {mul}}\) stands for the multiset extension of the standard order \(>\) on \(\mathbb {N}\) (see e.g. [2]). A rule labeling \(\phi \) for a TRS \(\mathcal {R}\) is a function from \(\mathcal {R}\) to \(\mathbb {N}\). The labeled step \(\xrightarrow {\alpha }_\mathcal {R}\) is defined as follows: \(s \rightarrow _{\mathcal {R},(k,m)} t\) if there are a rule \(\ell \rightarrow r\), a context C, and a substitution \(\sigma \) such that \(s = C[\ell \sigma ]\), \(t = C[r\sigma ]\), and \(\alpha = (w(C), \phi (\ell \rightarrow r))\).

In the next theorem we use the following abbreviations for labeled steps:

$$\begin{aligned} {\xrightarrow {I}} = \bigcup _{\alpha \in I} {\xrightarrow {\alpha }} \qquad \curlyvee \!\!\alpha = \{\beta \in I \mid \alpha \succ \beta \} \qquad \curlyvee \!\!\alpha \beta = (\curlyvee \alpha ) \cup (\curlyvee \beta ) \end{aligned}$$

where, \(\succ \) stands for the lexicographic order on \(\mathbb {N}\times \mathbb {N}\).

Theorem 13

(Rule Labeling). Left-linear TRSs \(\mathcal {R}\) and \(\mathcal {S}\) commute if there are an admissible weight function w and a rule labeling \(\phi \) for \(\mathcal {R}\cup \mathcal {S}\) such that

for all pairs \(\alpha , \beta \in \mathbb {N}\times \mathbb {N}\).   \(\Box \)

The final criterion is a trivial adaptation of Theorem 1 to the commutation property, integrating Lemmata 6, 8, and 9.

Theorem 14

(Church-Rosser Modulo). Let \(\mathcal {R},\mathcal {S}\) be left-linear TRSs and \(\mathcal {E}\in \{ {\mathsf {A}}, {\mathsf {AC}}\}\) such that \(\mathcal {R}/\mathcal {E}'\) is terminating for \(\mathcal {E}' = \mathcal {E}\cup {\mathsf {C}}\). The TRSs \(\mathcal {R}\cup \mathcal {E}'\) and \(\mathcal {S}\cup \mathcal {E}'\) commute if and only if the inclusion holds:

Here \(\mathcal {R}' = \mathsf {Ext}_\mathcal {E}(\mathcal {R})\) and \(\mathcal {S}' = \mathsf {Ext}_\mathcal {E}(\mathcal {S})\).   \(\Box \)

Note that our tool uses the algorithm in [15] for AC unification and flattened term representation for overcoming the coherence problem of AC-rewriting. Since we use the dedicated algorithms for A and AC unification, currently we cannot employ Theorem 1 with \(\mathcal {E}= {\mathsf {A}}\cup {\mathsf {AC}}\).

4.2 Commutation Theorem

The next theorem is known as Hindley’s Commutation Theorem [1].

Theorem 15

(Commutation Theorem). If \(\xrightarrow {\alpha }\) and \(\xrightarrow {\beta }\) commute for all \(\alpha \in I\) and \(\beta \in J\) then \(\xrightarrow {I}\) and \(\xrightarrow {J}\) commute.   \(\Box \)

Example 16

Consider the left-linear TRS \(\mathcal {R}_3\):

By using the Commutation Theorem we show self-commutation of \(\mathcal {R}_3\):

  1. (i)

    Self-commutation of \(\{1,\ldots ,8\}\) follows from Theorem 14.

  2. (ii)

    Commutation of \(\{ 1,\ldots ,8 \}\) and \(\{ 9 \}\) follows from Theorem 11.

  3. (iii)

    Self-commutation of \(\{ 9 \}\) is proved by Theorem 11.

Hence, \(\mathcal {R}_3\) is confluent.

It is a non-trivial task to find suitable commuting subsystems from an exponential number of candidates. In order to address the problem we introduce a decomposition method based on composability, which was introduced by Ohlebusch [16]. Let \(\mathcal {R}\) be a TRS. We write \(\mathcal {F}_\mathcal {R}\), \({\mathcal {D}}_\mathcal {R}\), and \(\mathcal {C}_\mathcal {R}\) for the following sets:

$$\begin{aligned} \mathcal {F}_\mathcal {R}= \bigcup _{\ell \rightarrow r \in \mathcal {R}} \mathcal {F}\mathsf {un}(\ell ) \cup \mathcal {F}\mathsf {un}(r) \qquad {\mathcal {D}}_\mathcal {R}= \{ \mathrm {root}(\ell ) \mid \ell \rightarrow r \in \mathcal {R}\} \qquad \mathcal {C}_\mathcal {R}= \mathcal {F}_\mathcal {R}\setminus {\mathcal {D}}_\mathcal {R}\end{aligned}$$

Definition 17

We say that TRSs \(\mathcal {R}\) and \(\mathcal {S}\) are composable if \(\mathcal {C}_\mathcal {R}\cap {\mathcal {D}}_\mathcal {S}= \mathcal {C}_\mathcal {S}\cap {\mathcal {D}}_\mathcal {R}= \varnothing \) and \(\{ \ell \rightarrow r \in \mathcal {R}\cup \mathcal {S}\mid \mathrm {root}(\ell ) \in {\mathcal {D}}_\mathcal {R}\cup {\mathcal {D}}_\mathcal {S}\} \subseteq \mathcal {R}\cap \mathcal {S}\).

Ohlebusch [16] posed the following question.

Question 18

Are left-linear composable TRSs \(\mathcal {R}\) and \(\mathcal {S}\) confluent if and only if \(\mathcal {R}\cup \mathcal {S}\) is confluent?

Although the question still remains open, the following variation is valid.

Theorem 19

Commuting composable TRSs \(\mathcal {R}\) and \(\mathcal {S}\) are confluent if and only if \(\mathcal {R}\cup \mathcal {S}\) is confluent.   \(\Box \)

Example 20

Recall the TRS \(\mathcal {R}_3\) from Example 16. The TRS is the union of the three commuting composable subsystems: \(\{ 1,2,5,6,7,8 \}\), \(\{ 3,4,5,6,7,8 \}\), and \(\{ 9 \}\). Confluence of each subsystem can be proved in the same method used in the previous example. Hence, \(\mathcal {R}_3\) is confluent.

5 Implementation

The confluence tool CoLL consists of about 5,000 lines of OCaml code. Given an input TRS, the tool first performs the next trivial redundant rule elimination.

Theorem 21

Let \(\mathcal {R}\) and \(\mathcal {S}\) be TRSs with \(\mathcal {S}\subseteq {\rightarrow _\mathcal {R}^*}\). The TRS \(\mathcal {R}\cup \mathcal {S}\) is confluent if and only if \(\mathcal {R}\) is confluent.   \(\Box \)

Example 22

We illustrate the elimination technique with a small example taken from the Confluence Problem Database (Cops)Footnote 1. Consider the TRS:

$$\begin{aligned} 1:\mathsf {f}(x) \rightarrow \mathsf {g}(x,\mathsf {f}(x)) \qquad 2:\mathsf {f}(\mathsf {f}(\mathsf {f}(\mathsf {f}(x)))) \rightarrow \mathsf {f}(\mathsf {f}(\mathsf {f}(\mathsf {g}(x,\mathsf {f}(x))))) \end{aligned}$$

Since \(\{2\} \subseteq {\rightarrow _{\{1\}}^*}\) holds, we eliminate the redundant rule 2. Confluence of the simplified system \(\{1\}\) is easily shown by Theorem 11. Note that CoLL cannot prove confluence without using the elimination technique.

Next, the tool employs Theorem 19 to split the simplified TRS into commuting composable subsystems \(\mathcal {R}_1,\ldots ,\mathcal {R}_n\). For each subsystem \(\mathcal {R}_i\) the tool performs the non-confluence test of [17, Lemma 1]. If non-confluence is detected, the tool outputs NO (non-confluence is proved). Otherwise, the tool uses the Commutation Theorem together with the three commutation criteria (Theorems 11, 13, and 14) to determine self-commutation of \(\mathcal {R}_i\). Suitable commuting subsystems are searched by enumeration. It outputs YES (confluence is proved) if all of \(\mathcal {R}_1,\ldots ,\mathcal {R}_n\) are confluent. Concerning automation, we employed AC-RPO for checking termination of \(\mathcal {R}/\mathcal {E}\) automatically. Automation of Theorem 13 is based on the SAT encoding technique of [18].

We tested the presented techniques on 188 left-linear TRSs in Cops Nos. 1–425, where we ruled out duplicated problems.Footnote 2 The tests were run on a PC equipped with an Intel Core i7-4500U CPU with 1.8 GHz and 3.8 GB of RAM using a timeout of 120 sec. For the sake of comparison we also ran the tools that participated in the 3rd Confluence Competition: ACP  v0.5 [9], CSI  v0.4.1 [17], and Saigawa  v1.7Footnote 3. The first table in Fig. 1 summarizes the results. The first three indicate the results of each commutation criterion without using the Commutation Theorem. The second table indicates the results of individual theories for Theorem 14. The row ‘all three’ in the first table is the summation of their results, and ‘all with elimination’ is the same but the elimination technique is enabled. The row CoLL corresponds to the strategy stated above. On our problem set, all confluence proofs by Saigawa are covered by CoLL. The results of CoLL, ACP, and CSI are incomparable.

Fig. 1.
figure 1

Experimental results.

Full size image

6 Conclusion

We presented the new confluence tool CoLL for left-linear TRSs, which proves confluence via commutation. Our primary contribution is automation of Jouannaud and Kirchner’s Church-Rosser modulo criterion for associativity and/or commutativity theory, where left-linearity is exploited in several ways.

We briefly compare CoLL with existing confluence tools. CRC 3 [19] is a powerful Church-Rosser checker for Maude and supports the Church-Rosser modulo theorem for any combination of associativity, commutativity, and/or identity theories, except associativity theory. When handling TRSs that contain reversible rules, ACP  [9] employs reduction-preserving completion [20]. This method effectively works for C and AC rules, but not for associativity rules. ACP and CSI  [17] employ layer-preserving decomposition [16] to split a TRS into subsystems. The technique is incomparable to Theorem 19. If Question 18 is affirmatively solved, it generalizes the two techniques for the class of left-linear TRSs. Finally, CoLL was designed for a complement of Saigawa. The two tools will be merged in the next version.

As future work we plan to investigate whether Theorem 19 can be generalized to cover a subclass of hierarchical combination [16]. Another interesting direction is the modularity of the commutation property. Since confluence is a modular property [21], it is closed under signature extension. Contrary to our expectation, (even local) commutation is not signature extensible. Consider the TRSs \(\mathcal {R}\) and \(\mathcal {S}\) over the signature \(\mathcal {F}= \{ \mathsf {f}^{(2)}, \mathsf {a}^{(0)}, \mathsf {b}^{(0)} \}\):

$$\begin{aligned} \mathcal {R}= \{\, \mathsf {a} \rightarrow \mathsf {b} \,\} \qquad \mathcal {S}&= \left\{ \begin{array}{l@{~~}l@{~~}l} \mathsf {f}(x,x) \rightarrow \mathsf {b}, &{} \mathsf {f}(\mathsf {a},x) \rightarrow \mathsf {b}, &{} \mathsf {f}(x,\mathsf {a}) \rightarrow \mathsf {b} \\ &{} \mathsf {f}(\mathsf {b},x) \rightarrow \mathsf {b}, &{} \mathsf {f}(x,\mathsf {b}) \rightarrow \mathsf {b} \end{array} \right\} \end{aligned}$$

Since \(C[t] \rightarrow _\mathcal {S}^* \mathsf {b}\) holds for all contexts C and \(t \in \{\mathsf {a},\mathsf {b}\}\), we obtain the strong commutation , which entails commutation of \(\mathcal {R}\) and \(\mathcal {S}\). However, if one extends the signature to \(\mathcal {F}\cup \{\mathsf {g}^{(1)}\}\), the local peak \(\mathsf {f}(\mathsf {g}(\mathsf {b}),\mathsf {g}(\mathsf {a})) \mathrel {{_{\mathcal {R}}}{\leftarrow }} \mathsf {f}(\mathsf {g}(\mathsf {a}),\mathsf {g}(\mathsf {a})) \rightarrow _\mathcal {S}\mathsf {b}\) no longer commutes. We conjecture that (local) commutation is closed under signature extension for left-linear TRSs.