## Chapter 14Variants and Variant Unification

### 14.1Introduction

As explained in Section 13.2, Maude (from version 2.7 on) features order-sorted unification modulo axioms Ax, including associativity1 (A), commutativity (C), commutativity-identity (CU), associativity-commutativity (AC), associativity-commutativity-identity (ACU), and (left-, right- or two-sided) identity (Ul, Ur, U). However, order-sorted equational unification in full generality considers a decomposition of an equational theory (Σ,E Ax) into two problems: one of Ax-unification, and another of E Ax-unification that uses an Ax-unification algorithm as a subroutine. As explained in Section 13.5.1, algorithms for E Ax-unification have been extensively defined by using narrowing-based unification, where for a unification problem t = ?t we obtain the search space associated to narrowing the term eq(t,t) using E modulo Ax and search for all paths from eq(t,t) to the truth constant tt. However, we use the notion of variants of a term for generating such a narrowing search space.

Comon-Lundh and Delaune’s notion of variant [36] characterizes the instances of a term w.r.t. an equational theory E Ax such that the equations E are confluent, terminating, and coherent modulo axioms Ax. The E,Ax-variants of a term t are pairs (t,𝜃), with 𝜃 a substitution and t the E,Ax-canonical form of 𝜃(t). A preorder relation of generalization that holds between such pairs provides a notion of most general variant and also of completeness of a set of variants. A complete set of E,Ax-variants (up to renaming) of a term t is a subset V of E,Ax-variants of t such that, for each substitution σ, there is a variant (t,𝜃) V and a substitution ρ such that: (i) t is E,Ax-irreducible, (ii) σ(t)E,Ax = Axρ(t), and (iii) (σE,Ax)|Var(t) = Ax(𝜃;ρ)|Var(t).

In order to avoid clashing of algorithms and notions, we have decided that the equations used for variant generation (and variant-based unification) should be identifiable and clearly distinguished from standard equations in Maude. For this purpose we have defined a new attribute for equations: the word variant. This implies that if the user wants to use an equation t = t’ both for variant generation and for simplification, it should be duplicated: eq t = t’ . and eq t = t’ [variant] . No equation with the variant attribute can have the owise attribute. Note that what this allows is a greater flexibility at the operational level when combining variant generation and simplification: by the above method, an equation can be used for either purpose (declared only once in the appropriate way), or for both, by a double declaration.

For example, consider the following functional module defining the addition function _+_ on natural numbers built from 0 and s:

``` fmod NAT-VARIANT is  sort Nat .  op 0 : -> Nat [ctor] .  op s : Nat -> Nat [ctor] .  op _+_ : Nat Nat -> Nat .  vars X Y : Nat .  eq [base] : 0 + Y = Y [variant] .  eq [ind] : s(X) + Y = s(X + Y) [variant] . endfm
```

The term X + s(0) has an infinite number of variants w.r.t. those equations, i.e.,

• (s(0),{X0}),
• (s(s(Y)),{Xs(Y)}),
• (s(s(0)),{Xs(0)}),
• (s(s(s(Y))),{Xs(s(Y))}),
• (s(s(s(0))),{Xs(s(0))}),

Indeed, there is no finite, complete, most general set of variants for that term. However, the term 0 + X has a finite number of most general variants w.r.t. those equations, i.e., (X,id). Obviously, there are many more variants, such as (0,{X0}), but they are all instances of the most general one.

An equational theory E Ax has the finite variant property iff there is a finite complete set of most general variants for each term. This property also ensures the existence of a generic finitary E Ax-unification algorithm based on computing variants, as shown in Section 14.7. However, if a theory does not have the finite variant property, we are still able to incrementally enumerate all the variants of a term, as explained below in Section 14.5.

Consider the following equational theory for exclusive or.

