1 Introduction

CSI  [44] is an automatic confluence prover for rewrite systems, which participates in the annual confluence competition (CoCo) [1].

In this paper we report on recent additions to CSI, in particular support for higher-order rewrite systems, efficient decision procedures for the unique normal form properties for ground rewrite systems, support for first-order systems with associative and commutative symbols, and more refined non-confluence techniques. Several techniques have been formalized to enable certification of the output of CSI, making it the most trustworthy confluence tool.

We assume familiarity with rewriting [7]. Here we only recall notions that will be used in Sect. 2. We consider terms built from a signature \(\mathcal {F}\) and a disjoint set of variables \(\mathcal {V}\). Given a subset \(\mathcal {F}_\mathsf {AC}\subseteq \mathcal {F}\) of binary function symbols, the term rewrite system (TRS for short) \(\mathsf {AC}\) consists of the AC rules \(f(x,y) \rightarrow f(y,x)\) and \(f(f(x,y),z) \rightarrow f(x,f(y,z))\) for every \(f \in \mathcal {F}_\mathsf {AC}\). We write \(\sim _\mathsf {AC}\) for the congruence induced by \(\mathsf {AC}\). Given a TRS \(\mathcal {R}\) over the signature \(\mathcal {F}\), we write \(\mathcal {R}^e\) for the union of \(\mathcal {R}\) and the extended rules \(f(\ell ,x) \rightarrow f(r,x)\) for all \(\ell \rightarrow r \in \mathcal {R}\) such that \(\mathsf {root}(\ell ) = f \in \mathcal {F}_\mathsf {AC}\). We write \(\rightarrow _{\mathcal {R}/\mathsf {AC}}\) for the relation \(\sim _\mathsf {AC}\cdot \rightarrow _\mathcal {R}\cdot \sim _\mathsf {AC}\). The relation \(\rightarrow _{\mathcal {R},\mathsf {AC}}\) is defined as follows: \(s \rightarrow _{\mathcal {R},\mathsf {AC}} t\) if there exists a position p in s, a rewrite rule \(\ell \rightarrow r\) in \(\mathcal {R}\), and a substitution \(\sigma \) such that \(s|p \sim _\mathsf {AC}\ell \sigma \) and \(t = s[r\sigma ]_p\). The relations \(\rightarrow _{\mathcal {R}/\mathsf {AC}}\) and \(\rightarrow _{\mathcal {R}^e,\mathsf {AC}} \cdot \sim _\mathsf {AC}\) coincide.

Consider two rewrite rules \(\ell _1 \rightarrow r_1\) and \(\ell _2 \rightarrow r_2\) without common variables and a function position p in \(\ell _2\) such that \(\ell _l\) and \(\ell _2|_p\) are unifiable modulo AC. Given a complete set S of AC unifiers of \(\ell _l\) and \(\ell _2|_p\), the pair \(\ell _2[r_1]_p\sigma \approx r_2\sigma \) with \(\sigma \in S\) is called an AC critical pair. The set of all AC critical pairs between rules of a TRS \(\mathcal {R}\) and a TRS \(\mathcal {S}\) is denoted by \(\mathsf {CP}_\mathsf {AC}(\mathcal {R},\mathcal {S})\).

The remainder of the paper is organized as follows. In the next section we report on the main extensions to CSI for (non-)confluence proving of TRSs. Section 3 is devoted to the support of CSI for the unique normal form properties. The extension to higher-order systems is covered in Sect. 4. An overview of the certified techniques in CSI is presented in Sect. 5. Some implementation details are given in Sect. 6 before we conclude in Sect. 7 with experimental data.

2 Extensions

In this section we describe the two features for (non-)confluence proving of TRSs that were added to CSI after CoCo 2016. Other extensions are briefly described in the one-page tool descriptions accompanying CoCo.Footnote 1

