key: cord-0060361-xd9hkysr
authors: Ayala-Rincón, Mauricio; Fernández, Maribel; Nantes-Sobrinho, Daniele; Vale, Deivid
title: Nominal Equational Problems
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_2
sha: 38dee3f389a74f86083646255c9aded2cf32e69f
doc_id: 60361
cord_uid: xd9hkysr

We define nominal equational problems of the form [Formula: see text] , where [Formula: see text] consists of conjunctions and disjunctions of equations [Formula: see text] , freshness constraints [Formula: see text] and their negations: [Formula: see text] and [Image: see text], where [Formula: see text] is an atom and [Formula: see text] nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo [Formula: see text] -equality) is decidable.

Nominal unification [23] is the problem of solving equations modulo α-equivalence. A solution consists of a substitution and a freshness context ∇, i.e., a set of primitive constraints of the form a#X (read: "a is fresh for X"), which intuitively means that a cannot occur free in the instances of X. Nominal unification is decidable and unitary [23] , and efficient algorithms exist [5, 17] , which can be used to solve problems of the form ∃X ( ∆ i s i ≈ α t i ), where s i , t i are nominal terms with variables X and ∆ i is a freshness context.

Similarly, nominal disunification is the problem of solving disequations i.e., negated equations of the form s ≈ α t. An algorithm to solve nominal constraint problems of the form

is available [1] , which finds solutions in the nominal term algebra T (Σ, A, X) by constructing suitable representation of the witnesses for the variables in P. Comon and Lescanne [10] investigated a more general version of this problem, called equational problem, in their words: "an equational problem is any firstorder formula whose only predicate symbol is =", that is, it has the form ∃w 1 , . . . , w n ∀y 1 , . . . , y m : P where P is a system, i.e., an equation s = t, or a disequation s = t, or a disjunction of systems P i , or a conjunction of systems P i , or a failure ⊥, or success . The study of such problems was motivated by applications in pattern-matching for functional languages, sufficient completeness for term rewriting systems, negation in logic programming languages, etc.

In order to extend these applications to languages that offer support for binders and α-equivalence following the nominal approach, such as αProlog [6] , αKanren [4] , αLeanTAP [20] , to nominal rewriting [14] and nominal (universal) algebra [15] , in this paper we consider nominal equational problems.

Based on Comon and Lescanne's work, the nominal extension of a first-order equational problem is a formula P ::= ∃W 1 . . . W n ∀Y 1 . . . Y m : P where P is a nominal system, i.e., a formula consisting of conjunctions and disjunctions of freshness, equality constraints, and their negations.