``` fmod EXCLUSIVE-OR is  sorts Nat NatSet .  op 0 : -> Nat [ctor] .  op s : Nat -> Nat [ctor] .   subsort Nat < NatSet .  op mt : -> NatSet [ctor] .  op _*_ : NatSet NatSet -> NatSet [ctor assoc comm] .   vars X Y Z : [NatSet] .  eq [idem] :   X * X = mt  [variant] .  eq [idem-Coh] : X * X * Z = Z [variant] .  eq [id] :    X * mt = X  [variant] . endfm
```

This theory has the finite variant property, as proved manually in [36] and automatically in [69]. For instance, the term X * X has a finite set of most general variants, just (mt,id). And the term X * Y has also a finite, complete set of most general variants:
1.
(X * Y,id),
2.
(Z,{Xmt,YZ}),
3.
(Z,{XZ,Ymt}),
4.
(Z,{XZ * U,YU}),
5.
(Z,{XU,YZ * U}),
6.
(mt,{XU,YU}), and
7.
(Z1 * Z2,{XU * Z1,YU * Z2})

Note that if variable X in the equational theory is changed from sort [NatSet] to Nat (or [Nat]), then the theory does not have the finite variant property, since every pair of similar elements has to be separately eliminated, whereas now chunks of similar elements can be eliminated at once. Also, note that the symbol _*_ cannot be made ACU instead of AC, because then the equation X * X * Z = Z is not ACU-terminating.2

The finite variant property happens to be an undecidable problem [14]. However, a new semi-decision procedure for checking the finite variant property has been developed which works well in practice: it has recently [23] been shown that, in order to prove the finite variant property for an equational theory (Σ,E Ax), it is enough to check, for each function symbol f Σ, whether or not each pattern of the form f(X1,,Xn) has a finite number of variants, where the Xi are distinct variables of the appropriate kind and n is the arity of f. This can be done by attempting to generate all the variants of f(X1,,Xn) as described in Section 14.3 below.

Variants are used for variant-based unification in Section 14.7, and such a variant-based unification is later used in Section 15.6 for symbolic reachability analysis. Before defining variant-based unification, in Section 14.2 we introduce the class of equational theories admissible for variant generation, and thus for variant-based unification. We also provide in Section 14.3 a command get variants for user generation of variants.

### 14.2Theories currently supported

The equational theories that are admissible for variant generation are as follows. Let fmod,E Ax) endfm (resp. fth,E Ax,R) endfth) be an order-sorted functional module (resp. functional theory) where E is a set of equations specified with the eq keyword and the attribute variant, and Ax is a set of axioms such that (Σ,Ax) satisfies the restrictions explained in Section 13.3. Furthermore, the equations E must satisfy the following extra conditions:

• The equations E are unconditional, confluent, terminating, sort-decreasing, and coherent modulo Ax (see also Section 21.5 for coherence details).
• An equation’s lefthand side cannot be a variable, and the owise feature is not allowed.

Any system module mod,GE Ax,R) endm (of system theory th,GE Ax,R) endth), where G is an additional set of equations (without the variant attribute!) and R is a set of rules, is also considered admissible for variant generation if the equational part (Σ,E Ax) satisfies the conditions described above. Note that when an equational theory (Σ,G E Ax) is entered into Maude, each equation in E (used for variant computation) must include the variant attribute. Note that equations in G do not have any restriction, i.e., they can be conditional equations, with the owise attribute, etc.

### 14.3The get variants command

Given a module ModId, Maude provides two variant generation commands of the form:

``` get variants [ n ] in ⟨ModId⟩ : ⟨Term⟩ . get irredundant variants [ n ] in ⟨ModId⟩ : ⟨Term⟩ .
```

where n is an optional argument providing a bound on the number of variants requested, so that if the cardinality of the set of variants is greater than the specified bound, the variants beyond that bound are omitted; and, as usual, if no module is mentioned, the current module is used.

Maude allows an incremental generation of variants, as described in Section 14.5 below. When a theory does not have the finite variant property, an incremental generation of the (possibly infinite) set of most general variants would be returned by the first command get variants. However, the second command, get irredundant variants, is useful for theories that do have the finite variant property, since it will provide the set of most general variants of a term, which is the basis for variant-based unification in Section 14.7.