TRSs that contain AC rules pose a challenge for confluence provers. The confluence problems database (Cops)Footnote 2 contains several such systems whose status is open. Aoto and Toyama [2] developed a special confluence technique for rewrite systems with AC rules and more general non-terminating rewrite systems, which is incorporated in the confluence prover ACP  [5]. A key idea in [2] is that AC rules are reversible. This idea was combined with the extended critical pair lemma of Jouannaud and Kirchner [13] in Saigawa  [15] and more recently in CoLL  [38], where the technique is extended to handle associative rules in the absence of commutation rules.

Theorem 1

(Jouannaud and Kirchner [13], Shintani and Hirokawa [38]). If for all \(s \approx t \in \mathsf {CP}_\mathsf {AC}(\mathcal {S},\mathcal {S}\cup \mathsf {AC}\cup \mathsf {AC}^{-1})\) and \(\mathcal {S}/\mathsf {AC}\) is terminating then \(\mathcal {R}\) is confluent.

In CSI we incorporated the version of the AC critical pair lemma based on extended rules [32], which is used in the modern completion tool mkbtt.Footnote 3

Theorem 2

If \(\mathcal {R}= \mathcal {S}\uplus \mathsf {AC}\) such that for all \(s \approx t \in \mathsf {CP}_\mathsf {AC}(\mathcal {S}^e,\mathcal {S}^e)\) and \(\mathcal {S}/\mathsf {AC}\) is terminating then \(\mathcal {R}\) is confluent.

We illustrate the use of Theorem 2 on two examples.

Example 3

The rewrite system (Cops 183)

$$\begin{aligned} +(\mathsf {0},x)&\rightarrow x&+(x,\mathsf {0})&\rightarrow x&-(+(x,y))&\rightarrow +(-(x),-(y)) \\ +(\mathsf {1},-(\mathsf {1}))&\rightarrow \mathsf {0}&+(-(\mathsf {1}),\mathsf {1})&\rightarrow \mathsf {0}&+(x,y)&\rightarrow +(y,x) \\ -(\mathsf {0})&\rightarrow \mathsf {0}&-(-(x))&\rightarrow x&+(+(x,y),z)&\rightarrow +(x,+(y,z)) \end{aligned}$$

cannot be handled by the recent ground confluence prover AGCP  [3, Example 25]. After removing the AC rules \(+(+(x,y),z) \rightarrow +(x,+(y,z))\) and \(+(x,y) \rightarrow +(y,x)\) we obtain a rewrite system \(\mathcal {S}\) such that the 18 AC critical pairs of \(\mathcal {S}^e\) are joinable modulo ACFootnote 4 (arising from 27 AC critical peaks). Since \(\mathcal {S}\) is easily shown to be AC terminating (e.g. ACRPO [36] applies), we conclude by Theorem 2 that the original rewrite system is confluent. In particular, it is ground confluent, answering the open problem in [3].

Interestingly, the CoCo 2015 version of CoLL-Saigawa, using Theorem 1, could already show confluence of the TRS of Example 3. In light of the next example, it remains to be seen whether this answer can be trusted.

Example 4

Consider the rewrite system

$$\begin{aligned} \mathsf {a} + \mathsf {b}&\rightarrow \mathsf {b}&\mathsf {c} + \mathsf {a}&\rightarrow \mathsf {a}&x + y&\rightarrow y + x&(x + y) + z&\rightarrow x + (y + z) \end{aligned}$$

consisting of \(\mathcal {S}= \{ \mathsf {a} + \mathsf {b} \rightarrow \mathsf {b}, \mathsf {c} + \mathsf {a} \rightarrow \mathsf {a} \}\) and the AC rules for \(+\). The two extended rules

$$\begin{aligned} (\mathsf {a} + \mathsf {b}) + z&\rightarrow \mathsf {b} + z&(\mathsf {c} + \mathsf {a}) + z&\rightarrow \mathsf {a} + z \end{aligned}$$

admit the AC critical peak