Contributions. This paper introduces nominal equational problems (NEPs) and presents simplification rules to find solutions in the ground nominal algebra. The simplification rules are shown to be terminating (by using a measure that strictly decreases with each rule application), and also sound and solution-preserving. The simplification process for NEPs is more challenging than in the syntactic case because it deals with two predicates (≈ α and #) and needs to consider the interaction between freshness and α-equality constraints, and quantifiers. The elimination of universal quantifiers requires careful analysis since universal variables may occur in freshness constraints and in their negations. To make the process more manageable, we define a set of rules together with a strategy of application (specified by rule conditions) that simplifies the termination proof.

Finally, we show that the irreducible forms are either ⊥ or problems from which a solution can be easily extracted. In particular, if the NEP consists only of existentially quantified conjunctions of freshness and α-equality constraints, we obtain solved forms consisting of a substitution and a freshness context, as in the standard nominal unification algorithm [23] .

Related Work. Comon and Lescanne [10] introduced first-order equational problems and studied their solutions in the algebra of rational trees, the initial term algebra, and the ground term algebra. A restricted version of equational problems, called disunification problems, which do not contain quantified variables, has been extensively studied in the first-order framework [8, 3, 11, 2, 22] . More recently, a nominal approach to disunification problems was proposed by Ayala et.al [1] , including only conjunctions of equations and disequations and freshness constraints, without quantified variables. Here we generalise this previous work to deal with general formulas including disjunction, conjunction and negation of equations and freshness constraints, as well as existential and universal quantification over variables. To deal with negation of freshness, disjunctive formulas, and quantification we extend the semantic interpretation and design a different set of simplification rules as well as a more elaborated strategy for rule application.

Extensions of first-order equational problems modulo equational theories have also been considered. Although the problem of solving disequations modulo an equational theory is not even semi-decidable in general (as shown by Comon [7] ), there are useful decidable and semi-decidable cases. For example, solvability of complement problems (a sub-class of equational problems) is decidable modulo theories with permutative operators (which include commutative theories) [9, 13] , and for linear complement problems solvability modulo associativity and commutativity is also decidable [16, 19, 12] . Buntine and Bürckert [3] solve systems of equations and disequations in equational theories with a finitary unification type. Fernández [11] shows that E-disunification is semi-decidable when the theory E is presented by a ground convergent rewrite system, and gives a sound and complete E-disunification procedure based on narrowing. Baader and Schulz [2] show that solvability of disunification problems in the free algebra of the combined theory E 1 ∪ . . . ∪ E n is decidable if solvability of disunification problems with linear constant restrictions in the free algebras of the theories E i (1 ≤ i ≤ n) is decidable. Lugiez [18] introduces higher-order disunification problems and gives some decidable cases for which equational problems can be extended to higher-order systems.

Organisation. Section 2 recalls the main concepts of nominal syntax and semantics. Section 3 introduces nominal equational problems and a notion of solution for such problems. Section 4 presents a rule-based procedure for solving NEPs, as well as soundness, preservation of solutions, and termination results. Section 5 shows that the simplification rules reach solved forms from which solutions can be easily extracted. Section 6 concludes and discusses future work.

We assume the reader is familiar with nominal techniques and recall some concepts and notations that shall be used in the paper; for more details, see [14, 21, 23] .

Nominal Terms. We fix countable infinite pairwise disjoint sets of atoms A = {a, b, c, . . .} and variables X = {X, Y, Z, . . .}. Atoms follow the permutative convention: names a, b range permutatively over A. Therefore, they represent different objects. Let Σ be a finite set of term-formers disjoint from A and X such that for each f ∈ Σ, a unique non-negative integer n (the arity of f , written as f : n) is assigned. We assume there is at least one f : n such that n > 0.

A permutation π is a bijection A → A with finite domain, i.e., the set dom(π) := {a ∈ A | π(a) = a} is finite. We shall represent permutations as lists of swappings π = (a 1 b 1 )(a 2 b 2 ) . . . (a n b n ). The identity permutation is denoted by id and π • π the composition of π and π . The set P of all such permutations together with the composition operation form a group (P, •) and it will be denoted simply by P. The difference set of π and γ is defined by ds(π, γ) = {a ∈ A | π(a) = γ(a)}.

The set T (Σ, A, X) of Nominal Terms, or just terms for short, is inductively defined by the following grammar:

where a is an atom, π · X is a moderated variable, [a]t is the abstraction of a in the term t, and f (t 1 , . . . , t n ) is a function application with f ∈ Σ and f : n. A term is ground if it does not contain variables.

In an abstraction [a]t, t is the scope of the binder [·] and it binds all free occurrences of a in t. An occurrence of an atom in a term is free if it is not under the scope of a binder. Notice that syntactical equality is not modulo α-equivalence; for example, [a]a ≡ [b]b. We may denote s ≡ t by s = t with the same intended meaning andt abbreviates an ordered sequence t 1 , . . . , t n of terms. We inductively extend the action of a permutation π to a term t, denoted as π · t, by setting: π · a = π(a), π · (π · X) = (π • π ) · X, π · ([a]t) = [π(a)](π · t), and π · f (t) = f (π ·t).

Substitutions, ranging over σ, γ, τ . . ., are maps (with finite domain) from variables to terms. The action of a substitution σ on a term t, denoted tσ, is inductively defined by: aσ = a, (π · X)σ = π · (Xσ), ([a]t)σ = [a](tσ) and f (t 1 , . . . , t n )σ = f (t 1 σ, . . . , t n σ). Notice that t(σγ) = (tσ)γ. Freshness and α-equality. A nominal equation is the symbol or an expression s ≈ α t where s and t are nominal terms. A trivial equation is either s ≈ α s or . Freshness constraints have the form a#t where a is an atom and t a term. A freshness context is a finite set of primitive freshness constraints of the form a#X, we use ∆, ∇, and Γ to denote them. We extend the notation to sets of atoms: A#X denotes that a#X for every a ∈ A.

α-derivability is given by the deduction rules in Figure 1 , which define an equational theory called CORE. -Write ∇ a#t when there exists a derivation of ∇ a#t. The judgement ∇ a#t intuitively means that using freshness constraints from ∇ as assumptions a does not occur free in t. -Write ∇ s ≈ α t when there exists a derivation of ∇ s ≈ α t.

The judgement ∇ s ≈ α t intuitively means that using freshness constraints from ∇ as assumptions s is α-equivalent to t.

Semantic Notions. Nominal equational theory has a natural semantic denotation in nominal sets since we can easily interpret freshness and abstraction. A P-set X is an ordinary set equipped with an action in P × X → X (written as π · x) such that id · x = x and π · (π · x) = (π • π ) · x. A set of atoms A ⊂ A supports x ∈ X iff for all permutations π ∈ P fixing every element of A · acts trivially on x via π, i.e., if π(a) = a for all a ∈ A then π · x = x. Semantic freshness is defined in terms of support as follows: an atom a is fresh for x ∈ X iff a / ∈ supp(x). We denote this by writing a# sem x. A nominal set is a P-set such that every element is finitely supported.

To build an algebraic ground term-model of CORE, we fix the set G consisting of equivalence classes of provable α-equivalent ground terms. More precisely, given a ground term g, the class g is the set of ground terms g for which there exist a derivation g ≈ α g . Note that G is a nominal set by defining the natural action: π ·g = π · g. Each function symbol f ∈ Σ is interpreted by an equivariant function

Signature interpretation is homomorphically extended to the set of terms as follows: Fix a valuation function ς that assigns to every variable X ∈ X an element of G. The interpretation of a term t under ς, t ς , is defined as:

with domain A and ς a valuation function assigning for every variable X ∈ X an element of A. We say that:

A model of a nominal theory is an interpretation that validates all of its axiomatic judgements ∇ s ≈ α t. It is easy to see that the interpretation we define above is a model of CORE. For the rest of the paper, we slightly abuse notation by calling CORE both the theory and its model making distinctions when necessary.

It is worth noticing the syntactic character of CORE: by interpreting atoms as themselves and since there are no equational axioms, we easily connect ∇ |= a#t and ∇ a#t. This behaviour is not the rule if equational axioms are considered. For instance, consider the theory LAM that axiomatises β-equality in the λ-calculus. It is a fact that a# sem (λ[a]b)a in LAM but there is no syntactic derivation for a#(λ[a]b)a. Furthermore, by completeness for equality derivation, we establish a connection between ∇ |= s ≈ α t and ∇ s ≈ α t.

There are alternative definitions of nominal terms where the syntax is manysorted. We chose to work with an unsorted syntax for simplicity; all the results below can be extended to the many-sorted case, indeed they are proved for any infinite subalgebra of the ground nominal algebra.

In this section, we introduce nominal equational problems (NEPs) as our main object of study. A NEP is a fist-order formula built only with the predicates ≈ α and #. Their negations, denoted ≈ α and #, are used to build disequations and non-freshness constraints. A trivial disequation is either s ≈ α s or ⊥.

Intuitively, a non-freshness constraint a #t -read a is not fresh for t -states that there exists at least one instance of t where a occurs free. Similarly, for disequations: s ≈ α t states that s and t are not α-equivalent.

A nominal system is a formula defined by the following grammar:

In the next definition, we make a distinction between the set of variables occurring in a NEP: the mutually disjoint sets W = {W 1 , . . . , W n } and Y = {Y 1 , . . . , Y m } denote existentially and universally quantified variables, respectively. The former we call auxiliary variables and the latter parameters.

A NEP is a formula of the form below, where P is a nominal system.

The set Fv(P) contains the free variables occurring in P. For the rest of the paper, we use the following implicit naming scheme for variables: W denotes an auxiliary variable, Y a parameter, X a free variable, and Z an arbitrary variable.

Example 2. Nominal disunification constraints [1] are pairs of the form P :

This problem is a particular NEP: taking the judgement ∆ s ≈ α t as ∆ ⇒ s ≈ α t, or yet as ¬∆ ∨ s ≈ α t 4 , we obtain the formula:

Sufficient completeness, that is, deciding whether a set of pattern (rules) covers all possible cases, is a well-known problem in functional programming. In the next example, we show how to naturally represent such problems as NEPs.

Example 3. Consider the function map which applies a function [a]F to every element of any list L. It may be defined by the rules below:

where {a → } is a binary term-former representing (explicit) substitutions; see [14, Example 43] for more details. Since we are not imposing a type discipline on nominal terms it is possible to construct ill-typed terms, for instance map(a, [a]t). In what follows we ignore those expressions by noticing that a type discipline will not allow such constructions. Then sufficient completeness can be checked using the following NEP:

If the problem has a solution then R map is not complete, and the solution indicates the missing pattern cases in the definition.

Solutions of Nominal Equational Problems. We are interested in solutions for NEPs in the ground nominal algebra. From now on, A denotes an infinite subalgebra of CORE with domain A. Below we define solutions using idempotent substitutions, which can be seen as a representation for valuations that map variables to elements of the ground term algebra.

We first extend the interpretation function under a valuation ς · ς (see Section 2) to the negated form of freshness and α-equality constraints.

it is not the case that a# sem t ς , this is written a #t ς ; and, respectively,

In standard unification algorithms, idempotent substitutions are used as a compact representation of a set of valuations in the ground term algebra. Similarly, given a valuation in the ground term algebra, one can build a ground substitution representing it. In the case of the ground nominal algebra, where elements are α-equivalence classes of terms, the representative is generally not unique, but any representative can be used.

Given a substitution σ = [X 1 /t 1 , . . . , X n /t n ], for any valuation ς, we denote by ς σ the valuation such that ς σ (X) = ς(X) if X ∈ dom(σ), and ς σ (X) = Xσ ς otherwise.

Given

, and a finite set X of variables, we denote by σ ς X any ground substitution such that for each

We say that σ ς X is a grounding substitution for X .

The next lemma states that under mild conditions we can extend substitutions to valuations preserving semantic equality. The next definition allows us to use idempotent substitutions to represent solutions of constraints. A-validation) . Let σ be an idempotent substitution whose domain includes all the variables occurring in a constraint C. Then σ A-validates C iff C ς σ is valid in A for any valuation ς.

