# Second-order Church-Rosser modulo, without normalization

Thiago Felicissimo

► To cite this version:

Thiago Felicissimo. Second-order Church-Rosser modulo, without normalization. IWC 2024 – 13th International Workshop on Confluence, Jul 2024, Tallinn, Estonia. hal-04835978

HAL Id: hal-04835978

https://hal.science/hal-04835978v1

Submitted on 13 Dec 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Second-order Church-Rosser modulo, without normalization

Thiago Felicissimo

Université Paris-Saclay, INRIA, Deducteam, Laboratoire de Méthodes Formelles, ENS Paris-Saclay
thiago.felicissimo@inria.fr

## Abstract

We investigate criteria for proving Church-Rosser modulo of second-order rewrite systems without relying on normalization.

## 1 Introduction

Rewriting modulo is an alternative to standard rewriting in which one considers not only rewriting rules $l \mapsto r \in \mathcal{R}$ but also undirected equations $t \approx u \in \mathcal{E}$, allowing to handle theories defined by axioms that cannot be oriented in a well-behaved manner, such as commutativity. In this setting, the Church-Rosser property must be adapted into *Church-Rosser modulo*, stating that $t (\rightarrow \cup \leftarrow \cup \simeq)^* u$ implies $t \xrightarrow{\sim}^* \circ \simeq \circ \xleftarrow{\sim} u$, where $\simeq$ is the congruence generated by $\mathcal{E}$, $\rightarrow$ is the rewrite relation generated by $\mathcal{R}$, and $\xrightarrow{\sim}$ is a relation that can be $\rightarrow$ [9], or $\simeq \circ \rightarrow$, or something in between [10] depending on the considered variant of this definition.

Unfortunately, most criteria for Church-Rosser modulo rely on normalization [9, 10, 13, 6], posing a challenge in an ongoing line of study [2] to extend Dedukti [5], a rewriting-based framework for defining type theories, with rewriting modulo. Indeed, confluence proofs for dependent type theories are usually carried out on untyped terms, for which normalization does not hold due to rules such as $\beta$-reduction. The situation is made worse by the fact that type theories rely not on first- but second-order rewriting, for which criteria for Church-Rosser modulo are much rarer.

*Example 1.* Consider the following second-order rewrite system modulo, defining (a fragment of) the conversion of a type theory with an addition satisfying commutativity and associativity. Function symbols are written in *blue*, and *metavariables* in *typewriter font*. We would like to show this example (or a variant of it) to be Church-Rosser modulo.<fnref n="1" />

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l@{\qquad}l}
+(t, 0) \approx t & +(t, S(u)) \approx S(+(t, u)) & +(t, u) \approx +(u, t) & +(+(t, u), v) \approx +(t, +(u, v)) \\
@(\lambda(x.t\{x\}), u) \mapsto t\{u\} & \mathbf{N}_{\text{rec}}(0, p\theta, xy.pS\{x, y\}) \mapsto p\theta & & \\
& \mathbf{N}_{\text{rec}}(S(n), p\theta, xy.pS\{x, y\}) \mapsto pS\{n, \mathbf{N}_{\text{rec}}(n, p\theta, xy.pS\{x, y\})\} & &
\end{array}
$$

In this work, we investigate criteria for proving Church-Rosser modulo of second-order rewrite systems without relying on normalization. We start by proposing a first criterion, which relies on a notion of *unblocked* term. We then discuss a second criterion, which can be shown almost directly from a well-known result. The proofs not given here can be found in a technical report [7].

## 2 Preliminaries

We work in the setting of (untyped) second-order rewriting.<fnref n="2" /> An *arity* is a natural number *n* and a *binding arity* is a list of natural numbers (*n*₁, ..., *n*ₖ). Given a set *V* of variables *x*, *y*, ...,

<footnote n="1">¹Among other things, this is needed to establish the *injectivity of Π-types*: Π(A₁, x.A₂) ≡ Π(A'₁, x.A'₂) should imply Aᵢ ≡ A'ᵢ. This is then used to establish subject reduction of β-reduction.</footnote>

<footnote n="2">²This can be seen as Hamana's Second-order Computational Systems [8], or a simply-typed version of Klop's Combinatory Reduction Systems (CRSs) [12] with a single base type, or Nipkow's Pattern Rewrite</footnote>
a set $\mathcal{M}$ of metavariables $t, u, x, \dots$ equipped with arities, and a set $\mathcal{F}$ of (function) symbols $f, g, \dots$ equipped with binding arities, we define the terms by the following grammar, where we write $|\vec{x}|$ for the number $k$ of variables in a list of variables $\vec{x} = x_1 \dots x_k$. Here, the (simple) arity $\text{arity}(x) = k$ of $x$ specifies that it takes $k$ arguments, and the binding arity $\text{arity}(f) = (n_1, \dots, n_k)$ of $f$ specifies that it takes $k$ arguments and binds $n_i$ variables $\vec{x}_i$ in its $i$-th argument $t_i$. Given $\mathcal{F}' \subseteq \mathcal{F}$, we write $\mathcal{T}(\mathcal{F}')$ for the set of terms containing only symbols in $\mathcal{F}'$.

$$ 
\begin{array}{l@{\qquad}l}
t, u, v ::= & |x & x \in \mathcal{V} \\
& |x\{t_1, \dots, t_k\} & x \in \mathcal{M} \text{ with } \text{arity}(x) = k \\
& |f(\vec{x}_1.t_1, \dots, \vec{x}_k.t_k) & f \in \mathcal{F} \text{ with } \text{arity}(f) = (n_1, \dots, n_k) \text{ and } |\vec{x}_i| = n_i
\end{array}
$$

We write $fv(t)$ for the set of free variables of $t$ and $mv(t)$ for its set of metavariables. We often abbreviate $t_1, \dots, t_k$ as $\vec{t}$, and $\vec{x}_1.t_1, \dots, \vec{x}_k.t_k$ as $\textbf{t}$. A substitution $\sigma$ is a set of pairs either of the form $t/x$ or $\vec{x}.t/x$ where $\text{arity}(x) = |\vec{x}|$. We write $t[\sigma]$ for the application of $\sigma$ to $t$, the interesting cases being $x[\sigma] = t$ if $t/x \in \sigma$ and $x\{\vec{t}\}[\sigma] = u[\vec{t}[\sigma]/\vec{x}]$ if $\vec{x}.u/x \in \sigma$.

