Nominal AC-Matching

Abstract

The nominal syntax is an extension of the first-order syntax that smoothly represents languages with variable bindings. Nominal matching is first-order matching modulo alpha-equivalence. This work extends a certified first-order AC-unification algorithm to solve nominal AC-matching problems. To our knowledge, this is the first mechanically-verified nominal AC-matching algorithm. Its soundness and completeness were verified using the proof assistant PVS. The formalisation enriches the first-order AC-unification algorithm providing structures and mechanisms to deal with the combinatorial aspects of nominal atoms, permutations and abstractions. Furthermore, by adding a parameter for “protected variables” that cannot be instantiated during the execution, it enables nominal matching. Such a general treatment of protected variables also gives rise to a verified nominal AC-equality checker as a byproduct.

1 Introduction

The nominal approach to the specification of systems with binders [20, 25] extends first-order syntax with notions of name and binding that allow us to represent systems with binders smoothly. Such systems frequently appear in the formalisation of mathematics and when reasoning about the properties of programming languages. Taking into account $\alpha$-equivalence is essential to represent bindings correctly. For example, the formulas $\forall x : x + 1 > 0$ and $\forall y: y +1 > 0$ should be considered equivalent despite being syntactically different. From the user point of view it is easier to use systems with variable names than systems with indices. Hence, instead of using indices to represent bound variables, as in explicit substitution calculi à la de Bruijn, the nominal theory uses atoms, atom permutations and freshness constraints to represent binders more naturally [19, 25].

Given terms t and s, syntactic unification is the problem of finding a substitution $\sigma$ such that $\sigma t = \sigma s$ and syntactic matching is the problem of finding a substitution $\sigma$ such that $\sigma t = s$. Algorithms to solve matching problems are an essential component of functional languages and equational theorem provers: matching is used to decide if an equation can be applied to a term. The problem of syntactic matching can be generalised to consider an equational theory E. In this case, called E-matching, we must find a substitution $\sigma$ such that $\sigma t$ and s are equal modulo E, which we denote $\sigma t \approx _{E} s$. For example, if the system includes associative and commutative (AC) operators, such as $+$ in the example above, then the matching algorithm should consider the AC axioms. Furthermore, equational programming languages, such as Maude, require efficient implementations of AC-matching to deal with AC-theories (see [16]).

If the system under study includes binders and AC operators, then $\alpha$-equivalence should also be considered: for example, $\forall x : x + 1 > 0$ should be considered equivalent to $\forall y : 1 + y >0$. This paper focuses on the matching problem for languages that include binders and AC operators.

Nominal matching is the extension of first-order matching to the nominal syntax, replacing the notion of syntactic equality by $\alpha$-equivalence. It has applications in rewriting, functional programming, and metaprogramming. For instance, various versions of matching modulo $\alpha$-equivalence are used in functional programming languages that provide constructs for manipulating abstract syntax trees involving binders (e.g. [26, 29]). In this work, we specify a nominal matching algorithm modulo AC function symbols (nominal AC-matching, for short) and prove its correctness and completeness using the proof assistant PVS.

Related Work. Nominal syntactic (i.e. modulo $\alpha$-equivalence) equality-check, matching and unification were solved since the beginning of the development of the nominal approach; more than twenty years ago, Urban et al. [34] developed the first rule-based algorithm for nominal syntactic unification and further, Urban mechanised its correctness and completeness in Isabelle/HOL as part of the formalisation of the nominal approach in this proof assistant [32, 33]. Furthermore, different approaches were designed to deal with nominal syntactic unification efficiently. Calvès and Fernández [11, 12] and Levy and Villaret [22, 23] developed efficient nominal syntactic unification algorithms to solve nominal unification problems. Furthermore, Ayala-Rincón et al. [6] developed a nominal syntactic unification algorithm specified as a functional program and verified it in the proof assistant PVS. Enriching the nominal equational analysis with equational theories started with developing rule-based techniques for commutative operators. Such developments were initially checked in the proof assistant Coq and further in PVS [1, 4]. Remarkable differences between nominal unification and nominal C-unification were discovered, such as the fact that when expressing solutions as pairs consisting of a freshness context and substitutions, nominal unification is unitary whereas nominal C-unification is not finitary [2, 3].

Avoiding freshness constraints through a fixed-point approach was also studied as a mechanism to obtain finite complete sets of solutions [5]. Such fixed-point equations also appear in nominal techniques designed to deal with higher-order recursive let operators [27, 28].