We now extend semantic validity to the syntax of systems. The interpretation for the logical connectives is defined as expected.

For an idempotent substitution σ whose domain includes all variables occurring in a system P , we say that σ A-validates P iff 1. P = ; or 2. P = C and σ A-validates C; or 3. P = P 1 ∧ . . . ∧ P n and σ A-validates each P i , 1 ≤ i ≤ n; or 4. P = P 1 ∨ . . . ∨ P m and σ A-validates at least one

Solutions of equational problems instantiate free variables and satisfy existential and universal requirements for auxiliary variables and parameters, respectively. To define this notion, we extend the domain of the substitution to include also existential and universally quantified variables as follows. In Definition 10, δ is the substitution that instantiates auxiliary variables, so there can be many (possibly infinite) number of such δ's.

If σ is an A-solution of the NEP P then for any permutation π, π · σ (defined by [X i /π · t i ], as expected) is an A-solution of π · P. In particular, if an A-solution contains an atom not occurring in P, that atom can be swapped for any other atom not occurring in P.

Lemma 2 is a direct consequence of the fact that interpretations are equivariant, and shows that solutions are closed by permutation. It allows us to use permutations to represent infinite choices for atoms in solutions. 

If σ is an A-solution of the NEP P = ∃W ∀Y : P then any idempotent substitution σ obtained as an instance of σ such that dom(σ ) = dom(σ) is also an A-solution of P. In particular, for any such ground instance σ of σ there is a ground substitution δ, where dom(δ) = W , such that for all ground substitution λ, where dom(λ) = Y , σ δλ A-validates P .