$$\begin{aligned} \mathsf {c} + \mathsf {b} \leftarrow (\mathsf {c} + \mathsf {a}) + \mathsf {b} \rightarrow \mathsf {a} + \mathsf {b} \end{aligned}$$

where \(\mathsf {c} + \mathsf {b}\) is in normal form and \(\mathsf {a} + \mathsf {b}\) rewrites in one step to the normal form \(\mathsf {b}\). These normal forms are obviously not AC equivalent. Hence Theorem 2 does not apply and CSI correctly reports that the system is not confluent. Surprisingly, CoLL-Saigawa wrongly reports the opposite. The reason could be that the peak

$$ \mathsf {b} + z \mathrel {{ {\rightarrow }_{\mathcal {S}}}{\leftarrow }} (\mathsf {a} + \mathsf {b}) + z \rightarrow _{\mathsf {AC}} \mathsf {a} + (\mathsf {b} + z) $$

is joinable modulo AC (as \(\mathsf {a} + (\mathsf {b} + z) \rightarrow _{\mathcal {S}/\mathsf {AC}} \mathsf {b} + z\)) but \(\mathsf {a} + (\mathsf {b} + z)\) is a normal form with respect to \(\rightarrow _{\mathcal {S},\mathsf {AC}}\) and hence Theorem 1 does not apply.

The second extension we describe is a non-confluence technique, or more precisely, a technique for finding non-joinable conversions. Let us first consider an example.

Example 5

Consider the TRS \(\mathcal {R}\) due to Klop [16] consisting of the three rules

figure a

Because of the rewrite sequence \(\mathsf {c} \rightarrow \mathsf {g}(\mathsf {c}) \rightarrow \mathsf {f}(\mathsf {c},\mathsf {g}(\mathsf {c})) \rightarrow \mathsf {f}(\mathsf {g}(\mathsf {c}),\mathsf {g}(\mathsf {c})) \rightarrow \mathsf {a}\) we also have \(\mathsf {c} \rightarrow \mathsf {g}(\mathsf {c}) \rightarrow ^* \mathsf {g}(\mathsf {a})\) and since \(\mathsf {a}\) and \(\mathsf {g}(\mathsf {a})\) are not joinable,Footnote 5 \(\mathcal {R}\) is not confluent.

However, finding the above conversion is non-trivial and indeed none of the participants of CoCo 2016 can show non-confluence of this system. The technique of redundant rules [22] can be used to strengthen other criteria in such situations. The basic idea is to add or remove rules that can be simulated by the other rules, thus reflecting (non-)confluence. A systematic method for finding redundant rules is presented below.

Definition 6

Given two variable disjoint rewrite rules \(\ell _1 \rightarrow r_1\) and \(\ell _2 \rightarrow r_2\) of a TRS \(\mathcal {R}\), a function position p in \(r_1\), and an mgu \(\sigma \) of \(r_1|_p\) and \(\ell _2\), the rewrite rule \(\ell _1\sigma \rightarrow r_1\sigma [r_2\sigma ]_p\) is a forward closure of \(\mathcal {R}\). We write \(\mathsf {FC}(\mathcal {R})\) for the extension of \(\mathcal {R}\) with all its forward closures.

Since the rules in \(\mathsf {FC}(\mathcal {R}) \setminus \mathcal {R}\) are redundant (as they can be simulated using the rules of the original TRS \(\mathcal {R}\)), the following result is obvious.

Lemma 7

A TRS \(\mathcal {R}\) is confluent if and only if the TRS  \(\mathsf {FC}(\mathcal {R}) \cup \mathsf {FC}(\mathcal {R}^{-1})^{-1}\) is confluent    \(\square \)

The reason for including \(\mathsf {FC}(\mathcal {R}^{-1})^{-1}\) will become clear in the next section. Returning to Example 5 we find