A term $t$ is said to be a $\vec{x}$-pattern if $fv(t) \subseteq \vec{x}$ and all metavariable occurrences are of the form $x\{\vec{x}, \vec{y}\}$ where $\vec{y}$ are the variables bound between the root of the term and this occurrence of $x^3$. A pattern is then just a $\varepsilon$-pattern, where $\varepsilon$ is the empty list.

A rewrite system $\mathcal{R}$ is a set of rewrite rules $l \mapsto r$, where $l$ is a pattern headed by a symbol and $mv(r) \subseteq mv(l)$ and $fv(r) = \emptyset$ (we already have $fv(l) = \emptyset$ from the definition of pattern). An equational system $\mathcal{E}$ is a set of equations $t \approx u$, where $t, u$ are both patterns.<fnref n="4" /> Given a rewrite system $\mathcal{R}$, we write $\rightarrow$ for the rewrite relation generated by $\mathcal{R}$, and given an equational system $\mathcal{E}$ we write $\simeq$ for the congruence on terms generated by $\mathcal{E}$. We write $\mathcal{F}_{\mathcal{R}} \subseteq \mathcal{F}$ for the symbols appearing in some left-hand side of $\mathcal{R}$, and $\mathcal{F}_{\mathcal{E}} \subseteq \mathcal{F}$ for the symbols appearing in some equation of $\mathcal{E}$.

A rewrite system modulo is a pair $(\mathcal{R}, \mathcal{E})$, and we write $\equiv$ for the least equivalence relation containing $\rightarrow$ and $\simeq$. As previously mentioned, there are many different definitions of Church-Rosser modulo in the literature, so here we will say that $(\mathcal{R}, \mathcal{E})$ is weak (resp. strong) Church-Rosser modulo when $t \equiv u$ implies $t (\simeq \circ \rightarrow)^* \circ \simeq \circ \circ (\leftarrow \circ \simeq) u$ (resp. $t \rightarrow^* \circ \simeq \circ \circ \leftarrow u$).

A context $C$ is a linear pattern on distinguished metavariables $\square_1, \square_2, \dots$ called holes. Given a context $C$ with $k$ holes and $\textbf{t} = \vec{x}_1.t_1, \dots, \vec{x}_k.t_k$ with $\text{arity}(\square_i) = |\vec{x}_i|$ for all $i$, we write $C[\textbf{t}]$ for $C[\vec{x}_1.t_1/\square_1, \dots, \vec{x}_k.t_k/\square_k]$.

Finally, we will also consider the definition of orthogonal rewriting $\Rightarrow$ (also known as de velopements, or simultaneous reduction [3]), given by the following rules. Here we write $\vec{t}_1 \Rightarrow \vec{t}_2$ when $\vec{t}_i = t_{i,1}, \dots, t_{i,k}$ and $t_{1,j} \Rightarrow t_{2,j}$, and $\textbf{t}_1 \Rightarrow \textbf{t}_2$ when $\textbf{t}_i = \vec{x}_1.t_{i,1}, \dots, \vec{x}_k.t_{i,k}$ and $t_{1,j} \Rightarrow t_{2,j}$, and $\sigma_1 \Rightarrow \sigma_2$ when $\text{dom}(\sigma_1) = \text{dom}(\sigma_2)$ and $t_1 \Rightarrow t_2$ whenever $t_i/x \in \sigma_i$ or $\vec{x}_i.t_i/x \in \sigma_i$.