Proof. By definition of A-solution, to show that σ is an A-solution of P we need to consider all the valuations of the form ς σ δλ as indicated in Definitions 8, 9, 10 . The result follows from the fact that for any valuation ς σ δλ there exists an equivalent valuation ς σδλ by Lemma 1.

In this section we present a set of simplification rules to solve NEPs. A simplification step, denoted P =⇒ P , transforms P into an equivalent problem P from which solutions are easier to extract.

Rules may have application conditions (rule controls) that define a strategy of simplification. Our strategy gives priority to rules according to their role. We split the rules into groups R i as shown in Figures 2, 3 and 4: R 1 eliminates trivial constraints, R 2 deals with clash and occurs check, R 3 eliminates unneeded quantifiers, R 4 and R 5 decompose positive and negative constraints, respectively, R 6 eliminates parameters and R 7 instantiates variables. The Explosion and Elimination of Disjunction rules in R 8 search for solutions as explained below. Finally, R 9 eliminates the remaining universal quantifiers. A rule R ∈ R i can only be applied if no rules from R j , where j < i, can be applied.

Since we are dealing with formulas that contain disjunction and conjunction connectives, we need to take into account the standard Boolean axioms. To simplify, instead of working modulo the Boolean axioms we apply a Boolean normalisation step before a rule is applied. Following Comon and Lescanne [10] , we choose to take conjunctive normal form: Before the application of each rule P is reduced to a conjunction of disjunctions.