and hence we obtain the non-joinable critical pair \(\mathsf {a} \approx \mathsf {g}(\mathsf {a}) \in \mathsf {CP}(\mathsf {FC}^4(\mathcal {R}))\). By Lemma 7 this implies non-confluence of \(\mathcal {R}\).

3 Unique Normal Forms

In addition to confluence, CSI includes preliminary support for two unique normal form properties, namely \(\mathsf {UNC}\) (any two convertible normal forms are equal; two terms s and t are convertible if \(s \leftrightarrow ^*t\)) and \(\mathsf {UNR}\) (any term reaches at most one normal form). Note that in contrast to CSI \(\mathbf {\hat{~}}\) ho (described in the next section), which has to deal with a whole new rewriting mechanism, adding support for \(\mathsf {UNR}\) and \(\mathsf {UNC}\) is similar to adding a new confluence criterion, which is why there is no separate CSI \(\mathbf {\hat{~}}\) un tool. Furthermore, the implications

$$\begin{aligned} \mathsf {CR} \implies \mathsf {UNC} \implies \mathsf {UNR} \end{aligned}$$
(1)

mean that any confluence criterion can also serve as a criterion for \(\mathsf {UNC}\) and \(\mathsf {UNR}\), which is another reason for using a confluence tool as the basis of a tool for unique normal forms. (The reverse implications do not hold, as witnessed by the well-known TRSs \(\mathcal {R}_1 = \{ \mathsf {b} \rightarrow \mathsf {a}, \mathsf {b} \rightarrow \mathsf {c}, \mathsf {c} \rightarrow \mathsf {c} \}\) and \(\mathcal {R}_2 = \mathcal {R}_1 \cup \{ \mathsf {d} \rightarrow \mathsf {c}, \mathsf {d} \rightarrow \mathsf {e} \}\). The first one is \(\mathsf {UNC}\) but not \(\mathsf {CR}\) because \(\mathsf {a}\) and \(\mathsf {c}\) do not have a common reduct; the second one is \(\mathsf {UNR}\) but not \(\mathsf {UNC}\) because the normal forms \(\mathsf {a}\) and \(\mathsf {e}\) are convertible.)

CSI incorporates efficient decision procedures for both \(\mathsf {UNC}\) and \(\mathsf {UNR}\) for ground term rewrite systems, which are TRSs without variables. The former property can be decided in \(O(n \log n)\) time, where n is the size of the input TRS, based on currying, the congruence closure algorithm by Nelson and Oppen [26], and an ad hoc enumeration of runs of a tree automaton that accepts convertible normal forms. The latter property is decided in \(O(n^3)\) time, using currying and ground tree transducers that accept normal forms which are related by a peak. For details of these two algorithms, see [9]. Furthermore, CSI implements the following criterion for \(\mathsf {UNC}\) for non-ground systems.

Theorem 8

(Kahrs and Smith [14]). Every non-\(\omega \)-overlapping TRS has unique normal forms with respect to conversions \((\mathsf {UNC})\).

A TRS is \(\omega \) -overlapping if it has overlaps that may be infinite terms. In order to check for \(\omega \)-overlaps, CSI implements a unification algorithm without occurs-check.

Example 9

The TRS consisting of the rules

figure b

of [12] is not \(\mathsf {UNR}\) because \(\mathsf {a} \leftarrow \mathsf {f}(\mathsf {c},\mathsf {c}) \rightarrow \mathsf {f}(\mathsf {c}, \mathsf {g}(\mathsf {c})) \rightarrow \mathsf {b}\) is a peak connecting two distinct normal forms. This TRS is non-overlapping but \(\omega \)-overlapping because \(\mathsf {f}(\mathsf {g}^\omega , \mathsf {g}^\omega )\) is an instance of both \(\mathsf {f}(x,x)\) and \(\mathsf {f}(y,\mathsf {g}(y))\) by substituting \(\{ x \mapsto \mathsf {g}^\omega , y \mapsto \mathsf {g}^\omega \}\). The TRS from Example 5 on the other hand is non-\(\omega \)-overlapping and hence \(\mathsf {UNC}\) by Theorem 8.