$$ 
\begin{array}{l@{\qquad}l}
l \mapsto r \in \mathcal{R} & \sigma \Rightarrow \sigma' \\
\text{mv}(l) = \text{dom}(\sigma) & l[\sigma] \Rightarrow r[\sigma'] \\
& \textbf{t} \Rightarrow \textbf{t}' \\
& f(\textbf{t}) \Rightarrow f(\textbf{t}') \\
& \overline{\textbf{t} \Rightarrow \textbf{t}'} \\
& \overline{\textbf{x}\{\vec{t}\} \Rightarrow \textbf{x}\{\vec{t}'\}} \\
& x \Rightarrow x
\end{array}
$$

### 3 The first criterion

In order to explain our criterion and the intuition behind it, it is instructive to start with the following simple criterion for abstract rewriting. Recall that an abstract rewrite system modulo is given by a set $\mathcal{A}$ equipped with a binary relation $>.$ and an equivalence relation $\sim$.

<footnote>Systems (PRSs) [13] over a single base type but with only function symbols of order at most two and variables of order at most one. In particular, this allows us to use results developed for any of these formalisms.</footnote>

<footnote n="3">³Compared with Miller's original definition, we require patterns to be fully applied.</footnote>

<footnote n="4">⁴Note that we allow equations such as $(+n, 0) \approx n$, in which one of the sides is a metavariable.</footnote>
**Definition 1** (Unblocking subset of $\mathcal{A}$). Given an abstract rewrite system modulo, we say that a subset $\mathcal{U} \subseteq \mathcal{A}$ is unblocking for it if:

(A) For all $a \in \mathcal{A}$ there is some $b \in \mathcal{U}$ with $a \sim b$.

(B) For all $a, a' \in \mathcal{A}$ and $b \in \mathcal{U}$ with $b \succ a \succ a'$ we have $b \succ b' \sim a'$ for some $b' \in \mathcal{A}$.

Condition (B) intuitively states that in elements $b \in \mathcal{U}$ redexes are maximally unblocked with respect to $\sim$, so that if $b \sim a$, then any redex that is available in $a$ is also available in $b$. (A) then imposes that for every $\sim$ equivalence class one can always find an element in $\mathcal{U}$.

An interesting consequence of having an unblocking subset $\mathcal{U}$ is that we do not need to search the whole $\sim$ equivalence class for redexes, but instead we can just appeal to (A) to obtain a term in which all redexes are available. This motivates us to define the relation $\succ_U$ by $a \succ_U b$ iff $a \sim c \succ b$ for some $c \in \mathcal{U}$. We then have the following easy result — in the statement, we think of $\succ$ as orthogonal rewriting, which is why supposing the diamond property is reasonable.

**Proposition 1.** Suppose that $\succ$ satisfies the diamond property and that we have an unblocking subset $\mathcal{U} \subseteq \mathcal{A}$. Then $a (\succ \cup \prec \cup \sim)^* b$ implies $a \succ_U^* \circ \sim \circ_U^* \prec b$.

The main insight of our criterion is then that, under suitable conditions (satisfied for instance by Example 1), we can find an unblocking subset of terms. The intuition is that the only two ways that a redex can be blocked in Example 1 is if (1) some collapsable term is inserted in the middle of the redex (as in @+(λ(x.t), 0), u), where we have +(x, 0) ≃ x), or (2) some symbol in $\mathcal{E}$ matched by a rule left-hand side is not maximally exposed (as in $\mathbb{N}_{\text{rec}}(+(x, S(y)), p, xy.q)$, where S could be exposed using +(x, S(y)) ≃ S+(x, y))). This motivates the following definition:

**Definition 2** (Unblocked terms). A context $E$ is an $\mathcal{E}$-fragment of $t$ if $E \in \mathcal{T}(\mathcal{F}_{\mathcal{E}})$ and $E[u]$ is a subterm of $t$ for some $u$. A term $t$ is said to be unblocked if, for all $\mathcal{E}$-fragments $E$ of $t$:

(1) $E \simeq \Box_i$ implies $E = \Box_i$.

(2) $E \simeq f(\mathbf{t})$ with $f \in \mathcal{F}_{\mathcal{E}} \cap \mathcal{F}_{\mathbb{R}}$ implies $E = f(\mathbf{t}')$ with $\mathbf{t} \simeq \mathbf{t}'$.

Let us now state the assumptions of our criterion:

(i) Equations $t_1 \approx t_2 \in \mathcal{E}$ are linear, and we have $mv(t_1) = mv(t_2)$.

(ii) Symbols in $\mathcal{F}_{\mathcal{E}}$ have a binding arity of the form $(0, \dots, 0)$, the list being possibly empty.

(iii) For every context $E \in \mathcal{T}(\mathcal{F}_{\mathcal{E}})$, there is some unblocked $E' \in \mathcal{T}(\mathcal{F}_{\mathcal{E}})$ with $E \simeq E'$.

(iv) $\mathbb{R}$ is left-linear and no left-hand side is headed by a symbol in $\mathcal{F}_{\mathcal{E}} \cap \mathcal{F}_{\mathbb{R}}$.

(v) Orthogonal rewriting ($\Rightarrow$) with $\mathbb{R}$ satisfies the diamond property.

The goal of the rest of this section is then to show the following theorem, where we write $\tilde{\to}$ for the relation defined by $t \tilde{\to} t'$ iff $t \simeq u \to t'$ for some unblocked $u$.

**Theorem 1.** Suppose (i)-(v). Then $t \equiv u$ implies $t \xrightarrow{\sim}^* \circ \simeq \circ \xleftarrow{\sim}^* u$ for all $t, u$. In particular, $(\mathbb{R}, \mathcal{E})$ is weak Church-Rosser modulo.

Before showing the proof of Theorem 1, let us see how it can be applied to Example 1. Conditions (i), (ii) and (iv) can be directly verified, whereas (v) follows from the fact that $\mathbb{R}$ is orthogonal [14, Theorem 4.8]. To show (iii), let us first note that each context $E \in \mathcal{T}(\mathcal{F}_{\mathcal{E}})$ can be put in a normal-form. Indeed, writing $\langle \bar{t} \rangle$ for +(t₁, ..., +(tk−₁, tk)) or 0 when $\bar{t}$ is empty, then for each context $E \in \mathcal{T}(\mathcal{F}_{\mathcal{E}})$ we have $E \simeq S^k(\langle \Box_1, \dots, \Box_n \rangle)$ for some unique $k$ when $E$ has $n$ holes. We can easily see that this normal form is unblocked, showing (iii).
**Proof of Theorem 1**

To prove **Theorem 1**, we set out to show that unblocked terms satisfy properties (A) and (B) of **Definition 1** for the abstract rewrite system modulo defined by $\implies$ and $\simeq$, which will be achieved by **Propositions 2 and 3** respectively, and then apply **Proposition 1**.

A central tool of our proof is the fact that every term $t$ can be decomposed as $t = \bar{E}[\bar{t}]$ where $\bar{E}$ is a context with $\bar{E} \in \mathcal{T}(\mathcal{F}_\mathcal{E})$, and none of the terms in $\bar{t}$ is headed by a symbol in $\mathcal{F}_\mathcal{E}$. We call $\bar{E}[\bar{t}]$ the $\mathcal{E}$-decomposition of $t$, which is unique modulo renaming of $\bar{E}$. A main property of $\mathcal{E}$-decompositions is that $\mathcal{E}$-conversions can be split along them, in the sense of the following lemma. Let us write $t_1 \cong t_2$ when we have $t_i = x$ or $t_i = x\{\vec{v}_i\}$ and $\vec{v}_1 \simeq \vec{v}_2$ or $t_i = f(\mathbf{v}_i)$ and $\mathbf{v}_1 \simeq \mathbf{v}_2$. Let us then write $\bar{t}_1 \cong \bar{t}_2$ for its pointwise extension to the elements of $\bar{t}_i$.

**Lemma 1** (Splitting of an $\mathcal{E}$-conversion). Suppose (i), (ii), and $t_1 \simeq t_2$ for some $t_1, t_2$. Writing $\bar{E}_i[\bar{u}_i]$ for the $\mathcal{E}$-decomposition of $t_i$, we then must have $\bar{E}_1 \simeq \bar{E}_2$ and $\bar{u}_1 \cong \bar{u}_2$.

*Proof.* By induction on $t_1 \simeq t_2$. For the case $t_i = u_i[\sigma]$ with $u_1 \approx u_2 \in \mathcal{E}$ we crucially rely on the fact that equations are linear, which ensures that matching is completely local. $\square$

**Lemma 2.** Suppose (i), (ii) and that we have $t_1 \simeq t_2$ with $t_1$ an unblocked term and $t_2$ a term not headed by a symbol in $\mathcal{F}_\mathcal{E}$. Then we have $t_1 \cong t_2$.

*Proof.* We consider the $\mathcal{E}$-decompositions $t_i = \bar{E}_i[\bar{u}_i]$ and apply **Lemma 1** to get $\bar{E}_1 \simeq \bar{E}_2$ and $\bar{u}_1 \cong \bar{u}_2$. But because $t_2$ is not of the form $f(\mathbf{t})$ for some $f \in \mathcal{F}_\mathcal{E}$, we must have $\bar{E}_2 = \square$, and because $t_1$ is unblocked we get $\bar{E}_1 = \square$, so we conclude $\bar{u}_i = t_i$ and thus $t_1 \cong t_2$. $\square$

We can now show that the set of unblocking terms satisfies property (A) of **Definition 1**.

**Proposition 2.** Suppose (i)-(iii). For each $t$, there is some unblocked term $u$ with $t \simeq u$.

*Proof.* By induction on $t$. Case $t = x$ is trivial. Cases $t = x\{\bar{t}\}$ and $t = f(\mathbf{t})$ with $f \notin \mathcal{F}_\mathcal{E}$ follow directly by the ih. For $t$ headed by a symbol in $\mathcal{E}$, consider its decomposition $t = \bar{E}[\bar{t}]$. By ih we have $\bar{u}$ unblocked with $\bar{t} \simeq \bar{u}$, so by **Lemma 2** we have $\bar{t} \cong \bar{u}$. Finally, by (iii) we get $\bar{E}' \in \mathcal{T}(\mathcal{F}_\mathcal{E})$ unblocked with $\bar{E} \simeq \bar{E}'$, and so $\bar{E}'[\bar{u}]$ is unblocked and $\bar{E}'[\bar{u}] \simeq t$. $\square$

To show that the set of unblocking terms satisfies property (B) of **Definition 1** we now only need the following technical lemma, shown by induction on $t_1$ and using **Lemma 2**.

**Lemma 3.** Suppose (i)-(iv), and $t_1[\sigma] \simeq t_2$ with $t_2$ unblocked and $t_1 \in \mathcal{T}(\mathcal{F}_R)$ a linear $\vec{x}$-pattern and $\text{dom}(\sigma) = \text{mv}(t_1)$. Then we have $t_2 = t_1[\sigma']$ for some $\sigma' \simeq \sigma$.

In the following, let us write $\rho(t \implies u)$ for the number of redexes contracted in $t \implies u$ (even if there might be many derivations of $t \implies u$, the relevant one can be inferred from the context).

**Proposition 3.** Suppose (i)-(v). If $u$ is unblocked and $u \simeq t \implies t'$ then $u \implies u' \simeq t'$ and $\rho(t \implies t') = \rho(u \implies u')$.

*Proof.* By induction on $t \implies t'$. Almost all cases are either trivial or follow directly by applying **Lemma 2** and the ih, and case $l[\sigma] \implies r[\sigma']$ also uses **Lemma 3**. The case $f(\mathbf{t}) \implies f(\mathbf{t}')$ is more interesting, and follows using **Lemma 2** when $f \notin \mathcal{F}_\mathcal{E}$, or using **Lemma 1** when $f \in \mathcal{F}_\mathcal{E}$. $\square$

**Corollary 1.** Suppose (i)-(v). If $u$ is unblocked and $u \simeq t \implies t'$ then $u \implies u' \simeq t'$.

We can now prove **Theorem 1**. Let us write $t \iff u$ when $t \simeq t' \implies u$ with some $t'$ unblocked.
*Proof of Theorem 1.* By Propositions 2 and 3, the set of unblocked terms is unblocking for $\Rightarrow$ and $\simeq$. So by Proposition 1, and the fact that $\equiv$ equals $(\Rightarrow \cup \Leftarrow \cup \simeq)^*$, we get that $\equiv$ is included in $\stackrel{\sim}{\Rightarrow}^* \circ \simeq \circ \leftarrow\leftarrow$. To conclude it now suffices to replace the $\stackrel{\sim}{\Rightarrow}$ by $\stackrel{\sim}{\Rightarrow}$. To do this, we first show that $\stackrel{\sim}{\Rightarrow}$ is included in $\stackrel{\sim}{\Rightarrow}^* \circ \simeq$ using Corollary 1, and then we show that $\stackrel{\sim}{\Rightarrow}^* \circ \simeq$ is included in $\stackrel{\sim}{\Rightarrow}^* \circ \simeq$ by induction on $\stackrel{\sim}{\Rightarrow}^*$. $\square$

Before concluding this section, let us mention that Theorem 1 can probably be strengthened. More precisely, we think the requirement that $mv(t_1) = mv(t_2)$ in (i) can be dropped, and that it might be possible to weaken (v) to only require $\mathcal{R}$ to be confluent. Assumption (ii) also does not seem to be essential, and was made here to simplify proofs, because all our use cases satisfy it. On the other hand, all linearity assumptions are essential in our proof.

# 4 The second criterion

We now discuss an alternative and much easier criterion, which follows almost directly from a well-known result. In the following, let us write $CP^{\pm}(\mathcal{R}_1, \mathcal{R}_2)$ for the set of critical pairs between rules of $\mathcal{R}_1$ and $\mathcal{R}_2$ (see for instance [13] for a definition), and $CP(\mathcal{R})$ for $CP^{\pm}(\mathcal{R}, \mathcal{R})$. Moreover, given $\mathcal{E}$ for which both sides of all equations are headed by symbols and have the same variables$^5$, let us write $\mathcal{E}^{\pm}$ for the rewrite system $\mathcal{E} \cup \mathcal{E}^{-1}$, and note that we have $\simeq_{\mathcal{E}} = \to_{\mathcal{E}^{\pm}}$. Then, given a second-order rewrite system modulo $(\mathcal{R} \cup \mathcal{S}, \mathcal{E})$, consider the assumptions:

(a) $\mathcal{R} \cup \mathcal{S}$ is left-linear

(b) For all equations $t \approx u \in \mathcal{E}$, we have $t, u$ linear and headed by symbols, and $mv(t) = mv(u)$

(c) $\mathcal{R}$ is confluent

(d) $(\mathcal{S}, \mathcal{E})$ is strong Church-Rosser modulo

(e) $CP^{\pm}(\mathcal{R}, \mathcal{S}) = \emptyset$ and $CP^{\pm}(\mathcal{R}, \mathcal{E}^{\pm}) = \emptyset$

**Theorem 2.** Suppose (a)-(e). Then $(\mathcal{R} \cup \mathcal{S}, \mathcal{E})$ is strong Church-Rosser modulo.

So to apply Theorem 2 we still have to prove strong Church-Rosser modulo of a smaller system. The point is that in some cases of interest this smaller system can be strongly-normalizing, enabling the use of criteria that rely on this property. Let us see an example of this.

*Example 2.* Consider a version of Example 1 in which equations $+(t, 0) \approx t$ and $+(t, S(u)) \approx S(+t, u)$ are removed from $\mathcal{E}$, and in which we consider an additional rewrite system $\mathcal{S}$ given by

$$ \mathcal{S} := +(t, 0) \mapsto t, \quad +(t, S(u)) \mapsto S(+t, u), \quad +(0, t) \mapsto t, \quad +(S(u), t) \mapsto S(+t, u) $$

Then conditions (a), (b) and (e) can be directly verified, while (c) follows by orthogonality and (d) follows by [13, Theorem 5.11]$^6$, using the fact that $\to_S \circ \simeq$ is strongly normalizing and that $CP^{\pm}(\mathcal{E}^{\pm}, \mathcal{S}) \cup CP(\mathcal{S}) \subseteq \to_S^1 \circ \simeq_{\mathcal{E}} \circ \to_S^1 \leftarrow$, where $\to_S^1$ denotes reduction to a normal form.

Let us now move to the proof of Theorem 2. As previously mentioned, it can be shown almost directly from a well-known result, more precisely the following:

**Theorem 3** (Shown locally in the proof of Theorem 6.8 in [15]). If $\mathcal{R}$ and $\mathcal{S}$ are left-linear Pattern Rewrite Systems (PRSs) with $CP^{\pm}(\mathcal{R}, \mathcal{S}) = \emptyset$ then they commute.

<footnote>$^5$This extra condition on $\mathcal{E}$ is important for the definition to make sense. For instance, if $\mathcal{E} := \{+(x, 0) \approx x\}$, then $\mathcal{E} \cup \mathcal{E}^{-1}$ does not define a rewrite system, as left-hand sides of rewrite rules should be headed by symbols.</footnote>

<footnote>$^6$Actually, [13, Theorem 5.11] is a criterion for confluence modulo, but by [3, Exercise 14.3.7] in this case this is equivalent to strong Church-Rosser modulo, given that $\mathcal{S}$ is strongly normalizing.</footnote>
*Proof of Theorem 2.* Let us start with the following claim:

Claim 1. We have $\simeq_{\mathcal{E}} \circ_{RS} \leftarrow \circ \to_S^* \circ \simeq_{\mathcal{E}} \subseteq \to_S^* \circ \simeq_{\mathcal{E}} \circ_{RS} \leftarrow$.

*Proof of Claim 1.* First of all, because $(S, \mathcal{E})$ is strong Church-Rosser modulo, it is easy to see that it suffices to prove $\circ_{RS}^* \leftarrow \circ \to_S^* \circ \simeq_{\mathcal{E}} \subseteq \to_S^* \circ \simeq_{\mathcal{E}} \circ_{RS}^* \leftarrow$. To do this, we now show that $t \circ_{RS}^* \leftarrow \circ \to_S^* \circ \simeq_{\mathcal{E}} u$ implies $t \to_S^* \circ \simeq_{\mathcal{E}} \circ_{RS}^* \leftarrow u$ by induction on $n$, the base case being trivial. For the induction step, we have $t \circ_{RS} \leftarrow t' \circ_{RS}^* \leftarrow \circ \to_S^* \circ \simeq_{\mathcal{E}} u$, so by ih we get $t \circ_{RS} \leftarrow t' \to_S^* \circ \simeq_{\mathcal{E}} \circ_{RS}^* \leftarrow u$. We now do a case analysis on $t \circ_{RS} \leftarrow t'$. For the case $t \circ_{RS} \leftarrow t'$ this follows because $\mathcal{R}$ commutes with $S$ and $\mathcal{E}^{\pm}$ (by Theorem 3) and the fact that $\simeq \to_{\mathcal{E}^{\pm}}^*$. For the case $t \circ_S \leftarrow t'$ this follows because $(S, \mathcal{E})$ is strong Church-Rosser modulo. $\square$

We now proceed with the proof of Theorem 2. We have $\equiv$ equal to $(\to_{RS} \cup_{RS} \leftarrow \cup \simeq_{\mathcal{E}})^*$, so we prove the theorem by showing that $t (\to_{RS} \cup_{RS} \leftarrow \cup \simeq_{\mathcal{E}})^n u$ implies $t \to_{RS}^* \circ \simeq_{\mathcal{E}} \circ_{RS}^* \leftarrow u$ by induction on $n$. The base case is trivial, and for the induction step we have $t (\to_{RS} \cup_{RS} \leftarrow \cup \simeq_{\mathcal{E}})^n u'$ $(\to_{RS} \cup_{RS} \leftarrow \cup \simeq_{\mathcal{E}}) u$, and by ih we have $t \to_{RS}^* \circ \simeq_{\mathcal{E}} \circ_{RS}^* \leftarrow u'$. We conclude by a case analysis on $u' (\to_{RS} \cup_{RS} \leftarrow \cup \simeq_{\mathcal{E}}) u$. Case $u' \to_S u$ and $u' \simeq_{\mathcal{E}} u$ follow by Claim 1, and case $u' \to_R u$ follows because $\mathcal{R}$ commutes with $S$ and $\mathcal{E}^{\pm}$ (by Theorem 3) and with itself (by confluence of $\mathcal{R}$). $\square$

# 5 Discussion

In this work, we discussed two criteria for proving Church-Rosser modulo without normalization.

As previously mentioned, Theorem 2 can be shown almost directly from the fact that two left-linear PRSs with no critical pairs between them commute, so it might not be original (maybe it was already clear for others that it could be derived)$^7$. However, until finding Theorems 1 and 2, it was unclear for us how to prove Church-Rosser modulo for second-order systems with non-terminating rules, and we think that this problem should be more discussed in the literature. With Theorem 2 in hand, showing this property can be possible by isolating a terminating subsystem $(S, \mathcal{E})$, proving it strong Church-Rosser modulo with the criteria available in the literature (such as [13, Theorem 5.11]), and trying to verify the other hypotheses of Theorem 2 (as illustrated in Example 2). Because of this, we consider important to document here the existence of Theorem 2 and the strategy of how it can be applied, which will certainly be useful in the future for showing Church-Rosser modulo in an upcoming version of Dedukti with rewriting modulo [2].

A natural question is then how the two criteria compare. First of all, both of them require equations to be linear and rewrite rules to be left-linear, two important limitations, but which seem reasonable: indeed, non-terminating higher-order rules (such as $\beta$-reduction) are known to interact badly with non-left-linearity (see Klop's countexample [11])$^8$. Then, some of the other hypotheses seem difficult to compare, and indeed each of our examples (Examples 1 and 2) only works with one of the two criteria. However, looking closer at the examples, we remark an interesting point: the unblocked terms in Example 1 turn out to be exactly the normal forms for the system $S$ in Example 2, so the move from Example 1 to Example 2 replaces the search for an unblocked term by rewriting with $S$. The latter option seems more desirable, as it yields the strong variant of Church-Rosser modulo, instead of just the weak. It is an open question for us whether there are interesting examples that can be covered by Theorem 1, but which do not admit a variant covered by Theorem 2, or if the second criterion is always more useful in practice.

<footnote>$^7$Let us mention that a similar result is given by Blanqui in [4, Theorem 15], yet it is neither stronger nor weaker than ours (e.g., it only shows confluence modulo, which is weaker than strong Church-Rosser modulo).</footnote>

<footnote>$^8$An alternative is to consider a setting with *confinement* to avoid interactions between the higher-order rules and the equations, as done in [1]. Unfortunately, this would forbid interesting examples like Examples 1 and 2.</footnote>
**Acknowledgements** The author would like to thank Bruno Barras, Théo Winterhalter, Jean-Pierre Jouannaud, Vincent van Oostrom and the anonymous reviewers of IWC 2024.

# A Missing definitions

$t \to u$

$$ \frac{l \mapsto r \in \mathcal{R} \quad \mathrm{dom}(\sigma) = \mathrm{mv}(l)}{l[\sigma] \to r[\sigma]} $$

$$ \frac{t_i \to t'_i \quad \text{for some } i}{f(\vec{x}_1.t_1, \dots, \vec{x}_i.t_i, \dots, \vec{x}_k.t_k) \to f(\vec{x}_1.t_1, \dots, \vec{x}_i.t'_i, \dots, \vec{x}_k.t_k)} $$

$t \simeq u$

$$ \frac{t \approx u \in \mathcal{E} \quad \mathrm{dom}(\sigma) = \mathrm{mv}(t) \cup \mathrm{mv}(u)}{t[\sigma] \simeq u[\sigma]} $$

$$ \frac{t_i \simeq t'_i \quad \text{for all } i}{x\{t_1, \dots, t_k\} \simeq x\{t'_1, \dots, t'_k\}} $$

$x \simeq x$

$$ \frac{t \simeq u}{u \simeq t} $$

$$ \frac{t \simeq u}{u \simeq v} $$

<caption>Figure 1: Definitions of $\to$ and $\simeq$ for some given $\mathcal{R}$ and $\mathcal{E}$</caption>

# B Complete Proofs

**Proposition 1.** Suppose that $\succ$ satisfies the diamond property and that we have an unblocking subset $\mathcal{U} \subseteq \mathcal{A}$. Then $a (\succ \cup \prec \cup \sim)^* b$ implies $a \triangleright_{\mathcal{U}}^* \circ \sim \circ \triangleright_{\mathcal{U}}^* b$.

*Proof.* First note that we have the following basic facts, that can be easily shown using (A) and (B): if $a \sim \circ \triangleright_{\mathcal{U}} b$ then $a \triangleright_{\mathcal{U}} b$, and if $a \succ b$ then $a \triangleright_{\mathcal{U}} \circ \sim b$. We will also need the following claims.

Claim 2. If $a \mathcal{U} \triangleleft \circ \triangleright_{\mathcal{U}} b$ then $a \triangleright_{\mathcal{U}} \circ \sim \circ \mathcal{U} \triangleleft b$.

*Proof of Claim 2.* We have $a \prec a' \sim b' \succ b$ with $a', b' \in \mathcal{U}$. By (B) we have $b' \succ b'' \sim a$ for some $b''$, and by the diamond property we have $b'' \succ \circ \prec b$. We thus have $a \sim b'' \triangleright_{\mathcal{U}} \circ \sim \circ \mathcal{U} \triangleleft b$, and hence $a \triangleright_{\mathcal{U}} \circ \sim \circ \mathcal{U} \triangleleft b$. $\square$

Claim 3. If $a \mathcal{U} \triangleleft \circ \triangleright_{\mathcal{U}}^* b$ then $a \triangleright_{\mathcal{U}}^* \circ \sim \circ \mathcal{U} \triangleleft b$.

*Proof of Claim 3.* We have $a \mathcal{U} \triangleleft \circ \triangleright_{\mathcal{U}}^* b$ for some $n \in \mathbb{N}$, so let us show the result by induction on $n$, the case $n = 0$ being trivial. For the induction step, we have $a \mathcal{U} \triangleleft \circ \triangleright_{\mathcal{U}} \circ \triangleright_{\mathcal{U}}^* b$, so by Claim 2 we get $a \triangleright_{\mathcal{U}} \circ \sim \circ \mathcal{U} \triangleleft \circ \triangleright_{\mathcal{U}}^* b$. By the ih we then get $a \triangleright_{\mathcal{U}} \circ \sim \circ \triangleright_{\mathcal{U}}^* \circ \sim \circ \mathcal{U} \triangleleft b$, allowing us to conclude $a \triangleright_{\mathcal{U}}^* \circ \sim \circ \mathcal{U} \triangleleft b$. $\square$
Now let us move to the proof of the theorem. We have $a (\succ \cup \prec \cup \sim)^n b$ for some $n$, so let us show the result by induction on $n$, the base case being trivial. For the induction step, we have $a (\succ \cup \prec \cup \sim)^n c (\succ \cup \prec \cup \sim) b$, and by i.h. we have $a \triangleright_U^* a' \sim c' \triangleright_U^* c$ for some $a', c'$. We now proceed by case analysis on $c (\succ \cup \prec \cup \sim) b$. Cases $c \sim b$ and $c \prec b$ are trivial, and the case $c \succ b$ follows by noting $a \triangleright_U^* a' \sim c' \triangleright_U^* c \prec \triangleright_U \sim b$ and then applying Claim 3 to get $a \triangleright_U^* a' \sim c' \triangleright_U \sim \sim \triangleright_U^* c \sim b$, which implies the result. $\square$

**Lemma 1** (Splitting of an $\mathcal{E}$-conversion). Suppose (i), (ii), and $t_1 \simeq t_2$ for some $t_1, t_2$. Writing $\bar{E}_i[\bar{u}_i]$ for the $\mathcal{E}$-decomposition of $t_i$, we then must have $\bar{E}_1 \simeq \bar{E}_2$ and $\bar{u}_1 \cong \bar{u}_2$.

*Proof.* By induction on $t_1 \simeq t_2$. The cases when $t_1 \simeq t_2$ follows by an application of convexity, symmetry or transitivity are either trivial or follow directly by the ih.

* Case $t_i = e_i[\sigma]$ for some $e_1 \approx e_2 \in \mathcal{E}$. Then because each $e_i$ is fully contained in $\bar{E}_i$, we have $\bar{E}_1 \simeq \bar{E}_2$ and $\bar{u}_1 = \bar{u}_2$. Note that this crucially relies on the fact that equations in $\mathcal{E}$ are linear, so that matching is completely local and does not depend on subterms.

* Case $t_1 = x\{\vec{v}_1\} \simeq x\{\vec{v}_2\} = t_2$ with $\vec{v}_1 \simeq \vec{v}_2$. Then we have $\bar{E}_i = \square$, so the result follows.

* Case $t_1 = f(v_1) \simeq f(v_2) = t_2$ with $v_1 \simeq v_2$. If $f \notin \mathcal{F}_\mathcal{E}$ then we have $\bar{E}_i = \square$ so the result follows trivially. For the case $f \in \mathcal{F}_\mathcal{E}$, because of (ii) we know that $f$ binds no variables, so we have $v_i = v_i^1, \dots, v_i^k$. Let us now consider the $\mathcal{E}$-decompositions $v_i^j = \bar{E}_i^j[\vec{u}_{i,j}]$. By applying the ih to each $v_1^j \simeq v_2^j$ we get $\bar{E}_1^j \simeq \bar{E}_2^j$ and $\vec{u}_{1,j} \cong \vec{u}_{2,j}$. Writing $t_i = \bar{E}_i[\vec{u}_i]$ for the decomposition of $t_i$, we now conclude by noting that we must have $\bar{E}_i = f(\bar{E}_i^1, \dots, \bar{E}_i^k)$ and $\vec{u}_i = \vec{u}_{i,1}, \dots, \vec{u}_{i,k}$. $\square$

**Lemma 3.** Suppose (i)-(iv), and $t_1[\sigma] \simeq t_2$ with $t_2$ unblocked and $t_1 \in \mathcal{T}(\mathcal{F}_R)$ a linear $\vec{x}$-pattern and $\text{dom}(\sigma) = \text{mv}(t_1)$. Then we have $t_2 = t_1[\sigma']$ for some $\sigma' \simeq \sigma$.

*Proof.* By induction on $t_1$.

* Case $t_1 = x$. We have $\sigma = \emptyset$ and by Lemma 2 we get $t_2 = x$, so we can take $\sigma' = \emptyset$.

* Case $t_1 = x\{\vec{x}\}$. Then we have $\sigma = \vec{x}.u/x$ for some $u$. Defining $\sigma' := \vec{x}.t_2/x$ we then get $t_1[\sigma'] = t_2$ and $\sigma \simeq \sigma'$.

* Case $t_1 = f(v_1)$. First note that we must have $t_2 = f(v_2)$ for some $v_2 \simeq v_1[\sigma]$. Indeed, we have either $f \notin \mathcal{F}_\mathcal{E}$, in which case this claim follows by Lemma 2, or $f \in \mathcal{F}_\mathcal{E}$, in which case the claim directly follows from the fact that $t_2$ is unblocked. Now write $v_i = \vec{x}_1.v_{i,1}, \dots, \vec{x}_k.v_{i,k}$, and note that because $t_1$ is linear we must have $\text{mv}(v_{1,j}) \cap \text{mv}(v_{1,j'}) = \emptyset$ for $j \neq j'$. Let us then consider the decomposition $\sigma = \sigma_1 \cup \dots \cup \sigma_k$ given by the decomposition $\text{mv}(t_1) = \text{mv}(v_{1,1}) \cup \dots \cup \text{mv}(v_{1,k})$. By applying the ih to each $v_{1,j}[\sigma_j] \simeq v_{2,j}$ we get some $\sigma'_j$ satisfying $\sigma_j \simeq \sigma'_j$ and $v_{2,j} = v_{1,j}[\sigma'_j]$. Defining $\sigma' := \sigma'_1 \cup \dots \cup \sigma'_k$, we conclude $t_2 = t_1[\sigma']$ and $\sigma \simeq \sigma'$. $\square$

**Proposition 3.** Suppose (i)-(v). If $u$ is unblocked and $u \simeq t \implies t'$ then $u \implies u' \simeq t'$ and $\rho(t \implies t') = \rho(u \implies u')$.

*Proof.* By induction on $t \implies t'$. All cases are either trivial or follow directly by applying Lemma 2 and then the ih, except for the following two:

* Case $t = l[\sigma]$ and $t' = r[\sigma']$ with $\sigma \implies \sigma'$. By Lemma 3 we have $u = l[\theta]$ with $\theta \simeq \sigma$. By the ih we have $\theta \implies \theta' \simeq \sigma'$ and $\rho(\sigma \implies \sigma') = \rho(\theta \implies \theta')$. Hence we get $u = l[\theta] \implies r[\theta'] \simeq r[\sigma'] = t'$ and $\rho(l[\sigma] \implies r[\sigma']) = 1 + \rho(\sigma \implies \sigma') = 1 + \rho(\theta \implies \theta') = \rho(l[\theta'] \implies r[\theta'])$.
* Case $t = f(t) \Rightarrow f(t') = t'$. If $f \notin \mathcal{F}_\mathcal{E}$ then the result follows directly by applying Lemma 2 and then the ih. So let us now suppose $f \in \mathcal{F}_\mathcal{E}$, and consider the decompositions $t = \bar{E}_t[\vec{t}]$ and $u = \bar{E}_u[\vec{u}]$. By Lemma 1 we have $\bar{E}_t \simeq \bar{E}_u$ and $\vec{t} \simeq \vec{u}$. Now note that, because no symbol in $\mathcal{E}$ appears in the head of a rewrite rule, then $\bar{E}_t[\vec{t}] \Rightarrow t'$ implies $t' = \bar{E}_t[\vec{t}]$ with $\vec{t} \Rightarrow \vec{t}'$. Moreover, because $t$ is headed by a symbol in $\mathcal{E}$, it follows that the proof of $\vec{t} \Rightarrow \vec{t}'$ is smaller than the one of $t \Rightarrow t'$ we started with. Therefore, by the ih we get $\vec{u} \Rightarrow \vec{u}' \simeq \vec{t}'$ and $\rho(\vec{t} \Rightarrow \vec{t}') = \rho(\vec{u} \Rightarrow \vec{u}')$. We conclude $u = \bar{E}_u[\vec{u}] \Rightarrow \bar{E}_u[\vec{u}'] \simeq \bar{E}_t[\vec{t}'] = t'$ and $\rho(t \Rightarrow t') = \rho(\vec{t} \Rightarrow \vec{t}') = \rho(\vec{u} \Rightarrow \vec{u}') = \rho(u \Rightarrow u')$. $\square$

**Corollary 1.** Suppose (i)-(v). If $u$ is unblocked and $u \simeq t \longrightarrow t'$ then $u \longrightarrow u' \simeq t'$.

*Proof.* We have $u \simeq t \Rightarrow t'$, so Proposition 3 gives $u \Rightarrow u' \simeq t'$ for some $u'$. But because $\rho(u \Rightarrow u') = \rho(t \Rightarrow t') = 1$, then we have $u \longrightarrow u'$.

**Theorem 1.** Suppose (i)-(v). Then $t \equiv u$ implies $t \rightsquigarrow^* \circ \simeq \circ \leftarrow^* u$ for all $t, u$. In particular, $(\mathcal{R}, \mathcal{E})$ is weak Church-Rosser modulo.

*Proof.* By Propositions 2 and 3, the set of unblocked terms is unblocking for $\Rightarrow$ and $\simeq$. So by Proposition 1, and the fact that $\equiv$ equals $(\Rightarrow \cup \Leftarrow \cup \simeq)^*$, we get that $\equiv$ is included in $\rightsquigarrow^* \circ \simeq \circ \leftarrow^*$. To conclude it now suffices to replace the $\rightsquigarrow$ by $\rightsquigarrow$. To do this, we will need the following claims.

**Claim 4.** If $t \Rightarrow u$ then $t \rightsquigarrow^* \circ \simeq u$.

*Proof.* Because $\Rightarrow \sqsubseteq \Rightarrow^*$, we have $t \simeq \circ \longrightarrow^n u$ for some $n \in \mathbb{N}$, so let us show the result by induction on $n$, the base case being trivial. For the induction step, we write $t \simeq \circ \longrightarrow^n u'$ $\longrightarrow u$, and by ih we have $t \rightsquigarrow^* t' \simeq u'$ $\longrightarrow u$ for some $t'$. By Proposition 2 we have some $t''$ unblocked with $t'' \simeq u'$, so by Corollary 1 we get $t'' \longrightarrow \circ \simeq u$. We thus have $t' \rightsquigarrow \circ \simeq u$, so we conclude $t \rightsquigarrow^* \circ \simeq u$. $\square$

**Claim 5.** If $t \rightsquigarrow^* \circ \simeq u$ then $t \rightsquigarrow^* \circ \simeq u$.

*Proof.* We have $t \rightsquigarrow^n \circ \simeq u$ for some $n$, so we show the result by induction on $n$, the base case being trivial. For the induction step, we write $t \rightsquigarrow \circ \rightsquigarrow^n \circ \simeq u$, and by ih we have $t \rightsquigarrow \circ \rightsquigarrow^* \circ \simeq u$. By Claim 4 we then get $t \rightsquigarrow^* \circ \simeq \circ \rightsquigarrow^* \circ \simeq u$ and thus $t \rightsquigarrow^* \circ \simeq u$ $\square$

By applying Claim 5 two times, we then obtain that $\rightsquigarrow^* \circ \simeq \circ \leftarrow^* \rightsquigarrow$ is included in $\rightsquigarrow^* \circ \simeq \circ \leftarrow^* \rightsquigarrow$, concluding the proof. $\square$

## References

[1] Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, and Jiaxiang Liu. Untyped Confluence In Dependent Type Theories. working paper or preprint, April 2017.

[2] Bruno Barras, Thiago Felicissimo, and Theo Winterhalter. Towards a logical framework modulo rewriting and equational theories. In *30th International Conference on Types for Proofs and Programs (TYPES 2024)*. https://types2024.itu.dk/abstracts.pdf#section.0.40.

[3] Marc Bezem, Jan Willem Klop, and Roel de Vrijer. *Term rewriting systems*. 2003.

[4] Frédéric Blanqui. Rewriting modulo in deduction modulo. In Robert Nieuwenhuis, editor, *Rewriting Techniques and Applications*, pages 395–409, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.

[5] Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, and François Thiré. A modular construction of type theories. *Logical Methods in Computer Science*, 2023.
[6] Alexandre Boudet and Evelyne Contejean. About the confluence of equational pattern rewrite systems. In Claude Kirchner and Hélène Kirchner, editors, *Automated Deduction — CADE-15*, pages 88–102, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.

[7] Thiago Felicissimo. Second-order church-rosser modulo, without normalization. Technical report, 2024. Can be found at http://www.lsv.fr/~felicissimo/.

[8] Makoto Hamana. Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding. *Mathematical Structures in Computer Science*, 32(4):542–573, 2022.

[9] Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. *Journal of the ACM (JACM)*, 1980.

[10] Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. In *11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages*, 1984.

[11] Jan Willem Klop. *Combinatory reduction systems*. PhD thesis, Rijksuniversiteit Utrecht, 1963.

[12] Jan Willem Klop, Vincent Van Oostrom, and Femke Van Raamsdonk. Combinatory reduction systems: introduction and survey. *Theoretical computer science*, 121(1-2):279–308, 1993.

[13] Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. *Theoretical computer science*, 192(1):3–29, 1998.

[14] Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. In *International Conference on Typed Lambda Calculi and Applications*, pages 306–317. Springer, 1993.

[15] Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: The higher-order case. Technical report, 1994. http://www.javakade.nl/research/ps/ISRL-94-5.ps.