Nominal C-Unification

Abstract

Nominal unification is an extension of first-order unification that takes into account the $\alpha$-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixed point constraints, whose solutions can be generated by algebraic techniques on combinatorics of permutations.

Work supported by the Brazilian agencies FAPDF (DE 193.001.369/2016), CAPES (Proc. 88881.132034/2016-01, 2nd author) and CNPq (PQ 307009/2013, 1st author).

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

1 Introduction

Unification, where the goal is to solve equations between first-order terms, is a key notion in logic programming systems, type inference algorithms, protocol analysis tools, theorem provers, etc. Solutions to unification problems are represented by substitutions that map variables ($X, Y, \dots$) to terms.

When terms include binding operators, a more general notion of unification is needed: unification modulo $\alpha$-equivalence. In this paper, we follow the nominal approach to the specification of binding operators [20, 26, 30], where the syntax of terms includes, in addition to variables, also atoms ($a, b, \dots )$, which can be abstracted, and $\alpha$-equivalence is axiomatised by means of a freshness relation $a\#t$ and name-swappings $(a\,b)$. For example, the first-order logic formula $\forall a. a \ge 0$ can be written as a nominal term $\forall ([a]geq(a,0))$, using function symbols $\forall$ and geq and an abstracted atom a. Nominal unification [30] is the problem of solving equations between nominal terms modulo $\alpha$-equivalence; it is a decidable problem and efficient nominal unification algorithms are available [9, 11, 24], that compute solutions consisting of freshness contexts (containing freshness constraints of the form $a\# X$) and substitutions.

In many applications, operators obey equational axioms. Nominal reasoning and unification have been extended to deal with equational theories presented by rewrite rules (see, e.g., [5, 17, 18]) or defined by equational axioms (see, e.g., [14, 19]). The case of associative and commutative nominal theories was considered in [3], where a parametric $\{\alpha , AC\}$-equivalence relation was formalised in Coq. However, only equational deduction was considered (not unification). In this paper, we study nominal C-unification.

Contributions: We present a nominal C-unification algorithm, based on a set of simplification rules. The algorithm transforms a given nominal C-unification problem $\langle {\Delta }, Q\rangle$, where ${\Delta }$ is a freshness context and Q a set of freshness constraints and equations, respectively of the form $a \#_? s$ and $s \approx _? t$, into a finite set of triples of the form $\langle \nabla ,\sigma , P\rangle$, consisting of a freshness context $\nabla$, a substitution $\sigma$ and a set of fixed point equations (for short, FP equations) P of the form $\pi .X \approx _? X$. The simplifications are based on a set of deduction rules for freshness and $\alpha$-C-equivalence (denoted as $\approx _{\{\alpha , C\}}$).

The role of FP equations in nominal C-unification is tricky: while in standard nominal unification [30], solving a FP equation of the form $(a \ b).X \approx _? X$ reduces to checking whether the constraints $a\# X, b \# X$ (a and b fresh in X) are satisfied, and in this case the solution is the identity substitution, in nominal C-unification, for $*$ and $+$ commutative operators, one can have additional combinatory solutions of the form $\{X/ a + b \}, \{X/(a + b)* \ldots * (a + b)\}$, $\{X/f(a)+f(b)\}$, etc. We show that in general there is no finitary representation of solutions using only freshness contexts and substitutions, hence a nominal C-unification problem may have a potentially infinite set of independent most general unifiers (unlike standard C-unification, which is well-known to be finitary).

We adapt the proof of NP-completeness of syntactic C-unification to show that nominal C-unification is NP-complete as well. Soundness and completeness of the simplification rules were formalised in Coq. The formalisation, an extended version of the paper with all proof details and an OCaml implementation are available at http://ayala.mat.unb.br/publications.html.

Related work: To generate the set of combinatorial solutions for FP equations we can use an enumeration procedure given in [4], which is based on the combinatorics of permutations. By combining the simplification and enumeration methods, we obtain a nominal C-unification procedure in two phases: a simplification phase, described in this paper, which outputs a finite set of most general solutions that may include FP constraints, and a generation phase, which eliminates the FP constraints according to [4].

Several extensions of the nominal unification algorithm have been defined, in addition to the equational extensions already mentioned.

An algorithm for nominal unification of higher-order expressions with recursive let was proposed in [23]; as in the case of nominal C-unification, FP equations are obtained in the process. Using the techniques in [4], it is possible to proceed further and generate the combinatorial solutions of FP equations.

Recently, Aoto and Kikuchi [1] proposed a rule-based procedure for nominal equivariant unification [13], an extension of nominal unification that is useful in confluence analysis of nominal rewriting systems [2, 16].

Furthermore, several formalisations and implementations of the nominal unification algorithm are available. For example, formalisations of its soundness and completeness were developed by Urban et al [29, 30], Ayala-Rincón et al [6], and Kumar and Norrish [22] using, respectively, the proof assistants Isabelle/HOL, PVS and HOL4. An implementation in Maude using term graphs [10] is also available. Urban and Cheney used a nominal unification algorithm to develop a Prolog-like language called $\alpha$-Prolog [12]. Our formalisation of nominal C-unification is based on the formalisation of equivalence modulo $\{\alpha , AC\}$ presented in [3]. The representations of permutations and terms are similar, but here we deal also with substitutions and unification rules, and prove soundness and completeness of the unification algorithm.

Reasoning modulo equational theories (but without considering the nominal approach to deal with $\alpha$-equivalence) has been subject of formalisations. For instance, Nipkow [25] presented a set of Isabelle/HOL tactics for reasoning modulo A, C and AC; Braibant and Pous [8] designed a plugin for Coq, with an underlying AC-matching algorithm, that extends the system tactic rewrite to deal with AC function symbols; also, Contejean [15] formalised in Coq the correction of an AC-matching algorithm implemented in CiME.

Syntactic unification with commutative operators is an NP-complete problem and its solutions can be finitely generated [21, 28]. Since C-unification problems are a particular case of nominal C-unification problems, our simplification algorithm, checked in Coq, is also a formalisation of the C-unification algorithm.

Organisation: Section 2 presents basic concepts and notations. Section 3 introduces the formalised equational and freshness inference rules for nominal C-unification, and briefly discusses NP-completeness; Sect. 4 shows that a single FP equation can have infinite independent solutions; Sect. 5 shortly discusses the formalisation in Coq and Sect. 6 concludes and proposes future work.

2 Background