Finally, there is a simple check for non-\(\mathsf {UNR}\), where CSI attempts to find two distinct normal forms reachable from the same term by starting from critical peaks and overlaps at variables. Including variable overlaps enables CSI to find the peak in Example 9. Note that Lemma 7 also holds for \(\mathsf {UNR}\). This enables an alternative approach to finding a suitable peak for Example 9: There is an overlap between \(\mathsf {f}(\mathsf {c},\mathsf {c}) \rightarrow \mathsf {b} \in \mathsf {FC}(\mathcal {R}^{-1})^{-1}\) and \(\mathsf {f}(x,x) \rightarrow \mathsf {a} \in \mathcal {R}\), resulting in the critical pair \(\mathsf {a} \approx \mathsf {b}\). Note that considering \(\mathsf {FC}(\mathcal {R})\) alone does not yield any progress in this example.

We aim for having a single tool that simultaneously attempts to prove and disprove all three properties \(\mathsf {UNR}\), \(\mathsf {UNC}\) and \(\mathsf {CR}\), fully exploiting the chain of implications (1) for optimization. For example, if \(\mathsf {UNC}\) has been established, any effort spent on proving \(\mathsf {UNR}\) would be wasted, but the current implementation cannot use this information. For the time being, however, there are separate tool invocations for each of these properties.

4 Higher-Order Confluence

CSI \(\mathbf {\hat{~}}\) ho is an extension of CSI for proving confluence of higher-order rewrite systems. Higher-order rewriting combines first-order rewriting with notions and concepts from (typed) \(\lambda \)-calculus, resulting in rewriting systems with higher-order functions and bound variables. More precisely we consider pattern rewrite systems (PRSs) as introduced by Nipkow [20, 27], i.e., terms are simply typed lambda terms with constants modulo \(\lambda \beta \eta \) and rewriting uses higher-order matching. Additionally left-hand sides of rewrite rules are required to be patterns [21].Footnote 6 This restriction is essential for obtaining decidability of unification and thus makes it possible to compute critical pairs. To this end CSI \(\mathbf {\hat{~}}\) ho implements a version of Nipkow’s algorithm for higher-order pattern unification [28].

Example 10

The untyped lambda calculus with \(\beta \) and \(\eta \)-reduction can be encoded as a PRS as follows:

figure c

Next we briefly explain the confluence criteria supported by CSI \(\mathbf {\hat{~}}\) ho. The first criterion is based on a higher-order version of the critical pair lemma.

Lemma 11

(Nipkow [27]). A PRS \(\mathcal {R}\) is locally confluent if and only if \(s \downarrow t\) for all critical pairs \(s \approx t\) of \(\mathcal {R}\).

The definition of critical pairs is essentially the same as in the first-order setting, with some additional technicalities to account for the presence of bound variables, see e.g. [20] for a formal definition. Together with Newman’s Lemma this yields a confluence criterion for PRSs.

Corollary 12

A terminating PRS \(\mathcal {R}\) is confluent if and only if \(s \downarrow t\) for all critical pairs \(s \approx t\) of \(\mathcal {R}\).

For showing termination CSI \(\mathbf {\hat{~}}\) ho uses a basic higher-order recursive path ordering [33] and static dependency pairs with dependency graph decomposition and the subterm criterion [19]. Alternatively, one can also use an external termination tool like WANDA  [18] as an oracle.

For potentially non-terminating systems CSI \(\mathbf {\hat{~}}\) ho supports two more classical criteria based on critical pairs. The first states that weakly orthogonal systems are confluent.

Theorem 13

(van Oostrom and van Raamsdonk [30]). A left-linear PRS \(\mathcal {R}\) is confluent if \(s = t\) for all critical pairs \(s \approx t\) of \(\mathcal {R}\).

