Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting

Abstract

Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. A distinctive feature of nominal rewriting is that $\alpha$-equivalence is not implicitly dealt with at the meta-level but explicitly dealt with at the object-level. In this paper, we introduce the notion of strong commutation modulo $\alpha$-equivalence and give a sufficient condition for it. Using the condition, we present a new criterion for confluence modulo $\alpha$-equivalence (on ground terms) of possibly non-terminating left-linear nominal rewriting systems.

1 Introduction

In languages with variable binding and variable names, $\alpha$-equivalence needs to be treated. Usually $\alpha$-equivalence is implicitly dealt with at the meta-level, but in the literature some authors seriously take it into account at the object-level (e.g. [6, 20]). The nominal approach [5, 13] is one of such studies, where variables that are possibly bound are called atoms. It deals with $\alpha$-equivalence explicitly at the object-level, incorporating permutations and freshness constraints as basic ingredients.

Nominal rewriting [3, 4] is a framework introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. It has a device to avoid accidental capture of free atoms on the way of rewriting, using the explicit $\alpha$-equivalence and freshness constraints in rewrite rules.

Confluence is a fundamental property of rewriting systems that guarantees uniqueness of results of computation. Confluence of nominal rewriting systems has been discussed in [1, 3, 9, 16, 17]. Their aim is to provide confluence criteria for particular classes of nominal rewriting systems in the same way as discussed in the field of first-order term rewriting.

In the present paper, we study confluence of nominal rewriting systems that are defined by rewrite rules with atom-variables in the style of [10], where rewriting is performed only on ground nominal terms (so confluence properties discussed in this paper correspond to ground confluence etc. in terms of traditional nominal rewriting). In previous work [8], we have proved (ground) confluence for this style of nominal rewriting systems whose rewrite rules have no overlaps which are computed using nominal unification with atom-variables [15]. In this paper, we present a sufficient condition for (ground) confluence of the same style of nominal rewriting systems possibly with overlaps of rewrite rules.

To discuss confluence in nominal rewriting, it is necessary to examine whether two terms can rewrite to $\alpha$-equivalent terms. For doing this, we make use of suitable notions that are defined modulo an equivalence relation in terms of abstract reduction systems [11, 12]. Such an approach was suggested in [20] (page 220). Precisely speaking, we present a sufficient condition for (ground) Church-Rosser modulo $\alpha$-equivalence rather than confluence. The proof method using the sufficient condition can be seen as a generalisation of that for confluence of first-order term rewriting systems using the lemma of Hindley [6] and Rosen [14]. We will explain details of the methods in Sect. 3.

Contributions of the Paper. The contributions of the present paper are summarised as follows:

• We introduce the notion of strong commutation modulo $\alpha$-equivalence and give a sufficient condition for it in left-linear uniform nominal rewriting systems. This notion has not been treated in [11, 12] (in the case of a general equivalence relation $\sim$).

• Using the sufficient condition, we present a new criterion for Church-Rosser modulo $\alpha$-equivalence (on ground nominal terms) of left-linear uniform nominal rewriting systems that are possibly non-terminating and may have overlaps of rewrite rules.

Organisation of the Paper. The present paper is organised as follows. In Sect. 2, we explain basic notions of nominal rewriting systems with atom-variables. In Sect. 3, we give a sufficient condition for strong commutation modulo $\alpha$-equivalence, and use it to present a criterion for Church-Rosser modulo $\alpha$-equivalence. In Sect. 4, we conclude with suggestions for further work.

2 Nominal Rewriting Systems with Atom-Variables

Nominal rewriting [3, 4] is a framework that extends first-order term rewriting by a binding mechanism. In this section, we recall basic notions and notations concerning nominal rewriting systems with atom-variables [10]. For differences from the system of [3], see [8]. For simplicity, we treat a subset of the systems in [8, 10].

2.1 Preliminaries

We fix a countably infinite set $\mathcal {X}$ of variables ranged over by $X,Y,\dots$, a countably infinite set $\mathcal {A}$ of atoms ranged over by $a,b,\dots$, and a countably infinite set $\mathcal {X}_{\!A}$ of atom-variables ranged over by $A,B,\dots$. A nominal signature $\varSigma$ is a set of function symbols ranged over by $f,g,\dots$. Each $f\in \varSigma$ has a unique non-negative integer $arity (f)$. We assume that $\mathcal {X}$, $\mathcal {A}$, $\mathcal {X}_{\!A}$ and $\varSigma$ are pairwise disjoint. Unless otherwise stated, different meta-variables for objects in $\mathcal {X}$, $\mathcal {A}$, $\mathcal {X}_{\!A}$ or $\varSigma$ denote different objects.

The domain $dom (\phi )$ of a mapping $\phi : D\rightarrow E$ is defined as the set $\{d \in D \mid \phi (d)\ne d\}$ if $D \subseteq E$, and D otherwise. A mapping $\phi : D\rightarrow E$ is finite if its domain $dom (\phi )$ is a finite set.

Let $\bowtie$ be a binary relation. We write $\bowtie ^=$ for the reflexive closure and $\bowtie ^*$ for the reflexive transitive closure. If $\bowtie$ is written using $\rightarrow$, then the inverse $\bowtie ^{-1}$ is written using $\leftarrow$. We use $\circ$ for the composition of two binary relations.

2.2 Ground Nominal Terms

In this subsection, we introduce the set of ground nominal terms, which we call $NL _a$ following [8, 10, 15].

The set $NL _a$ of ground nominal terms, or simply ground terms, is generated by the following grammar:

$$ t,s :\,\!:= a \mid [a]t \mid f{\langle t_1,\dots ,t_n \rangle } $$

where $n= arity (f)$. Ground terms of the forms in the right-hand side are called, respectively, atoms, abstractions and function applications. We assume that function applications bind more strongly than abstractions. We abbreviate $f{\langle \, \rangle }$ as f, and refer to it as a constant. An abstraction $[a]t$ is intended to represent t with a bound. The set $FA (t)$ of free atoms occurring in t is defined as follows: $FA (a) = \{a\}$; $FA ([a]t) = FA (t) \setminus \{a\}$; $FA (f{\langle t_1,\dots ,t_n \rangle }) = \bigcup _i FA (t_i)$.

Example 1

The nominal signature of the lambda calculus has two function symbols $\texttt{lam}$ with $arity (\texttt{lam})=1$, and $\texttt{app}$ with $arity (\texttt{app})=2$. The ground nominal term $\texttt{app}{\langle \texttt{lam}{\langle [a]\texttt{lam}{\langle [b]\texttt{app}{\langle b, a \rangle } \rangle } \rangle },b \rangle }$ represents the lambda term $(\lambda a.\lambda b.b a) b$ in the usual notation. For this ground term t, we have $FA (t)=\{b\}$.    $\square$