For example, we can check that the EXCLUSIVE-OR module above has the finite variant property by simply generating the variants for the exclusive-or symbol .

``` Maude> get irredundant variants in EXCLUSIVE-OR : X * Y .  Variant #1 [NatSet]: #1:[NatSet] * #2:[NatSet] X --> #1:[NatSet] Y --> #2:[NatSet]  Variant #2 NatSet: mt X --> %1:[NatSet] Y --> %1:[NatSet]  Variant #3 [NatSet]: %1:[NatSet] * %3:[NatSet] X --> %1:[NatSet] * %2:[NatSet] Y --> %2:[NatSet] * %3:[NatSet]  Variant #4 [NatSet]: %1:[NatSet] X --> %1:[NatSet] * %2:[NatSet] Y --> %2:[NatSet]  Variant #5 [NatSet]: %2:[NatSet] X --> %1:[NatSet] Y --> %1:[NatSet] * %2:[NatSet]  Variant #6 [NatSet]: %1:[NatSet] X --> mt Y --> %1:[NatSet]  Variant #7 [NatSet]: %1:[NatSet] X --> %1:[NatSet] Y --> mt  No more variants.
```

The above example illustrates a difference between unifiers returned by the built-in unification modulo axioms and unifiers returned by variant generation or variant-based unification: two forms of fresh variables, the former #n:Sort and the new %n:Sort. The reasons for this distinction are irrelevant and connected to efficiency of algorithms. Both forms represent fresh variables and both share the same counter for new fresh variables. The user is required not to use variables of these two forms in submitted unification problems (either modulo axioms or variant-based). And when used at the metalevel, the counter for new fresh variables must take into account the numbers used for both forms of fresh variables.

Recall that memberships are discarded completely. For instance, we can modify the previous example to include a membership definition for a new sort Empty.

``` fmod EXCLUSIVE-OR-MB is  sorts Nat NatSet .  op 0 : -> Nat [ctor] .  op s : Nat -> Nat [ctor] .   subsort Nat < NatSet .  op mt : -> NatSet [ctor] .  op _*_ : NatSet NatSet -> NatSet [ctor assoc comm] .   sort Empty .  subsort Empty < NatSet .  mb mt : Empty .   vars X Y Z : [NatSet] .  eq [idem] :   X * X = mt  [variant] .  eq [idem-Coh] : X * X * Z = Z [variant] .  eq [id] :    X * mt = X  [variant] . endfm
```

We can ask then for the variants of the exclusive-or symbol when restricted to the sort Empty, and the results use the variant equations but not the membership information.

``` Maude> get irredundant variants in EXCLUSIVE-OR-MB : X:Empty * Y:Empty .  Variant #1 NatSet: #1:Empty * #2:Empty X:Empty --> #1:Empty Y:Empty --> #2:Empty  Variant #2 Empty: mt X:Empty --> %1:Empty Y:Empty --> %1:Empty  No more variants.
```

Note that the membership is used to compute the least sort of terms involved in the results (like the constant mt above), but is not used during variant generation. For example, this process is not able to instantiate any of the two variables to the constant mt.

Consider now the following version of the vending machine to buy apples (a) or cakes (c) with dollars (\$) and/or quarters (q). The reader can check that the only difference with the UNIF-VENDING-MACHINE module in Section 13.4 is the change equation, where we have added the attribute variant and a variable M to make it ACU-coherent (see Section 21.5 for details on ACU-coherence).

``` mod VARIANT-VENDING-MACHINE is  sorts Coin Item Marking Money State .  subsort Coin < Money .  op empty : -> Money .  op __ : Money Money -> Money [assoc comm id: empty] .  subsort Money Item < Marking .  op __ : Marking Marking -> Marking [assoc comm id: empty] .  op <_> : Marking -> State .  ops \$ q : -> Coin .  ops a c : -> Item .  var M : Marking .  rl [buy-c] : < M \$ > => < M c > .  rl [buy-a] : < M \$ > => < M a q > .  eq [change] : q q q q M = \$ M [variant] . endm
```