The PRS from Example 10 has two trivial critical pairs and hence is confluent. This result was extended by van Oostrom to allow for non-trivial critical pairs that are connected by a development step.Footnote 7

Theorem 14

(van Oostrom [29]). A left-linear PRS \(\mathcal {R}\) is confluent if for all critical pairs \(s \approx t\) of \(\mathcal {R}\).

As a divide-and-conquer technique CSI \(\mathbf {\hat{~}}\) ho implements modularity, i.e., decomposing a PRS into parts with disjoint signatures, for left-linear PRSs [6]. Note that the restriction to left-linear systems is essential—unlike for the first-order setting confluence is not modular in general. The following example illustrates the problem.

Example 15

Consider the PRS \(\mathcal {R}\) from [6] consisting of the three rules

figure d

The first two rules and the third rule on their own are confluent, e.g. by Corollary 12 and Theorem 13 respectively. However, because of the peak

$$ \mathsf {a} \leftarrow \mathsf {f}(\mu (\lambda { x{}.\,} \mathsf {g}(x)),\mu (\lambda { x{}.\,} \mathsf {g}(x))) \rightarrow \mathsf {f}(\mu (\lambda { x{}.\,} \mathsf {g}(x)),\mathsf {g}(\mu (\lambda { x{}.\,} \mathsf {g}(x)))) \rightarrow \mathsf {b} $$

\(\mathcal {R}\) is not confluent. Note that \(\mathcal {R}\) does not have critical pairs, making it non-trivial to find this peak.

As described in Sect. 2 redundant rules can used to find such peaks. Implementing transformations based on redundant rules for PRSs is straightforward, one just has to take care to only add rules that do not violate the pattern restriction.

Example 16

Consider the PRS from Example 15. After adding the redundant rule \(\mathsf {f}(\mu (\lambda { x{}.\,} \mathsf {g}(x)),\mu (\lambda { x{}.\,} \mathsf {g}(x))) \rightarrow \mathsf {b}\) there is a critical pair \(\mathsf {a} \approx \mathsf {b}\) and non-confluence is obvious.

To find new rules like the one above we again use narrowing, applying rules in both directions. In Example 16 unifying \(Z(\mu (\lambda { x{}.\,} Z(x)))\) with \(\mathsf {g}(x)\) and applying the reversed third rule to the left-hand side of the second rule yields the desired new rule. The following example illustrates removal of redundant rules.

Example 17

Consider the following encoding of lambda-calculus with Regnier’s \(\sigma \)-reduction [34]:

$$\begin{aligned} \mathsf {app}(\mathsf {abs}(\lambda { x{}.\,} T(x)), S)&\rightarrow T(S) \\ \mathsf {app}(\mathsf {abs}(\lambda { y{}.\,} \mathsf {abs}(\lambda { x{}.\,} M(y, x))), S)&\rightarrow \mathsf {abs}(\lambda { x{}.\,} \mathsf {app}(\mathsf {abs}(\lambda { y{}.\,} M(y, x)), S)) \\ \mathsf {app}(\mathsf {app}(\mathsf {abs}(\lambda { x{}.\,} T(x)), S), U)&\rightarrow \mathsf {app}(\mathsf {abs}(\lambda { x{}.\,} \mathsf {app}(T(x), U)), S) \end{aligned}$$

Since the left- and right-hand side of the second and third rule are convertible using the first rule, they can be removed and confluence of the first rule alone can be established by Theorem 13.

5 Certification

Due to the increasing interest in automatic analysis of rewrite systems in recent years, it is of great importance whether a proof, generated by an automatic tool, is indeed correct (cf. Example 4). Since the proofs produced by such tools are often complex and large, checking correctness is impractical for humans. Hence there is strong interest in verifying them using an independent certifier. A certifier is a tool that reads proof certificates, and either accepts them as correct or rejects them as erroneous. To ensure correctness of the certifier, the predominant solution is to use proof assistants like Coq or Isabelle to first formalize the underlying theory in the proof assistant and then use the formalization to obtain verified functions for inspecting the certificates.