A swapping is a pair of atoms, written $(a\ b)$. Permutations $\pi$ are bijections on $\mathcal {A}$ such that $dom (\pi )$ is finite. Permutations are represented by lists of swappings applied in the right-to-left order. For example, $((b\ c)(a\ b))(a)=c$, $((b\ c)(a\ b))(b)=a$, $((b\ c)(a\ b))(c)=b$. The permutation action $\pi {\cdot } t$, which operates on terms extending a permutation on atoms, is defined as follows: $\pi {\cdot } a = \pi (a)$; $\pi {\cdot } ([a]t) = [\pi {\cdot } a](\pi {\cdot } t)$; $\pi {\cdot } (f{\langle t_1,\dots ,t_n \rangle }) = f{\langle \pi {\cdot } t_1,\dots ,\pi {\cdot } t_n \rangle }$.

Positions are finite sequences of positive integers. The empty sequence is denoted by $\varepsilon$. The set $Pos (t)$ of positions in a ground term t is defined as follows: $Pos (a) = \{\varepsilon \}$; $Pos ([a]t) = \{ 1p \mid p \in Pos (t) \}\cup \{\varepsilon \}$; $Pos (f{\langle t_1,\dots ,t_n \rangle }) = \bigcup _i \{ ip \mid p \in Pos (t_i) \}\cup \{\varepsilon \}$. The subterm of t at a position $p\in Pos (t)$ is written as $t|_p$. For positions p and q, we say that p is deeper than q if there exists a position o such that $p=qo$. In that case, o is denoted by $p\setminus q$.

A context is a ground term in which a distinguished constant $\square$ occurs. The ground term obtained from a context C by replacing each $\square$ at positions $p_i$ by ground terms $t_i$ is written as $C[t_1,\dots ,t_n]_{p_1,\dots ,p_n}$ or simply $C[t_1,\dots ,t_n]$.

A pair $a\# t$ of an atom a and a ground term t is called a freshness relation. The rules in Fig. 1 define the validity of freshness relations. Note that the defined $\vdash _{ NL _a}a\# t$ coincides with $a\notin FA (t)$.

Fig. 1.

Rules for freshness relations on $NL _a$

The rules in Fig. 2 define the relation $\vdash _{ NL _a}t \approx _\alpha s$. This is a congruence relation [3] and coincides with usual $\alpha$-equivalence (i.e. the relation reached by renamings of bound atoms) [5]. The bottom-right rule in the figure is about the case where the ground terms t and s are abstracted by different atoms. In $(a\ b) {\cdot } t$, the free occurrences of a in t are replaced by b which is fresh in t under the right premise of the rule. We often write $t \approx _\alpha s$ for $\vdash _{ NL _a}t \approx _\alpha s$.

Fig. 2.

Rules for $\alpha$-equivalence on $NL _a$

The following properties are shown in [3, 19].

Proposition 1

• 1. $\vdash _{ NL _a}a\# t$ if and only if $\vdash _{ NL _a}\pi {\cdot } a\# \pi {\cdot } t$.

• 2. $\vdash _{ NL _a}t \approx _\alpha s$ if and only if $\vdash _{ NL _a}\pi {\cdot } t \approx _\alpha \pi {\cdot } s$.

• 3. If $\vdash _{ NL _a}a\# t$ and $\vdash _{ NL _a}t \approx _\alpha s$ then $\vdash _{ NL _a}a\# s$.

2.3 Nominal Term Expressions

Next we introduce the set of term expressions, which we call $NL _{\!AX}$. Each rewrite rule is defined using them to represent a schema of rules.

The set $NL _{\!AX}$ of nominal term expressions, or simply term expressions, is generated by the following grammar:

$$ e :\,\!:= A \mid X \mid [A]e \mid f{\langle e_1,\dots ,e_n \rangle } $$

where $n= arity (f)$. We write $Var _{\!\mathcal {X}}(e)$ and $Var _{\!\mathcal {X}_{\!A}\!}(e)$ for the sets of variables and atom-variables occurring in a term expression e, respectively. Also, we write $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(e)$ for $Var _{\!\mathcal {X}}(e)\cup Var _{\!\mathcal {X}_{\!A}\!}(e)$. A term expression e is linear if each variable $X\in Var _{\!\mathcal {X}}(e)$ occurs only once in e.

The set $Pos (e)$ of positions in a term expression e is defined similarly to that for a ground term (using atom-variables for atoms) with the additional clause that $Pos (X) = \{\varepsilon \}$. The subexpression of e at a position $p\in Pos (e)$ is written as $e|_p$. A position $p\in Pos (e)$ is called a variable position if $e|_p$ is a variable, and a non-variable position otherwise.

A ground substitution is a finite mapping that assigns ground terms to variables and atoms to atom-variables. We use $\sigma ,\delta$ for ground substitutions. We write $\sigma _{\!\mathcal {X}}$ and $\sigma _{\!\mathcal {X}_{\!A}\!}$ for ground substitutions obtained from $\sigma$ by restricting the domain to $dom (\sigma )\cap \mathcal {X}$ and $dom (\sigma )\cap \mathcal {X}_{\!A}$, respectively. When $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(e)\subseteq dom (\sigma )$, the application of $\sigma$ on e is written as $e\sigma$ and called a ground instance of e. The application of $\sigma$ simply replaces the variables X and atom-variables A occurring in e by $\sigma (X)$ and $\sigma (A)$, respectively, without considering capture of free atoms. Then we have $e\sigma \in NL _a$ for every ground instance $e\sigma$.

A pair $A\# e$ of an atom-variable A and a term expression e is called a freshness constraint. A finite set of freshness constraints is called a freshness context. For a freshness context $\nabla$, we define $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(\nabla ) = \bigcup _{A\# e\in \nabla }(\{A\}\cup Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(e))$ and $\nabla \sigma = \{A\sigma \# e\sigma \mid A\# e\in \nabla \}$.

2.4 Nominal Rewriting Systems with Atom-Variables

Next we define nominal rewrite rules and nominal rewriting systems with atom-variables.

Definition 1

A nominal rewrite rule with atom-variables, or simply rewrite rule, is a triple of a freshness context $\nabla$ and term expressions $l,r\in NL _{\!AX}$ such that $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(\nabla ) \cup Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(r) \subseteq Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(l)$ and l is not a variable. We write $\nabla \vdash l \rightarrow r$ for a rewrite rule, and identify rewrite rules modulo renaming of variables and atom-variables. A rewrite rule $\nabla \vdash l \rightarrow r$ is left-linear if l is linear.

Definition 2 (Nominal rewriting system with atom-variables)

A nominal rewriting system with atom-variables ($NRS _{\!AX}$ for short) is a finite set of rewrite rules. An $NRS _{\!AX}$ is left-linear if so are all its rewrite rules.

The following example of an $NRS _{\!AX}$ corresponds to the system in Example 43 of [3] written in the style of traditional nominal rewriting. Note that the freshness constraint $A\# B$ in the rule $(\textsf{sub}_{\textsf{lam}})$ below is used to mean that the atom-variables A and B should be instantiated by distinct atoms.

Example 2

