Nominal Syntax with Atom Substitutions: Matching, Unification, Rewriting

Abstract

Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: nominal unification takes into account $\alpha$-equivalence; however, it does not take into account non-capturing substitutions, which are not primitive in nominal syntax. We consider an extension of nominal syntax with non-capturing substitutions and show that matching is decidable and finitary but unification is undecidable. We provide a matching algorithm and characterise problems for which matching is unitary, giving rise to expressive and efficient rewriting systems.

1 Introduction

Nominal syntax is a generalisation of first-order syntax that deals with variable binding using atom permutations and freshness constraints (see [17, 28]). Nominal syntax uses two kinds of variables: atoms $a,b,\ldots$, which can be abstracted but not substituted ($[a]t$ means that a is abstracted in t), and meta-variables $X, Y, \ldots$, called simply variables, which may be decorated with atom permutations. Unification of nominal terms (i.e., modulo $\alpha$-equivalence) is decidable and unitary [28]. Efficient algorithms exist that solve nominal unification problems in polynomial time [5, 7, 21]. Nominal matching (a form of unification where only one of the terms can be instantiated) can be solved in linear time [6].

Nominal unification and matching have applications in logic and functional languages [2, 8, 25, 26] and automated reasoning [10, 11, 13, 16, 23, 27] among others. However, nominal terms do not provide a built-in form of substitution for atoms that would permit direct definitions of systems such as the $\lambda$-calculus. Instead, atom substitution has to be defined explicitly, by rewrite rules or equations [14, 15], as in the following system, where (explicit) substitutions are sugared to $t\mathtt {\{}a\mapsto t'\mathtt {\}}$ and $a\mathbin {{\#}}t$ means that a is not free in t.

$$\begin{array}{cllcl} \mathsf{(Beta)} &{} &{}\mathtt {app}(\lambda [a]X,X') &{} \rightarrow &{} X\mathtt {\{}a\mapsto X'\mathtt {\}} \\ (\sigma _{\mathtt {var}}) &{} &{}a\mathtt {\{}a\mapsto X\mathtt {\}} &{} \rightarrow &{} X \\ (\sigma _\epsilon ) &{} a\mathbin {{\#}}Y\vdash &{}Y\mathtt {\{}a\mapsto X\mathtt {\}}&{} \rightarrow &{} Y \\ (\sigma _{\mathtt {app}}) &{} &{}\mathtt {app}(X,X')\mathtt {\{}a\mapsto Y\mathtt {\}}&{} \rightarrow &{} \mathtt {app}(X\mathtt {\{}a\mapsto Y\mathtt {\}},X'\mathtt {\{}a\mapsto Y\mathtt {\}}) \\ (\sigma _\mathtt {lam}) &{} b\mathbin {{\#}}Y \vdash &{}(\lambda [b]X)\mathtt {\{}a\mapsto Y\mathtt {\}}&{} \rightarrow &{} \lambda [b](X\mathtt {\{}a\mapsto Y\mathtt {\}}) \end{array} $$

An extension of nominal syntax with a primitive capture-avoiding atom substitution, which avoids the need to introduce explicit substitution rules, was presented in [12]; however, its rewriting theory was not developed. Here we show that unification in this extended syntax is undecidable in general but matching remains decidable (albeit no longer unitary) and the rewriting relation can be effectively computed. The undecidability result is obtained by reducing Hilbert’s tenth problem to extended nominal unification, inspired by Goldfarb’s proof of undecidability of second-order unification [18]. Our main contributions are an algorithm that computes complete sets of solutions for solvable matching problems, and a characterisation of a wide class of problems for which matching is unitary, inducing a well-behaved rewriting relation. This class includes the Beta and Eta reduction rules of the $\lambda$-calculus (we give details in Sect. 5). These results open the way for the development of expressive reasoning frameworks based on nominal syntax.

Related Work. Our syntax for extended nominal terms is inspired by [12], where a dependent type system for extended terms is presented. Matching was used in [12] to type-check terms given a set of declarations for function symbols. It was noted that restrictions were needed to ensure unitary matching, however, no matching algorithm was provided. Capture-avoiding atom substitution was previously studied in the context of nominal algebra by Gabbay and Mathijssen [15, 16], but its unification theory was not considered.

In [13], a nominal reduction system for the $\lambda$-calculus is given, with an explicit atom-substitution operation defined by a set of rewrite rules. The extended nominal syntax proposed here reduces the verbosity of such systems by internalising capture-avoiding substitutions.

Efficient nominal unification algorithms were developed by Calvès and Fernández [4, 5] and Levy and Villaret [21]. Both approaches were later unified by Calvès [3]. Kumar and Norrish [19] also studied efficient forms of nominal unification. Cheney [9] proved that a more general version of nominal unification, called equivariant unification, is NP-complete.

We followed Goldfarb’s methodology [18] to prove the undecidability of nominal unification extended with atom substitutions. Goldfarb [18] proved that second-order unification is undecidable by reducing Hilbert’s tenth problem to a second-order unification problem. An alternative undecidability proof for second-order unification by a direct encoding of the Halting problem is given by Levy and Veanes [20], which could also be adapted to our language.

2 Background

Fix countably infinite, pairwise disjoint sets of atoms, $a,b,c,$ $\ldots \in \mathcal {A}$; variables, $X,Y,Z,$ $\ldots \in \mathcal {X}$; and term-formers $f,g, \ldots \in \mathcal {F}$. A permutation $\pi$ is a bijection on a finite subset of $\mathcal {A}$ called support of $\pi$, $\mathcal {S}upport(\pi )$. A swapping $(a\ b)$ is a particular case where a maps to b, b maps to a and all other atoms c map to themselves. We follow the permutative convention [15, Convention 2.3] for atoms throughout the paper, i.e., atoms a, b, c range permutatively over $\mathcal {A}$ so that they are always distinct unless stated otherwise. Atom substitutions $\phi$, or just a-substitutions, are mappings with finite domain from atoms to terms, i.e., the set of atoms such that $\phi (a) \not =a$, written $\mathcal {D} om(\phi )$, is finite. Permutations $\pi$, a-substitutions $\phi$, and terms with atom substitutions s, t, or just (extended) terms, are generated by the following grammar.

Definition 1

(Syntax).

$$\begin{aligned}\begin{gathered} \pi \,{:}{:=} \mathsf {Id}\mid \pi (a\ b) \quad \phi \,{:}{:=} \mathsf {Id}\mid [a\mapsto s] \phi \quad s, t \,{:}{:=} a \mid \phi \hat{\ } \pi {\cdot }X \mid [a] s \mid f s \mid (s_1, \ldots , s_n) \end{gathered}\end{aligned}$$

The final $\mathsf {Id}$ is usually omitted from permutations and a-substitutions. Write $\pi ^{\text {-}1}$ for the inverse of $\pi$, e.g., if $\pi = (a\ b)(b\ c)$ then $\pi (c) =a$ and $c =\pi ^{\text {-}1}(a)$. A-substitutions are simultaneous bindings, abbreviated as $[a_1 \mapsto s_1; \ldots ; a_n \mapsto s_n]$ where atoms $a_i$ are pairwise distinct. Write $\phi ^{-a_1,\ldots ,a_n}$ for the a-substitution $\phi$ with domain restricted to $\mathcal {D} om(\phi )\setminus \{a_1,\ldots ,a_n\}$. $\mathcal {I}mg(\phi )$ denotes the set of terms $\{\phi (a) \mid a \in \mathcal {D} om(\phi )\}$. Term constructors as given in Definition 1 are called respectively atoms, moderated variables, abstractions, function applications (where f() is denoted as f) and tuples ($n \ge 0$). A moderated variable $\phi \hat{\ } \pi {\cdot }X$ comprises a variable X, and suspended permutation $\pi$ and a-substitution $\phi$. As in first-order syntax, variables denote unknown parts of the term, but here they are decorated with permutations and atom-substitutions, that will act when the variable is instantiated, as shown below. We abbreviate $\mathsf {Id}\hat{\ } \pi {\cdot }X$ (resp. $\phi \hat{\ }\mathsf {Id}{\cdot }X$) as $\pi {\cdot }X$ (resp. $\phi {\cdot }X$) and $\mathsf {Id}\hat{\ }\mathsf {Id}{\cdot }X$ as X if there is no ambiguity.

Permutations act on terms and a-substitutions; $\circ$ denotes composition:

$$\begin{aligned}\begin{gathered} \pi {\cdot }a \triangleq \pi (a) \quad \pi {\cdot }[a]t \triangleq [\pi (a)] \pi {\cdot }t \qquad \pi {\cdot }f t \triangleq f \pi {\cdot }t \quad \pi {\cdot }(t_1, \ldots , t_n) \triangleq (\pi {\cdot }t_1, \ldots , \pi {\cdot }t_n) \\ \pi {\cdot }(\phi \hat{\ } \pi '{\cdot }X) \triangleq (\pi {\cdot }\phi ) \hat{\ } (\pi \circ \pi ') {\cdot }X ~\text {where} ~ \pi {\cdot }\mathsf {Id}\triangleq \mathsf {Id}, ~ \pi {\cdot }([a \mapsto t]\phi ) \triangleq [\pi (a) \mapsto \pi {\cdot }t](\pi {\cdot }\phi ) \end{gathered}\end{aligned}$$

Write $V (t)$ for the set of variable symbols appearing in a term t and $A (t)$ for the set of atoms in t; this includes atoms in the domain and image of a-substitutions and atoms in the support of permutations.

A position p, q is a string of positive integers denoting a path in the abstract syntax tree of a term. The set of positions of a term s, $\mathcal {P}os(s)$, is defined inductively as usual [1] with an additional case for a moderated variable:

$$\begin{aligned} \mathcal {P}os( [a_1\mapsto t_1;\cdots ; a_n\mapsto t_n]\hat{\ } \pi {\cdot }X) \triangleq \{\epsilon \}\cup {\overset{n}{\underset{i=1}{\bigcup }}} \{i \cdot p \mid p \in \mathcal {P}os(t_i)\}. \end{aligned}$$

An arbitrary ordering (e.g., lexicographic) is chosen when defining the positioning of the terms in the image of suspended a-substitutions. Since we are dealing with simultaneous a-substitutions, the choice of ordering does not matter. The size of a term t, |t|, is the cardinality of $\mathcal {P}os(t)$. Call $t|_p$ the subterm of t at position p. If $p \in \mathcal {P}os(t)$, then $t[s]_p$ denotes the term obtained from t by replacing its subterm at position p by the term s and $(\cdots (s[t_1]_{p_1})\cdots )[t_n]_{p_n}$ is abbreviated as $s[t_1\cdots t_n]_{p_1\cdots p_n}$.

Example 1

Let $\mathtt {map}, \mathtt {cons}$ and $\mathtt {nil}$ be term-formers; $\mathtt {map}([a]F, \mathtt {cons}{{(}H,\mathtt {nil}{)}})$ is a term and so is t defined as $\mathtt {cons}{{(}[a\mapsto H]{\cdot }F, \mathtt {map}{{(}[b]F,\mathtt {nil}{)}}{)}}$. $A {{(}t{)}}=\{a,b\},V {{(}t{)}}=\{F, H\}$. $\mathcal {P}os(t)=\{\epsilon , 1, 11, 111, 12, 121, 1211, 12111, 1212\}$ so that, $t|_{111}=H$ and $t|_{1212}=\mathtt {nil}$, for instance. See [12, 13, 28] for more examples.

Call $a \mathbin {{\#}}t$ a freshness constraint. Let $\varDelta , \nabla ,\ldots$ range over finite sets of primitive constraints of the form $a \mathbin {{\#}}X$; call such sets freshness contexts. Call $s \mathbin {{\approx }_{\scriptstyle {\alpha }}}t$ an $\alpha$-equivalence constraint. Write $\nabla \vdash a \mathbin {{\#}}t$ and $\nabla \vdash s \mathbin {{\approx }_{\scriptstyle {\alpha }}}t$, called freshness and $\alpha$-equivalence judgements respectively, when a derivation exists using the syntax-directed rules from Definition 2 where, for a-substitutions $\phi ,\phi '$ and permutations $\pi ,\pi '$, $\mathcal {D} om(\phi ) \cup \mathcal {D} om(\phi ')$ is abbreviated as $\mathcal {D} omP(\phi ,\phi ')$ and $\mathcal {S}upport(\pi )\cup \mathcal {S}upport(\pi ')$ as $\mathcal {S}upportP(\pi ,\pi ')$. We write $a, b \mathbin {{\#}}t$ (resp. $a \mathbin {{\#}}s, t$) instead of $a \mathbin {{\#}}t, b \mathbin {{\#}}t$ (resp. $a \mathbin {{\#}}s, a \mathbin {{\#}}t$), and abbreviate $\varnothing \vdash s\mathbin {{\approx }_{\scriptstyle {\alpha }}}t$ as $s\mathbin {{\approx }_{\scriptstyle {\alpha }}}t$.

Definition 2

(Freshness and $\alpha$-equivalence judgements).

The most interesting rules are $\mathrm {\scriptstyle \mathbf (\# X)}$ and $\mathrm {\scriptstyle \mathbf (\mathbin {{\approx }_{\scriptstyle {\alpha }}}X)}$. The first one specifies that a is fresh in $\phi \hat{\ } \pi {\cdot }X$ if it is fresh in the image by $\phi$ of any atom that could occur in an instance of $\pi {\cdot }X$. The second ensures that the atom actions produce the same effect for any valid instance of X, in other words, any atom that could be affected by the atom actions suspended in X is either affected in the same way on both sides of the equality constraint, or it must be fresh in X. The relation $\mathbin {{\approx }_{\scriptstyle {\alpha }}}$ is indeed an equivalence relation [12].

Example 2

We can derive $a\mathbin {{\#}}[b\mapsto Y]\hat{\ }(a\ c){\cdot }X$ from $\nabla _1=\{ a\mathbin {{\#}}Y,c\mathbin {{\#}}X\}$ or from $\nabla _2=\{ b\mathbin {{\#}}X,c\mathbin {{\#}}X\}$ using rule $\mathrm {\scriptstyle \mathbf (\# X)}$, and $[c\mapsto (a\ b){\cdot }Y]{\cdot }X\mathbin {{\approx }_{\scriptstyle {\alpha }}}$ $[b\mapsto Y]{\cdot }(b\ c){\cdot }X$ from ${\nabla _1=\{ b\mathbin {{\#}}X,a\mathbin {{\#}}Y,b\mathbin {{\#}}Y\}}$ or $\nabla _2=\{ b\mathbin {{\#}}X,c\mathbin {{\#}}X\}$ using rule $\mathrm {\scriptstyle \mathbf (\mathbin {{\approx }_{\scriptstyle {\alpha }}}X)}$. In contrast, using standard (non-extended) nominal syntax, for each derivable constraint there exists a unique least freshness context entailing it [28].

The action of an a-substitution $\phi$ on a term t relies on a freshness context $\nabla$ and therefore is defined over terms-in-context, written $\nabla \vdash t$, or simply $\vdash t$ if $\nabla =\varnothing$. Below we abbreviate $(\nabla \vdash t) \phi$ as $\nabla \vdash t\phi$.

Definition 3

(A-substitution action).

$$\begin{aligned} \nabla \vdash a \phi \triangleq \nabla \vdash \phi (a) \quad \nabla \vdash (f t)\phi \triangleq \nabla \vdash ft\phi \qquad \qquad \quad \\ \nabla \vdash {{(}t_1, \ldots , t_n{)}} \phi \triangleq \nabla \vdash {{(}t_1 \phi , \ldots , t_n \phi {)}} \qquad \qquad \qquad \\ \qquad \nabla \vdash (\phi ' \hat{\ } \pi {\cdot }X) \phi \triangleq \nabla \vdash (\phi '\bullet \phi ) \hat{\ } \pi {\cdot }X ~~ where~\bullet ~denotes ~composition \\ \nabla \vdash ([a]t) \phi \triangleq \nabla \vdash [b]((a\ b){\cdot }t)\phi ^{-b} ~~ where~ \nabla \vdash b \mathbin {{\#}}t, \mathcal {I}mg(\phi )\quad \,\,\, \end{aligned}$$

A-substitutions work uniformly on $\alpha$-equivalence classes of terms, that is, the choice of b in Definition 3 is irrelevant [12]. Capture-avoidance is guaranteed by selecting an $\alpha$-equivalent representative of $\nabla \vdash [a]t$, i.e., $\nabla \vdash [b](a\ b){\cdot }t$, with fresh b. There exists always some $b \in (\mathcal {A}\setminus (A (t) \cup A (\mathcal {I}mg(\phi )) ) )$ such that $\nabla \vdash b \mathbin {{\#}}t, \mathcal {I}mg(\phi )$, assuming primitive constraints $b \mathbin {{\#}}X$ in $\nabla$ for each X in $(V (t) \cup V (\mathcal {I}mg(\phi )))$, since variables have finite support [24]. We assume $\nabla$ is large enough (in practice, it can be augmented whenever required). This approach is also taken in [8, 12, 13] and tacitly assumed in the rest of the paper.

Variable substitutions $\sigma ,\theta ,\ldots$, or just v-substitutions, are mappings from variables to terms, with finite domain $\mathcal {D} om(\sigma )$. They are generated by the grammar: $\sigma ,\theta \,::\,= \mathsf {Id}\mid [X \mapsto s] \sigma$ where $\mathsf {Id}$ is commonly omitted, and interpreted as simultaneous bindings, abbreviated $[X_1 \mapsto s_1; \ldots ; X_n \mapsto s_n]$ where variables $X_i$ are pairwise distinct. The application of a v-substitution $\theta$ to a moderated variable $\phi \hat{\ } \pi {\cdot }X$ induces the action of $\phi$ on the term $\pi {\cdot }\theta (X)$. The action of v-substitutions, $\sigma$, on terms, t, written $t\sigma$, is also parameterised by freshness contexts but left implicit in Definition 4. Given v-substitution $\sigma$ and freshness contexts $\nabla , \varDelta$, we write $\varDelta \vdash \nabla \sigma$ to denote $\varDelta \vdash a \mathbin {{\#}}\sigma (X)$ for each $a \mathbin {{\#}}X \in \nabla$.

Definition 4

(V-substitution action).

$$\begin{aligned} a \sigma \triangleq a \quad \quad ([a]t)\sigma \triangleq [a]t\sigma \quad (f t)\sigma \triangleq f t\sigma \quad (t_1,\ldots ,t_n)\sigma \triangleq (t_1\sigma , \ldots , t_n\sigma ) \\ (\phi \hat{\ } \pi {\cdot }X)\sigma \triangleq (\pi {\cdot }\sigma (X))(\phi \sigma )~ ~\text { where} ~~ \mathsf {Id}\sigma \triangleq \mathsf {Id}~\text { and }~ ([a\mapsto s]\phi ) \sigma \triangleq [a\mapsto s\sigma ](\phi \sigma ) \end{aligned}$$

Permutations and a-substitutions commute: $\nabla \vdash \pi {\cdot }(s\phi )\mathbin {{\approx }_{\scriptstyle {\alpha }}}(\pi {\cdot }s)(\pi {\cdot }\phi )$ and $\nabla \vdash (\pi {\cdot }s)\phi \mathbin {{\approx }_{\scriptstyle {\alpha }}}\pi {\cdot }(s (\pi ^{\text {-}1}{\cdot }\phi ))$. Also, v-substitutions commute with permutations, $\nabla \vdash \pi {\cdot }{{(}s\sigma {)}} \mathbin {{\approx }_{\scriptstyle {\alpha }}}{{(}\pi {\cdot }s{)}}\sigma$, and a-substitutions, $\nabla \vdash {{(}s\sigma {)}} \phi \sigma \mathbin {{\approx }_{\scriptstyle {\alpha }}}{{(}s\phi {)}}\sigma$.

3 Unification, Matching and Rewriting

Definition 5

Let C range over freshness and $\alpha$-equality constraints. A unification problem $\mathbf {P}$ is a finite set of such constraints, where $\alpha$-equivalence constraints are written as unification constraints $s \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}t$. A solution to $\mathbf {P}$ is a pair $(\mathbf {F} ,\sigma )$ of a non-empty collection $\mathbf {F}$ of freshness contexts and a v-substitution $\sigma$ such that $\varDelta \vdash C\sigma$ for each $\varDelta \in \mathbf {F}$ and $C \in \mathbf {P}$.

Write $\mathcal {U}(\mathbf {P})$ for the set of all solutions of $\mathbf {P}$. $(\mathbf {F} ,\sigma )\in \mathcal {U}(\mathbf {P})$ is more general than $(\mathbf {F} ',\sigma ')\in \mathcal {U}(\mathbf {P})$, written $(\mathbf {F} ,\sigma )$ $\le (\mathbf {F} ',\sigma ')$, if for each $\varDelta '\in \mathbf {F}'$ there exists $\varDelta \in \mathbf {F}$ and a v-substitution $\theta$ such that $\varDelta '\vdash X(\sigma \bullet \theta )\mathbin {{\approx }_{\scriptstyle {\alpha }}}X\sigma '$ for all X and $\varDelta '\vdash \varDelta \theta$. If there is no $(\mathbf {F} ',\sigma ')\in \mathcal {U}(\mathbf {P})$ such that $(\mathbf {F} ',\sigma ')< (\mathbf {F} ,\sigma )$ then $(\mathbf {F} ,\sigma )$ is a principal or most general solution.

The unification problem $\{[a\mapsto c] {\cdot }X \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}c\}$ has principal solutions $(\{\varnothing \}, [X\mapsto a])$ and $(\{\varnothing \},[X\mapsto c])$. In fact, the unification theory of extended nominal terms is infinitary. We give an example after defining complete sets of solutions. Note that solutions of unification problems use collections of contexts, since there may be several independent contexts that solve a constraint, as shown in Example 2.

Definition 6

Call W a complete set of solutions for $\mathbf {P}$ if $W \subseteq \mathcal {U}(\mathbf {P})$; $\forall (\mathbf {F} ,\theta ) \in W$, $\mathcal {D} om(\theta ) \subseteq V (\mathbf {P})$; and $\forall (\mathbf {F} ,\sigma ) \in \mathcal {U}(\mathbf {P}), \exists (\mathbf {F} ',\theta ) \in W: (\mathbf {F} ',\theta )\le (\mathbf {F} ,\sigma )$. W is a complete set of most general solutions if each element is principal.

The unification problem $\{ [c\mapsto f{{(}a,b{)}}]{\cdot }X \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}f(a,[c\mapsto b]{\cdot }X) \}$ has an infinite number of principal solutions of the form $(\{\varnothing \},\sigma _n)$ where $\sigma _n =[X\mapsto f{{(}a,f{{(}a,\ldots ,f{{(}a,c{)}}\cdots {)}}{)}}]$ and n is the number of occurrences of function symbol f and atom a in $\sigma _n(X)$. In particular, $\sigma _0=[X\mapsto c]$, $\sigma _1=[X\mapsto f(a,c)]$ and $\sigma _2=[X\mapsto f{{(}a,f{{(}a,c{)}}{)}}]$.

A matching constraint is a unification constraint $s \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}t$ where only variables in s may be instantiated; occurrences of variables in t are seen as constants. We sometimes write $s \mathbin {{}_{\scriptstyle {?}}{\approx }}t$ to emphasise that we are dealing with matching, and refer to s as the pattern and t as the matched term. Matching plays an important role in rewriting: given a set of rewriting rules, the nominal rewriting relation is generated by solving pattern-matching problems as defined below.

Definition 7

A matching problem $\mathbf {P}$ is a set of matching constraints $s_i\mathbin {{}_{\scriptstyle {?}}{\approx }}t_i$ such that $(\bigcup _i V (s_i))\cap (\bigcup _i V (t_i))=\varnothing$. We denote $\bigcup _i V (s_i)$ by $V_{LHS}(\mathbf {P})$ and $\bigcup _i V (t_i)$ by $V_{RHS}(\mathbf {P})$. A pattern matching problem consists of a pair of terms-in-context, written ${{(}\nabla \vdash l{)}}\mathbin {{}_{\scriptstyle {?}}{\approx }}{{(}\varDelta \vdash t{)}}$ such that $V (\nabla \vdash l)\cap V (\varDelta \vdash t)=\varnothing$.

A solution to a pattern matching problem ${{(}\nabla \vdash l{)}}\mathbin {{}_{\scriptstyle {?}}{\approx }}{{(}\varDelta \vdash s{)}}$ is a v-substitution $\sigma$, such that there exists $\mathbf {F}$ such that $(\mathbf {F} ,\sigma )$ is a solution to $\{l\mathbin {{}_{\scriptstyle {?}}{\approx }}s\}\cup \nabla$, and $\varDelta \vdash \nabla _i$ for some $\nabla _i\in \mathbf {F}$.

Definition 8

An extended nominal rewrite rule, or just rewrite rule, is a tuple, written $R=(\nabla \vdash l\rightarrow r)$, where $\nabla$ is a freshness context, and l, r are extended nominal terms such that $V (\nabla ,r)\subseteq V (l)$. We write $l\rightarrow r$ for $\varnothing \vdash l\rightarrow r$.

Example 3

• $\mathtt {par(out(a,b),in(a,[c]P))\rightarrow [c\mapsto b]{\cdot }P}$ is a rewrite rule , representing communication in the $\pi$ calculus.

• $\mathtt { a\mathbin {{\#}}X\vdash X \rightarrow lam([a]app (X,a))}$ is the $\eta$-expansion rule of the $\lambda$-calculus. The $\beta$ and $\eta$ reduction rules are:

  $$\begin{aligned} \begin{array}{ll} \mathrm {\scriptstyle \mathbf (\beta )}&{}\mathtt {app(lam([a]X),Y)\rightarrow [a\mapsto Y]{\cdot }X}\\ \mathrm {\scriptstyle \mathbf (\eta )}&{}\mathtt {a\mathbin {{\#}}X\vdash lam([a]app(X,a))\rightarrow X} \end{array} \end{aligned}$$

  Using standard nominal rules, four additional rules are needed to define explicit substitution (see the Introduction and [13]).

• The higher-order function map (see Example 1) is defined by rules:

  $$ \begin{array}{ll} \mathtt {map([a]F,nil)\rightarrow nil}\\ \mathtt {map([a]F,cons(H,T))\rightarrow cons([a\mapsto H]{\cdot }F,map([a]F,T))} \end{array} $$

To generate the rewrite relation, terms in rewrite rules are considered up to renaming of variables and atoms (metalevel equivariance [13, 24]), denoted $t^\pi$.

Definition 9

A rewrite system $\mathcal {R}$ induces a rewrite step $\varDelta \vdash s\xrightarrow {R} t$ if there exists $(\nabla \vdash l\rightarrow r)\in \mathcal {R}$, $p\in \mathcal {P}os(s)$ and a permutation $\pi$ such that the pattern-matching problem ${{(}\nabla ^{\pi }\vdash l^{\pi }{)}}\mathbin {{}_{\scriptstyle {?}}{\approx }}{{(}\varDelta \vdash s|_p{)}}$ has solution $\theta$, and $\varDelta \vdash s[r^{\pi }\theta ]_{p}\mathbin {{\approx }_{\scriptstyle {\alpha }}}t$:

The (multi-step) rewrite relation $\varDelta \vdash _{_\mathcal {R}} s\rightarrow t$ is the reflexive, transitive closure of the one-step rewrite relation.

Example 4

The term-in-context rewrites to a normal form in one step with the rule $\mathrm {\scriptstyle \mathbf (\beta )}$ (see Example 3), at position $\epsilon$ with permutation $\mathsf {Id}$ and v-substitution as follows,

Capture of the unabstracted atom $\mathtt {b}$ has been avoided by the internal machinery of the extended nominal framework implementing a-substitution. By relegating the semantics of capture-avoiding substitution to the metal-level, where they are managed by our formalism, we have reduced the set of rewrite rules necessary to provide a nominal representation of the rewrite system at hand. The same reduction requires several steps using explicit substitution rules [13].

4 Solving Matching Problems

A sound and complete matching algorithm can be built by converting the set of derivation rules given in Definition 2 into a simplification system. This algorithm can then be used to implement rewriting, and also to check closedness of terms and rewrite rules (see [13]). Principal solutions are not unique in general but matching is unitary for a restricted but practically useful class of problems (cf. Theorem 2).

In a matching problem $\mathbf {P}= s_1\mathbin {{}_{\scriptstyle {?}}{\approx }}t_, \ldots , s_n \mathbin {{}_{\scriptstyle {?}}{\approx }}t_n$, variables on the right-hand side of matching constraints are treated as constants. Hence, without loss of generality, we assume $a\mathbin {{\#}}X$ for any $X\in V _{RHS}(\mathbf {P})$ and $a\in \mathcal {A}$.

Although, initially, the sets of variables in left- and right-hand sides of matching constraints are disjoint, this property is not preserved during the process of solving matching problems (due to variable instantiations). Thus, given a matching problem $\mathbf {P}_0$ to solve, we start by computing the set $V_{RHS} {{(}\mathbf {P}_0{)}}$ of variables that should not be instantiated.

The following auxiliary functions Cap and $\varPsi$ are used in the matching algorithm to handle constraints where the pattern is a moderated variable: To solve a constraint of the form $\phi \hat{\ } \pi {\cdot }X \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}t$ where $t \not =\phi ' \hat{\ } \pi '{\cdot }X$, one checks if some subterm $t|_{p}$ of t is contained in the image of $\phi$, that is, $[\pi (a)\mapsto t|_p] \in \phi$. In order to find such position p and subterm $t|_p$, the matching algorithm generates cap constraints of the form $(t[a_1\cdots a_n]_{p_1\cdots p_n} )\phi \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}t$, where $p_i \in \mathcal {P}os(t)$ and $a_i \in \mathcal {D} om(\phi )$, using the function Cap defined below.

Definition 10

(Cap terms). Let t be a term, $\mathbb {A}$ a finite set of atoms.

${Cap}{{(}t,\mathbb {A}{)}}=\{ t[a_1\cdots a_n]_{p_1\cdots p_n} \mid n \in Nat, a_i \in \mathbb {A}, p_i \in \mathcal {P}os(t),1\le i\le n \}.$

Thus, ${Cap}(t,\mathbb {A})$ returns the set of all the terms obtained by replacing subterms of t with atoms from $\mathbb {A}$. Note that ${Cap}{{(}t,\mathbb {A}{)}}$ also includes the term t.

Example 5

${Cap}{{(}cons{{(}[a\mapsto H]{\cdot }F,T{)}},\{ b,c \}{)}}=\{ b,c,cons~b, cons~c, cons{{(}b,b{)}},$

$cons{{(}b,c{)}},cons{{(}c,b{)}},cons{{(}c,c{)}}, cons{{(}b,T{)}},cons{{(}c,T{)}}, cons{{(}[a\mapsto b]{\cdot }F,b{)}},$

$cons{{(}[a\mapsto c]{\cdot }F,b{)}},cons{{(}[a\mapsto b]{\cdot }F,c{)}},cons{{(}[a\mapsto c]{\cdot }F,c{)}},cons{{(}[a\mapsto b]{\cdot }F,T{)}},$

$cons{{(}[a\mapsto c]{\cdot }F,T{)}}, cons{{(}[a\mapsto H]{\cdot }F,b{)}}, {{(}[a\mapsto H]{\cdot }F,c{)}}, cons{{(}[a\mapsto H]{\cdot }F,T{)}} \}.$

The function $\varPsi$ is used to handle constraints of the form $\phi \hat{\ } \pi {\cdot }X\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}\phi ' \hat{\ } \pi '{\cdot }X$ or $a\mathbin {{\#}}\phi \hat{\ } \pi {\cdot }X$, i.e., $\varPsi$ deals with the premises of rules $\mathrm {\scriptstyle \mathbf (\mathbin {{\approx }_{\scriptstyle {\alpha }}}X)}$ and $\mathrm {\scriptstyle \mathbf (\mathbin {{\#}}X)}$ (see Definition 2).

Definition 11

(Function $\varPsi$). Let s and t be either two moderated variables $\phi \hat{\ } \pi {\cdot }X$ and $\phi ' \hat{\ } \pi '{\cdot }X$, or an atom a and a moderated variable $\phi \hat{\ } \pi {\cdot }X$. Let $\mathbf {P}$ be a matching problem, $\mathbb {A}$ a finite set of atoms and b an atom in $\mathbb {A}$. Then, $\varPsi (s,t)^{\mathbb {A}} =\varPsi '(s,t,\varnothing )^{\mathbb {A}}$ where $\varPsi '$ computes a set of problems (i.e., a collection of sets of constraints) as follows: $\varPsi '(s,t,\mathbf {P})^{\mathbb {A}} \triangleq$

$\varPsi '$ deals with one atom from the given finite set $\mathbb {A}$ in each recursive call (thus ensuring termination); the order in which elements of $\mathbb {A}$ are considered is irrelevant since $\varPsi '{{(}s,t,\mathbf {P}{)}}^{\mathbb {A}}$ is a collection of sets. Hence $\varPsi '$ is indeed a function.

Freshness constraints of form $a\mathbin {{\#}}a$ are inconsistent. A matching constraint $s\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}t$ is clashing when s, t have different term constructors at the root except if s is a moderated variable $\phi \hat{\ } \pi {\cdot }X$ and $X \not \in V_{RHS} (\mathbf {P})$. For example, if $V_{RHS} {(\mathbf {P})}=\{Y\}$ then $a\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}(a\ b) {\cdot }Y$, $f\, a \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}g\, a$ and $[a\mapsto b] {\cdot }Y \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}[b]a$ are clashing but $[a\mapsto b] {\cdot }X \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}f {{(}c,b{)}}$ and $[a\mapsto b] {\cdot }Y \mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}[b\mapsto a] {\cdot }Y$ are not. Clashing and inconsistent constraints are not derivable; failure rules ($\bot$) will be specified to deal with them.

Definition 12

(Matching steps). Let $\mathbf {P}_0$ be a matching problem and $\mathbb {X}=V_{RHS} (\mathbf {P}_0)$. $\mathcal {P}, \mathcal {Q}$ denote sets of pairs $(\mathbf {P},\theta )$, where $\mathbf {P}$ is a unification problem and $\theta$ a v-substitution. Write (resp. $\mathcal {P}\Longrightarrow _{{\scriptscriptstyle \mathbin {{\#}}}} \mathcal {Q}$), if $\mathcal {Q}$ is obtained from $\mathcal {P}$ by application of one matching (resp. freshness) reduction rule below. As usual, $\Longrightarrow _{{\scriptscriptstyle \mathbin {{}_{\scriptstyle {?}}{\approx }}}}^*$ (resp. $\Longrightarrow _{{\scriptscriptstyle \mathbin {{\#}}}}^*$) denotes reflexive transitive closure; arrow subindices are omitted if there is no ambiguity.

¹

Rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}\equiv )}$ has priority; it is an optimisation to reduce trivial matching constraints in one step, subsuming rule $\mathrm {\scriptstyle \mathbf (\mathbin {{\approx }_{\scriptstyle {\alpha }}}a)}$ (Definition 2). The right-hand side of rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}\bot )}$ is the empty set since this pair cannot produce solutions (but other pairs in the problem could, so we do not use $\bot$). Rules $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}Inst)}$ and $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}{XY})}$ are instantiating rules. Note that the matching steps in Definition 12 provide an algorithmic presentation of Definition 2, where instantiating rules have been added and the symbol $\mathbin {{\approx }_{\scriptstyle {\alpha }}}$ has been replaced by $\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}$ to represent the constraints to be solved.

Termination of the simplification process follows from the fact that the instantiating rules decrease the number of variables in the problem. For any other rule, an interpretation based on the multiset of sizes of the constraints in the problem can be shown to be strictly decreasing using the multiset extension of the standard ordering on natural numbers, $\le _{mul}$. Confluence under the imposed strategy then follows by Newman’s Lemma, since there are only trivial overlaps. Hence normal forms are unique.

Remark 1

(Matching algorithm). The algorithm has two phases.

Input: Assume $\mathbf {P}_0$ is the given matching problem, where $\mathbb {X} = V_{RHS} (\mathbf {P}_0)$.

where $\langle \mathbf {P}_0\rangle _{\mathtt {nf_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}}}$ is the normal form of $\{ (\mathbf {P}_0,\mathsf {Id}) \}$ by application of $\Longrightarrow _{{\scriptscriptstyle \mathbin {{}_{\scriptstyle {?}}{\approx }}}}$.

$\forall (\mathbf {P}_i, \theta _i) \in \langle \mathbf {P}_0\rangle _{\mathtt {nf_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}}}$, compute $\{\mathbf {P}_i\} {\mathop {\Longrightarrow }\limits ^{\scriptstyle }}_{\mathbin {{\#}}}^{*} \langle \mathbf {P}_i\rangle _{\mathtt {nf_{\mathbin {{\#}}}}}$ where $\langle \mathbf {P}_i\rangle _{\mathtt {nf_{\mathbin {{\#}}}}}$ is the normal form of the set of freshness constraints $\mathbf {P}_i$ by application of $\Longrightarrow _{{\scriptscriptstyle \mathbin {{\#}}}}$.

Output: $\langle \mathbf {P}_0\rangle _{\mathtt { {out}}}=\{ (\langle \mathbf {P}_i\rangle _{\mathtt {nf_{\mathbin {{\#}}}}}\setminus \bot ,\theta _i)\mid {{(}\mathbf {P}_{i},\theta _i{)}}\in \langle \mathbf {P}_0\rangle _{\mathtt {nf_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}}}, \langle \mathbf {P}_i\rangle _{\mathtt {nf_{\mathbin {{\#}}}}}\not =\bot \}$.

Informally, Phase 1 reduces the matching problem until no matching constraints are left, resolving into a set of pairs $(\{C_{ij}\},\theta _i) (i,j \in Nat)$ where each $C_{ij}$ is a (possibly empty) set of freshness constraints and $\theta _i$ a v-substitution. Then, Phase 2 reduces each $C_{ij}$ into freshness contexts $C'_{ij}$, discarding along the way any set $C_{ij}$ containing inconsistent freshness constraints. Finally, the remaining pairs $(C'_{ij},\theta _i)$ in the set are solutions to the initial matching problem $\mathbf {P}_0$. If no pairs are left, i.e., all sets of freshness constraints have been discarded, then the matching problem is unsolvable.

Example 6

The matching problem $\mathbf {P}={{(}\{[a\mapsto Y]{\cdot }X\mathbin {{}_{\scriptstyle {?}}{\approx }}[a\mapsto b]{\cdot }Z\}{)}}$ has principal solutions ${{(}\{a \mathbin {{\#}}Z\}, [X \mapsto Z]{)}}$, ${{(}\varnothing , [X \mapsto Z; Y \mapsto b]{)}}$, ${{(}\varnothing , [X \mapsto [a\mapsto b] {\cdot }Z]{)}},$ ${{(}\{a \mathbin {{\#}}Z\}, [X \mapsto a; Y \mapsto Z]{)}}$, ${{(}\varnothing , [X \mapsto a; Y \mapsto [a\mapsto b] {\cdot }Z]{)}}$ computed by the algorithm as follows. Below, the affected parts of each reduction are highlighted and outer brackets in singleton collections of freshness contexts are omitted for readability. Here $V_{RHS}(\mathbf {P}) = \{Z\}$.

Phase 2 is trivial and thus omitted.

As a consequence of the termination and confluence properties, the relation $\Longrightarrow _{{\scriptscriptstyle }}$ defines a function from matching problems to their unique normal form. Write $\langle \mathbf {P}\rangle _{\mathtt { {out}}}$ for the normal form of $\{(\mathbf {P},\mathsf {Id})\}$. $\langle \mathbf {P}\rangle _{\mathtt { {out}}}$ may contain solutions $(\mathbf {F} ,\sigma ), (\mathbf {F} ',\sigma ')$ with $\alpha$-equivalent substitutions but different collections of freshness contexts. For instance, $(\varnothing , [X \mapsto a;Y\mapsto [a\mapsto b] {\cdot }Z])$ and $(\{ a \mathbin {{\#}}Z \}, [X\mapsto a; Y\mapsto Z])$ in Example 6 could be merged as $(\varnothing , [X \mapsto a;Y\mapsto [a\mapsto b] {\cdot }Z])$.

Definition 13

(Merging solutions). Let W be a set of solutions, such that there are two different elements $(\mathbf {F} ,\sigma )$ and $(\mathbf {F} ',\sigma ')$ in W satisfying $\forall \varDelta \in \mathbf {F}.\varDelta \vdash \sigma \mathbin {{\approx }_{\scriptstyle {\alpha }}}\sigma '$. This pair of solutions can be replaced with a single solution as follows:

$$\begin{aligned} \mathrm {\scriptstyle \mathbf ([W_1])} \qquad (\mathbf {F} ,\sigma ), (\mathbf {F} ',\sigma ') \quad \Longrightarrow _{{\scriptscriptstyle [W]}} \quad (\mathbf {F} '\cup \mathbf {F},\sigma ') \end{aligned}$$

Further, if $(\mathbf {F} ,\sigma )$ contains the empty set as one of the freshness contexts in $\mathbf {F}$, then any other freshness context in $\mathbf {F}$ is redundant and can be discarded:

$$\begin{aligned} \mathrm {\scriptstyle \mathbf ([W_2])} \quad (\mathbf {F} ,\sigma ) \quad \Longrightarrow _{{\scriptscriptstyle [W]}} \quad {{(}\{\varnothing \},\sigma {)}}\quad \text {if } \mathbf {F}\not =\{\varnothing \},~\varnothing \in \mathbf {F} \end{aligned}$$

Write [W] for the normal form of W by the rules above. $\langle \mathbf {P}\rangle _{\mathtt { {sol}}}$ denotes the normal form by $\mathrm {\scriptstyle \mathbf ([W_1])}$ and $\mathrm {\scriptstyle \mathbf ([W_2])}$ of $\langle \mathbf {P}\rangle _{\mathtt { {out}}}$, that is: $\langle \mathbf {P}\rangle _{\mathtt { {sol}}} = [\langle \mathbf {P}\rangle _{\mathtt { {out}}}]$.

Example 7

(Merging solutions). By application of rules $[W_1]$ and $[W_2]$ to the solution set W from Example 6, solution ${{(}\varnothing , [X\mapsto a;Y\mapsto [a\mapsto b]{\cdot }Z] {)}}$ replaces in W the pair ${{(}\varnothing , [X\mapsto a;Y\mapsto [a\mapsto b]{\cdot }Z] {)}}$, ${{(}\{a\mathbin {{\#}}Z\}, [X\mapsto a;Y\mapsto Z] {)}}$. Similarly, ${{(} \varnothing , [X \mapsto [a\mapsto b]{\cdot }Z] {)}}$ replaces the pair ${{(}\varnothing , [X\mapsto [a\mapsto b]{\cdot }Z] {)}}$, ${{(}\{a\mathbin {{\#}}Z\}, [X\mapsto Z] {)}}$.

Theorem 1

(Soundness and completeness).$\langle \mathbf {P}\rangle _{\mathtt { {sol}}}\subseteq \mathcal {U}(\mathbf {P})$ (soundness);

$\forall (\mathbf {F} ,\sigma )\in \mathcal {U}(\mathbf {P})$, $\exists (\mathbf {F} _{i},\theta _i)\in \langle \mathbf {P}\rangle _{\mathtt { {sol}}}$ such that $(\mathbf {F} _{i},\theta _i)\le (\mathbf {F} ,\sigma )$ (completeness).

5 Unitary Matching for Simple Problems

When using matching to generate, for instance, rewrite steps for a given nominal rewriting rule, it is useful to have a unique most general matching solution. Below we characterise a class of matching constraints, which we call simple, for which matching is unitary. The idea is to require each variable symbol in a pattern to have at least one occurrence with trivial suspended a-substitution ($\mathsf {Id}$) and not in a suspension (see below). Constraints whose pattern is a moderated variable with non-trivial a-substitutions will be postponed.

Moderated variables occurring in suspended a-substitutions will be called suspended (variable) occurrences, and the others will be called fixed (variable) occurrences. For instance, in the term ${{(}[a\mapsto Z]{\cdot }X,[a\mapsto b]{\cdot }Y{)}}$, both $[a\mapsto Z]{\cdot }X$ and $[a\mapsto b]{\cdot }Y$, are fixed, but Z is a suspended occurrence since it occurs in the image of the a-substitution suspended over X. Write $V _{f} (t)$ for the subset of $V (t)$ such that each variable has at least one fixed occurrence with trivial a-substitutions. The set $V _{f} (t)$ will play an important role in the characterisation of unitary matching problems.

Definition 14

A term s is simple if $V (s) \subseteq V _f(s)$, that is, for each variable $X \in V (s)$ there is one or more fixed occurrences of the form $\mathsf {Id}\hat{~}\pi {\cdot }X$.²

A simple matching constraint is a matching constraint $s \mathbin {{}_{\scriptstyle {?}}{\approx }}t$ such that s is a simple term and $V (s) \cap V (t) =\varnothing$. A simple matching problem is a problem as specified in Definition 7 where ${{(}\ldots ,s_i,\ldots {)}}\mathbin {{}_{\scriptstyle {?}}{\approx }}{{(}\ldots , t_i, \ldots {)}}$ is simple.³

Example 8

The constraints $\mathtt {cons}([a\mapsto Y]{\cdot }X, \mathtt {map}{{(}[b]X,Y{)}}) \mathbin {{}_{\scriptstyle {?}}{\approx }}\mathtt {cons}{{(}H,\mathtt {nil}{)}}$ and $\mathtt {map}{{(}[a]X,\mathtt {cons}{{(}Y,\mathtt {nil}{)}}{)}} \mathbin {{}_{\scriptstyle {?}}{\approx }}\mathtt {map}{{(}[a\mapsto H]{\cdot }F,\mathtt {cons}{{(}H,\mathtt {nil}{)}}{)}}$ are simple but the constraint $\mathtt {map}([a\mapsto Y]{\cdot }X, X)\mathbin {{}_{\scriptstyle {?}}{\approx }}\mathtt {map}([a\mapsto \mathtt {nil}]{\cdot }F, F)$ is not; the latter does not have a simple pattern term, there is no fixed occurrence of Y.

Given a simple matching problem $\mathbf {P}$, postponed constraints (of the form $\phi \hat{\ } \pi {\cdot }X \mathbin {{}_{\scriptstyle {?}}{\approx }}t$ where $t\not =\phi ' \hat{\ } \pi '{\cdot }X$, $\phi \not =\mathsf {Id}$ and $X\not \in \{ X \mid s\mathbin {{}_{\scriptstyle {?}}{\approx }}t\in \mathbf {P}, X\in V (t) \}$) are delayed until an instantiation for X is readily available. The definition of simple constraint (Definition 14) ensures such instantiation exists. The matching rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}XY)}$ is not included in the simple-matching algorithm and rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}Inst)}$ is adapted following the standard instantiating rule (see [28, Fig. 3]) as follows.

Definition 15

(Simple-matching algorithm). Let $\mathbf {P}$ be a simple matching problem, $\mathbb {X} = V_{RHS}(\mathbf {P})$ and assume $X \not \in \mathbb {X}$. Take the rule set of Definition 12, discard rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}XY)}$ and replace rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}Inst)}$ with:

$\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}\sigma )}~ (\{\pi {\cdot }X\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}t\} \cup \mathbf {P},\theta ) {\mathop {\Longrightarrow }\limits ^{\scriptstyle \mathbb {X}}}_{\mathbin {{}_{\scriptstyle {?}}{\approx }}} (\mathbf {P}[X \mapsto \pi ^{\text {-}1}{\cdot }t], \theta \bullet [X \mapsto \pi ^{\text {-}1}{\cdot }t])$

The simple-matching algorithm follows the two-phase reduction strategy described in Remark 1, using the modified rule set where rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}\sigma )}$ has the highest priority along with rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}\equiv )}$, rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}X)}$ has the lowest priority and all other rules have equal priority. Let $\langle \mathbf {P}\rangle _{\mathtt {nf_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}}}$ be the normal form of $\mathbf {P}$ with respect to the set of updated rules.

The priority imposed on rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}\sigma )}$ forces the generation of v-substitutions as soon as possible, whilst by giving lowest precedence to the rule $\mathrm {\scriptstyle \mathbf (\mathbin {{}_{\scriptstyle {?}}{\approx }}X)}$, we ensure it is simply checking $\alpha$-equality (as specified by $\mathrm {\scriptstyle \mathbf (\mathbin {{\approx }_{\scriptstyle {\alpha }}}X)}$) since no variables are left to be instantiated. As a result, each distinct solution $(\mathbf {F} ,\sigma )$ from the solution set W shares the same unifier, $\sigma$, and by application of the merging rule to W in the final part of the algorithm, the solution set is reduced to $[W] =\{ (\bigcup \mathbf {F}, \sigma ) \}$. We formalise this claim in Theorem 2. Write $\mathtt {Match}(\mathbf {P},V _{RHS}(\mathbf {P}))$ for the normal form of the matching problem $\mathbf {P}$ by the simple-matching algorithm (Definition 15). Then, $\langle \mathbf {P}\rangle _{\mathtt { {sol}}_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}}$ is the result of applying function $[\cdot ]$ from Definition 13 to $\mathtt {Match}(\mathbf {P},V _{RHS}(\mathbf {P}))$. The following theorem is the main result of this section.

Theorem 2

(Normal form of a simple problem). Given a simple matching problem $\mathbf {P}$, either $\langle \mathbf {P}\rangle _{\mathtt { {sol}}_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}} =[\mathtt {Match}(\mathbf {P},V _{RHS}(\mathbf {P}))] =\{ (\mathbf {F} ,\theta ) \}$ and $(\mathbf {F} ,\theta )$ is a solution for $\mathbf {P}$, or $\langle \mathbf {P}\rangle _{\mathtt { {sol}}_{\mathbin {{}_{\scriptstyle {?}}{\approx }}}}=\varnothing$ and $\mathbf {P}$ has no solution.

Example 9

The rewriting rules in Example 3 have simple terms as patterns and the rewrite relation generated uses only simple matching: indeed, all the terms used in left-hand sides of rewrite rules are standard nominal terms (without atom substitutions), only the matched terms may have a-substitutions.

A-substitutions are used in the right-hand side of rules in Example 3 to implement function application in a direct way (avoiding the introduction of an additional set of rewrite rules to define non-capturing atom substitution as in standard nominal rewriting systems).

6 Undecidability of Extended Nominal Unification

To prove the undecidability of extended nominal unification, we encode Hilbert’s tenth problem, proved undecidable in [22]. The main idea is to build unification problems for which ground unifiers simulate addition or multiplication. Then, one can represent Diophantine equations. To simplify the encoding, we consider a restricted language.

Definition 16

$\mathtt {L}$-terms are generated from a triple $(\mathcal {A}, \mathcal {X},\mathcal {F}_L)$ of pairwise disjoint sets, where $\mathcal {F}_L$ is empty and $\mathcal {X},\mathcal {A}$ are countable sets of variables and atoms respectively (as described in Sect. 2), using the grammar given in Definition 1 without abstraction terms.

Our representation of natural numbers is inspired by Goldfarb numbers [18], which are themselves inspired by Church numerals. In $\mathtt {L}$, the natural number n is written: $\overline{n}_{a}c={{(}a,{{(}a,\ldots {{(}a,c{)}}{)}}{)}}$ with n occurrences of a and a single occurrence of c, where $a, c\in \mathcal {A}$. $\mathtt {L}$-terms of this form, which we call $\mathtt {L}$-Goldfarb numbers, are exactly those that solve extended nominal unification problems of the form

$$\begin{aligned} \{{{(}a,[c\mapsto a]{\cdot }F{)}}\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}[c\mapsto {{(}a,a{)}}]{\cdot }F\}. \end{aligned}$$

(1)

Example 10

($\mathtt {L}$-Goldfarb numbers). The number 0 is represented as $\overline{0}_{a} c$, that is, c; the number 1 is represented as $\overline{1}_{a} c=(a,c)$; 3 is represented as $\overline{3}_{a} c=(a,(a,(a,c)))$. The term $\overline{2}_{a}(\overline{1}_{a}a)$ is in $\mathtt {L}$ but is not an $\mathtt {L}$-Goldfarb number (it does not solve Eq. 1). Note also that, $\overline{2}_{a}(\overline{1}_{a}a) =(a,(a,(a,a)))=\overline{2+1}_{a}a$.

To simulate addition, we adapt Church’s $\lambda$-term $add=\lambda n.\lambda m.\lambda x.n{{(}m{{(}x{)}}{)}}$: we use a constraint $[c\mapsto X_i]{\cdot }X_j\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}X_k$. To simulate multiplication we use nested a-substitutions. Undecidability of extended nominal unification follows from Lemmas 1 and 2.