Note that the change equation satisfies the finite variant property, as proved by generating the variants of symbol __.

``` Maude> get irredundant variants in VARIANT-VENDING-MACHINE : X:Marking Y:Marking .  Variant #1 State: #1:Marking #2:Marking X:Marking --> #1:Marking Y:Marking --> #2:Marking  Variant #2 State: %1:Marking %2:Marking X:Marking --> q q q %1:Marking Y:Marking --> q %2:Marking  Variant #3 State: %1:Marking %2:Marking X:Marking --> q q %1:Marking Y:Marking --> q q %2:Marking  Variant #4 State: %1:Marking %2:Marking X:Marking --> q %1:Marking Y:Marking --> q q q %2:Marking
```

We can also generate the variants of the state < \$ q q X:Marking > containing at least a dollar and two quarters.

``` Maude> get irredundant variants in VARIANT-VENDING-MACHINE : < \$ q q X:Marking > .  Variant #1 State: < \$ q q #1:Marking > X:Marking --> #1:Marking  Variant #2 State: < \$ \$ %1:Marking > X:Marking --> q q %1:Marking
```

These two variants form a finite, complete, and most general set of variants for the given term; for example, the variant

``` {< \$ \$ q q Y:Marking >, X:Marking --> q q q q Y:Marking}
```

is an instance of the first variant above, i.e., the canonical form < \$ \$ q q Y:Marking > is an instance of the normal form < \$ q q #1:Marking > of the first variant, and the (normalized version) of the instantiating substitution, i.e., #1:Marking --> \$ Y:Marking, is an instance of the empty substitution of the first variant.

We can consider a more complex equational theory such as the one of Abelian groups specified in the following module.

``` fmod ABELIAN-GROUP is  sorts Element .  op _+_ : Element Element -> Element [comm assoc prec 30] .  op -_ : Element -> Element [prec 20] .  op 0 : -> Element .  vars X Y Z : Element .  eq X + 0 = X [variant] .  eq X + - X = 0 [variant] .  eq X + - X + Y = Y [variant] .  eq - - X = X [variant] .  eq - 0 = 0 [variant] .  eq - X + - Y = -(X + Y) [variant] .  eq -(X + Y) + Y = - X [variant] .  eq -(- X + Y) = X + - Y [variant] .  eq - X + - Y + Z = -(X + Y) + Z [variant] .  eq -(X + Y) + Y + Z = - X + Z [variant] . endfm
```

The generation of the variants for the addition symbol takes more time and provides 47 variants:

``` Maude> get irredundant variants in ABELIAN-GROUP : X + Y .  Variant #1 Element: #1:Element + #2:Element X --> #1:Element Y --> #2:Element  Variant #2 Element: %1:Element X --> 0 Y --> %1:Element ...  Variant #46 Element: %2:Element + - (%3:Element + %4:Element) X --> %5:Element + - (%1:Element + %3:Element) Y --> %1:Element + %2:Element + - (%4:Element + %5:Element)  Variant #47 Element: - (%2:Element + %3:Element) X --> %4:Element + - (%1:Element + %2:Element) Y --> %1:Element + - (%3:Element + %4:Element)
```

And the minus sign symbol has four variants:

``` Maude> get irredundant variants in ABELIAN-GROUP : - X .  Variant #1 Element: - #1:Element X --> #1:Element  Variant #2 Element: %1:Element X --> - %1:Element  Variant #3 Element: 0 X --> 0  Variant #4 Element: %1:Element + - %2:Element X --> %2:Element + - %1:Element
```

### 14.4Variant generation with irreducibility constraints