We extend the nominal signature in Example 1 by a function symbol $\texttt{sub}$ with $arity (\texttt{sub})=2$. By $\texttt{sub}{\langle [a]t,s \rangle }$, we represent an explicit substitution $t\langle a:=s\rangle$. Then, an $NRS _{\!AX}$ to perform $\beta$-reduction is defined by the rule $(\textsf{Beta})$:

$$ \begin{array}{rcrclr}&\vdash&\texttt{app}{\langle \texttt{lam}{\langle [A]X \rangle },Y \rangle }\rightarrow & {} \texttt{sub}{\langle [A]X,Y \rangle }&\quad (\textsf{Beta}) \end{array} $$

together with an $NRS _{\!AX}$ $\mathcal {R}_{\textsf{sub}}$ to execute substitution:

In a standard notation, the system $\mathcal {R}_{\texttt{sub}}$ is represented as follows:

$$ \begin{array}{rcrclr} &{} \vdash &{} (XY)\langle A:=Z\rangle &{} \rightarrow &{} (X\langle A:=Z\rangle )(Y\langle A:=Z\rangle ) &{} (\textsf{sub}_{\textsf{app}}) \\ &{} \vdash &{} A\langle A:=X\rangle &{} \rightarrow &{} X &{} (\textsf{sub}_{\textsf{var}}) \\ A\# X &{} \vdash &{} X\langle A:=Y\rangle &{} \rightarrow &{} X &{} (\textsf{sub}_{\epsilon }) \\ A\# B,B\# Y &{} \vdash &{} (\lambda B.X)\langle A:=Y\rangle &{} \rightarrow &{} \lambda B.(X\langle A:=Y\rangle ) &{} (\textsf{sub}_{\textsf{lam}}) \end{array} $$

   $\square$

In the sequel, $\vdash _{ NL _a}$ is extended to mean to hold for all members of the set in the right-hand side.

Definition 3 (Rewrite relation)

Let $R = \nabla \vdash l \rightarrow r$ be a rewrite rule. For ground terms $s,t\in NL _a$, the rewrite relation is defined by

$$ s \rightarrow _{\langle R,p,\sigma \rangle } t \overset{\textrm{def}}{\iff }\vdash _{ NL _a}\! \nabla \sigma ,\ s = C[s']_p,\ \vdash _{ NL _a}\! s' \approx _\alpha l\sigma ,\ t = C[r\sigma ]_p $$

Here the subterm $s'$ of s is called the R-redex, or simply redex if R is understood. We write $s {\mathop {\rightarrow }\limits ^{p}}_{R} t$ if there exists $\sigma$ such that $s \rightarrow _{\langle R,p,\sigma \rangle } t$. We write $s \rightarrow _{R} t$ if there exist p and $\sigma$ such that $s \rightarrow _{\langle R,p,\sigma \rangle } t$. For an $NRS _{\!AX}$ $\mathcal {R}$, we write $s \rightarrow _{\mathcal {R}} t$ if there exists $R\in \mathcal {R}$ such that $s \rightarrow _{R} t$.

An example of rewriting can be found in Example 4 of [8].

Lemma 1

Let $R = \nabla \vdash l \rightarrow r$ be a rewrite rule, and let s, t be ground terms. If $p\in Pos (s)$ and $s {\mathop {\rightarrow }\limits ^{p}}_{R} t$ then $\pi {\cdot } s {\mathop {\rightarrow }\limits ^{p}}_{R} \pi {\cdot } t$ for every permutation $\pi$.

Proof

This is proved in the same way as Lemma 2 of [8].    $\square$

2.5 Overlaps

The notion of overlap is useful for analysing confluence properties of rewriting systems. In the setting of the present paper, it can be defined using nominal unification with atom-variables [15]. Here we restrict the language of unification problems to $NL _{\!AX}$.

Definition 4 (Variable-atom nominal unification problem)

Let $\varGamma$ be a finite set of equations of the form $e_1 \approx e_2$ where $e_1$ and $e_2$ are term expressions, and let $\nabla$ be a freshness context. Then the pair $(\varGamma ,\nabla )$ is called a variable-atom nominal unification problem (VANUP for short).

Definition 5 (Solution of a VANUP)

A ground substitution $\sigma$ is a solution of a VANUP $(\varGamma ,\nabla )$ if $\vdash _{ NL _a}e_1\sigma \approx _\alpha e_2\sigma$ for every equation $e_1 \approx e_2 \in \varGamma$ and $\vdash _{ NL _a}A\sigma \# e\sigma$ for every freshness constraint $A\# e \in \nabla$. A VANUP $(\varGamma ,\nabla )$ is solvable if there exists a solution of $(\varGamma ,\nabla )$.

Example 3

Consider the nominal signature of the lambda calculus in Example 1, and let P be the VANUP $(\{ \texttt{lam}{\langle [A]\texttt{app}{\langle X, A \rangle } \rangle } \approx \texttt{lam}{\langle [B]Y \rangle }\}, \{A\# X \})$. Then, the ground substitution $[A:=a,B:=b,X:=c,Y:=\texttt{app}{\langle c,b \rangle }]$ is a solution of P.    $\square$

Definition 6 (Overlap)

Let $R_i=\nabla _i \vdash l_i\rightarrow r_i$ $(i=1,2)$ be rewrite rules. We assume without loss of generality that $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(l_1) \cap Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(l_2)=\emptyset$. If the variable-atom nominal unification problem $(\{ l_1 \approx l_2|_p \} ,\nabla _1 \cup \nabla _2)$ is solvable for some non-variable position p of $l_2$, then we say that $R_1$ overlaps on $R_2$, and the situation is called an overlap of $R_1$ on $R_2$. If $R_1$ and $R_2$ are identical modulo renaming of variables and atom-variables, and $p=\varepsilon$, then the overlap is said to be self-rooted. An overlap that is not self-rooted is said to be proper.

Example 4

Let $R_1$ and $R_2$ be the rules $(\textsf{Eta})$ $A\# X \vdash \texttt{lam}{\langle [A]\texttt{app}{\langle X, A \rangle } \rangle } \rightarrow X$ and $(\textsf{Beta})$ $\vdash \texttt{app}{\langle \texttt{lam}{\langle [B]Y \rangle },Z \rangle } \rightarrow \texttt{sub}{\langle [B]Y,Z \rangle }$, respectively. Then, $R_1$ overlaps on $R_2$, since the VANUP $(\{ \texttt{lam}{\langle [A]\texttt{app}{\langle X, A \rangle } \rangle } \approx \texttt{app}{\langle \texttt{lam}{\langle [B]Y \rangle },Z \rangle }|_{1} (= \texttt{lam}{\langle [B]Y \rangle })\}, \{A\# X \})$ is solvable as seen in Example 3. This overlap is proper.    $\square$

Example 5

There exists a self-rooted overlap of the rule $(\textsf{Beta})$ on its renamed variant, since the VANUP $(\{ \texttt{app}{\langle \texttt{lam}{\langle [A]X \rangle },Y \rangle } \approx \texttt{app}{\langle \texttt{lam}{\langle [B]Z \rangle },W \rangle } \}, \emptyset )$ is solvable by taking the ground substitution $[A:=a,B:=b,X:=a,Y:=c,Z:=b,W:=c]$ as a solution.    $\square$

Unlike in first-order term rewriting, self-rooted overlaps need to be analysed in the case of nominal rewriting (cf. [1, 16]). We check the cases corresponding to self-rooted overlaps too in the sufficient conditions given in the next section.

2.6 Parallel Reduction

A key notion for proving confluence of left-linear rewriting systems is parallel reduction. Here we define it inductively, using grammatical contexts [8, 16].

Definition 7

The grammatical contexts, ranged over by $G$, are the contexts defined by

$$ G:\,\!:= a \mid [a]\square \mid f{\langle \square _1,\dots ,\square _n \rangle } $$

where $n= arity (f)$. For each rewrite rule R, the relation is defined inductively by the following rules:

where $n\,(\ge 0)$ depends on the form of $G$.

The following properties of parallel reduction hold.

Lemma 2

• 1. .

• 2. If then .

• 3. If $s \rightarrow _{{\langle R,p,\sigma \rangle }} t$ then .

• 4. If then $s \rightarrow _R^* t$.

Proof

• 1. By induction on the structure of s.

• 2. By induction on the context C.

• 3. By 2 and the rule $(\textsf{B})$.

• 4. By induction on the derivation of .    $\square$

3 Confluence Criteria by Strong Commutation

In this section, we present a proof method for confluence of left-linear $NRS _{\!AX}$’s using strong commutation modulo $\alpha$-equivalence. First we review a basic proof method in rewriting systems with first-order rules. Then we introduce notions to discuss confluence in nominal rewriting, and give a criterion for $NRS _{\!AX}$’s.

3.1 Proof Method for Confluence by Strong Commutation

In this subsection, we survey the proof method for confluence by strong commutation. For first-order $TRS$’s, the method is known, e.g. in [18]. Here we consider a restricted class of $NRS _{\!AX}$’s consisting only of first-order rules. Note however that the rewrite relation is still defined for ground nominal terms in $NL _a$.

Definition 8

An $NRS _{\!AX}$ $\mathcal {R}$ is called a $TRS _{\!AX}$ if for every $\nabla \vdash l \rightarrow r \in \mathcal {R}$, $\nabla =\emptyset$, and l and r are term expressions with neither atom-variables nor abstractions.

For a $TRS _{\!AX}$, we restrict the rewrite relation to the one with matching by identity instead of modulo $\alpha$-equivalence (i.e. $s' = l\sigma$ instead of $\vdash _{ NL _a}\! s' \approx _\alpha l\sigma$ in Definition 3).

Definition 9

Let $\mathcal {R}$ be a $TRS _{\!AX}$. ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}}$ is confluent if for all ground terms s and t, $s \mathrel {(\leftarrow ^*_{\mathcal {R}} \circ \rightarrow ^*_{\mathcal {R}})} t$ implies $s \mathrel {(\rightarrow ^*_{\mathcal {R}} \circ \leftarrow ^*_{\mathcal {R}})} t$.

The basic strategy in the proof method is to show commutation of any combination of two rules of the $TRS _{\!AX}$. We recall definitions and lemmas on commutation (cf. [2, pp. 31–33]).

Definition 10

Let $R_1$ and $R_2$ be rewrite rules of a $TRS _{\!AX}$.

• 1. ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_2}$ commute iff for all ground terms $s_1$ and $s_2$, if $s_1 \mathrel {(\leftarrow ^*_{R_1} \circ \rightarrow ^*_{R_2})} s_2$ then $s_1 \mathrel {(\rightarrow ^*_{R_2} \circ \leftarrow ^*_{R_1})} s_2$.