Lemma 1

(Addition). For all $m,n,p\ge 0$, there exists a ground unifier $\theta$ for the unification problem $\{[c\mapsto X_i]{\cdot }X_j\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}X_k\}$ such that $\{ [X_i\mapsto \overline{n}_{a}c; X_j\mapsto \overline{m}_{a}c; X_k\mapsto \overline{p}_{a}c]\}\subseteq \theta$ if and only if $p=m+n$.

Lemma 2

(Multiplication). Let $\mathbf {P}^{\times }=\{s_1\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}s_2, s_3\mathbin {{}_{\scriptstyle {?}}{\approx }_{\scriptstyle {?}}}s_4\}$ where

$s_1=[c_1\mapsto a;c_2\mapsto b;c_3\mapsto {{(}{{(}[c\mapsto a]{\cdot }X_{k},[c\mapsto b]{\cdot }X_{j}{)}},a{)}}]{\cdot }G$,

$s_2={{(}{{(}a,b{)}},[c_1\mapsto [c\mapsto a]{\cdot }X_{i}; c_2\mapsto \overline{1}_{a}b; c_3\mapsto a]{\cdot }G{)}}$,

$s_3=[c_1\mapsto b;c_2\mapsto a;c_3\mapsto {{(}{{(}[c\mapsto b]{\cdot }X_{k},[c\mapsto a]{\cdot }X_{j}{)}},b{)}}]{\cdot }G$,

$s_4={{(}{{(}b,a{)}},[c_1\mapsto [c\mapsto b]{\cdot }X_{i}; c_2\mapsto \overline{1}_{a}a; c_3\mapsto b]{\cdot }G{)}}$.

For all $m,n,p\ge 0$, there is a ground unifier $\theta$ for $\mathbf {P}^{\times }$ such that $\sigma =[X_{i}\mapsto \overline{m}_{a}c; X_{j}\mapsto \overline{n}_{a}c; X_{k}\mapsto \overline{p}_{a}c]$ and $\sigma \subset \theta$ if and only if $p= m\times n$.

Theorem 3

There is an effective reduction of Hilbert’s tenth problem to nominal unification of $\mathtt {L}$-terms. Therefore unification of extended terms is undecidable.

7 Conclusion

The matching algorithm provided in this paper induces a notion of rewriting that avoids the need to introduce extra rules to encode non-capturing substitutions. In future work, we will analyse the relationship between higher-order matching/unification and the corresponding problems in our language. The study of the complexity of the algorithms and the development of efficient implementations using graph representations of terms will also be subject of future research.