Variant generation is useful to many applications (see Sections 13.5 and 15.2) but especially for variant-based unification, as explained in Section 14.7 below. One special version of the variant generation algorithm implemented in Maude 3.0 includes irreducibility conditions, i.e., a term is not allowed to be reducible after applying a substitution. This is useful when, for example, the variants of a term may have been generated before and one is not interested in generating the variants of a variant of a term, since the variant t3 of a variant t2 of a term t1 must be already covered by a variant of t1 (maybe t2 itself). The irreducibility condition is appended by using the keywords such that T1, T2, T3, ... irreducible.

For example, we may reconsider the generation of the set of irredundant variants of the expression X * Y in page 382 but now assuming that the term itself is irreducible, that is, no further variant must be computed.

``` get irredundant variants in EXCLUSIVE-OR : X * Y such that X * Y irreducible .  Variant #1 [NatSet]: #1:[NatSet] * #2:[NatSet] X --> #1:[NatSet] Y --> #2:[NatSet]
```

Similarly, we may reconsider the generation of the set of irredundant variants of the state < \$ q q X:Marking > in page 383 but assuming that different subterms separated by commas are irreducible.

``` get irredundant variants in VARIANT-VENDING-MACHINE : < \$ q q X:Marking > such that q q X:Marking, q X:Marking, X:Marking irreducible .  Variant #1 State: < \$ q q #1:Marking > X:Marking --> #1:Marking
```

This command clearly discards the variant where X:Marking is mapped to q q %1:Marking, since it violates the condition that q q X:Marking must be irreducible under substitution.

### 14.5Incremental variant generation

Another interesting feature is that variant generation is incremental and in this way we are able to give partial support to theories that do not have the finite variant property. Let us consider the functional module for addition NAT-VARIANT in Section 14.1 that does not have the finite variant property. On the one hand, it is possible to have a term with a finite number of most general variants although the theory does not have the finite variant property. For instance, the term s(0) + X is simplified into s(X).

``` Maude> get variants in NAT-VARIANT : s(0) + X:Nat .  Variant #1 Nat: s(#1:Nat) X:Nat --> #1:Nat
```

On the other hand, we can approximate the number of variants of a term that we suspect does not have a finite number of most general variants. For instance, the term X + s(0) has an infinite number of most general variants and we can approximate that infinite set of variants by including a bound in the command, as it is also done for unification modulo axioms.

``` Maude> get variants [10] in NAT-VARIANT : X:Nat + s(0) .  Variant #1 Nat: #1:Nat + s(0) X:Nat --> #1:Nat  Variant #2 Nat: s(0) X:Nat --> 0  ...  Variant #10 Nat: s(s(s(s(s(0))))) X:Nat --> s(s(s(s(0))))
```

Note that typing get irredundant variants in the previous command would force Maude to generate the infinite set of variants before collecting the ten most general ones.

This incremental variant generation may be useful in applications where obtaining a complete set of variants when possible is important. If we do not know a priori whether a term has a finite number of most general variants, we can incrementally increase the bound and if we obtain a number of variants smaller than the bound, we know for sure that it had a finite number of most general variants.

When an equational theory satisfies the requirements in Section 14.2 and does not have the finite variant property, it is because there are terms with an infinite set of most general variants. Of course, if the user does not provide a bound, Maude does not stop because it always returns a complete set of variants. However, when the user provides such a bound, the process will always terminate with Maude returning a finite set of variants. As said above, the number of returned variants can be smaller than the given bound when the term has indeed a finite set of variants, but it will coincide with the bound otherwise.

### 14.6Variant generation in incomplete unification examples

The unification infrastructure now supports the notion of incomplete unification algorithms (see Section 13.4.6) and variant generation and variant unification have been updated.

Let us consider an equational theory combining variant equations and associativity.

``` fmod VARIANT-UNIFICATION-ASSOC is  protecting NAT .  sort NList .  subsort Nat < NList .   op _:_ : NList NList -> NList [assoc ctor] .   var E : Nat .  var L : NList .   ops tail prefix : NList ~> NList .  ops head last : NList ~> Nat .  eq head(E : L) = E [variant] .  eq tail(E : L) = L [variant] .  eq prefix(L : E) = L [variant] .  eq last(L : E) = E [variant] .   op duplicate : NList ~> Bool .  eq duplicate(L : L) = true [variant] . endfm
```