• 2. ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ strongly commutes with iff for all ground terms $s_1$ and $s_2$, if then .

By Hindley’s results [6] and the properties shown in Lemma 2, we have the following.

Lemma 3

If ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ strongly commutes with then ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_2}$ commute.

Lemma 4

Let $\mathcal {R}$ be a $TRS _{\!AX}$. If ${\mathop {\rightarrow }\limits ^{}}_{R_i}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_j}$ commute for every $R_i,R_j\in \mathcal {R}$ then ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}}$ is confluent.

By Lemmas 3 and 4, to prove confluence of ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}}$, it is sufficient to show that for every combination of two rules $R_i,R_j\in \mathcal {R}$ (including the case $R_i=R_j$), ${\mathop {\rightarrow }\limits ^{}}_{R_i}$ strongly commutes with , or ${\mathop {\rightarrow }\limits ^{}}_{R_j}$ strongly commutes with .

Next we give conditions for strong commutation of ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ with .

Definition 11

Let $R_1$ and $R_2 (=\;\vdash l_2 \rightarrow r_2)$ be rewrite rules of a $TRS _{\!AX}$. The conditions $\textsf{sc}_1(R_1,R_2)$ and $\textsf{sc}_2(R_1,R_2)$ are defined as follows:

• $\textsf{sc}_1(R_1,R_2){\mathop {\Longleftrightarrow }\limits ^{\textrm{def}}}$ If $s{\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_1}s_1$ and is derived with $(\textsf{C})$ as the last                    applied rule, then there exists $t$ such that and                    $s_2\mathrel {{\rightarrow }^{*}_{R_1}}t$.

• $\textsf{sc}_2(R_1,R_2){\mathop {\Longleftrightarrow }\limits ^{\textrm{def}}}$ If $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ and $s{\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_2}s_2$ where p is a non-variable position                    of $l_2$, then there exists $t$ such that and $s_2\mathrel {{\rightarrow }^{*}_{R_1}}t$.

Note that the conditional part of $\textsf{sc}_2(R_1,R_2)$ arises only when $R_1$ overlaps on $R_2$.

The next lemma guarantees that $\textsf{sc}_1(R_1,R_2)$ and $\textsf{sc}_2(R_1,R_2)$ are a sufficient condition for strong commutation of ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ with . In Subsect. 3.3, we present a version of this lemma generalised to the case of $NRS _{\!AX}$.

Lemma 5

Let $R_1$ and $R_2$ be left-linear rewrite rules of a $TRS _{\!AX}$. If the conditions $\textsf{sc}_1(R_1,R_2)$ and $\textsf{sc}_2(R_1,R_2)$ hold, then ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ strongly commutes with  : 

Proof

We prove by induction on the derivation of that if $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ and then there exists $t$ such that and $s_2\mathrel {{\rightarrow }^{*}_{R_1}}t$.