As certifier we use CeTA  [41], which reads certificates in CPF (certification problem format) [40]. Given a certificate CeTA will either answer CERTIFIED, or return a detailed error message why the proof was REJECTED. Its correctness is formally proved as part of IsaFoR, the Isabelle Formalization of Rewriting. IsaFoR contains executable check-functions for each formalized proof technique together with formal proofs that whenever such a check succeeds, the technique was indeed applied correctly. Isabelle ’s code-generation facility is used to obtain a trusted Haskell program from these check functions: the certifier CeTA.Footnote 8 Since 2012 CeTA supports checking (non-)confluence certificates. CSI supports certifiable output for the following criteria checkable by CeTA: Knuth and Bendix’ criterion [17, 39], (weak) orthogonality [25, 35], Huet’s results on strongly closed and parallel closed critical pairs and Toyama’s extenson of the latter [12, 24, 42], the rule labeling heuristic for decreasing diagrams [23, 45], and transformations based on redundant rules [22]. For non-confluence CeTA can check that, given derivations \(s \rightarrow ^* t_1\) and \(s \rightarrow ^* t_2\), \(t_1\) and \(t_2\) cannot be joined. Here the justifications used by CSI are: using \(\mathsf {tcap}\) [44] (i.e., test that \(\mathsf {tcap}(t_1 \sigma )\) and \(\mathsf {tcap}(t_2 \sigma )\) are not unifiable), and reachability analysis using tree automata [11]. Experimental results for certified confluence analysis are presented in Sect. 7.

6 Implementation Details

Fig. 1.
figure 1

The new web-interface of CSI.

Full size image

CSI is open source and available as pre-compiled binary or via the web-interface shown in Fig. 1 from http://cl-informatik.uibk.ac.at/software/csi, CSI \(\mathbf {\hat{~}}\) ho can be obtained from http://cl-informatik.uibk.ac.at/software/csi/ho. Since its first release one of CSI ’s defining features has been its strategy language, which enables the combination techniques in a flexible manner and facilitates integration of new criteria. Some of the combinators provided to combine methods that we will use below are: sequential composition of strategies ;, alternative composition | (which executes its second argument if the first fails), parallel execution ||, and iteration *. A postfix n* executes a strategy at most n times while [n] executes its argument for at most n seconds. Finally ? applies a strategy optionally (i.e., only if it makes progress), and ! ensures that its argument only succeeds if confluence could be (dis)proved. For a full grammar of the strategy language pass the option -h to CSI. To illustrate its power we briefly compare the strategy used in CSI 0.1 with the one from CSI 1.0. The original strategy was

(KB || NOTCR || (((CLOSED || DD) | add)2*)! || sorted -order)*

where sorted -order applies order-sorted decomposition and methods written in capitals are abbreviations for sub-strategies: KB applies Knuth-Bendix’ criterion, CLOSED tests whether the critical pairs of a TRS are strongly or development closed, DD implements decreasing diagrams, and NOTCR tries to establish non-confluence. The current strategy is

(if trs then (sorted -order*;

(((GROUND || KB || AC || KH || AT || SIMPLE || CPCS2 ||

(REDUNDANT_DEL?; (CLOSED || DD || SIMPLE || KB || AC ||

GROUND))3*! || ((CLOSED || DD) | REDUNDANT_RHS)3*! ||

((CLOSED || DD) | REDUNDANT_JS)3*! || fail)[30] | CPCS[5]2*)2* ||

(NOTCR | REDUNDANT_FC)3*!)

) else fail)