Some terms have a finite set of most general variants modulo associativity.

``` Maude> get variants in VARIANT-UNIFICATION-ASSOC : head(prefix(tail(L))) .  Variant #1 Nat: head(prefix(tail(#1:NList))) L --> #1:NList  Variant #2 Nat: head(prefix(%2:NList)) L --> %1:Nat : %2:NList  Variant #3 Nat: head(#2:NList) L --> #1:Nat : #2:NList : #3:Nat  Variant #4 Nat: %3:Nat L --> %1:Nat : %3:Nat : %4:NList : %2:Nat  No more variants.
```

However, some terms may hit incomplete associative unification calls (see Section 13.4.6), and an incompleteness warning for associative unification will be printed.

``` Maude> get variants in VARIANT-UNIFICATION-ASSOC :        duplicate(prefix(L) : tail(L)) .  Variant #1 [Bool]: duplicate(prefix(#1:NList) : tail(#1:NList)) L --> #1:NList  Variant #2 [Bool]: duplicate(%1:NList : tail(%1:NList : %2:Nat)) L --> %1:NList : %2:Nat  Variant #3 [Bool]: duplicate(prefix(%1:Nat : %2:NList) : %2:NList) L --> %1:Nat : %2:NList  Variant #4 [Bool]: duplicate(#1:Nat : #2:NList : #2:NList : #3:Nat) L --> #1:Nat : #2:NList : #3:Nat  Variant #5 [Bool]: duplicate(#1:Nat : #2:Nat) L --> #1:Nat : #2:Nat  Warning: Unification modulo the theory of operator _:_ has encountered an instance for which it may not be complete. Variant #6 Bool: true L --> %1:Nat : %1:Nat : %1:Nat  Variant #7 Bool: true L --> %1:Nat : %1:Nat  No more variants. Warning: Some variants may have been missed due to incomplete unification algorithm(s).
```

Note that the term duplicate(prefix(L) : tail(L)) has an infinite set of most general variants for the case of returning the variant term true, i.e., the family of substitutions {L:NListN:Nat  :   :  N:Nat}. This is due to the associative unification call (N:Nat:L:NList) = ?(L:NList:N:Nat) invoked internally by the variant generation process (see Section 13.4.6 for a similar associative unification problem with an infinite set of most general unifiers).

### 14.7Variant-based equational order-sorted unification

The intimate connection between E,Ax-variants and E Ax-unification is as follows. Suppose that we extend the equational theory (Σ,E Ax) to (Σ,E Ax) by adding to Σ a new sort Truth, not related to any sort in Σ, with a constant tt, and, for each top sort of a connected component [s], an operator eq : [s] [s] -> Truth; and where E is the result of adding for each top sort [s] an extra (oriented) equation eq(x,x) = tt (where x is a variable of sort [s]) to E. Then, given any two terms t,t, if 𝜃 is an E Ax-unifier of t and t, then the E,Ax-canonical forms of 𝜃(t) and 𝜃(t) must be Ax-equal and therefore the pair (tt,𝜃) must be a variant of the term eq(t,t). Furthermore, if the term eq(t,t) has a finite set of most general variants, then we are guaranteed that the set of most general E Ax-unifiers of t and t is finite.