• Suppose that the last part of the derivation of has the form

  

  • First we consider the case where the reduction $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ takes place in $G[u_1,\ldots ,u_n]$ with $u_i{\mathop {\rightarrow }\limits ^{}}_{R_1}u_i'$ for some $i\in \{1,\ldots ,n\}$. Then by the induction hypothesis, there exists $v_i'$ such that and $v_i\mathrel {{\rightarrow }^{*}_{R_1}}v_i'$. Hence by applying the rule $(\textsf{C}_{})$, we have

    

    Also, from $v_i\mathrel {{\rightarrow }^{*}_{R_1}}v_i'$ we have

    $$ s_2 = G[v_1,\ldots ,v_i,\ldots ,v_n]\mathrel {{\rightarrow }^{*}_{R_1}} G[v_1,\ldots ,v_i',\ldots ,v_n] $$

    Thus the claim follows by taking $t= G[v_1,\ldots ,v_i',\ldots ,v_n]$.

  • Next we consider the case where the redex of $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ is not in any $u_i$ of $G[u_1,\ldots ,u_n]$. Then we can assume that the $R_1$-redex is at the root (i.e. $s{\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_1}s_1$). Hence the claim follows from the condition $\textsf{sc}_1(R_1,R_2)$.

• Suppose that is derived by the rule $(\textsf{B})$

  

  where $R_2 =\;\vdash l_2 \rightarrow r_2$. Then by the definition of rewrite relation, there exists $\sigma$ such that $s = l_2\sigma$ and $s_2 = r_2\sigma$.

  • First we consider the case where the reduction $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ takes place in s with $X \sigma {\mathop {\rightarrow }\limits ^{}}_{R_1}X \delta$ for some $X\in Var _{\!\mathcal {X}}(l_2)$, and $Y \sigma =Y \delta$ for all $Y(\ne X)\in Var _{\!\mathcal {X}}(l_2)$. Then by the left-linearity of $R_2$, we have $s_1 = l_2\delta {\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_2} r_2\delta$, and so by the rule $(\textsf{B})$. Also, we have $s_2 = r_2\sigma \mathrel {{\rightarrow }^{*}_{R_1}} r_2\delta$. Hence the claim follows by taking $t= r_2\delta$.

  • Otherwise, the reduction $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ takes place in s with $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ where p is a non-variable position of $l_2$. Then the claim follows from the condition $\textsf{sc}_2(R_1,R_2)$.    $\square$

By Lemmas 3, 4 and 5, we have the following theorem.

Theorem 1

Let $\mathcal {R}$ be a left-linear $TRS _{\!AX}$. If for every $R_i,R_j\in \mathcal {R}$, $\textsf{sc}_1(R_i,R_j)$ and $\textsf{sc}_2(R_i,R_j)$, or $\textsf{sc}_1(R_j,R_i)$ and $\textsf{sc}_2(R_j,R_i)$, then ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}}$ is confluent.

We give an example of application of the theorem.

Example 6

We extend the nominal signature in Example 1 by function symbols (constants) $\texttt{S}$ and $\texttt{K}$. Consider the $TRS _{\!AX}$ $\mathcal {R}_{\textsf{CL}}$ consisting of the rewrite rules of combinatory logic (CL):

$$ \begin{array}{rcrclr} &{} \vdash &{} \texttt{app}{\langle \texttt{app}{\langle \texttt{app}{\langle \texttt{S}, X \rangle }, Y \rangle }, Z \rangle } &{} \rightarrow &{} \texttt{app}{\langle \texttt{app}{\langle X, Z \rangle }, \texttt{app}{\langle Y, Z \rangle } \rangle } &{} \quad (\texttt{S}) \\ &{} \vdash &{} \texttt{app}{\langle \texttt{app}{\langle \texttt{K}, X \rangle }, Y \rangle } &{} \rightarrow &{} X &{} \quad (\texttt{K}) \end{array} $$

We check the condition $\textsf{sc}_1((\texttt{S}),(\texttt{K}))$. Suppose $\texttt{app}{\langle \texttt{app}{\langle \texttt{app}{\langle \texttt{S}, u_1 \rangle }, u_2 \rangle }, u_3 \rangle } {\mathop {\rightarrow }\limits ^{\varepsilon }}_{\texttt{S}} \texttt{app}\langle \texttt{app}\langle u_1,$ $u_3\rangle , \texttt{app}{\langle u_2, u_3 \rangle }\rangle$ and with its last applied rule $(\textsf{C})$. Then the derivation of the latter must have the form

Hence we can construct a derivation of

$\texttt{app}\langle \texttt{app}{\langle v_1, v_3 \rangle }, \texttt{app}{\langle v_2, v_3 \rangle }\rangle$ from $D_1,D_2$ and $D_3$ by using the rule $(\textsf{C})$. We also have $s_2 = \texttt{app}{\langle \texttt{app}{\langle \texttt{app}{\langle \texttt{S}, v_1 \rangle }, v_2 \rangle }, v_3 \rangle } {\mathop {\rightarrow }\limits ^{}}_{\texttt{S}} \texttt{app}{\langle \texttt{app}{\langle v_1, v_3 \rangle }, \texttt{app}{\langle v_2, v_3 \rangle } \rangle }$, and so the condition $\textsf{sc}_1((\texttt{S}),(\texttt{K}))$ is satisfied. On the other hand, it is seen that the condition $\textsf{sc}_2((\texttt{S}),(\texttt{K}))$ is vacuously satisfied.

Next we consider the case where both rules are the rule $(\texttt{S})$. The condition $\textsf{sc}_1((\texttt{S}),(\texttt{S}))$ can be checked similarly to the above case. For the condition $\textsf{sc}_2((\texttt{S}),(\texttt{S}))$, we only have to check the case where both redexes are at the root, and in that case the claim clearly holds.

The case where both rules are the rule $(\texttt{K})$ can be checked similarly.

Therefore by Theorem 1, ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}_{\textsf{CL}}}({=}{\mathop {\rightarrow }\limits ^{}}_{\texttt{S}}\cup {\mathop {\rightarrow }\limits ^{}}_{\texttt{K}})$ is confluent.    $\square$

Note that ground terms here include countably many atoms (cf. Subsects. 2.1 and 2.2). By considering atoms as variables (rather than constants), we can see that confluence of a $TRS _{\!AX}$ discussed above is an extension of confluence of the standard first-order $TRS$ with the same function symbols and rewrite rules (so it is a property stronger than ground confluence of the first-order $TRS$). The $TRS _{\!AX}$ $\mathcal {R}_{\textsf{CL}}$ in Example 6 treats ground terms with atoms, and this is natural when considering an operator like $\lambda ^*$ (Definition 2.14 of [7]).

3.2 Confluence Properties in Nominal Rewriting

To discuss confluence in nominal rewriting, it is necessary to examine whether two terms can rewrite to the same term modulo $\alpha$-equivalence. For doing this, we make use of suitable notions that are defined modulo an equivalence relation in terms of abstract reduction systems [11, 12].

Definition 12

Let $\mathcal {R}$ be an $NRS _{\!AX}$.