Consider countable disjoint sets of variables ${\mathcal {X}} := \{X, Y, Z, \cdots \}$ and atoms ${\mathcal {A}} := \{a, b, c, \cdots \}$. A permutation $\pi$ is a bijection on $\mathcal {A}$ with a finite domain, where the domain (i.e., the support) of $\pi$ is the set $dom(\pi ) := \{a \in {\mathcal {A}}\;|\;\pi \cdot a \ne a\}$. The inverse of $\pi$ is denoted by $\pi ^{-1}$. Permutations can be represented by lists of swappings, which are pairs of different atoms $(a\,b)$; hence a permutation $\pi$ is a finite list of the form $(a_1\,b_1)\,{:}{:}\,\ldots \,{:}{:}\,(a_n\,b_n)\,\,{:}{:}\,\, {nil }$, where the empty list nil corresponds to the identity permutation; concatenation is denoted by $\oplus$ and, when no confusion may arise,  :  :  and nil are omitted. We follow Gabbay’s permutative convention: Atoms differ on their names, so for atoms a and b the expression $a\ne b$ is redundant. Also, $(a\,b)$ and $(b\,a)$ have identical action: they exchange a and b; thus, they represent the same swapping.

We will assume as in [3] countable sets of function symbols with different equational properties such as associativity, commutativity, idempotence, etc. Function symbols have superscripts that indicate their equational properties; thus, $f^C_k$ will denote the $k^{th}$ function symbol that is commutative and $f^\emptyset _j$ the $j^{th}$ function symbol without any equational property.

Nominal terms are generated by the following grammar:

$$\begin{aligned} s, t := \langle \rangle \,\,|\,\, \bar{a} \,\,|\,\, [a]t \,\, | \,\,\langle s, t\rangle \,\,|\,\, f^E_k\,t \,\,|\,\, \pi .X \end{aligned}$$

$\langle \rangle$ denotes the unit (that is the empty tuple), $\bar{a}$ denotes an atom term, [a]t denotes an abstraction of the atom a over the term t, $\langle s, t\rangle$ denotes a pair, $f^E_k\,t$ the application of $f^E_k$ to t and, $\pi .X$ a moderated variable or suspension. Suspensions of the form ${ nil} . X$ will be represented just by X.

The set of variables occurring in a term t will be denoted as Var(t). This notation extends to a set S of terms in the natural way: $Var(S) = \bigcup _{t \in S} Var(t)$. As usual, $|\,\_ \,|$ will be used to denote the cardinality of sets as well as to denote the size or number of symbols occurring in a given term.

Definition 1

(Permutation action). The action of a permutation on atoms is defined as: $\text{ nil }\cdot a := a$; $(b\,c)\,\,{:}{:}\,\,\pi \cdot a := \pi \cdot a$; and, $(b\,c)\,\,{:}{:}\,\,\pi \cdot b := \pi \cdot c$. The action of a permutation on terms is defined recursively as:

Notice that according to the definition of the action of a permutation over atoms, the composition of permutations $\pi$ and $\pi '$, usually denoted as $\pi \circ \pi '$, corresponds to the append $\pi '\oplus \pi$. Also notice that $\pi '\oplus \pi \cdot t = \pi \cdot (\pi '\cdot t$). The difference set between two permutations $\pi$ and $\pi '$ is the set of atoms where the action of $\pi$ and $\pi '$ differs: $ds(\pi ,\pi ') := \{a \in {\mathcal {A}} \;|\; \pi \cdot a \ne \pi '\cdot a\}$.

A substitution $\sigma$ is a mapping from variables to terms such that its domain, $dom(\sigma ) :=\{X \mid X\ne X\sigma \}$, is finite. For $X\in dom(\sigma )$, $X\sigma$ is called the image of X. Define the image of $\sigma$ as $im(\sigma ) := \{X\sigma \mid X\in dom(\sigma )\}$. Let $dom(\sigma ) = \{X_1, \cdots , X_n\}$, then $\sigma$ can be represented as a set of bindings in the form $\{X_1/t_1, \cdots , X_n/t_n\}$, where $X_i\sigma = t_i$, for $1 \le i \le n$.

Definition 2

(Substitution action). The action of a substitution $\sigma$ on a term t, denoted $t\sigma$, is defined recursively as follows:

$\begin{array}{lcl@{}lcl@{}lcl} \langle \rangle \sigma &{} := &{} \langle \rangle &{} \overline{a}\sigma &{} := &{} \overline{a} &{} (f_k^E\,t)\sigma &{} := &{} f_k^E\,t\sigma \\ \langle s, t\rangle \sigma &{} := &{}\langle s\sigma , t\sigma \rangle &{} ([a]t)\sigma &{} := &{} [a]t\sigma &{} (\pi .X)\sigma &{} := &{} \pi \cdot X\sigma \end{array}$

The following result can be proved by induction on the structure of terms.

Lemma 1

(Substitutions and Permutations Commute). $(\pi \cdot t)\sigma = \pi \cdot (t\sigma )$

The inference rules defining freshness and $\alpha$-equivalence are given in Figs. 1 and 2. The symbols $\nabla$ and ${\Delta }$ are used to denote freshness contexts that are sets of constraints of the form $a\#X$, meaning that the atom a is fresh in X. The domain of a freshness context $dom(\nabla )$ is the set of atoms appearing in it; $\nabla |_X$ denotes the restriction of $\nabla$ to the freshness constraints on X: $\{a\#X\;|\; a\#X\in \nabla \}$. The rules in Fig. 1 are used to check if an atom a is fresh in a nominal term t under a freshness context $\nabla$, also denoted as $\nabla \vdash a\#t$. The rules in Fig. 2 are used to check if two nominal terms s and t are $\alpha$-equivalent under some freshness context $\nabla$, written as $\nabla \vdash s\approx _\alpha t$. These rules use the inference system for freshness constraints: specifically freshness constraints are used in rule $\mathbf {(\approx _\alpha [ab])}$.

Example 1

Let $\sigma = \{X/[a]a\}$. Verify that $\langle (a \ b ). X, f(e)\rangle \sigma \approx _{\alpha } \langle X, f(e)\rangle \sigma$.

By $dom(\pi )\#X$ and $ds(\pi ,\pi ')\#X$ we abbreviate the sets $\{a\#X\;|\;a \in dom(\pi )\}$ and $\{a\#X\;|\;a \in ds(\pi ,\pi ')\}$, respectively.

Fig. 1.

Rules for the freshness relation

Fig. 2.

Rules for the relation $\approx _\alpha$

Key properties of the nominal freshness and $\alpha$-equivalence relations have been extensively explored in previous works [3, 6, 29, 30].

2.1 The Relation $\approx _{\{\alpha , C\}}$ as an Extension of $\approx _\alpha$

In [3], the relation $\approx _\alpha$ was extended to deal with associative and commutative theories. Here we will consider $\alpha$-equivalence modulo commutativity, denoted as $\approx _{\{\alpha , C\}}$. This means that some function symbols in our syntax are commutative, and therefore the rule for function application $\mathbf {(\approx _\alpha app)}$ in Fig. 2 should be replaced by the rules in Fig. 3.

Fig. 3.

Additional rules for $\{\alpha ,C\}$-equivalence

The following properties for $\approx _{\{\alpha , C\}}$ were formalised as simple adaptations of the formalisations given in [3] for $\approx _\alpha$.

Lemma 2

(Inversion). The inference rules of $\approx _{\{\alpha , C\}}$ are invertible.

This means, for instance, that for rules $\mathbf {(\approx _\alpha [ab])}$ one has $\nabla \vdash [a]s \approx _{\{\alpha , C\}}[b]t$ implies $\nabla \vdash s \approx _{\{\alpha , C\}}(a\,b)\cdot t$ and $\nabla \vdash a \,\#\, t$; and for $\mathbf {(\approx _{\{\alpha , C\}}app)}$, $\nabla \vdash f^C_k\,\langle s_0, s_1 \rangle \approx _{\{\alpha , C\}}f^C_k\,\langle t_0, t_1 \rangle$ implies $\nabla \vdash s_0 \approx _{\{\alpha , C\}}t_0$ and $\nabla \vdash s_1 \approx _{\{\alpha , C\}}t_1$, or $\nabla \vdash s_0 \approx _{\{\alpha , C\}}t_1$ and $\nabla \vdash s_1 \approx _{\{\alpha , C\}}t_0$.

Lemma 3

(Freshness preservation). If $\nabla \vdash a\,\#\,s$ and $\nabla \vdash s \approx _{\{\alpha , C\}}t$ then $\nabla \vdash a\,\#\,t$.

Lemma 4

(Intermediate transitivity for $\approx _{\{\alpha , C\}}$ with $\approx _\alpha$). If $\nabla \vdash s \approx _{\{\alpha , C\}}t$ and $\nabla \vdash t \approx _\alpha u$ then $\nabla \vdash s \approx _{\{\alpha , C\}}u$.

Lemma 5

(Equivariance).  $\nabla \vdash \pi \cdot s \approx _{\{\alpha , C\}}\pi \cdot t$ whenever $\nabla \vdash s \approx _{\{\alpha , C\}}t$.

Lemma 6

(Equivalence).  $\_ \vdash \_ \approx _{\{\alpha , C\}}\_$ is an equivalence relation.

Remark 1

According to the grammar for nominal terms, function symbols have no fixed arity: any function symbol can apply to any term. Despite this, in the syntax of our Coq formalisation commutative symbols apply only to tuples.

3 A Nominal C-Unification Algorithm

Inference rules are given that transform a nominal C-unification problem into a finite family of problems that consist exclusively of FP equations of the form $\pi .X \approx _? X$, together with a substitution and a set of freshness constraints.

Definition 3

(Unification problem). A unification problem is a pair $\langle \nabla , P\rangle$, where $\nabla$ is a freshness context and P is a finite set of equations and freshness constraints of the form $s \approx _? t$ and $a \#_? s$, respectively, where $\approx _?$ is symmetric, s and t are terms and a is an atom. Nominal terms in the equations preserve the syntactic restriction that commutative symbols are only applied to tuples.

Given $\langle \nabla , P\rangle$, by $P_\approx , P_\#, P_{\text{ fp }_\approx }$ and $P_{\text{ nfp }_\approx }$ we will resp. denote the sets of equations, freshness constraints, FP and non FP equations in the set P.

Example 2

Given the nominal unification problem $\mathcal {P}\!=\!\langle \emptyset , \{[a][b]X \approx _? [b][a]X\}\rangle$, the standard unification algorithm [30] reduces it to $\langle \emptyset , \{X \approx _? (a\,b).X\}\rangle$, which gives the solution $\langle \{a\#X, b\#X\}, id \rangle$. However, we will see that infinite independent solutions are feasible when there is at least a commutative operator.

We design a nominal C-unification algorithm using one set of transformation rules to deal with equations (Fig. 4) and another set of rules to deal with freshness constraints and contexts (Fig. 5). These rules act over triples of the form $\langle \nabla , \sigma , P\rangle$, where $\sigma$ is a substitution. The triple that will be associated by default with a unification problem $\langle \nabla , P\rangle$ is $\langle \nabla , id , P\rangle$. We will use calligraphic uppercase letters (e.g., $\mathcal {P},\mathcal {Q},\mathcal {R},$ etc) to denote triples.

Remark 2

Let $\nabla$ and $\nabla '$ be freshness contexts and $\sigma$ and $\sigma '$ be substitutions.

• $\nabla ' \vdash \nabla \sigma$ denotes that $\nabla ' \vdash a\,\#\,X\sigma$ holds for each $(a \# X) \in \nabla$, and

• $\nabla \vdash \sigma \approx \sigma '$ that $\nabla \vdash X\sigma \approx _{\{\alpha , C\}}X\sigma '$ for all X (in $dom(\sigma ) \cup dom(\sigma ')$).

Definition 4

(Solution for a triple or problem). A solution for a triple ${\mathcal {P}} = \langle {\Delta }, \delta , P\rangle$ is a pair $\langle \nabla , \sigma \rangle$, where the following conditions are satisfied:

$$\begin{aligned} \begin{array}{@{}l@{}l} { 1.}~ \nabla \vdash {\Delta }\sigma ; &{} { 3.}~ \nabla \vdash s\sigma \approx _{\{\alpha , C\}}t\sigma , if \,\, s\,\, \approx _? t \in P;\\ { 2.} ~\nabla \vdash a \,\#\,t\sigma ,\,\, if\,\, a \#_? t \in P;~ &{} { 4.}~ there~is~ a~substitution~ \lambda ~ such~ that~\nabla \!\vdash \! \delta \lambda \!\approx \! \sigma . \end{array} \end{aligned}$$

A solution for a unification problem $\langle {\Delta }, P\rangle$ is a solution for the associated triple $\langle {\Delta }, id , P\rangle$. The solution set for a problem or triple ${\mathcal {P}}$ is denoted by $\mathcal {U}_C({\mathcal {P}})$.

Definition 5

(More general solution and complete set of solutions). For $\langle \nabla , \sigma \rangle$ and $\langle \nabla ', \sigma '\rangle$ in ${\mathcal {U}}_C({\mathcal {P}})$, we say that $\langle \nabla , \sigma \rangle$ is more general than $\langle \nabla ', \sigma '\rangle$, denoted $\langle \nabla , \sigma \rangle \preccurlyeq \langle \nabla ', \sigma '\rangle$, if there exists a substitution $\lambda$ satisfying $\nabla ' \vdash \sigma \lambda \approx \sigma '$ and $\nabla ' \vdash \nabla \lambda$. A subset $\mathcal {V}$ of ${\mathcal {U}}_C({\mathcal {P}})$ is said to be a complete set of solutions of $\mathcal {P}$ if for all $\langle \nabla ', \sigma '\rangle \in {\mathcal {U}}_C({\mathcal {P}})$, there exists $\langle \nabla , \sigma \rangle$ in $\mathcal {V}$ such that $\langle \nabla , \sigma \rangle \preccurlyeq \langle \nabla ', \sigma '\rangle$.

We will denote the set of variables occurring in the set P of a problem $\langle {\Delta }, P\rangle$ or triple ${\mathcal {P}}=\langle \nabla ,\sigma , P\rangle$ as Var(P). We also will write $Var({\mathcal {P}})$ to denote this set.

Fig. 4.

Reduction rules for equational problems

The unification algorithm proceeds by simplification. Derivation with rules of Figs. 4 and 5 is respectively denoted by $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$. Thus, $\langle \nabla ,\sigma ,P\rangle \Rightarrow _{\approx }\langle \nabla ,\sigma ',P'\rangle$ means that the second triple is obtained from the first one by application of one rule. We will use the standard rewriting nomenclature, e.g., we will say that $\mathcal {P}$ is a normal form or irreducible by $\Rightarrow _{\approx }$, denoted by $\Rightarrow _{\approx }$-nf, whenever there is no $\mathcal {Q}$ such that ${\mathcal {P}}\Rightarrow _{\approx }{\mathcal {Q}}$; $\Rightarrow _{\approx }^*$ and $\Rightarrow _{\approx }^+$ denote respectively derivations in zero or more and one or more applications of the rules in Fig. 4.

The only rule that can generate branches is $\mathbf {(\approx _?C)}$, which is an abbreviation for two rules providing the different forms in which one can relate the arguments s and t in an equation $f^C_k\,s \approx _? f^C_k\,t$ for a commutative function symbol (s, t are tuples, by the syntactic restriction in Definition 3): either $\langle s_0, s_1\rangle \approx _? \langle t_0, t_1\rangle$ or $\langle s_0, s_1\rangle \approx _? \langle t_1, t_0\rangle$.

The syntactic restriction on arguments of commutative symbols being only tuples, is not crucial since any equation of the form $f_k^C \pi . X \approx _? t$ can be translated into an equation of form $f_k^C \langle \pi .X_1, \pi .X_2\rangle \approx _? t$, where $X_1$ and $X_2$ are new variables and $\nabla$ is extended to $\nabla '$ in such a way that both $X_1$ and $X_2$ inherit all freshness constraints of X in $\nabla$: $\nabla ' =\nabla \cup \{a\#X_i \;|\; i=1,2, \text{ and } a\#X\in \nabla \}$.

In the rule $\mathbf {(\approx _? inst)}$ the inclusion of new constraints in the problem, given in

is necessary to guarantee that the new substitution $\sigma '$ is compatible with the freshness context $\nabla$.

Fig. 5.

Reduction rules for freshness problems

Examples 3, 4 and 5 are running examples of the C-unification procedure. A graphic representation of the derivation tree for these examples, generated using the OCaml implementation, is depicted in the extended version of this paper.

Example 3

Let $*$¹ be a commutative function symbol. Below, we show how the problem $\mathcal {P}=\langle \emptyset , \{[e](a\,b).X * Y \approx _? [f] (a\,c)(c\,d).X * Y\}\rangle$ reduces (via rules in Figs. 4 and 5). Application of rule $\mathbf {(\approx _? C)}$ gives two branches that reduce into two FP problems: ${\mathcal {Q}}_1$ and ${\mathcal {Q}}_2$. Highlighted terms show where the rules are applied. For brevity, let $\pi _1 = (a\,c)(c\,d)(e\,f)$, $\pi _2 = (a\,b)(e\,f)(c\,d)(a\,c)$, $\pi _3= (a\,c)(c\,d)(e\,f)(a\,b)$ and $\sigma =\{X / (e\,f)(a\,b).Y\}$.

Definition 6

(Set of $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$-normal forms). We denote by ${\mathcal {P}}_{\Rightarrow _{\approx }}$ (resp. ${\mathcal {P}}_{\Rightarrow _{\#}}$) the set of normal forms of ${\mathcal {P}}$ with respect to $\Rightarrow _{\approx }$ (resp. $\Rightarrow _{\#}$).

Definition 7

(Fail and success for $\Rightarrow _{\approx }$). Let ${\mathcal {P}}$ be a triple, such that the rules in Fig. 4 give rise to a normal form $\langle \nabla , \sigma , P\rangle$. The rules in Fig. 4 are said to fail if P contains non FP equations. Otherwise $\langle \nabla , \sigma , P\rangle$ is called a successful triple regarding $\Rightarrow _{\approx }$ (i.e., in a successful triple, P consists only of FP equations and, possibly, freshness constraints).

The rules in Fig. 5 will only be applied to successful triples regarding $\Rightarrow _{\approx }$.

Definition 8

(Fail and success for $\Rightarrow _{\#}$). Let ${\mathcal {Q}} = \langle \nabla , \sigma , Q\rangle$ be a successful triple regarding $\Rightarrow _{\approx }$, and ${\mathcal {Q}}' = \langle \nabla ', \sigma , Q'\rangle$ its normal form via rules in Fig. 5, that is ${\mathcal {Q}}\Rightarrow _{\#}^*{\mathcal {Q}}'$ and ${\mathcal {Q}}'$ is in ${\mathcal {Q}}_{\Rightarrow _{\#}}$. If $Q'$ contains freshness constraints it is said that $\Rightarrow _{\#}$ fails for $\mathcal {Q}$; otherwise, ${\mathcal {Q}}'$ will be called a successful triple for $\Rightarrow _{\#}$.

Remark 3

Since in a successful triple regarding $\Rightarrow _{\approx }$, $\mathcal {Q}$, one has only FP equations and $\Rightarrow _{\#}$ acts only over freshness constraints, $Q'$ in the definition above contains only FP equations and freshness constraints. Also, by a simple case analysis on t one can check that any triple with freshness constraints $a\#_?t$ is reducible by $\Rightarrow _{\#}$, except when $t\equiv \bar{a}$. Hence the freshness constraints in $Q'$ would be only of the form $a \#_? \bar{a}$.

The relation $\Rightarrow _{\approx }$, starts from a triple with the identity substitution and always maintains a triple $\langle \nabla , \sigma ', P' \rangle$ in which the substitution $\sigma '$ does not affect the current problem $P'$. The same happens for $\Rightarrow _{\#}$ since the substitution does not change with this relation. This motivates the next definition and lemma.

Definition 9

(Valid triple). ${\mathcal {P}} = \langle \nabla , \sigma , P \rangle$ is valid if $im(\sigma )\cap dom(\sigma ) = \emptyset$ and $dom(\sigma ) \cap Var(P) = \emptyset$.

Remark 4

A substitution $\sigma$ in a valid triple $\mathcal {P}$ is idempotent, that is, $\sigma \sigma = \sigma$.

Lemma 7 is proved by case analysis on the rules used by $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$.

Lemma 7

(Preservation of valid triples). If ${\mathcal {P}} = \langle \nabla , \sigma , P \rangle$ is valid and ${\mathcal {P}} \Rightarrow _{\approx }\cup \Rightarrow _{\#}\mathcal {P'} = \langle \nabla ', \sigma ', P' \rangle$, then ${\mathcal {P}}'$ is also valid.

From now on, we consider only valid triples.

Lemma 8

(Termination of $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$). There is no infinite chain of reductions $\Rightarrow _{\approx }$ (or $\Rightarrow _{\#}$) starting from an arbitrary triple ${\mathcal {P}} = \langle \nabla , \sigma , P\rangle$.

Proof

• The proof for $\Rightarrow _{\approx }$ is by well-founded induction on $\mathcal {P}$ using the measure $\Vert {\mathcal {P}}\Vert =\langle |Var(P_\approx )|, \Vert P\Vert , |P_{\text{ nfp }_\approx }|\rangle$ with a lexicographic ordering, where $\Vert P\Vert = \sum _{s \approx _? t \,\in \,P_\approx } |s| + |t| + \sum _{a \#_? u \in P_\#} |u|$. Note that this measure decreases after each step $\langle \nabla , \sigma , P\rangle \Rightarrow _{\approx }\langle \nabla , \sigma ', P'\rangle$: for $\mathbf {(\approx _?inst)}$, $|Var(P_\approx )|>|Var(P'_\approx )|$; for $\mathbf {(\approx _?refl)}$, $\mathbf {(\approx _? pair)}$, $\mathbf {(\approx _? app)}$, $\mathbf {(\approx _?[aa])}$, $\mathbf {(\approx _?[ab])}$ and $\mathbf {(\approx _?C)}$, $|Var(P_\approx )|$ $\ge$ $|Var(P'_\approx )|$, but $\Vert P\Vert >\Vert P'\Vert$; and, for $\mathbf {(\approx _?inv)}$, both $|Var(P_\approx )| = |Var(P'\approx )|$ and $\Vert P\Vert =\Vert P'\Vert$, but $|P_{\text{ nfp }_\approx }|>|P'_{\text{ nfp }_\approx }|$.

• The proof for $\Rightarrow _{\#}$ is by induction on $\mathcal {P}$ using as measure $\Vert P_\#\Vert$. It can be checked that this measure decreases after each step: $\langle \nabla , \sigma , P\rangle \Rightarrow _{\#}\langle \nabla , \sigma ', P'\rangle$.

To solve a unification problem, $\langle \nabla , P\rangle$, one builds the derivation tree for $\Rightarrow _{\approx }$, labelling the root node with $\langle \nabla , id , P\rangle$. This tree has leaves labelled with $\Rightarrow _{\approx }$-nf’s that are either failing or successful triples. Then, the tree is extended by building $\Rightarrow _{\#}$-derivations starting from all successful leaves. The extended tree will include failing leaves and successful leaves. The successful leaves will be labelled by triples ${\mathcal {P}}'$ in which the problem $P'$ consists only of FP equations. Since $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$ are both terminating (Lemma 8), the process described above must be also terminating.

Definition 10

(Derivation tree for $\langle {\Delta }, P\rangle$). A derivation tree for the unification problem $\langle {\Delta }, P\rangle$, denoted as ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$, is a tree with root label ${\mathcal {P}} = \langle {\Delta }, id , P\rangle$ built in two stages:

• Initially, a tree is built, whose branches end in leaf nodes labelled with the triples in ${\mathcal {P}}_{\Rightarrow _{\approx }}$. The labels in each path from the root to a leaf correspond to a $\Rightarrow _{\approx }$-derivation.

• Further, for each leaf labelled with a successful triple $\mathcal {Q}$ in ${\mathcal {P}}_{\Rightarrow _{\approx }}$, the tree is extended with a path to a new leaf that is labelled with a $\bar{\mathcal {Q}} \in {\mathcal {Q}}_{\Rightarrow _{\#}}$. The labels in the extended path from the node with label $\mathcal {Q}$ to the new leaf correspond to a $\Rightarrow _{\#}$-derivation.

Remark 5

For $\langle {\Delta }, P\rangle$, all labels in the nodes of ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$ are valid by Lemma 7.

The next lemma is proved by case analysis on elements of ${\mathcal {P}}_{\Rightarrow _{\approx }}$ and ${\mathcal {P}}_{\Rightarrow _{\#}}$.

Lemma 9

(Characterisation of leaves of ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$). Let $\langle {\Delta }, P\rangle$ be a unification problem. If $\mathcal {P'} = \langle \nabla , \sigma ', P'\rangle$ is the label of a leaf in ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$, then $P'$ can be partitioned as follows: $P' = P'' \cup P_\bot$, where $P''$ is the set of all FP equations in $P'$ and $P_\bot = P' - P''$. If $P_\bot \ne \emptyset$ then $\mathcal {U}_C(\mathcal {P'}) = \emptyset$.

The next definition is motivated by the previous characterisation of the labels of leaves in derivation trees.

Definition 11

(Successful leaves). Let $\langle {\Delta }, P\rangle$ be a unification problem. A leaf in ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$ that is labelled with a triple of the form $\mathcal {Q} = \langle \nabla , \sigma , Q\rangle$, where Q consists only of FP equations, is called a successful leaf of ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$. In this case $\mathcal {Q}$ is called a successful triple of ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$. The sets of successful leaves and triples of ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$ are denoted respectively by $SL({\mathcal {T}}_{\langle {\Delta }, P\rangle })$ and $ST({\mathcal {T}}_{\langle {\Delta }, P\rangle })$.

The soundness theorem states that successful leaves of ${\mathcal {T}}_{\langle {\Delta }, P\rangle }$ produce correct solutions. The proof is by induction on the number of steps of $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$ and uses Lemma 9 and auxiliary results on the preservation of solutions by $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$. Proving preservation of solutions for rules $\mathbf {(\approx _? [ab])}$ and $\mathbf {(\approx _? inst)}$ is not straightforward and uses Lemmas 1, 2, 3 and 5 to check that the four conditions of Definition 4 are valid before, if one supposes their validity after the rule application.

Theorem 1

(Soundness of $\mathcal {T}_{\langle {\Delta }, P\rangle }$). $\mathcal {T}_{\langle {\Delta }, P\rangle }$ is correct, i.e., if ${\mathcal {P}}' = \langle \nabla , \sigma , P' \rangle$ is the label of a leaf in $\mathcal {T}_{\langle {\Delta }, P\rangle }$, then 1. $\mathcal {U}_C(\mathcal {P'}) \subseteq \mathcal {U}_C(\langle {\Delta }, id , P\rangle )$, and 2. if $P'$ contains non FP equations or freshness constraints then $\mathcal {U}_C(\mathcal {P'}) = \emptyset$.

The completeness theorem guarantees that the set of successful triples provides a complete set of solutions. Its proof uses case analysis on the rules of the relations $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$ by an argumentation similar to the one used for Theorem 1. For $\Rightarrow _{\#}$ one has indeed equivalence: ${\mathcal {P}}\Rightarrow _{\#}{\mathcal {P}'}$, implies $\mathcal {U}_C(\mathcal {P})=\mathcal {U}_C(\mathcal {P'})$. The same is true for all rules of the relation $\Rightarrow _{\approx }$ except the branching rule $\mathbf {(\approx _?C)}$, for which it is necessary to prove that all solutions of a triple reduced by $\mathbf {(\approx _?C)}$ must belong to the set of solutions of one of its children triples.

Theorem 2

(Completeness of $\mathcal {T}_{\langle {\Delta }, P\rangle }$). Let $\langle {\Delta }, P\rangle$ and $\mathcal {T}_{\langle {\Delta }, P\rangle }$ be a unification problem and its derivation tree. Then ${\mathcal {U}}_C(\langle {\Delta }, id , P\rangle ) = \bigcup _{{\mathcal {Q}}\in ST(\mathcal {T}_{\langle {\Delta }, P\rangle })} {\mathcal {U}}_C({\mathcal {Q}})$.

Corollary 1

(Generality of successful triples). Let ${\mathcal {P}}= \langle {\Delta }, P\rangle$ be a unification problem and $\langle \nabla '', \sigma '\rangle \in {\mathcal {U}}_C({\mathcal {P}})$. Then there exists a successful triple ${\mathcal {Q}} \in ST({\mathcal {T}}_{\langle {\Delta }, P\rangle })$ where ${\mathcal {Q}} = \langle \nabla , \sigma , Q\rangle$ such that $\langle \nabla '', \sigma '\rangle \in {\mathcal {U}}_C({\mathcal {Q}})$, and hence, $\nabla ''\vdash \nabla \sigma '$ and there exists $\lambda$ such that $\nabla ''\vdash \sigma \lambda \approx \sigma '$.

Proof

By Theorem 2, ${\mathcal {U}}_C({\mathcal {P}}) = \bigcup _{{\mathcal {P}}'\in ST({\mathcal {T}}_{\langle {\Delta }, P\rangle })} {\mathcal {U}}_C({\mathcal {P}}')$. Then there exists ${\mathcal {Q}} \in ST({\mathcal {T}}_{\langle {\Delta }, P\rangle })$ such that $\langle \nabla '', \sigma '\rangle \in {\mathcal {U}}_C({\mathcal {Q}})$. Suppose ${\mathcal {Q}} = \langle \nabla , \sigma , Q\rangle$. Then by the first and fourth conditions of the definition of solution (Definition 4) we have that $\nabla ''\vdash \nabla \sigma '$ and there exists $\lambda$ such that $\nabla ''\vdash \sigma \lambda \approx \sigma '$.

Remark 6

The nominal C-unification problem is to decide, for a given $\mathcal {P}$, if ${\mathcal {U}}_C({\mathcal {P}})$ is non empty; that is, whether $\mathcal {P}$ has nominal C-unifiers. To prove that this problem is in NP, a non-deterministic procedure using the reduction rules in the same order as in Definition 10 is designed. In this procedure, whenever rule $\mathbf {(\approx _?C)}$ applies, only one of the two possible branches is guessed. In this manner, if the derivation tree has a successful leaf, this procedure will guess a path to the successful leaf, answering positively to the decision problem. According to the measures used in the proof of termination (Lemma 8), reduction with both the relations $\Rightarrow _{\approx }$ and $\Rightarrow _{\#}$ is polynomially bound, which implies that this non-deterministic procedure is polynomially bound.

To prove NP-completeness, one can polynomially reduce the well-known NP-complete positive 1-in-3-SAT problem into nominal C-unification, as done in [7] for the C-unification problem. An instance of the positive 1-in-3-SAT problem consists of a set of clauses ${\mathcal {C}} = \{{\mathcal {C}}_i | 1\le i\le n\}$, where each ${\mathcal {C}}_i$ is a disjunction of three propositional variables, say ${\mathcal {C}}_i = p_i\vee q_i\vee r_i$. A solution of $\mathcal {C}$ is a valuation with exactly one variable true in each clause. The proposed reduction of $\mathcal {C}$ into a nominal C-unification problem would require just a commutative function symbol, say $\oplus$, two atoms, say a and b, a variable for each clause ${\mathcal {C}}_i$, say $Y_i$, and a variable for each propositional variable p in $\mathcal {C}$, say $X_p$. Instantiating $X_p$ as $\overline{a}$ or $\overline{b}$, would be interpreted as evaluating p as true or false, respectively. Each clause ${\mathcal {C}}_i = p_i\vee q_i\vee r_i$ in $\mathcal {C}$ is translated into an equation $E_i$ of the form $((X_{p_i}\oplus X_{q_i})\oplus X_{r_i})\oplus Y_i \approx _? ((\overline{b}\oplus \overline{b}) \oplus \overline{a})\oplus ((\overline{b}\oplus \overline{a}) \oplus \overline{b})$. The nominal C-unification problem for $\mathcal {C}$ is given by ${\mathcal {P}_\mathcal {C}}= \langle \emptyset , \{E_i | 1\le i\le n\}\rangle$. Simplifying ${\mathcal {P}_\mathcal {C}}$ would not introduce freshness constraints since the problem does not include abstractions. Thus, to conclude it is only necessary to check that $\langle \emptyset , \sigma \rangle$ is a solution for $\mathcal {P}_\mathcal {C}$ if and only if $\sigma$ instantiates exactly one of the variables $X_{p_i}, X_{q_i}$ and $X_{r_i}$ in each equation with $\overline{a}$ and the other two with $\overline{b}$, which means that $\mathcal {C}$ has a solution.

4 Generation of Solutions for Successful Leaves of $\mathcal {T}_{\langle {\Delta }, P\rangle }$

To build solutions for a successful leaf ${\mathcal {P}} = \langle \nabla , \sigma , P\rangle$ in the derivation tree of a given unification problem, we will select and combine solutions generated for FP equations $\pi .X \approx _? X$, for each $X\in Var(P)$. We introduce the notion of pseudo-cycle of a permutation, in order to provide precise conditions to build terms t by combining the atoms in $dom(\pi )$, such that $\pi \cdot t \approx _{\{\alpha , C\}}t$. For convenience, we use the algebraic cycle representation of permutations. Thus, instead of sequences of swappings, permutations in nominal terms will be read as products of disjoint cycles [27].

Example 4

(Continuing Example 3) The permutations $(a\,b) \,\,{:}{:}\,\, (e\,f) \,\,{:}{:}\,\,(c\,d) \,\,{:}{:}$ $(a\,c) \,\,{:}{:}\,\, nil$ and $(a\,b) \,\,{:}{:}\,\, (c\,d) \,\,{:}{:}\,\, (a\,c) \,\,{:}{:}\,\,\!nil$ are respectively represented as the product of permutation cycles $(a\,b\,c\,d)(e\,f)$ and $(a\,b\,c\,d)(e)(f)$.

Permutation cycles of length one are omitted. In general the cyclic representation of a permutation consists of the product of all its cycles.

Let $\pi$ be a permutation with $dom(\pi ) =n$. Given $a\in dom(\pi )$ the elements of the sequence $a, \pi (a), \pi ^2(a), \ldots$ cannot be all distinct. Taking the first $k\le n$, such that $\pi ^k(a)=a$, we have the k-cycle $(a \ \pi (a) \ \ldots \pi ^{k-1}(a))$, where $\pi ^{j+1}(a)$ is the successor of $\pi ^j(a)$. For the 4-cycle in the permutation $(a\, b\, c\, d)\, (e\, f)$, the 4-cycles generated by a, b, c and d are the same: $(a\, b\, c\, d) = (b\, c\, d\, a) = (c\, d\, a\, b) = (d\, a\, b\, c)$.

Definition 12 establishes the notion of a pseudo-cycle w.r.t. a k-cycle $\kappa$. Intuitively, given a k-cycle $\kappa$ and a commutative function symbol $*$, a pseudo-cycle w.r.t $\kappa$, $(A_0 \ldots A_l)$, is a cycle whose elements are either atom terms built from the atoms in $\kappa$ or terms of the form $A_i' * A_j'$, for $A_i', A_j'$ elements of a pseudo-cycle w.r.t $\kappa$.

Definition 12

(Pseudo-cycle). Let $\kappa =(a_0 \ a_1 \ \ldots \ a_{k-1})$ be a k-cycle of a permutation $\pi$. A pseudo-cycle w.r.t. $\kappa$ is inductively defined as follows:

• 1. $\overline{\kappa } = (\overline{a_0} \cdots \overline{a_{k-1}})$ is a pseudo-cycle w.r.t. $\kappa$, called trivial pseudo-cycle of $\kappa$.

• 2. $\kappa ' = (A_0\; ...\,A_{k'-1})$ is a pseudo-cycle w.r.t. $\kappa$, if the following conditions are simultaneously satisfied:

  • (a) each element of $\kappa '$ is of the form $B_i* B_j$, where $*$ is a commutative function symbol in the signature, and $B_i, B_j$ are different elements of $\kappa ''$, a pseudo-cycle w.r.t. $\kappa$. $\kappa '$ will be called a first-instance pseudo-cycle of $\kappa ''$ w.r.t. $\kappa$.

  • (b) $A_i\not \!\approx _{\alpha ,C} A_j$ for $i\ne j$, $0\le i,j\le k'-1$;

  • (c) for each $0 \le i < k'-1$, ${\kappa } \cdot A_i \approx _{\{\alpha , C\}}A_{(i+1) mod \, k'}$.

The length of the pseudo-cycle $\kappa$, denoted by $|\kappa |$, consists of the number of elements in $\kappa$. A pseudo-cycle of length one will be called unitary.

Example 5

• A (Continuing Example 2) The unitary pseudo-cycles of $\kappa = (a\,b)$ are of the form $(\overline{a}*\overline{b})$ for $*$ any commutative symbol in the signature. These pseudo-cycles are the basis for a more elaborated construction used to build infinite independent solutions for the leaf $\langle \emptyset , id , \{X \approx _? (a\,b).X\} \rangle$. Examples of these solutions are: $\langle \emptyset , \{X / \overline{a} * \overline{b}\}\rangle$, $\langle \emptyset , \{X / (\overline{a} * \overline{a}) * (\overline{b} * \overline{b})\}\rangle$, $\langle \emptyset , \{X / (\overline{a} * \overline{b}) * (\overline{a} * \overline{b})\}\rangle$, $\langle \emptyset , \{X / ((\overline{a} * \overline{a}) * \overline{a}) * ((\overline{b} * \overline{b}) * \overline{b})\}\rangle$, $\langle \emptyset , \{X / (\overline{a} * (\overline{a} * \overline{a})) * (\overline{b} * (\overline{b} * \overline{b}))\}\rangle$, etc.

• B (Continuing Examples 3 and 4) In ${\mathcal {Q}}_1$ and ${\mathcal {Q}}_2$ we have the occurrences of the 4-cycle $\kappa = (a\,b\,c\,d)$. Suppose $*,\oplus ,+$ are commutative operators in the signature. The following are pseudo-cycles w.r.t. $\kappa$: $\overline{\kappa }=(\overline{a} \ \overline{b} \ \overline{c} \ \overline{d} )$; $\kappa _1 = ( (\overline{a}* \overline{b}) \ (\overline{b}* \overline{c}) \ (\overline{c}* \overline{d}) \ (\overline{d}*\overline{a}))$; $\kappa _2=( (\overline{a}\oplus \overline{c}) \ (\overline{b}\oplus \overline{d}))$; $\kappa _{11} =( ((\overline{a}* \overline{b}) + (\overline{b}* \overline{c}) ) \ ((\overline{b}* \overline{c}) + (\overline{c}*\overline{d})) ((\overline{c}* \overline{d}) + (\overline{d}* \overline{a}) ) \ ((\overline{d}* \overline{a}) + (\overline{a}*\overline{b})) )$; $\kappa _{12} =( ((\overline{a}* \overline{b}) * (\overline{c}* \overline{d}) ) \ ((\overline{b}* \overline{c}) * (\overline{d}*\overline{a})))$; $\kappa _{21} = ( ((\overline{a}\oplus \overline{c}) * (\overline{b}\oplus \overline{d}) ) )$; $\kappa _{121} =( ((\overline{a}* \overline{b}) * (\overline{c}* \overline{d}) ) * ((\overline{b}* \overline{c}) * (\overline{d}*\overline{a})))$. $\kappa _1$ and $\kappa _2$ are first-instance pseudo-cycles of $\overline{\kappa }$, and $\kappa _{11}$ and $\kappa _{12}$ of $\kappa _1$ and $\kappa _{21}$ of $\kappa _2$. Notice that, $|\overline{\kappa }|=|\kappa _1| = |\kappa _{11}|=4$, $|\kappa _{12}|=2$, and $|\kappa _{21}| = |\kappa _{121} | = 1$. Also, $\kappa _{1}$ corresponds to $((\overline{a}*\overline{d})\, (\overline{b}*\overline{a})\,(\overline{c}*\overline{b})\,(\overline{d}*\overline{c}))$, a first-instance pseudo-cycle of $\overline{\kappa }$. Finally, observe that for the elements of the unitary pseudo-cycles $\kappa _{21}$ and $\kappa _{121}$, say $s=(\overline{a}\oplus \overline{c}) * (\overline{b}\oplus \overline{d})$ and $t=((\overline{a}* \overline{b}) * (\overline{c}* \overline{d}) ) * ((\overline{b}* \overline{c}) * (\overline{d}*\overline{a}))$, $\{X/s\}$ and $\{X/t\}$ (resp. $\{Y/s\}$ and $\{Y/t\}$) are solutions of the FP equation $(a\ b \ c \ d)(e \ f).X \approx _? X$ (resp. $(a\ b\ c\ d).Y \approx _? Y$).

Let $\kappa$ be a pseudo-cycle. Notice that only item 2 of Definition 12 may build a first-instance pseudo-cycle $\kappa '$ w.r.t. $\kappa$ with fewer elements. If $|\kappa '| < |\kappa |$ then, due to algebraic properties of cycles and commutativity of the operator applied ($*$), one must have that $|\kappa '| = |\kappa |/2$. Thus, unitary pseudo-cycles can only be generated from cycles of length a power of two. This is the intuition behind the next theorem, proved by induction on the size of the cycle $\kappa$.

Theorem 3

A pseudo-cycle $\kappa$ generates unitary pseudo-cycles iff $|\kappa |$ is a power of two.

Notice that, according to item 2.c of Definition 12, if $\kappa ' = (A_0 \ldots A_{k'-1})$ is a pseudo-cycle w.r.t. $\pi$ then $\pi \cdot A_{k'-1} \approx _{\{\alpha , C\}}A_0$; particularly, if $k' = 1$ then $\pi \cdot A_0 \approx _{\{\alpha , C\}}A_0$. Below, given ${\mathcal {P}}=\langle \emptyset , \{\pi . X \approx _? X\}\rangle$ a FP equational problem, we call a combinatory solution of ${\mathcal {P}}$, a substitution $\{ X/ t\}$, such that $\pi \cdot t \approx _{C} t$, and t contains only atoms from $\pi$ and commutative function symbols, built as unary pseudo-cycles w.r.t. $\kappa$ a cycle in $\pi$.

The next theorem is proved by contradiction, supposing that $\kappa$ has an odd factor and using Theorem 3.

Theorem 4

Let ${\mathcal {P}}=\langle \emptyset , \{\pi .X \approx _? X\}\rangle$ be a FP problem. ${\mathcal {P}}$ has a combinatory solution iff there exists a unitary pseudo-cycle $\kappa$ w.r.t. $\pi$.

Remark 7

Since one can generate infinitely many unitary pseudo-cycles from a given $2^n$-cycle $\kappa$ in $\pi$, $n\in \mathbb {N}$, there exist infinite independent solutions for the FP problem $\langle \emptyset , \{\pi .X\approx _? X\}\rangle$.

General solutions for FP problems. To compute the set of solutions for a FP equation, we use a method described in [4], which is based on the computation of unitary extended pseudo-cycles (epc). We refer to [4] for the definition of extended pseudo-cycles and an algorithm to enumerate all the solutions of a successful leaf in the derivation tree.

Pseudo-cycles are built just from atom terms in $dom(\pi )$ and commutative function symbols, while epc’s consider all nominal syntactic elements including new variables, and also non commutative function symbols. The soundness and completeness of the generator of solutions described in [4] relies on the properties of pseudo-cycles described above, in particular the fact that only unitary pseudo-cycles generate solutions.

5 Formal Proofs

In the Coq formalisation, nominal terms are specified inductively, which permits to use induction to formalise properties of terms (to check nominal $\alpha$-equality modulo C we use the rules given in [3]; see Fig. 3). The relations $\Rightarrow _{\#}$ and $\Rightarrow _{\approx }$ are inductivelty specified, as propositions from problems to problems, resp. as and , and normal forms and their reflexive-transitive closures are specified using abstract relations as shown below.

A unification step, , is a reduction step either with the relation or with the relation , the latter restricted to FP problems; and a is a normal form for this relation.

Unification paths are derivations with the relation :

Soundness is specified as the Theorem below, which reads: for any unification problem that reduces into a problem with the relation , and such that Sl is a solution of , Sl is also a solution of .

The formalisation of soundness is given in a theory that consists of 902 lines or 35 KB. This theory also includes lemmas that characterise successful leaves and their solutions. The theorem uses three auxiliary lemmas, also proved by induction. A lemma expresses preservation of the set of solutions of unification problems under reduction by the relation $\Rightarrow _{\#}$:

Another lemma, the longer one, states that the solutions of a unification problem obtained from a given problem through application of the relation $\Rightarrow _{\approx }$ are solutions of the given problem:

Finally, the last auxiliary lemma applied to prove soundness states that solutions are preserved in each unification step:

Since except $\mathbf {(\approx _{\{\alpha , C\}}C)}$ unification rules are invertible, the formalisation of the proof of completeness is shorter, consisting only of 351 lines or 13 KB. The additional element to be considered is the nondeterminism of $\mathbf {(\approx _{\{\alpha , C\}}C)}$, indeed implemented as two rules. The key theorem states that is a solution for iff there exists a unification path form to some with solution .

Excluding formalisation of nominal terms and E-equivalence, subject of [3], the whole theory consists of theories Completeness, Soundness, Termination, C-Unif, Substs, Problems and C-Equiv, which consist of 5474 lines or 204 KB.

6 Conclusions and Future Work

A Coq formalisation of a sound and complete nominal C-unification algorithm was obtained by combining $\Rightarrow _{\approx }$- and $\Rightarrow _{\#}$-reduction. The algorithm builds finite derivation trees, such that the leaves, which may contain FP equations, represent a complete set of unifiers. We have shown that nominal C-unification is infinitary and NP-complete. An OCaml implementation of the simplification phase has been developed, which outputs derivation trees. Extensions to deal with different equational theories will be considered in future work.