First-order AC-unification algorithms were proposed almost half a century ago, when Stickel [30, 31] showed the connection between solving this problem and computing solutions to linear Diophantine equations until a certain bound. Almost a decade later, Fages [17, 18] fixed a mistake in Stickel’s proof of termination. Since then, ideas to obtain more efficient AC-unification algorithms have been proposed, either by using a smaller bound when computing the solutions to the linear Diophantine equation [14], or by solving those equations more efficiently [14], or even by solving whole systems of linear Diophantine equations and using suitable data structures to represent the problem [8, 10]. First-order AC-unification algorithms were not formalised until recently when a version of Fages’ AC-unification algorithm was proved correct and complete using the proof assistant PVS [7]. This mechanisation applies the linear-Diophantine AC unification method discovered and fixed in works by Stickel and Fages [17, 18, 30, 31], and can easily be adapted to deal with AC-equality and AC-matching problems as well. It is important to stress that such mechanisation was not a routine-formalisation effort; before this formalisation, only a formalisation of AC-matching (which has simpler combinatorics) was reported in the proof assistant Coq [15].

Contributions. Adapting first-order syntactic AC unification to the nominal setting is challenging since the new variables included in the Diophantine systems (used to generate new possible AC combinations) give rise to new AC-unification problems of the same complexity as the input problems. This paper shows that such cyclicity is not possible when only nominal AC-matching problems are considered. We present a novel nominal AC-matching algorithm adapted from the Stickel-Fages linear-Diophantine approach and prove its termination, correctness and completeness in the proof assistant PVS.

Organisation. Section 2 recalls the main concepts and notations needed in the paper. In Sect. 3, we present and explain the pseudocode for the algorithm specified in PVS. Section 4 discusses the main features of the formalisation, while Sect. 5 discusses the challenges in adapting our approach to nominal AC-unification. Finally, in Sect. 6, we conclude the paper and suggest possible paths for future work. We assume familiarity with PVS (see [24]) and include hyperlinks (with the icon) to specific points of interest of the PVS formalisation. An extended version of this paper is available at https://www.mat.unb.br/ayala/publications.html.

2 Background

2.1 Nominal Terms, Permutations and Substitutions

Assume disjoint countable sets of atoms $\mathbb {A} = \{a, b, c, \ldots \}$ and of variables $\mathbb {X} = \{X, Y, Z, \ldots \}$, and a signature $\Sigma$ of function symbols which contains associative-commutative function symbols. A permutation $\pi$ is a bijection of the form $\pi : \mathbb {A} \rightarrow \mathbb {A}$ such that the domain of $\pi$ (i.e., the set of atoms modified by $\pi$) is finite. Permutations are usually represented as a list of swappings, where the swapping $(a \ b)$ exchanges atoms a and b and fixes all the other atoms. Therefore, a permutation is represented as $\pi = (a_1 \ b_1)\,{::}\, ... {::}\,(a_n \ b_n)\,{::}\,nil$. The inverse of this permutation, denoted by $\pi ^{-1}$, can be computed simply by reversing the list. The identity permutation is denoted by id.

Definition 1

(). The set $\mathcal {T}(\Sigma , \mathbb {A}, \mathbb {X})$ of nominal terms is generated according to the grammar:

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

(1)

where $\langle \rangle$ is the unit, a is an atom term, $\pi \cdot X$ is a moderated variable or suspension (the permutation $\pi$ is suspended on the variable X), [a]t is an abstraction (a term with the atom a abstracted), $\langle s, t \rangle$ is a pair, $f \ t$ is a function application and $f^{AC}\, t$ is an associative-commutative function application.

Remark 1

We represent moderated variables of the form $id \cdot X$ simply as X. We follow Gabbay’s name convention, which says that atoms differ in their names. Therefore, if we consider atoms a and b, it is redundant to say $a \ne b$.

Definition 2

(). We say that a term t is well-formed if t is not a pair and every AC-function application that is a subterm of t has at least two arguments.

As was done in [7], we have restricted the terms that our algorithm receives to well-formed terms to ease our formalisation (more details in the extended version). Excluding pairs is a natural decision since they are used to encode a list of arguments to a function.

Definition 3

(Permutation Action). The is defined recursively: $nil \cdot c = c$ and $((a \ b)\,{::}\,\pi ) \cdot c = a$, if $\pi \cdot c = b$; $((a \ b)\,{::}\,\pi ) \cdot c = b$, if $\pi \cdot c = a$; $((a \ b)\,{::}\,\pi ) \cdot c = \pi \cdot c$ otherwise. The is defined recursively:

$$ \begin{array}{l@{}l@{}l} \pi \cdot \langle \rangle = \langle \rangle &{} \pi \cdot (\pi ' \cdot X) = (\pi \,{::}\,\pi ') \cdot X &{} \pi \cdot [a]t = [\pi \cdot a] \pi \cdot t \\ \pi \cdot \langle s, t \rangle = \langle \pi \cdot s, \pi \cdot t \rangle &{} \pi \cdot f \ t = f \ \pi \cdot t &{} \pi \cdot f^{AC} t = f^{AC} \pi \cdot t \end{array} $$

Notation 1

When convenient, we may mention that a function symbol f is an AC-function symbol, omit the superscript and write simply f instead of $f^{AC}$.

A substitution $\sigma$ is a function from variables to terms, such that $\sigma X \ne id \cdot X$ only for a finite set of variables, called the domain of $\sigma$ and denoted as $dom (\sigma )$. The image of $\sigma$ is then defined as $im(\sigma ) = \{\sigma X \ | \ X \in dom (\sigma ) \}$. We denote the identity substitution by id. From now on, when composing substitution $\sigma$ with $\delta$ we may omit the composition symbol and write $\sigma \delta$ instead of $\sigma \circ \delta$.

A only instantiates variables to well-formed terms. In the proofs of soundness and completeness of the algorithm, we restrict ourselves to well-formed substitutions. Let V be a set of variables. If $dom (\sigma ) \subseteq V$ and $Vars (im(\sigma )) \subseteq V$ we write $\sigma \subseteq V$. In our PVS code, substitutions are represented by a list, where each entry of the list is called a nuclear substitution and is of the form $\{X \rightarrow t \}$.

Definition 4

(). A nuclear substitution $\{X \rightarrow t\}$ acts over a term by induction as shown below:

Definition 5

(). Since a substitution $\sigma$ is a list of nuclear substitutions, the action of a substitution is defined as:

• $\textsc {nil}\ t = t$, where nil is the null list, used to represent the identity substitution.

• $\textsc {cons}(\{X \rightarrow s\}, \ \sigma ) \ t = \{X \rightarrow s \} (\sigma t)$.

Remark 2

The notion of substitution used here differs from the more traditional view of a substitution as a simultaneous application of nuclear substitutions, although both are correct. The way we defined substitution here is closer to triangular substitutions [21]. In the definition of action of substitutions the nuclear substitution in the head of the list is applied last. This lets us, given substitutions $\sigma$ and $\delta$, obtain the substitution $\sigma \circ \delta$ in our code simply as append ($\sigma , \delta$).

2.2 Freshness and $\alpha$-Equality

Freshness and $\alpha$-equality are two valuable notions in nominal theory and are represented by the predicates $\#$ and $\approx _\alpha$. Intuitively, $a\#t$ means that if a occurs in t then it does so under an abstractor [a], and $s \approx _\alpha t$ means that s and t are $\alpha$-equivalent, that is, they are equal modulo the renaming of bound atoms. These concepts are given in Definitions 6 and 7.

Definition 6

(). A freshness context $\nabla$ is a set of constraints of the form $a\#X$. We denote contexts by letters $\Delta , \Gamma , \nabla , \ldots$ An atom a is said to be fresh on t under a context $\nabla$, denoted by $\nabla \vdash a\#t$, if it is possible to build a proof using the rules:

Definition 7

(). Let f be an AC function symbol, $S_n(f\, t)$ be an operator that selects the nth argument of $f\, t$ (considering the flattened form) and $D_n(f\, t)$ be an operator that deletes the nth argument of $f\, t$ (considering the flattened form). If there exist i and j such that $\Delta \vdash S_i(f^{AC} s) \approx _\alpha S_j(f^{AC} t)$ and $\Delta \vdash D_i(f^{AC} s) \approx _\alpha D_j(f^{AC} t)$, then $\Delta \vdash f^{AC} s \approx _\alpha f^{AC} t$. In other words, the rule of $\alpha$-equality for an AC-function application is:

Two terms t and s are said to be $\alpha$-equivalent under the freshness context $\Delta$ ($\Delta \vdash t \approx _\alpha s$) if it is possible to build a proof using rule $(\approx _\alpha AC)$ and the rules:

Notation 2

We define the difference set between two permutations $\pi$ and $\pi '$ as $ds(\pi , \pi ') = \{a \in \mathcal {A} | \pi \cdot a \ne \pi ' \cdot a\}$. By extension, $ds(\pi , \pi ')\#X$ is the set containing every constraint of the form $a\#X$ for $a \in ds(\pi , \pi ')$.

2.3 Solution to Quintuples and Additional Notation