• 1. $\rightarrow _{\mathcal {R}}$ is confluent modulo $\approx _\alpha$ iff for all ground terms s and t, if $s \mathrel {(\leftarrow ^*_{\mathcal {R}} \circ \rightarrow ^*_{\mathcal {R}})} t$ then $s \mathrel {(\rightarrow ^*_{\mathcal {R}} \circ \approx _\alpha \circ \leftarrow ^*_{\mathcal {R}})} t$.

• 2. $\rightarrow _{\mathcal {R}}$ is Church-Rosser modulo $\approx _\alpha$ iff for all ground terms s and t, if $s \mathrel {(\leftarrow _{\mathcal {R}} \cup \rightarrow _{\mathcal {R}} \cup \approx _\alpha )}^* t$ then $s \mathrel {(\rightarrow ^*_{\mathcal {R}} \circ \approx _\alpha \circ \leftarrow ^*_{\mathcal {R}})} t$.

In general, Church-Rosser modulo an equivalence relation $\sim$ is a stronger property than confluence modulo $\sim$ [11]. So, in the rest of this section, we aim to give a sufficient condition for Church-Rosser modulo $\approx _\alpha$ of left-linear $NRS _{\!AX}$’s.

To this end, we restrict the class of $NRS _{\!AX}$’s further by (an adaptation of) the uniformity condition [3]. Intuitively, uniformity means that if an atom a is not free in s and s rewrites to t then a is not free in t.

Definition 13

A rewrite rule $\nabla \vdash l \rightarrow r$ is uniform if the following holds: for every atom a and every ground substitution $\sigma$ such that $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(l)\subseteq dom (\sigma )$, if $\vdash _{ NL _a}\nabla \sigma$ and $\vdash _{ NL _a}a\# l\sigma$ then $\vdash _{ NL _a}a\# r\sigma$. A rewriting system is uniform if so are all its rewrite rules.

For uniform rewrite rules, the following properties hold.

Lemma 6

Suppose $s\rightarrow _R t$ for a uniform rewrite rule R. Then, for every atom a, if $\vdash _{ NL _a}a\# s$ then $\vdash _{ NL _a}a\# t$.

Proof

This is proved in the same way as Proposition 2 of [8].    $\square$

Definition 14

A relation $\rightarrow$ on ground terms is strongly compatible with $\approx _\alpha$ iff for all ground terms s and t, if $s \mathrel {(\approx _\alpha \circ \rightarrow )} t$ then $s \mathrel {(\rightarrow ^= \circ \approx _\alpha )} t$.

Lemma 7

If R is a uniform rewrite rule, then $\rightarrow _{R}$ is strongly compatible with $\approx _\alpha$ and is strongly compatible with $\approx _\alpha$.

Proof

This is proved in the same way as Lemmas 3 and 8 of [8].    $\square$

3.3 A Sufficient Condition for Church-Rosser Modulo $\alpha$-equivalence

Now we present a sufficient condition for Church-Rosser modulo $\approx _\alpha$ extending the sufficient condition for confluence in Theorem 1. First we introduce the notions of commutation and strong commutation modulo $\approx _\alpha$. The latter is not treated in [11, 12] (in the case of a general equivalence relation $\sim$).

Definition 15

Let $R_1$ and $R_2$ be rewrite rules of an $NRS _{\!AX}$.

• 1. $\rightarrow _{R_1}$ and $\rightarrow _{R_2}$ commute modulo $\approx _\alpha$ iff for all ground terms $s_1$ and $s_2$, if $s_1 \mathrel {(\leftarrow ^*_{R_1} \circ \rightarrow ^*_{R_2})} s_2$ then $s_1 \mathrel {(\rightarrow ^*_{R_2} \circ \approx _\alpha \circ \leftarrow ^*_{R_1})} s_2$.

• 2. ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ strongly commutes with modulo $\approx _\alpha$ iff for all ground terms $s_1$ and $s_2$, if then .

The following lemmas are counterparts of Lemmas 3 and 4 in Subsect. 3.1.

Lemma 8

If ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ strongly commutes with modulo $\approx _\alpha$, and both ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ and are strongly compatible with $\approx _\alpha$, then ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_2}$ commute modulo $\approx _\alpha$.

Proof

First we consider the claim that for all ground terms $s,s_1$ and $s_2$, if then there exist ground terms $t_1$ and $t_2$ such that . This is proved by induction on the length of the steps of $s_1 \leftarrow _{R_1}^* s$.

Next we show that for all ground terms $s,s_1$ and $s_2$, if then there exist ground terms $t_1$ and $t_2$ such that . This is proved by induction on the length of the steps of . By Lemma 2, , so we have that ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_2}$ commute modulo $\approx _\alpha$.    $\square$

Lemma 9

Let $\mathcal {R}$ be a uniform $NRS _{\!AX}$. If ${\mathop {\rightarrow }\limits ^{}}_{R_i}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_j}$ commute modulo $\approx _\alpha$ for every $R_i,R_j\in \mathcal {R}$, then ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}}$ is Church-Rosser modulo $\approx _\alpha$.

Proof

By Lemma 7, $\rightarrow _{R_i}$ is strongly compatible with $\approx _\alpha$ for every $R_i \in \mathcal {R}$. Then the claim follows by Corollary 2.6.5 of [12].    $\square$

Next we give conditions for strong commutation of ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ with modulo $\approx _\alpha$.

Definition 16

Let $R_1$ and $R_2$ ($= \nabla \vdash l_2 \rightarrow r_2$) be rewrite rules of an $NRS _{\!AX}$. The conditions $\textsf{sc}_1(R_1,R_2,\approx _\alpha )$ and $\textsf{sc}_2(R_1,R_2,\approx _\alpha )$ are defined as follows:

• $\textsf{sc}_1(R_1,R_2,\approx _\alpha ) {\mathop {\Longleftrightarrow }\limits ^{\textrm{def}}}$ If $s{\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_1}s_1$ and is derived with $(\textsf{C})$ as the                        last applied rule, then there exist $t_1$ and $t_2$ such that                        , $s_2\mathrel {{\rightarrow }^{*}_{R_1}}t_2$ and $t_1\approx _\alpha t_2$.

• $\textsf{sc}_2(R_1,R_2,\approx _\alpha ) {\mathop {\Longleftrightarrow }\limits ^{\textrm{def}}}$ If $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ and $s{\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_2}s_2$ where p is a non-variable                        position of $l_2$, then there exist $t_1$ and $t_2$ such that                        , $s_2\mathrel {{\rightarrow }^{*}_{R_1}}t_2$ and $t_1\approx _\alpha t_2$.

Note that the conditional part of $\textsf{sc}_2(R_1,R_2,\approx _\alpha )$ arises only when $R_1$ overlaps on $R_2$.

The next lemma guarantees that $\textsf{sc}_1(R_1,R_2,\approx _\alpha )$ and $\textsf{sc}_2(R_1,R_2,\approx _\alpha )$ are a sufficient condition for strong commutation of ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ with modulo $\approx _\alpha$.

Lemma 10