The explosion rule creates new branches by instantiating variables considering all possible ways of constructing terms (i.e., each f ∈ Σ, abstractions and atoms). Note that Σ ∪ Atoms(P ) ∪ {a } is a finite set (we can represent all possible constructions with a finite number of cases), so the rule is finitely branching.

The rule Elimination of Disjunctions also builds a finite number of branches. Therefore, our procedure builds a finitely branching tree of problems to be solved.

Rules R 1 -R 8 are not sufficient to eliminate all parameters from a NEP (see Example 6) in contrast with the syntactic case [7] , where similar rules produce parameterless normal forms. This is because we are dealing with both freshness and α-equality. Indeed, normal forms for rules R 1 -R 8 may contain parameters, but only in disjunctions involving both freshness and equality constraints for the same parameter as the following lemma states. The rules in R 9 (Figure 4 ) are introduced to deal with this problem.

(CL1) s ≈α t =⇒ (CL2) s ≈α t =⇒ ⊥ Conditions for (CL1) and (CL2): s( ) = t( ) and neither is a moderated variable. (O1) π · Z ≈α t =⇒ ⊥ (O2) π · Z ≈α t =⇒ Conditions for (O1) and (O2): Z ∈ vars(t) and t ≡ π · Z R3: Elimination of parameters and auxiliary unknowns.

(C1) ∀Y , Y : P =⇒ ∀Y : P, Y / ∈ vars(P ) (C2) ∃W , W : P =⇒ ∃W : P, W / ∈ vars(P ) (C3) ∃W , W : π · W ≈α t ∧ P =⇒ ∃W : P, W / ∈ vars(P, t)

R4: Equality and freshness simplification

-Each equation in the disjunction contains at least one occurrence of a parameter and πi · Zi ≡ ti for each i = 1, . . . , n. -Q does not contain any parameter.

-If π = id then Z is not a parameter and Z occurs in P and if t is a variable then t occurs in P .

-If π = id then Z occurs in P and if t is a variable then t occurs in P .

-If π = id then t is not of the form id · Z . 1. X is a free or existential variable occurring in P , W are newly chosen auxiliary variables not occurring anywhere in the problem; 2. f ∈ Σ and a ∈ Atoms(P ) ∪ {a }, where a is a new atom; 3. there exists an equation X ≈α u (or disequation X ≈α u) in P such that u is not a variable and contains at least one parameter; and 4. no other rule can be applied.

are irreducible: neither (U 4 ) nor (ED 1 ) apply since all the disjuncts contain parameters; (ED 2 ) does not apply since each constraint has a parameter that occurs in another constraint; (Exp) does not apply because there is no equation or disequation with a free or existentially quantified variable in one side.

The following lemma characterises the irreducible disjunctions with respect to rules R 1 -R 8 where parameters may remain.

Let P be a disjunction of constraints irreducible w.r.t. R 1 -R 8 . For each parameter Y such that P = a#Y ∨ Q (resp. P = a #Y ∨ Q), for some atom a, the following holds:

1. a #Y (resp. a#Y ) cannot occur in Q; 2. Y has to occur in Q;

Y ≈ α t, where Y / ∈ vars(t), or Y ≈ α t, with Y ∈ vars(t);

Proof. In an irreducible disjunction of constraints at least one of the sides of equations (or disequations) is a variable, otherwise we could simplify the equation/disequation. Condition 1. It holds, otherwise we could apply (T 9 ). Condition 2. It holds, otherwise we could apply (ED 2 ). Condition 3. If Q had an equation of the form X ≈ α t, for some free or existentially quantified variable, then t could not contain a parameter, otherwise we could apply rule (Exp). Therefore, t = t[Z 1 , . . . , Z n ], for n ≥ 0 where each Z i R9: Simplification of parameters in freshness constraints