At a practical level, variants are generated using narrowing (see Chapter 15 for narrowing capabilities in Maude). Narrowing with oriented equations E (with or without modulo Ax) enjoys well-known completeness results, including the generation of complete sets of unifiers and covering all rewriting sequences from instances of a term using normalized substitutions (i.e., variants). For instance, [84] showed that narrowing with E without axioms enjoyed good completeness results, and [85] showed that narrowing with E modulo axioms Ax enjoyed also good completeness results. But narrowing can be quite inefficient, generating a huge search space, and different narrowing strategies have been devised to reduce the search space while remaining complete, specially for unification purposes (see [5] for a survey on narrowing termination). The basic narrowing strategy of [84] provided a restriction of narrowing that, while being complete, it was terminating for specific classes of theories. However, very little was known about effective narrowing strategies in the modulo case, and some of the known anomalies ring a cautionary note, to the effect that the naive extensions of standard narrowing strategies, for example basic narrowing modulo AC, were incomplete [13536]. In [71], the folding variant narrowing strategy is defined for the modulo case and it is proved to be complete for variants and with good termination properties, providing a finitary and complete unification algorithm for equational unification for the theories described in Section 14.2 that also satisfy the finite variant property. Moreover, it is even better than the basic narrowing strategy in the case without axioms, since it can terminate for equational theories where basic narrowing cannot (see [71]).

In Maude 2.6, variant generation and variant-based equational unification were implemented in Maude and made available in Full Maude. Instead, since Maude 2.7 variant generation and variant-based equational unification are implemented in Core Maude’s C++ level for efficiency purposes and using the Ax-unification algorithm described in Section 13.4. Furthermore, the variant generation and variant-based equational unification available in Maude 2.6 were accepting only equational theories where the righthand side of the equations was a strongly irreducible term (e.g., a variable or a constant), while the current version implements the folding variant narrowing strategy in full generality. By “full generality” we mean not just any equational theory (Σ,E Ax) having the finite variant property with Ax satisfying the requirements in Section 13.3 (so that unification is finitary), but any confluent, coherent, and terminating modulo Ax decomposition (Σ,Ax,E), thus obtaining an incremental generation for the (in general infinite) set of E Ax-unifiers in that case.

The key distinction, now supported for the first time in Maude in full generality, is one between dedicated unification algorithms for a limited set of axioms Ax and generic unification algorithms which can be applied to a much wider range of user-definable theories and can even deal with incremental generation of infinite sets of unifiers.

### 14.8The variant unify command

Given a module ModId, of the general form mod,G E Ax,R) endm where (Σ,E Ax) satisfies the requirements of Section 14.2 and satisfies also the finite variant property, Maude provides a command for E Ax-equational unification based on variant generation of the form:

``` variant unify [ n ] in ⟨ModId⟩ :    ⟨Term-1⟩ =? ⟨Term’-1⟩ /\ ... /\ ⟨Term-k⟩ =? ⟨Term’-k⟩ .
```

where k 1; n is an optional argument providing a bound on the number of unifiers requested, so that if the cardinality of the set of unifiers is greater than the specified bound, the unifiers beyond that bound are omitted; and, as usual, if no module is mentioned, the current module is used.

Consider again the module VARIANT-VENDING-MACHINE introduced in Section 14.3. We can ask whether there is an E Ax-equational unifier of two configurations, one containing at least two quarters, and another containing at least one dollar, by invoking the following command:

``` Maude> variant unify in VARIANT-VENDING-MACHINE :       < q q X:Marking > =? < \$ Y:Marking > .  Unifier #1 X:Marking --> \$ %1:Marking Y:Marking --> q q %1:Marking  Unifier #2 X:Marking --> q q #1:Marking Y:Marking --> #1:Marking
```

There are no most general unifiers; for instance, the unifier X:Marking --> q q, Y:Marking --> empty is an instance of the second solution by using the identity property of the operator for markings.

And we can ask again whether there is an E Ax-equational unifier of the two previous configurations but variable Y:Marking also appears in a second unification problem with two new configurations, one containing again at least two quarters, and another with just variable Y:Marking.

``` Maude> variant unify in VARIANT-VENDING-MACHINE :       < q q X:Marking > =? < \$ Y:Marking > /\       < q q Z:Marking > =? < Y:Marking > .  Unifier #1 X:Marking --> \$ %1:Marking Z:Marking --> %1:Marking Y:Marking --> q q %1:Marking  Unifier #2 X:Marking --> \$ q q %1:Marking Z:Marking --> q q %1:Marking Y:Marking --> \$ %1:Marking
```