For the proofs of soundness and completeness of the algorithm, we need the notion of a solution to a quintuple (Definition 8). This definition depends on a parameter $\mathcal {X}$, a set of “protected variables”, i.e., variables that cannot be instantiated.

Let P be a finite set of equational constraints. We denote the left-hand side of P by and the right-hand side of P by . The set of variables in $t \approx _? s$ is denoted as . Finally, if $\Gamma$ is a context then we denote by the set $\{X \ | \ a \# X \in \Gamma , \text {for some atom } a \}$.

Notation 3

Let $\nabla$ and $\nabla '$ be freshness contexts and $\sigma$ and $\sigma '$ substitutions. We need the following notation to define a solution to a quintuple:

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

• $\nabla \vdash \sigma \approx _{V} \sigma '$ denotes that $\nabla \vdash \sigma X \approx _\alpha \sigma ' X$ for all X in V. When V is the set of all variables $\mathbb {X}$, we write $\nabla \vdash \sigma \approx \sigma '$.

Definition 8

(). Suppose that $\Gamma$ is a context, P is a set of freshness constraints (of the form $a \#_? t)$ and equational constraints (of the form $t \approx _? s$), $\sigma$ is a substitution, V is a set of variables and $\mathcal {X}$ is a set of protected variables that cannot be instantiated. A solution for a quintuple $(\Gamma , P, \sigma , V, \mathcal {X})$ is a pair $(\Delta , \delta )$, where the following conditions are satisfied:

• 1. $\Delta \vdash \delta \Gamma$.

• 2. if $a \#_? t \in P$ then $\Delta \vdash a \# \delta t$.

• 3. if $t \approx _? s \in P$ then $\Delta \vdash \delta t \approx _\alpha \delta s$.

• 4. there exists $\lambda$ such that

  $\Delta \vdash \lambda \sigma \approx _{V} \delta$.

• 5. $dom (\delta ) \cap \mathcal {X} = \emptyset$.

Remark 3

Note that if $(\Delta , \delta )$ is a solution of $(\Gamma , \textsc {nil}, \sigma , \mathbb {X}, \mathcal {X})$ this corresponds to the notion of $(\Delta , \delta )$ being an instance of $(\Gamma , \sigma )$ that does not instantiate variables in $\mathcal {X}$.

Definition 9

(Solution for an AC-unification/matching/equality problem). A solution for an AC-unification problem with protected variables $(\Gamma , P, \mathcal {X})$ is a solution for the associated quintuple $(\Gamma , P, id, Vars (P), \mathcal {X})$. When $\mathcal {X} = Vars ( rhs (P))$, we have the definition for an AC-matching problem and when $\mathcal {X} = Vars (P)$ we have the definition of solution to an AC-equality checking problem.

3 Algorithm

We present the algorithm’s pseudocode instead of the actual PVS code for readability. We developed a nominal algorithm () for matching terms t and s. The algorithm is recursive and needs to keep track of the current context $\Gamma$, the equational constraints P that we have to unify, the substitution $\sigma$ computed so far, the set of variables V that are/were in the problem and the set of protected variables $\mathcal {X}$. Hence, its input is a quintuple $(\Gamma , P, \sigma , V, \mathcal {X})$. The output is a list of solutions, each of the form $(\Gamma _1, \sigma _1)$. The freshness constraints are treated by auxiliary functions (see Sect. 3.1), and the equational constraints P are represented as a list in our PVS code, where each element of the list is a pair $(t_i, s_i)$ that represents an equation $t_i \approx _? s_i$. The first call to the algorithm, in order to match t to s, is done with $P = \{t \approx _? s\}$; $\Gamma = \emptyset$ and $\sigma = id$ (because we have not computed any freshness constraint or substitution yet); $V = Vars (t, s)$ and $\mathcal {X} = Vars (s)$.

Although extensive, Algorithm 1 is simple. It starts by analysing the list P of terms to match. If it is empty (line 2), it has finished and can return the answer computed so far, a list with a unique element: $(\Gamma , \sigma )$. Otherwise, the algorithm calls the auxiliary function chooseEq (line 4), which returns a pair (t, s) and a list of equational constraints $P_1$ such that $P = \{t \approx _? s \} \cup P_1$. Then, P is updated by simplifying $\{t \approx _? s \}$ and it does so by seeing the form of t (an atom, a moderated variable, a unit, and so on).

3.1 Functions chooseEq and decompose

The function selects an equational constraint $t \approx _? s$ in P, picking the equation with the biggest size. This heuristic aims to aid us in the proof of termination (see Sect. 4.2).

The function (lines 15, 19 and 24) receives two terms t and s, and if they are both pairs, it recursively tries to decompose them, returning a tuple $(P, flag )$, where P is a list of equational constraints and $flag$ is a boolean that is True if the decomposition was successful. This function guarantees that only well-formed terms are in the matching problem.

Example 1

Examples of the function decompose are given below.

• $\textsc {decompose} (\langle a, \langle b, c \rangle \rangle , \ \langle c, \langle X, Y \rangle \rangle ) = (\{a \approx _? c, \ b \approx _? X, \ c \approx _? Y \}, \ True )$.

• $\textsc {decompose} (a, Y) = (\{ a \approx _? Y \}, \ True )$.

• $\textsc {decompose} (X, \langle c, d \rangle ) = (\textsc {nil}, \ False )$.

3.2 Handling Freshness Constraints - Functions freshSubs? and fresh?

Following the approach of [6], freshness constraints are handled separately by the auxiliary functions and . These functions were already implemented in [6], and extending them to handle AC-functions is straightforward. freshSubs? ($\sigma , \Gamma$) returns the minimal context ($\Gamma _1$ in Algorithm 1) in which $a\#_{?}\sigma X$ holds, for every $a\#X$ in the context $\Gamma$. fresh? (a, t) computes and returns the minimal context ($\Gamma _1$ in Algorithm 1) in which a is fresh for t. Both functions also return a boolean ($flag$ in Algorithm 1), indicating if it was possible to find the aimed context.

3.3 The Function applyACStep

The function was adapted from the formalisation of first-order AC-unification (see [7]). It handles equations $t \approx _? s$, where t and s are rooted by the same AC function symbol. This function returns a list (InputLst in line 28 of Algorithm 1) with each entry in this list corresponding to a branch ACMatch will explore. ACMatch explores every branch generated by calling itself recursively on every input in InputLst (line 29 of the algorithm). The algorithm’s output is a list of solutions of the form $(\Gamma , \sigma )$, where $\Gamma$ is a context and $\sigma$ is a substitution. In addition, the result of calling map (ACMatch, InputLst), LstResults in line 29 of Algorithm 1, is a list of lists of solutions. Hence, LstResults is flattened and then returned.

Remark 4

(solveAC and instantiateStep). applyACStep relies on two functions: and , which are fully described in [7]. In synthesis, the function solveAC finds the linear Diophantine equational system associated with the AC-matching equational constraint, generates the basis of solutions, and uses these solutions to generate the new AC-matching equational constraints. The function instantiateStep instantiates the moderated variables that it can.

3.4 An Example of First-Order AC-Unification and How We Adapted It to the Nominal Setting

We give a very high-level example (taken from [31] and more detailed in the extended version) of how we would solve the first-order AC-unification problem $\{f(X, X, Y, a, b, c) \approx _? f(b, b, b, c, Z)\}$. The first step is to eliminate common arguments. Next we associate our unification problem with a linear Diophantine equation ($2U_1 + U_2 + U_3 = 2 V_1 + V_2$ in our case) and generate a basis of solutions to this equation, associating a new variable ($Z_1, Z_2, \ldots , Z_7$ in our case) to each solution. The algorithm may branch into (possibly) many unification problems and these new variables will be the building blocks for these unification problems. Finally, before proceeding to unify the new unification problems, we can drop the cases where a variable term is paired with an AC-function application. In the end, the solutions computed are:

$$\begin{aligned} \begin{aligned} \sigma _1 \!&= \! \{Y \! \mapsto f(b, b), Z \mapsto f(a, X, X)\}&\sigma _2 \!&= \! \{Y \! \mapsto f(Z_2, b, b), Z \mapsto f(a, Z_2, X, X) \} \\ \sigma _3 \!&= \! \{X \mapsto b, Z \mapsto f(a, Y) \}&\sigma _4 \!&= \! \{X \mapsto f(Z_6, b), Z \mapsto f(a, Y, Z_6, Z_6) \} \\ \end{aligned} \end{aligned}$$

With this example in mind, there are four main modifications (more details in the extended version) when moving from first-order AC-unification to nominal AC-matching. When eliminating common arguments we do not eliminate arguments $t_i$ and $s_j$ of t and s if they are equal modulo AC, we eliminate them if they are $\alpha$-equivalent (modulo AC) under the context $\Gamma$ that we are working with. Regarding the new variables introduced: the permutation suspended on them is always the identity. Additionally, we drop the cases where a moderated variable $\pi \cdot X$, with $X \in \mathcal {X}$, is paired with an AC-function application. Finally, we must guarantee that the new variables $Z_i$s introduced by the algorithm can be instantiated, i.e. $Z_i \not \in \mathcal {X}$.

4 Formalisation

As is done in [7], to help us in the proofs of termination (Sect. 4.2), soundness (Sect. 4.3) and completeness (Sect. 4.4) we define the notion of a nice input (Sect. 4.1).

4.1 Nice Inputs

Nice inputs are invariant under the action of the ACMatch function with valuable properties. Notice that Item 7 of Definition 10 would need to be removed for the proofs of termination, soundness, and completeness to be used in unification.

Definition 10

(). An input $(\Gamma , P, \sigma , V, \mathcal {X})$ is said to be nice if:

• 1. $\sigma$ is idempotent.

• 2. $Vars (P) \cap dom (\sigma ) = \emptyset$.

• 3. $\sigma \subseteq V$.

• 4. $Vars (P) \subseteq V$.

• 5. $Vars (\Gamma ) \subseteq V$.

• 6. $\mathcal {X} \subseteq V$.

• 7. $Vars ( rhs (P)) \subseteq \mathcal {X}$.

4.2 Termination

For the lexicographic measure used in the proof of termination, we need the definition of the size of an equational constraint $t \approx _? s$ (Definition 11).

Definition 11

(). The size of an equational constraint $t \approx _? s$ is $size(t) + size(s)$, where the is recursively defined as follows:

• $size(a) = 1$.

• $size(\pi \cdot X) = 1$.

• $size(\langle \rangle ) = 1$.

• $size(\langle t_1, t_2 \rangle ) = 1 + size(t_1) + size(t_2)$.

• $size(f \ t_1) = 1 + size(t_1)$.

• $size(f^{AC} \ t_1) = 1 + size(t_1)$.

• $size([a] t_1) = 1 + size(t_1)$

Although the nominal AC-matching algorithm is based on the first-order AC-unification algorithm ([7]), the proof of termination was much easier for nominal AC-matching than for first-order AC-unification. Instead of the intricate lexicographic measure used in [7] (which came from the work of [17]), it was possible to prove that for the particular case of matching (unlike unification) all the new moderated variables introduced by solveAC are instantiated by instantiateStep.

Hence, the lexicographic measure used has as its first component the number of variables in the equational constraints P and as a second component the multiset order of the size of each equation $t \approx _? s \in P$. Although PVS does not directly implement multiset orders, this part can be emulated easily by analysing the maximum size n of all equations $t \approx _? s$ in P and the number of equations $t \approx _? s$ in P with maximal size (in this order). The algorithm selects an equation with maximal size to simplify (the heuristic selection is enforced by the function chooseEq).

4.3 Soundness

As mentioned, to match terms t and s we first call the Algorithm 1 with parameters $\Gamma = \emptyset$, $P = \{t \approx _? s \}$, $\sigma = id$, $V = Vars (t, s)$ and $\mathcal {X} = Vars (s)$. However, since the parameters of ACMatch change after recursive calls, the proof of soundness (Corollary 1) cannot be done directly by induction, and we must instead prove first the Theorem 1 with generic parameters $\Gamma$, P, $\sigma$, V and $\mathcal {X}$. Once the Theorem 1 is proved, it is also immediate to adapt the algorithm to solve nominal AC-equality checking and to prove its soundness (Corollary 2).

Theorem 1

(). Let the pair $(\Gamma _1, \sigma _1)$ an output of $\textsc {ACMatch} (\Gamma , P, \sigma , V, \mathcal {X})$ and suppose that $(\Gamma , P, \sigma , V, \mathcal {X})$ is a nice input. If $(\Delta , \delta )$ is a solution to $(\Gamma _1, \textsc {nil}, \sigma _1, \mathbb {X},\mathcal {X})$ then $(\Delta , \delta )$ is a solution to $(\Gamma , P, \sigma , \mathbb {X}, \mathcal {X})$.

Corollary 1

(). Let the pair $(\Gamma _1, \sigma _1)$ an output of $\textsc {ACMatch} (\emptyset , \{t \approx _? s \}, id, Vars (t, s), Vars (s))$. If $(\Delta , \delta )$ is an instance of $(\Gamma _1, \sigma _1)$ that does not instantiate the variables in s, then $(\Delta , \delta )$ is a solution to $(\emptyset , \{t \approx _? s \}, id, \mathbb {X}, Vars (s))$.

Corollary 2

(). Let $(\Gamma _1, \sigma _1)$ be an output of $\textsc {ACMatch} (\emptyset , \{t \approx _? s \}, id, Vars (t, s), Vars (t, s))$. If $(\Delta , \delta )$ is an instance of $(\Gamma _1, \sigma _1)$ that does not instantiate the variables in t or s, then $(\Delta , \delta )$ is a solution to $(\emptyset , \{t \approx _? s \}, id, \mathbb {X}, Vars (t, s))$.

Remark 5

An interpretation of Corollary 1 is that if $(\Delta , \delta )$ is an AC-matching instance to one of the outputs of ACMatch, then $(\Delta , \delta )$ is an AC-matching solution to the original problem. Corollary 2 has a similar interpretation, replacing AC-matching with AC-equality checking.

4.4 Completeness

Completeness of Algorithm 1 is given by the Corollary 3 and similarly to the soundness proof, it is derived easily after proving the Theorem 2.

Theorem 2

(). Let $(\Gamma , P, \sigma , V, \mathcal {X})$ be a nice input. Suppose that $(\Delta , \delta )$ is a solution to $(\Gamma , P, \sigma , \mathbb {X}, \mathcal {X})$, that $\delta \subseteq V$ and that $Vars (\Delta ) \subseteq V$. Then, there exists $(\Gamma _1, \sigma _1) \in \textsc {ACMatch} (\Gamma , P, \sigma , V, \mathcal {X})$ such that $(\Delta , \delta )$ is an instance (restricted to the variables of V) of $(\Gamma _1, \sigma _1)$ that does not instantiate the variables in $\mathcal {X}$.

Corollary 3

(). Suppose that $(\Delta , \delta )$ is a solution to $(\emptyset , \{t \approx _? s \}, id, \mathbb {X}, Vars (s))$, that $\delta \subseteq V$ and that $Vars (\Delta ) \subseteq V$. Then, there exists $(\Gamma _1, \sigma _1) \in \textsc {ACMatch} (\emptyset , \{t \approx _? s \}, id, V, Vars (s))$ such that $(\Delta , \delta )$ is an instance (restricted to the variables of V) of $(\Gamma _1, \sigma _1)$ that does not instantiate the variables of s.

Corollary 4

(). Suppose $(\Delta , \delta )$ is a solution to $(\emptyset , \{t \approx _? s\}, id, \mathbb {X}, Vars (t, s))$ satisfying $\delta \subseteq V$ and $Vars (\Delta ) \subseteq V$. Then, there exists $(\Gamma _1, \sigma _1) \in \textsc {ACMatch} (\emptyset , \{t \approx _? s \}, id, V, Vars (t, s))$ such that $(\Delta , \delta )$ is an instance (restricted to the variables of V) of $(\Gamma _1, \sigma _1)$ that does not instantiate the variables of t or s.

Remark 6

An interpretation of Corollary 3 is that if $(\Delta , \delta )$ is an AC-matching solution to the initial problem, then $(\Delta , \delta )$ is an AC-matching instance of one of the outputs of ACMatch. Corollary 4 has a similar interpretation, replacing AC-matching with AC-equality checking.

As was the case for first-order AC-unification (see [7]), the hypothesis $\delta \subseteq V$ in the proof of completeness is merely a technicality that was put in order to guarantee the new variables introduced by the algorithm in the AC-part do not clash with the variables in $dom (\delta )$ or in the terms in $im(\delta )$. This mechanism could be replaced by a different one that assures that the variables introduced by the AC-part of ACMatch are indeed new. When going from the first-order setting to the nominal setting, we go from having a unifier $\delta$ to a pair $(\Delta , \delta )$ and hence we must add the hypothesis $Vars (\Delta ) \subseteq V$.

Remark 7

(High-level description of how to remove hypotheses $\delta \subseteq V$ and $Vars (\Delta ) \subseteq V$). The critical step to prove a variant of Corollary 3 with $V = Vars (t, s)$ and without the hypothesis $\delta \subseteq V$ and $Vars (\Delta ) \subseteq V$ is to prove that the outputs computed when we call ACMatch with input $(\Gamma , P, \sigma , V, \mathcal {X})$ “differ only by the name of the new variables” from the outputs computed when we call ACMatch with input $(\Gamma , P, \sigma , V', \mathcal {X})$. However, this cannot be proved directly by induction because if V and $V'$ differ and ACMatch enters in the AC-part, the new variables introduced for each input may “differ only by a renaming” and once we instantiate those variables, it may happen that the substitutions computed so far (the third component in the input quintuple) will also “differ only by the name of the new variables”. Similar to what was done in first-order AC-unification, the solution is to prove the more general statement that if the inputs $(\Gamma , P, \sigma , V, \mathcal {X})$ and $(\Gamma , P, \sigma ', V', \mathcal {X'})$ “differ only by the name of the new variables”, then the output of ACMatch with the first input “differ only by the name of the new variables” from the output of ACMatch with the second input.

5 Towards a Nominal AC-Unification Algorithm

Stickel’s AC-unification algorithm relies on solving Diophantine equations where new variables are used to represent arguments of AC operators. Using the same approach to solve nominal AC-unification problems leads to non-termination in cases where the same variable occurs as an argument of an AC operator multiple times with different suspended permutations.

As an example, suppose that we are working under an empty context (i.e. $\Gamma = \emptyset$) and want to solve the equational constraint $f(X, W) \approx _? f(\pi \cdot X, \pi \cdot Y)$, with $\mathcal {X} = \emptyset$. Additionally, assume that we apply Stickel’s AC-unification algorithm to this equational constraints and let $Z_1, W_1, Y_1, X_1$ be the name of the new variables introduced (we choose these names deliberately to make the loop in nominal AC-unification clearer). Then, 7 branches (more details in the extended version) are generated and one of them is:

$$ \{X \approx _? Y_1 + X_1, W \approx _? Z_1 + W_1, \pi \cdot X \approx _? W_1 + X_1, \pi \cdot Y \approx _? Z_1 + Y_1 \} $$

After instantiating the variables we obtain

$$\begin{aligned} \sigma = \{X \mapsto f(Y_1, X_1), \ W \mapsto f(Z_1, W_1), Y \mapsto f(\pi ^{-1} \cdot Z_1, \pi ^{-1} \cdot Y_1) \} \end{aligned}$$

and one equational constraint remain: $f(X_1, W_1) \approx _? f(\pi \cdot X_1, \pi \cdot Y_1)$. Notice that our final problem is essentially a renaming of our initial problem:

$$\begin{aligned} f(X, W)&\approx _? f(\pi \cdot X, \pi \cdot Y) \\ f(X_1, W_1)&\approx _? f(\pi \cdot X_1, \pi \cdot Y_1) \end{aligned}$$

This problem does not arise in first-order AC-unification because, in the corresponding first-order problem, we would not have two different permutations (id and $\pi$ in this case) suspended on the same variable (X in this case). Instead, we would have the same variable X as an argument to both terms and eliminate it. Finally, this problem also does not arise in nominal AC-matching because X would be a protected variable. Hence, we would not compute the substitution $\sigma = \{X \mapsto f(Y_1, X_1), W \mapsto W_1, Y \mapsto \pi ^{-1} \cdot Y_1 \}$, we would instead discard this branch. In future work, we will consider the alternative approach to AC-unification proposed by Boudet, Contejean and Devie [8, 10], which was used to define AC higher-order pattern unification [9]. To our knowledge, this AC unification approach has not been formalised yet. However, it has the advantage of generating simpler Diophantine systems, which could simplify the task of nominal AC-unification.

6 Conclusion and Future Work

We propose the first (to the best of our knowledge) nominal AC-matching algorithm, together with proofs of its termination, soundness and completeness. All proofs were formalised in the proof assistant PVS. As a byproduct, we also obtained a formalised nominal AC-equality checking algorithm. Nominal AC-matching has applications for nominal AC-rewriting, being the first step towards a nominal AC-unification algorithm.

Our formalisation extends the formalisation of first-order AC-unification by Ayala-Rincón et al. [7] to nominal terms and uses the functions that deal with freshness constraints from [6], extending them to deal with AC-function symbols. Furthermore, by adding a parameter $\mathcal {X}$ for protected variables, it enables both AC-matching and AC-equality checking, according to whether $\mathcal {X}$ is the set of variables in the right-hand side of the problem or the set of variables in the problem. The .pvs files have a combined size of 290 KB and contain the specification of functions and the statements of the theorems. The .prf files contain the proofs of the theorems and have a combined size of 22 MB.

Future work will explore ways to define a nominal AC-unification algorithm, avoiding the loop described in Sect. 5. We will consider alternative AC-unification algorithms as a starting point [9, 10] and explore the connection between higher-order pattern unification and nominal unification (e.g., [13, 23]).

A nominal AC-unification algorithm would have applications in logic programming languages that employ the nominal paradigm, such as $\alpha$-Prolog. A second possible future work path is to use this formalisation to formalise a more efficient nominal AC-matching algorithm. Finally, a third future work path would be formalising matching/unification algorithms for different equational theories and a fourth path would be investigating if/how nominal unification algorithms can be used for term indexing.