if R1-R8 do not apply (so Q does not contain a #Y ) and Y ∈ vars(Q).

if R1-R8 do not apply (so Q does not contain a#Y ) and Y ∈ vars(Q).

is either a free or existentially quantified variable, and one could apply rule ED 1 . Thus, if an equation exists, one of the sides has to be a parameter, say Y ≈ α t, and Y cannot occur in t otherwise rule O 2 applies. Condition 4. If Q were to contain a disequation, say X ≈ α t then t could not contain a parameter, otherwise we could apply (Exp) as above, but then we could apply rule (ED 1 ). Therefore, if Q were to contain a disequation, it would be of the form Y ≈ α t, then it would either reduce with (O 2 ) or with (U 2 ). Thus, Q does not contain disequations. Similary, if Q contained a primitive freshness constraint for a free or existentially quantified variable then (ED 1 ) would apply.

The remaining disjunctions with parameters can be simplified using the rules in R 9 , since they will not produce solutions (as shown in Theorem 1).

We end this section with an example of application of the simplification rules.

Example 7. Let P be a NEP, using the signature from Example 1, as follows:

Rules in R 1 -R 7 cannot be applied and the explosion rule produces six problems:

Reducing the first problem we get:

At this point P1 has reached a normal form without any parameter. Solutions of P1 can be easily obtained by taking any instance of X of the form λλt. It is easy to check that this choice indeed generates solutions of P. Similar reductions apply to Pi, 2 ≤ i ≤ 6.

As we will see in the next section, application of such simplification rules is well-behaved in the sense that we do not loose any solution along the way.

The next step is to ensure that the application of rules does not change the set of solutions of an equational problem.

A be any infinite subalgebra of CORE.

A-sound if, P =⇒ R P implies S(P ) ⊆ S(P). 2. A rule R is A-preserving if, P =⇒ R P implies S(P) ⊆ S(P ).

A-globally preserving if given any problem P, S(P) ⊆ P → R π · P i supp(π) ∩ Atoms(P) = ∅ S(P i ).

All our rules, except those in R 8 , are sound and preserving (Theorem 1). The rules in R 8 create branches in the derivation tree; they are sound and only globally preserving (Theorem 2). Theorem 1. The rules in R 1 to R 7 and the rules in R 9 are A-sound and A-preserving for any infinite subalgebra A of CORE.

Proof. Rules in R 1 , R 2 , and R 3 : soundness and preservation of solutions are easy to deduce. For instance, for clash rules, (CL 1 ) and (CL 2 ), it follows by inspection of deduction rules that the judgement sγ ≈ α tγ is not derivable for any valuation ς and corresponding grounding substitution γ = σ ς vars(s,t) (see Definition 7) if the root constructors of s and t are different (hence every γ is a solution for the disequation). For (C 3 ) observe that we can take [W/t] as a witness for W on a validation for ∃W : P , if W / ∈ vars(P, t). Rules in R 4 and R 5 . It follows from soundness and preservation of simplification rules in [14] . We use the fact that nominal equality and freshness rules from Fig.  1 are reversible; for instance, let γ be a grounding substitution, a judgement f (s)γ ≈ α f (ũ)γ fails, which makes f (s)γ ≈ α f (ũ)γ valid, iff one of the premises s i γ ≈ α u i γ does not hold. Rules in R 6 : The result is straightforward for rules U 1 and U 3 . U 2 . To prove soundness for U 2 notice that the solution set of a conjunction is the intersection of the solution set of each of its members. We have to show that every solution of Q[Y /π −1 · t] is a solution of (π · Y ≈ α t ∨ Q). Let γ be a solution of Q[Y /π −1 · t] and take any substitution λ satisfying the conditions of Definition 10. So (Q[Y /π −1 · t])γλ is valid and we need to show the validity of (π · Y ≈ α t)γλ ∨ Qγλ.

(1)

For each such λ there are two possible cases: First, π · Y λ ≈ α tγλ (note that λ is a ground substitution so both sides of this equation are ground); then we have that γλ = γλ [Y /π −1 · tγλ]. By hypothesis, γλ validates Q[Y /π −1 · t] so γλ [Y /π −1 · tγλ] validates Q. Second; π · Y λ ≈ α tγλ, then γλ validates π · Y ≈ α t. Hence γ a solution of (1).

To prove preservation for U 2 , take γ a solution of ∀Y , Y : π · Y ≈ α t ∨ Q, we need to show that γ is also a solution of ∀Y , Y : Q[Y /π −1 · t]. Notice that γ is a solution of ∀Y , Y : π · Y ≈ α t or ∀Y , Y : Q but it clearly cannot solve the first problem. Hence, γ solves ∀Y , Y : Q. By Definition 10, for all substitutions λ with domain Y ∪ {Y } we have that λγ validates Q. In particular, the substitution [Y /π −1 · tγ]λγ which is equivalent to [Y /π −1 · t]λγ (since γ is away from λ) must also validate Q. Consequently, λγ validates (Q[Y /π −1 · t]). U 4 . Soundness for this rule follows trivially. For preservation of solutions, we show that any solution of ∀Y : i Z i ≈ α t i ∨ Q is a solution of ∀Y : Q. The shape of the first problem induces a requirement that the disjunction i Z i ≈ α t i does not have a solution. To show this we prove that the negated form i Z i ≈ α t i has at least one solution. Notice that such a solution is a witness for the failure of i Z i ≈ α t i , since all of those equations have at least one parameter. Lemma 5 shows that this is true. Rules in R 7 . Soundness and preservation of (I 1 ) has been proved in previous works, since rule (I 1 ) is used in standard nominal unification algorithms [23] . Rule (I 2 ) is a direct adaptation of the rule used in the standard (syntactic) case, proved sound and preserving in [10] . Indeed, γ ∈ S(π · Z ≈ α t ∨ P ) if, and only if, for any grounding instance γ of γ, γ ∈ S(Z ≈ α π −1 · t) or γ ∈ S(P ) (by Lemma 3). Finally, notice that γ ∈ S(P ) \ S(Z ≈ α π −1 · t) if and only if γ ∈ S(P [Z/π −1 · t]). Rules in R 9 . Soundness follows trivially, since ⊥ has no solution. We show below that U 7 is A-preserving; the proof is analogous for rule (U 8 ).

Let P = ∃W ∀Y , Y : P ∧ (a#Y ∨ Q) where Q is fully reduced by R 1 -R 8 , Y ∈ vars(Q) and Q does not contain a #Y . We prove that P does not have solutions by induction on the number of freshness constraints in a#Y ∨ Q.

Base case: Q contains just equational constraints, each containing at least one occurrence of the parameter Y , as specified in Lemma 4. Suppose by contradiction that there exists an A-solution γ. Thus, γ is away from Y ∪ {Y }, dom(γ) = X = Fv(P), there is a ground substitution δ with dom(δ) = W and for all λ away from X, W , with dom(λ) = Y ∪ {Y }, γδλ A-validates P ∧ (a#Y ∨ Q). Then, it A-validates both P and (a#Y ∨ Q). The latter implies that γδλ A-validates Q for every λ (but then Q has a solution, which is impossible due to the form of the equational constraints) or Q implies a #Y (since there is at least one f ∈ Σ such that f : n and n > 0, and therefore a#Y is false for an infinite number of ground terms Y λ). The latter is impossible since a#Y is defined as a ∈ supp(Y ), which is defined as (a a ) · Y = Y for a new a , and reduced problems cannot contain fixed point equations or their negations (these are simplified using rules (E 1 ) and (D 1 ), respectively). The inductive step is proved similarly, using Lemma 4 as in the base case to deduce that the constraints in Q cannot entail a #Y .

A be any infinite subalgebra of CORE.

A-sound and A-globally preserving. 2. Rules (ED 1 ) and (ED 2 ) are A-sound and A-globally preserving.

Lemma 5 guarantees the existence of a solution for a conjunction of non-trivial disequations as long as the algebra considered has sufficient ground terms.

Let P be a conjunction of non-trivial disequations. Let A be any infinite subalgebra of CORE. Then P has at least one solution in A.

Proof. The proof proceeds by induction on the number of distinct variables occurring in P. For the base case P has no variables. Then every substitution solves P, since by hypothesis P does not contain any trivial disequation t ≈ α t.

Assume the result holds for problems with m − 1 variables. Let P be a conjunction of non-trivial disequations such that |vars(P )| = m and X ∈ vars(P ). For each disequation s ≈ α t ∈ P, the equation s ≈ α t has at most one solution (modulo α-renaming) when the variables distinct from X are considered as constants. Let S the set of such solutions for all these equations. Since A (the domain of A) is infinite, there exists a ∈ A such that [X/a] / ∈ S. Therefore, [X/a] is a solution for P. Now, consider the problem P = P[X/a] which has m − 1 variables. The result follows by induction hypothesis.

To prove termination we define a measure function for NEPs that strictly decreases with each application of a rule. The measure uses the following auxiliary functions: Definition 12 (Auxiliary Functions). The function sizePar(t) denotes the sum of the sizes of the parameter positions in t:

Given a disjunction of equations, disequations, freshness, and negated freshness constraints d = C 1 ∨ . . . ∨ C n we define auxiliary functions φ 1 and φ 2 over d. (b) otherwise, MSP(s ≈ α t) = MSP(s ≈ α t) = max(sizePar(s), sizePar(t)) and MSP(a#t) = MSP(a #t) = sizePar(t).

Definition 13 (Measure). Let P = ∃W ∀Y d 1 ∧. . .∧d n be a nominal equational problem in conjunctive normal form. P is measured using the tuple: Using this measure we can prove the termination of the simplification process.

Theorem 3. The procedure defined in Section 4 for application of rules, expressed as R := R 1 R 2 . . . R 9 , terminates.

We have shown that the simplification process terminates and each application of the transformation rules preserves solutions. We now characterise the normal forms, called solved forms. Intuitively, solved forms are simple enough that one can easily extract solutions from it. A first example of well-known solved form is that of unification solved form: a conjunction of equations X i = t i such that each X i occurs only once. It directly represents a solution mapping X i → t i . We show in Theorem 4 existence of solutions for certain solved forms, and in Theorem 5 we prove that our procedure is complete with respect to solved forms.

such that: -each Z i occurs only once in P; -each Z j is syntactically different from v j ; and -each C l is either a positive, a#X, or negative, a #X, freshness constraint such that each pair a, X occurs at most once in P.

Theorem 4 below shows that a problem reduced to definition with constraints solved form has at least one solution.

Theorem 4. Let A be any infinite subalgebra of CORE. If P ≡ ⊥ is in definition with constraints solved form, then it has at least one solution.

Proof. First assume P is in unification solved form (see Definition 14) . Let ∇ be the context containing all constraints C l occurring in P. Furthermore, define the substitution σ that assigns to each free variable X i the term t i , and the substitution δ mapping each existential variable W k to t k . Then ∇σδ ς , which is equivalent to ∇ ς σδ by Lemma 1, is valid in A. Consequently, ∇ X i σ ≈ α t i σδ ς and ∇ W k δ ≈ α t k δ ς are valid judgements. So, σ is an A-solution of P with existential witnesses given by δ. In the general case, when P is in definition with constraints solved form containing also negative constraints, the construction is similar. We can guarantee a solution for the disunification part of the problem, The next result states that a NEP's normal form with respect to the simplification rules given in the previous section is a definition with constraints. In particular, all parameters are removed from the problem. The proof is by case analysis, considering all possible occurrences of parameters in a problem. Figures 2, 3 , and 4 are complete for parameterless solved forms and definition with constraints solved forms.

In this paper, we introduced nominal equational problems (NEPs) as an extension of standard first-order equational problems to nominal terms which, besides equations and disequations, includes freshness and non-freshness constraints. We proposed a sound and preserving rule-based algorithm to solve NEPs in the nominal ground algebra CORE, and showed that this algorithm is complete for two main types of solved forms: parameterless and definition with constraints. As future work, we aim to investigate the purely equational approach to nominal syntax via the formulation of freshness constraints using fixed-point equations with the N-quantifier [21] , as well as the solvability of nominal equational problems in more complex algebras.

On Solving Nominal Disunification Constraints

Combination techniques and decision problems for disunification

On solving equations and disequations

earlier version available in the Proc. 2007 Workshop on Scheme and Functional Programming

Matching and alpha-equivalence check for nominal terms

αProlog: A Logic Programming Language with Names, Binding and α-Equivalence

Unification et disunification: Théorie et applications

Computational Logic: Essays in Honor of Alan Robinson

Negation elimination in equational formulae

Equational problems and disunification

Narrowing based procedures for equational disunification

AC complement problems: Satisfiability and negation elimination

Negation elimination in empty or permutative theories

Nominal rewriting. Information and Computation 205

Nominal (Universal) algebra: equational logic with names and binding

A Solution of the Complement Problem in Associative-Commutative Theories

An efficient nominal unification algorithm

Higher order disunification: Some decidable cases

Complement problems and tree automata in AC-like theories (extended abstract)

αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic

Nominal Sets: Names and Symmetry in Computer Science

Asymmetric Unification and Disunification

Nominal unification