### 14.9Variant-based unification with irreducibility constraints

Similarly to Section 14.4, we may need to perform variant-based unification but with some irreducibility conditions. The irreducibility condition is appended by using the keywords such that T1, T2, T3, ... irreducible.

For example, we may reconsider the unification problem of terms < q q X:Marking > and < \$ Y:Marking >  above but assuming that different subterms separated by commas are irreducible.

``` variant unify in VARIANT-VENDING-MACHINE : < q q X:Marking > =? < \$ Y:Marking > such that q q X:Marking, q X:Marking, X:Marking irreducible .  Unifier #1 rewrites: 0 in 0ms cpu (0ms real) (0 rewrites/second) X:Marking --> \$ %1:Marking Y:Marking --> q q %1:Marking
```

This command clearly discards the second unifier where X:Marking is mapped to q q %1:Marking, since violates the condition that q q X:Marking must be irreducible under substitution.

### 14.10Incremental variant unification

Similarly to the incremental generation of variants in Section 14.5, one can obtain an incremental number of unifiers for a given unification problem. Let us consider again the NAT-VARIANT module in Section 14.1 that does not have the finite variant property. On the one hand, it is possible to have a finite number of most general unifiers for a unification problem although the theory does not have the finite variant property. For instance, the unification problem between s(0) + X and s(s(s(0))) returns just one unifier.

``` Maude> variant unify in NAT-VARIANT : s(0) + X:Nat =? s(s(s(0))) .  Unifier #1 X:Nat --> s(s(0))  No more unifiers.
```

On the other hand, we can approximate the number of unifiers of a unification problem that we suspect does not have a finite number of most general unifiers. For instance, the unification problem between terms X + s(0) and s(s(s(0))) has only one solution Xs(s(0)) and we can obtain that solution by including a bound in the command, as it is also done for variant generation.

``` Maude> variant unify [1] in NAT-VARIANT : X:Nat + s(0) =? s(s(s(0))) .  Unifier #1 X:Nat --> s(s(0))
```

However, if we tried to obtain two unifiers, Maude would not stop because it would keep trying to generate a second unifier for a unification problem that has only one unifier, without knowing that it could stop. This differs from the incremental generation of variants (Section 14.5), where we can incrementally increase the bound even if the theory does not have the finite variant property and Maude will always stop with a new variant. The problem here is due to the fact that Maude needs to compute the set of variants before computing the set of unifiers; when the equational theory does not have the finite variant property, such a set of variants can be infinite and Maude is not able to complete this computation, even when the user provides a bound, because such a bound refers to the number of requested unifiers, but not to the number of variants, which in this process is just part of the internal process for computing unifiers. As in the example above, this can happen even when there are no further unifiers.

### 14.11Variant unification in incomplete unification examples

Similarly to the incomplete variant generation in Section 14.6, we can have variant unification calls that cannot provide a finitary set of most general unifiers. Let us consider again the VARIANT-UNIFICATION-ASSOC theory of Section 14.6.

We can force unification calls, within variant unification, to an associative unification problem with an infinite set of most general unifiers, e.g., the previously described associative unification problem N:Nat:L:NList = ?L:NList:N;Nat with the family of substitutions {L:NListN:Nat  :   :  N:Nat}:

``` Maude> variant unify in VARIANT-UNIFICATION-ASSOC :    head(L) =? last(L) /\ prefix(L) =? tail(L) .  Warning: Unification modulo the theory of operator _:_ has encountered an instance for which it may not be complete.  Unifier #1 L --> %1:Nat : %1:Nat : %1:Nat  Unifier #2 L --> %1:Nat : %1:Nat  No more unifiers. Warning: Some unifiers may have been missed due to incomplete unification algorithm(s).
```

Notice that the unification problem head(L) =? last(L) /\ prefix(L) =? tail(L) has the same solutions as the unification problem N:Nat : L:NList =? L:NList : N:Nat.