Let $R_1$ and $R_2$ be left-linear uniform rewrite rules of an $NRS _{\!AX}$. If the conditions $\textsf{sc}_1(R_1,R_2,\approx _\alpha )$ and $\textsf{sc}_2(R_1,R_2,\approx _\alpha )$ hold, then ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ strongly commutes with modulo $\approx _\alpha$ : 

Proof

We prove by induction on the derivation of that if $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ and then there exist $t_1$ and $t_2$ such that , $s_2\mathrel {{\rightarrow }^{*}_{R_1}}t_2$ and $t_1\approx _\alpha t_2$.

• Suppose that the last part of the derivation of has the form

  

  • First we consider the case where the reduction $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ takes place in $G[u_1,\ldots ,u_n]$ with $u_i{\mathop {\rightarrow }\limits ^{}}_{R_1}u_i'$ for some $i\in \{1,\ldots ,n\}$. Then by the induction hypothesis, there exist $v_{i1}'$ and $v_{i2}'$ such that , $v_i\mathrel {{\rightarrow }^{*}_{R_1}}v_{i2}'$ and $v_{i1}' \approx _\alpha v_{i2}'$. Hence by applying the rule $(\textsf{C}_{})$, we have

    

    Also, from $v_i\mathrel {{\rightarrow }^{*}_{R_1}}v_{i2}'$ we have

    $$ s_2 = G[v_1,\ldots ,v_i,\ldots ,v_n]\mathrel {{\rightarrow }^{*}_{R_1}} G[v_1,\ldots ,v_{i2}',\ldots ,v_n] $$

    Thus the claim follows by taking $t_1 = G[v_1,\ldots ,v_{i1}',\ldots ,v_n]$ and $t_2 = G[v_1,\ldots ,v_{i2}',\ldots ,v_n]$.

  • Next we consider the case where the redex of $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ is not in any $u_i$ of $G[u_1,\ldots ,u_n]$. Then we can assume that the $R_1$-redex is at the root (i.e. $s{\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_1}s_1$). Hence the claim follows from the condition $\textsf{sc}_1(R_1,R_2,\approx _\alpha )$.

• Suppose that is derived by the rule $(\textsf{B})$

  

  where $R_2 = \nabla \vdash l_2 \rightarrow r_2$. Then by the definition of rewrite relation, there exists $\sigma$ such that $\vdash _{ NL _a}\! \nabla \sigma$, $\vdash _{ NL _a}\! s \approx _\alpha l_2\sigma$ and $s_2 = r_2\sigma$.

  • First we consider the case where the reduction $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ takes place at a position p that is a variable position q of $l_2$ or deeper. Let $l_2|_q = X$. Then by Lemma 11 below, there exists $\delta$ such that $\vdash _{ NL _a}\! s_1 \approx _\alpha l_2\delta$, $X \sigma {\mathop {\rightarrow }\limits ^{}}_{R_1}X \delta$ and $Y \sigma =Y \delta$ for all $Y(\ne X)\in Var _{\!\mathcal {X}}(l_2)$. Since we can see $\vdash _{ NL _a}\! \nabla \delta$ using Lemma 6 (cf. Lemma 7(2) of [8]), we have $s_1 {\mathop {\rightarrow }\limits ^{\varepsilon }}_{R_2} r_2\delta$, and so by the rule $(\textsf{B})$. Also, we have $s_2 = r_2\sigma \mathrel {{\rightarrow }^{*}_{R_1}} r_2\delta$. Hence the claim follows by taking $t_1 = t_2 = r_2\delta$.

  • Otherwise, the reduction $s{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1$ takes place in s with $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ where p is a non-variable position of $l_2$. Then the claim follows from the condition $\textsf{sc}_2(R_1,R_2,\approx _\alpha )$.    $\square$

Lemma 11

Let $R_1$ and $R_2$ ($= \nabla \vdash l_2 \rightarrow r_2$) be left-linear uniform rewrite rules of an $NRS _{\!AX}$. Suppose that $\sigma$ is a ground substitution with $Var _{\!\mathcal {X}\!,\mathcal {X}_{\!A}\!}(l_2)\subseteq dom (\sigma )$ and $\vdash _{ NL _a}\! \nabla \sigma$. Suppose also that a reduction $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ takes place at a position p that is a variable position q of $l_2$ or deeper, and $l_2|_q = X$. Then, for every position $q'$ from $\varepsilon$ to q, if $\vdash _{ NL _a}s|_{q'} \approx _\alpha l_2|_{q'}\sigma$ then there exists $\delta$ such that $\vdash _{ NL _a}\! s_1|_{q'} \approx _\alpha l_2|_{q'}\delta$, $X \sigma {\mathop {\rightarrow }\limits ^{}}_{R_1}X \delta$, and $Y \sigma =Y \delta$ for all $Y(\ne X)\in Var _{\!\mathcal {X}}(l_2)$.

Proof

By induction on the length of $q\setminus q'$.

First we consider the case $q'=q$. Then $l_2|_{q'} = l_2|_q = X$. Suppose $\vdash _{ NL _a}s|_{q'} \approx _\alpha l_2|_{q'}\sigma = X\sigma$. Since $s{\mathop {\rightarrow }\limits ^{p}}_{R_1}s_1$ with a deeper position p than q, we have $s|_{q}{\mathop {\rightarrow }\limits ^{}}_{R_1}s_1|_{q}$. So by the strong compatibility of ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ (with ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ instead of $\mathrel {{\rightarrow }^{=}_{R_1}}$) there exists $t$ such that $X\sigma {\mathop {\rightarrow }\limits ^{}}_{R_1}t\approx _\alpha s_1|_{q}$. Hence we can take $\delta$ with $X\delta = t$ and $\vdash _{ NL _a}\! s_1|_{q} \approx _\alpha X\delta = l_2|_{q}\delta$.

For the other cases, the proof is by case analysis according to the form of $l_2|_{q'}$. This is shown analogously to the case analysis in the proof of Lemma 10 of [8].    $\square$

By Lemmas 7, 8, 9 and 10, we have the following theorem.

Theorem 2

Let $\mathcal {R}$ be a left-linear uniform $NRS _{\!AX}$. If for every $R_i,R_j\in \mathcal {R}$, $\textsf{sc}_1(R_i,R_j,\approx _\alpha )$ and $\textsf{sc}_2(R_i,R_j,\approx _\alpha )$, or $\textsf{sc}_1(R_j,R_i,\approx _\alpha )$ and $\textsf{sc}_2(R_j,R_i,\approx _\alpha )$ then ${\mathop {\rightarrow }\limits ^{}}_{\mathcal {R}}$ is Church-Rosser modulo $\approx _\alpha$.

In practice, if we know that $R_1$ does not overlap on $R_2$ and vice versa, we may use, instead of Lemma 8, Theorem 1 of [8] to show commutation modulo $\approx _\alpha$ of ${\mathop {\rightarrow }\limits ^{}}_{R_1}$ and ${\mathop {\rightarrow }\limits ^{}}_{R_2}$. So, to apply Theorem 2, we can concentrate on $R_i$ and $R_j$ such that there exists an overlap of $R_i$ on $R_j$ or $R_j$ on $R_i$. Moreover, for $R_i = R_j$, we may skip checking the case $p = \varepsilon$ in $\textsf{sc}_2(R_i,R_j,\approx _\alpha )$ when $R_i$ is $\alpha$-stable [16], so that we have only to check rules with proper overlaps when the $NRS _{\!AX}$ is $\alpha$-stable.

Definition 17

($\boldsymbol{\alpha }$-stability). A rewrite rule $R = \nabla \vdash l \rightarrow r$ is $\alpha$-stable if $\vdash _{ NL _a}s \approx _\alpha s'$, $s \rightarrow _{\langle R,\varepsilon ,\sigma \rangle } t$ and $s'\rightarrow _{\langle R,\varepsilon ,\sigma ' \rangle } t'$ imply $\vdash _{ NL _a}t \approx _\alpha t'$. An $NRS _{\!AX}$ $\mathcal {R}$ is $\alpha$-stable if so are all its rewrite rules.

We demonstrate Theorem 2 on two examples.

Example 7

The $NRS _{\!AX}$ $\mathcal {R}_{\textsf{sub}}$ in Example 2 is left-linear, uniform and $\alpha$-stable. In this $NRS _{\!AX}$, there are two pairs of rules that have proper overlaps: $((\textsf{sub}_{\textsf{app}})$, $(\textsf{sub}_{\epsilon }))$ and $((\textsf{sub}_{\textsf{lam}}),(\textsf{sub}_{\epsilon }))$.

For the pair $((\textsf{sub}_{\textsf{app}}), (\textsf{sub}_{\epsilon }))$, we first check the condition $\textsf{sc}_1((\textsf{sub}_{\textsf{app}}),(\textsf{sub}_{\epsilon })$, $\approx _\alpha )$. Suppose $\texttt{sub}{\langle [a]\texttt{app}{\langle u_1,u_2 \rangle },u_3 \rangle } {\mathop {\rightarrow }\limits ^{\varepsilon }}_{\textsf{sub}_{\textsf{app}}} \texttt{app}{\langle \texttt{sub}{\langle [a]u_1,u_3 \rangle },\texttt{sub}{\langle [a]u_2,u_3 \rangle } \rangle }$ and with its last applied rule $(\textsf{C})$. Then the derivation of the latter must have the form

Hence we can construct a derivation of from $D_1,D_2$ and $D_3$ by using the rule $(\textsf{C})$. We also have $s_2 = \texttt{sub}{\langle [a]\texttt{app}{\langle v_1,v_2 \rangle },v_3 \rangle } {\mathop {\rightarrow }\limits ^{}}_{\textsf{sub}_{\textsf{app}}} \texttt{app}{\langle \texttt{sub}{\langle [a]v_1,v_3 \rangle },\texttt{sub}{\langle [a]v_2,v_3 \rangle } \rangle }$, and so the condition $\textsf{sc}_1((\textsf{sub}_{\textsf{app}}),(\textsf{sub}_{\epsilon }))$ is satisfied.

Next we check the condition $\textsf{sc}_2((\textsf{sub}_{\textsf{app}}),(\textsf{sub}_{\epsilon }),\approx _\alpha )$. Suppose $\texttt{sub}\langle [a]\texttt{app}\langle$ $u_1,u_2\rangle ,u_3\rangle {\mathop {\rightarrow }\limits ^{\varepsilon }}_{\textsf{sub}_{\textsf{app}}} \texttt{app}{\langle \texttt{sub}{\langle [a]u_1,u_3 \rangle },\texttt{sub}{\langle [a]u_2,u_3 \rangle } \rangle }$ and $\texttt{sub}{\langle [a]\texttt{app}{\langle u_1,u_2 \rangle },u_3 \rangle }$ ${\mathop {\rightarrow }\limits ^{\varepsilon }}_{\textsf{sub}_{\epsilon }} \texttt{app}{\langle u_1,u_2 \rangle }$ $(= s_2)$. From the latter, we see $\vdash _{ NL _a}a\# u_1$ and $\vdash _{ NL _a}a\# u_2$, and so we have $\texttt{sub}{\langle [a]u_1,u_3 \rangle } {\mathop {\rightarrow }\limits ^{}}_{\textsf{sub}_{\epsilon }} u_1$ and $\texttt{sub}{\langle [a]u_2,u_3 \rangle } {\mathop {\rightarrow }\limits ^{}}_{\textsf{sub}_{\epsilon }} u_2$. Hence we can construct a derivation of . Thus $\textsf{sc}_2((\textsf{sub}_{\textsf{app}}),(\textsf{sub}_{\epsilon }),\approx _\alpha )$ holds by taking $t_1 = t_2 = \texttt{app}{\langle u_1,u_2 \rangle }$.

For the other pair of rules with a proper overlap, we can analogously check $\textsf{sc}_1((\textsf{sub}_{\textsf{lam}}),(\textsf{sub}_{\epsilon }),\approx _\alpha )$ and $\textsf{sc}_2((\textsf{sub}_{\textsf{lam}}),(\textsf{sub}_{\epsilon }),\approx _\alpha )$.

Therefore by Theorem 2, we see that $\rightarrow _{\mathcal {R}_{\textsf{sub}}}$ is Church-Rosser modulo $\approx _\alpha$.    $\square$

Example 8

Consider the $NRS _{\!AX}$ $\mathcal {R}_{\textsf{subdup}}$ obtained from $\mathcal {R}_{\textsf{sub}}$ in Example 2 by adding the following rewrite rule:

$$ \begin{array}{rcrclc} A\# Y&\vdash&\texttt{sub}{\langle [A]X,Y \rangle }\rightarrow & {} \texttt{sub}{\langle [A]\texttt{sub}{\langle [A]X,Y \rangle },Y \rangle }&\quad (\textsf{sub}_{\textsf{dup}}) \end{array} $$

This $NRS _{\!AX}$ $\mathcal {R}_{\textsf{subdup}}$ is left-linear, uniform and $\alpha$-stable. Also we see that it is non-terminating due to the rule $(\textsf{sub}_{\textsf{dup}})$. By applying Theorem 2, we can show that $\rightarrow _{\mathcal {R}_{\textsf{subdup}}}$ is Church-Rosser modulo $\approx _\alpha$.    $\square$

4 Conclusion

We presented a sufficient condition for Church-Rosser modulo $\alpha$-equivalence (on ground nominal terms) of left-linear uniform $NRS _{\!AX}$’s that may have overlaps of rewrite rules and may be non-terminating. This was achieved by introducing the notion of strong commutation modulo $\alpha$-equivalence and giving a sufficient condition for it.

Currently, we are working on implementation of a tool that verifies sufficient conditions as developed in this paper. To compute overlaps in $NRS _{\!AX}$’s and extract useful information, it is necessary to construct an appropriate unification procedure for variable-atom nominal unification problems.