which illustrates how to integrate new techniques independently or in combination with others, for instance the REDUNDANT_X strategies, which are different heuristics for finding redundant rules. The features described in Sect. 2 are reflected in AC and REDUNDANT_FC. The AC substrategy is simply tried in parallel to the existing methods for confluence and non-confluence. For the REDUNDANT_FC method, which modifies a problem, a different approach is used: first, a non-confluence proof (NOTCR) is attempted. If that fails, then rules from the forward closure are added, and the process is repeated, starting with another attempt at proving non-confluence. After 3 iterations, CSI gives up on the non-confluence check. Other additions are a decision procedure for ground systems [8] (GROUND), criteria by Klein and Hirokawa [15] (KH) and by Aoto and Toyama [2] (AT), simple to test syntactic criteria by Sakai, Oyamaguchi, and Ogawa [37], and Toyama and Oyamaguchi [43] (SIMPLE), and techniques based on critical pair closing systems [31] (CPCS). The full strategy configuration file (which consists of definitions of abbreviations like AC) grew from 76 to 233 lines since the initial release.

7 Experimental Results

For experimentsFootnote 9 we considered all 291 TRSs in the Cops database. Table 1 compares the power of the current version of CSI  (1.0) to its initial release (CSI  0.1 [44]) and to the version used in CoCo 2016 (0.6). For each problem, a tool may establish confluence (yes), non-confluence (no), or fail to give a conclusive answer (maybe), corresponding to the rows of the table. The progress achieved in the past few months is obvious. Of the 24 systems which CSI cannot handle, its main weakness is lack of special support for non-left-linear rules. Here for instance criteria based on quasi-linearity [4] and implemented in ACP are missing in CSI ’s repertoire. Some of the 24 systems are (currently) out of reach for all automatic confluence tools, like extensions of combinatory logic or self-distributivity.

Table 1. Confluence results.
Full size table

The fourth column shows the results when using CSI ’s certifiable strategy, i.e., only criteria that can be checked by CeTA. Note that the maybe answers, in principle, include proofs produced by CSI that are not accepted by CeTA. However, because we also use Cops for testing the tools, this case does not occur for this set of problems. While all non-confluence proofs produced by CSI are certifiable there is still a gap in confluence analysis. The main missing techniques are a criterion to deal with AC rules, e.g. the ones from Sect. 2 or the one by Aoto and Toyama [2], advanced decomposition techniques based on layer systems [10], and techniques for dealing with non-left-linear systems, in particular the criteria by Klein and Hirokawa [15] and by Sakai, Oyamaguchi, and Ogawa [37]. The formalization and subsequent certification of most of these techniques requires serious effort, which we leave as future work.

Table 2. Unique normal form results.
Full size table

Table 2 summarizes the results for \(\mathsf {UNR}\) and \(\mathsf {UNC}\). We include \(\mathsf {CR}\) in the table because proving confluence is a common way of establishing \(\mathsf {UNR}\) or \(\mathsf {UNC}\). The \(\top \) row (where \(\top \) stands for true) represents the positive (yes) results for the corresponding properties, whereas the \(\top \) column represents the negative results. For these experiments we used 120 TRSs which are comprised of the 100 Cops that at most one of the tools ACP, CoLL-Saigawa, or CSI could show confluent in the respective version used in CoCo 2016, and an additional 20 TRSs that were used in the \(\mathsf {UNR}\) demonstration category in CoCo 2016. Note that the table entries overlap. For example, there are 20 problems for which \(\mathsf {CR}\) has been disproved and \(\mathsf {UNR}\) has been established; these 20 problems include the 14 problems which have been shown to satisfy \(\mathsf {UNC}\) but not \(\mathsf {CR}\). The number of problems for which none of the properties \(\mathsf {UNR}\), \(\mathsf {UNC}\), or \(\mathsf {CR}\) was proved or disproved is \(120+20-81-43 = 16\).

For experiments in the higher-order setting we again used Cops, which contains 69 PRSs. CSI \(\mathbf {\hat{~}}\) ho can show confluence of 50 and non-confluence of 10 of these. Solving the remaining 9 systems will require serious effort—they contain e.g. lambda calculus with surjective pairing and self-distributivity of explicit substitution.