Chapter 13
Unification

13.1 Introduction

Unification is the solving of equations, either in free algebras of the form $T_{\mathrm{\Sigma }}(X)$, or in relatively free algebras modulo a set $E$ of equations, that is, in algebras of the form $T_{\mathrm{\Sigma }∕E}(X)$. The first case is sometimes called syntactic unification. The second case is sometimes called $E$-unification or unification modulo $E$; if $E$ is not explicitly mentioned, then it is called equational unification or semantic unification.

In solving any equation, such as, for example,

we look for instances of the variables appearing in the equation that make both sides equal. Variables can of course be instantiated by substitutions. A substitution that makes both sides of the equation equal, that is, a solution of the equation, is called a unifier. For example, if we are solving the above equation in the free algebra $T_{\mathrm{\Sigma }}(X)$ with $X$ a countable set of variables and with $\mathrm{\Sigma }$ having a single sort (unsorted unification), the substitution $\sigma =\{x\mapsto g(y),z\mapsto h(y)\}$ is a unifier, and indeed the so-called most general unifier, so that for any other unifier $\rho$ there exists a substitution $\mu$ such that $\rho =\sigma ;\mu$, where $\sigma ;\mu$ denotes composition of substitutions in diagrammatic order. That is, any other solution of the equation is an instance of the most general solution provided by $\sigma$.

Of course, some equations may not have syntactic unifiers, but may have semantic unifiers modulo some equations $E$. Consider, for example, the equation

which obviously does not have any solution in $T_{\mathrm{\Sigma }}(X)$. It does, however, have a solution in $T_{\mathrm{\Sigma }∕C}(X)$, where $C$ is the commutativity axiom $f(x,y)=f(y,x)$. Indeed, the exact same substitution $\sigma$ solving the first equation $f(x,h(y))=f(g(y),z)$ in a syntactic way, is now a unifier solving the second equation $f(h(y),x)=f(g(y),z)$ modulo $C$, because we have $f(h(y),g(y)){=}_{C}f(g(y),h(y))$.

Unification is a fundamental deductive mechanism used in many automated deduction tasks. It is also very important in combining the paradigms of functional programming and logic programming (in the Prolog sense of “logic programming”). Furthermore, in the context of Maude, unification can be very useful to reason not only about equational theories (functional modules or theories), but also about rewrite theories (system modules or theories) [100].

Therefore, it is very useful to have an efficient implementation of unification available in Maude, which is what this chapter describes. Specifically, we explain how order-sorted unification modulo frequently occurring equational axioms is supported in Maude. In Chapter 14, we explain order-sorted unification modulo convergent equational theories, also available in Maude.

13.2 Order-sorted unification

Although the most general equational theories supported by Maude are membership equational theories, to obtain practical unification algorithms, allowing us to effectively compute the solutions of an equational unification problem, it is important to restrict ourselves to order-sorted equational theories. We can define the basic concepts of order-sorted $E$-unification in full generality.

Given an order-sorted equational theory $(\mathrm{\Sigma },E)$, an $E$-unification problem consists of a nonempty set of unification equations of the form $t{=}^{?}{t}^{\prime }$, written in the notation

where $n\ge 1$ and the “conjunction” operator $\wedge$ is assumed to be associative and commutative.

Given such an $E$-unification problem, an $E$-unifier for it is an order-sorted substitution¹ $\sigma :Vars(t_1,t_1^{\prime },\dots ,t_n,t_n^{\prime })\to T_{\mathrm{\Sigma }}(X)$ (where we assume that the set $X$ of variables contains a countable number of variables for each sort) such that, for all $i=1,\dots ,n$,

where $Y_i=Vars(\sigma (t_i),\sigma (t_i^{\prime }))$, that is, all the equations $(\forall <!--FUNCTION\; APPLICATION-->Y_i)\sigma (t_i)=\sigma (t_i^{\prime })$ can be deduced in (membership) equational logic from the set of equations $E$.

A set $U$ of unifiers is called a complete set of $E$-unifiers for a given $E$-unification problem $t_1{=}^{?}{t}_1^{\prime }\wedge \dots \wedge t_n{=}^{?}{t}_n^{\prime }$ iff for any other $E$-unifier $\rho$ of the same $E$-unification problem there exists a substitution $\mu$ and a unifier $\sigma \in U$ such that $\rho {=}_E\sigma ;\mu$, that is, for each variable $x$ in the domain of $\rho$ we have $E⊢\rho (x)=\mu (\sigma (x))$. A complete set $U$ of $E$-unifiers is called minimal if any proper subset of $U$ fails to be complete.

For an order-sorted equational theory $(\mathrm{\Sigma },E)$, unification is said to be finitary if for any $E$-unification problem there is always a finite complete set $U$ of unifiers. Similarly, unification for $(\mathrm{\Sigma },E)$ is called unitary if it is finitary and for any $E$-unification problem a minimal complete set of unifiers is always either empty or a singleton set. We say that $(\mathrm{\Sigma },E)$ has a unification algorithm if there is an algorithm generating a complete set of $E$-unifiers for any $E$-unification problem in $(\mathrm{\Sigma },E)$.

Unlike unsorted syntactic unification, which always either fails or has a single most general unifier, order-sorted syntactic unification is not necessarily unitary, that is, there is in general no single most general unifier. What exists (if $\mathrm{\Sigma }$ is finite) is a finite minimal complete set of syntactic unifiers. For some commonly occurring theories having a unification algorithm, such as the theory $A$ of associativity of a binary function symbol, it is well-known that unification is not finitary: in general an infinite number of solutions may exist (see Section 13.4.6). However, for other theories, such as commutativity $C$ or associativity-commutativity $AC$, unification is finitary, both when $\mathrm{\Sigma }$ is unsorted and when $\mathrm{\Sigma }$ is order-sorted (and finite).

13.2.1 A hybrid approach to equational order-sorted unification

We define a hybrid approach, in which we take advantage of Maude’s structuring of a module’s equations into equational axioms $Ax$, such as associativity, and/or commutativity, and/or identity, and equations $E$, which are assumed to be coherent,² confluent, and terminating modulo $Ax$. We can then consider order-sorted equational theories of the form $(\mathrm{\Sigma },E\cup Ax)$ and decompose the $E\cup Ax$-unification problem into two problems: one of $Ax$-unification, and another of $E\cup Ax$-unification that uses an $Ax$-unification algorithm as a subroutine. The point of this decomposition is that $Ax$-unification needs to be very efficient in order to have $E\cup Ax$-unification be built on top of $Ax$-unification. Since the axioms $Ax$ are well-known and unification algorithms exist for them, the task of building in efficient $Ax$-unification algorithms, although highly nontrivial, becomes manageable; which is what this chapter describes. Chapter 14 describes such $E\cup Ax$-unification relying on this $Ax$-unification.

13.3 Theories currently supported

As mentioned above, a practical way of dealing with order-sorted equational unification is to consider order-sorted theories of the form $(\mathrm{\Sigma },E\cup Ax)$, with $Ax$ a set of commonly occurring axioms, declared in Maude as equational attributes (see Section 4.4.1), and $E$ the remaining equations specified with the eq or ceq keywords. We can then decompose the $E\cup Ax$-unification problem into an $Ax$-unification problem and an $E\cup Ax$-unification problem that uses an $Ax$-unification algorithm as a subroutine. In such a decomposition, the efficiency of the $Ax$-unification algorithm becomes crucial.

Maude currently provides an order-sorted $Ax$-unification algorithm for all order-sorted theories $(\mathrm{\Sigma },E\cup Ax)$ such that the order-sorted signature $\mathrm{\Sigma }$ is preregular modulo $Ax$ (see Sections 3.8 and 21.3.5) and the axioms $Ax$ associated to function symbols are as follows:

• there can be arbitrary function symbols and constants with no equational attributes;

• the iter equational attribute can be declared for some unary symbols;

• different equational attributes can be declared for some binary function symbols:

  • the assoc attribute³ ; usually referred to as A (for associative),

  • the comm attribute; usually referred to as C (for commutative),

  • the assoc comm attributes; usually referred to as AC (for associative and commutative),

  • the assoc comm id: attributes; usually referred to as ACU (for associative and commutative with identity, or unit),

  • the assoc id: attributes³; usually referred to as AU (for associative and identity, or unit),

  • the comm id: attributes; usually referred to as CU (for commutative and identity, or unit),

  • the id: attribute; usually referred to as U (for identity, or unit),

  • the left id: attribute; usually referred to as Ul (for left identity, or unit), and

  • the right id: attribute; usually referred to as Ur (for right identity, or unit),

  but no other equational attributes must be given for such symbols.

Explicitly excluded are theories with a binary symbol declared with the idem attribute and associativity with only left or right identity. However, these cases have the finite variant property, so that, used as variant equations, they can be combined with all the other just-mentioned attributes by means of variant unification algorithms (see Section 14.8).

If we give to Maude a unification problem in a functional module of the form fmod $(\mathrm{\Sigma },Ax)$ endfm where $\mathrm{\Sigma }$ and $Ax$ satisfy the above requirements, we get a complete⁴ set of order-sorted unifiers modulo the theory $(\mathrm{\Sigma },Ax)$. If, instead, we give the same problem to Maude in the functional module fmod $(\mathrm{\Sigma },E\cup Ax)$ endfm, then the equations $E$ are ignored, and we get the same unifiers as for the module or theory obtained by omitting the equations $E$. Similarly, if we provide the same unification problem in a functional theory fth $(\mathrm{\Sigma },E\cup Ax)$ endfth, a system module mod $(\mathrm{\Sigma },E\cup Ax,R)$ endm or a system theory th $(\mathrm{\Sigma },E\cup Ax,R)$ endth, we again get the same set of unifiers as for the theory $(\mathrm{\Sigma },Ax)$. All this is consistent with the decomposition idea mentioned above: to deal with order-sorted $E\cup Ax$-unification, other methods, that use the $Ax$-unification algorithm as a component, can later be defined.

Maude is even more tolerant than this. The user can give to Maude a unification problem in a functional module (or functional theory, or system module, or system theory) of the form fmod $(\mathrm{\Sigma },E\cup M\cup Ax\cup A{x}^{\prime })$ endfm (or the analogous specification in the other cases), where $(\mathrm{\Sigma },Ax)$ satisfies the conditions mentioned above, but $M$ is an optional set of membership axioms (that is, $(\mathrm{\Sigma },E\cup M\cup Ax\cup A{x}^{\prime })$ can be a membership equational theory and not just an order-sorted theory), and the axioms $A{x}^{\prime }$ violate those conditions mentioned above. Then what will happen is:

1.

As before, the additional equations $E$ (or the rules $R$ of a system module or theory) are completely ignored, and the membership axioms $M$ are likewise ignored.

2.

If a unification problem involves the occurrence of a symbol satisfying axioms $A{x}^{\prime }$ at the root position of a non-ground subterm, the unification process will fail and a warning will be printed (see Section 13.4.1).

3.

If a unification problem involves the occurrence of symbols satisfying axioms $A{x}^{\prime }$, but all such occurrences are always in ground subterms of the problem, then this special case of $Ax\cup A{x}^{\prime }$-unification is handled by Maude and the corresponding $Ax\cup A{x}^{\prime }$-unifiers are returned (see Section 13.4.1).

Furthermore, the functional module fmod$(\mathrm{\Sigma },E\cup M\cup Ax\cup A{x}^{\prime })$ endfm (or the analogous functional theory or system module or theory) may import predefined modules such as BOOL or NAT, so that function symbols in such predefined modules can also be used in unification problems.

13.4 The unify command

Given a functional module or theory, or a system module or theory, $⟨$ModId$⟩$, the user can give to Maude a unification command of the following two forms:

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

For a simple example of syntactic order-sorted unification problem illustrating:

• the use of the unify command;

• sort downgrading of a variable;

• the use of the predefined operator _^_ in the NAT module (see Section 8.3), representing exponentiation on natural numbers; and

• the, in general, non-unitary nature of order-sorted unification,

we can define the module

fmod UNIFICATION-EX1 is 
 extending NAT . 
 op f : Nat Nat -> Nat . 
 op f : NzNat Nat -> NzNat . 
 op f : Nat NzNat -> NzNat . 
endfm
     

Maude> unify f(X:Nat, Y:Nat) ^ B:NzNat =? A:NzNat ^ f(Y:Nat, Z:Nat) . 
 
Unifier 1 
X:Nat --> #1:Nat 
Y:Nat --> #2:NzNat 
B:NzNat --> f(#2:NzNat, #3:Nat) 
A:NzNat --> f(#1:Nat, #2:NzNat) 
Z:Nat --> #3:Nat 
 
Unifier 2 
X:Nat --> #1:NzNat 
Y:Nat --> #2:Nat 
B:NzNat --> f(#2:Nat, #3:NzNat) 
A:NzNat --> f(#1:NzNat, #2:Nat) 
Z:Nat --> #3:NzNat
     

The next example in the same module illustrates the use of the unify command with a unification problem consisting of two equations:

Maude> unify f(X:Nat, Y:NzNat) =? f(Z:NzNat, U:Nat) 
       /\ V:NzNat =? f(X:Nat, U:Nat) . 
 
Unifier 1 
X:Nat --> #1:NzNat 
Y:NzNat --> #2:NzNat 
Z:NzNat --> #1:NzNat 
U:Nat --> #2:NzNat 
V:NzNat --> f(#1:NzNat, #2:NzNat)
     

Note that, as already mentioned, we could instead invoke the unify command in a functional or system module or theory having additional equations, memberships, or rules, which are always ignored. For example, we could have instead declared the system theory

th UNIFICATION-EX2 is 
 including NAT . 
 op f : Nat Nat -> Nat . 
 op f : NzNat Nat -> NzNat . 
 op f : Nat NzNat -> NzNat . 
 eq f(f(N:Nat, M:Nat), K:Nat) = f(N:Nat, M:Nat) . 
 rl f(N:Nat, M:Nat) => 0 . 
endth
     

The following unification command in the predefined CONVERSION module (see Section 8.10) illustrates a further point on the handling of built-in constants and functions. Built-in constants, even though infinite in number (all strings, all quoted identifiers, all natural numbers, and so on), are handled and can be used in unification problems. But built-in functions are not considered built-in for unification purposes; therefore, built-in evaluation of such functions is not performed during the unification.

Maude> unify in CONVERSION : 
       X:String < "foo" + Y:Char =? 
         Z:String + string(pi) < "foo" + Z:String . 
 
Unifier 1 
X:String --> #1:Char + string(pi) 
Y:Char --> #1:Char 
Z:String --> #1:Char
     

The above examples illustrate a further point about the form of the returned unifiers, namely, that in each assignment $X$ –> $t$ in a unifier, the variables appearing in the term $t$ are always fresh variables of the form #n:Sort . The user is required⁵ not to use variables of this form in the submitted unification problem. A warning is printed if this requirement is violated:

Maude> unify in NAT : X:Nat ^ #1:Nat =? #2:Nat . 
Warning: unsafe variable name #1:Nat in unification problem.
     

13.4.1 Non-supported unification examples

The handling of unification problems in modules with operators whose equational axioms are excluded from the current unification algorithm can be illustrated by means of the following module:

fmod UNIFICATION-EX3 is 
 extending NAT . 
 op f : Nat Nat -> Nat [idem] . 
endfm
     

Maude> unify f(f(X:Nat, Y:Nat), Z:Nat) =? f(A:Nat, B:Nat) . 
Warning: Term f(X:Nat, Y:Nat, Z:Nat) is non-ground and unification 
 for its top symbol is not currently supported.
     

Maude> unify X:Nat + f(f(41, 42),43) =? Y:Nat + f(41,f(42,43)) . 
 
Unifier 1 
X:Nat --> #1:Nat + f(41, f(42, 43)) 
Y:Nat --> #1:Nat + f(f(41, 42), 43) 
 
Unifier 2 
X:Nat --> f(41, f(42, 43)) 
Y:Nat --> f(f(41, 42), 43)
     

Note, however, that, as already mentioned, unification modulo the idem attribute can be achieved by variant-based unification using the explicit equation f(N:Nat,N:Nat) = N:Nat (see Section 14.8).

13.4.2 Associative-commutative ($AC$) unification examples

The use of a bound on the number of unifiers, as well as the use of the associative-commutative (AC) operator + in the predefined NAT module (see Section 8.3), plus the fact that even small AC-unification problems can generate a large number of unifiers are all illustrated by the following command:

Maude> unify [100] in NAT : 
       X:Nat + X:Nat + Y:Nat =? A:Nat + B:Nat + C:Nat . 
Unifier 1 
X:Nat --> #1:Nat + #2:Nat + #3:Nat + #5:Nat + #6:Nat + #8:Nat 
Y:Nat --> #4:Nat + #7:Nat + #9:Nat 
A:Nat --> #1:Nat + #1:Nat + #2:Nat + #3:Nat + #4:Nat 
B:Nat --> #2:Nat + #5:Nat + #5:Nat + #6:Nat + #7:Nat 
C:Nat --> #3:Nat + #6:Nat + #8:Nat + #8:Nat + #9:Nat 
... 
 
Unifier 100 
X:Nat --> #1:Nat + #2:Nat + #3:Nat + #4:Nat 
Y:Nat --> #5:Nat 
A:Nat --> #1:Nat + #1:Nat + #2:Nat 
B:Nat --> #2:Nat + #3:Nat 
C:Nat --> #3:Nat + #4:Nat + #4:Nat + #5:Nat
     

The unification problem above has $381$ unifiers, though only $100$ were asked for. Indeed, it is the minimal set of most general unifiers and the irredundant unify command returns the same set with $381$ unifiers.

13.4.3 Unification examples with the iter attribute

The following example illustrates the efficiency of order-sorted unification modulo the iter theory (in this example in combination with the comm theory). Consider the following module:

fmod ITER-EXAMPLE is 
 sorts NzEvenNat EvenNat OddNat NzNat Nat EvenInt OddInt NzInt Int . 
 subsorts OddNat < OddInt NzNat < NzInt < Int . 
 subsorts EvenNat < EvenInt Nat < Int . 
 subsorts NzEvenNat < NzNat EvenNat < Nat . 
 
 op 0 : -> EvenNat . 
 
 op s : EvenNat -> OddNat [iter] . 
 op s : OddNat -> NzEvenNat [iter] . 
 op s : Nat -> NzNat [iter] . 
 op s : EvenInt -> OddInt [iter] . 
 op s : OddInt -> EvenInt [iter] . 
 op s : Int -> Int [iter] . 
 
 op _+_ : Int Int -> Int [comm gather (E e)] . 
 op _+_ : OddInt OddInt -> EvenInt [ditto] . 
 op _+_ : EvenInt EvenInt -> EvenInt [ditto] . 
 op _+_ : OddInt EvenInt -> OddInt [ditto] . 
 op _+_ : Nat Nat -> Nat [ditto] . 
 op _+_ : Nat NzNat -> NzNat [ditto] . 
 op _+_ : OddNat OddNat -> NzEvenNat [ditto] . 
 op _+_ : NzEvenNat EvenNat -> NzEvenNat [ditto] . 
 op _+_ : EvenNat EvenNat -> EvenNat [ditto] . 
 op _+_ : OddNat EvenNat -> OddNat [ditto] . 
endfm
   

We can then give the unification commands:

Maude> unify in ITER-EXAMPLE : 
       s^1000000(X:OddNat) =? s^100000000001(Y:Int) . 
 
Unifier 1 
X:OddNat --> s^99999000001(#1:EvenNat) 
Y:Int --> #1:EvenNat
     

Maude> unify in ITER-EXAMPLE : 
       s^1000000(X:OddNat) =? s^100000000001(Y:Int + Z:Int + W:Int) . 
 
Unifier 1 
X:OddNat --> s^99999000001(#1:OddNat + (#2:OddNat + #3:EvenNat)) 
W:Int --> #1:OddNat 
Z:Int --> #2:OddNat 
Y:Int --> #3:EvenNat 
 
Unifier 2 
X:OddNat --> s^99999000001(#1:OddNat + (#2:EvenNat + #3:OddNat)) 
W:Int --> #1:OddNat 
Z:Int --> #2:EvenNat 
Y:Int --> #3:OddNat 
 
Unifier 3 
X:OddNat --> s^99999000001(#1:EvenNat + (#2:OddNat + #3:OddNat)) 
W:Int --> #1:EvenNat 
Z:Int --> #2:OddNat 
Y:Int --> #3:OddNat 
 
Unifier 4 
X:OddNat --> s^99999000001(#1:EvenNat + (#2:EvenNat + #3:EvenNat)) 
W:Int --> #1:EvenNat 
Z:Int --> #2:EvenNat 
Y:Int --> #3:EvenNat
     

Note that the second command produces more unifiers than the first command even though both unification problems have only one most general unifier. We can, however, obtain just the single most general unifier for the second unification problem by giving the command:

Maude> irredundant unify in ITER-EXAMPLE : 
       s^1000000(X:OddNat) =? s^100000000001(Y:Int + Z:Int + W:Int) . 
 
Unifier 1 
X:OddNat --> s^99999000001(#1:EvenNat + (#2:EvenNat + #3:EvenNat)) 
W:Int --> #1:EvenNat 
Z:Int --> #2:EvenNat 
Y:Int --> #3:EvenNat
     

As already mentioned, assuming that no bound on the number of unifiers is specified by the user, Maude will always compute a complete set of order-sorted unifiers modulo $Ax$, for $Ax$ the supported equational axioms described in Section 13.3 for which unification is known to be finitary. However, the unify command does not guarantee that the computed set of unifiers is minimal, only the irredundant unify command guarantees that. That is, some of the unifiers in the computed set may be redundant, since they could be obtained as instances (modulo $Ax$) of other unifiers in the set.

13.4.4 Associative-commutative with identity ($ACU$) unification examples

To illustrate the use of the unification command in the presence of ACU operators, let us consider yet another version of the vending machine example (first presented in Section 5.1 and in other sections of this document in different forms):

mod UNIF-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 = $ . 
endm
     

We can ask whether there is an equational unifier of two configurations, one containing at least two quarters, and another containing at least one dollar.

Maude> unify in UNIF-VENDING-MACHINE : 
       < q q X:Marking > =? < $ Y:Marking > . 
 
Unifier 1 
X:Marking --> $ 
Y:Marking --> q q 
 
Unifier 2 
X:Marking --> $ #1:Marking 
Y:Marking --> q q #1:Marking
     

Maude> irredundant unify in UNIF-VENDING-MACHINE : 
       < q q X:Marking > =? < $ Y:Marking > . 
 
Unifier 1 
X:Marking --> $ #1:Marking 
Y:Marking --> q q #1:Marking
     

Recall that memberships are discarded completely. For instance, if we modify the previous example to include a membership definition for a new sort Quarter, a unification call with that sort may not succeed.

mod UNIF-VENDING-MACHINE-MB 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 . 
 
 sort Quarter . 
 subsort Quarter < Coin . 
 mb q : Quarter . 
 
 var M : Marking . 
 rl [buy-c] : < M $ > => < M c > . 
 rl [buy-a] : < M $ > => < M a q > . 
 eq [change]: q q q q = $ . 
endm
     

Maude> unify in UNIF-VENDING-MACHINE-MB : 
       < q q X:Marking > =? < $ Y:Quarter Z:Quarter > . 
 
No unifier.
     

13.4.5 Unification examples with an identity symbol

Let us illustrate the use of the different combinations of the identity attribute for unification. Let us consider first a module using the left-id attribute.

mod LEFTID-UNIFICATION-EX is 
 sorts Magma Elem . 
 subsorts Elem < Magma . 
 op __ : Magma Magma -> Magma [gather (E e) left id: e] . 
 ops a b c d e : -> Elem . 
endm
   

Then the following two unification problems have a different meaning, where we have swapped the position of the variables. First, when we unify two terms where variables of sort Magma are at the left of the terms, we have both a syntactic unifier and a unifier modulo identity.

Maude> unify in LEFTID-UNIFICATION-EX : X:Magma a =? Y:Magma a a . 
 
Unifier 1 
X:Magma --> a 
Y:Magma --> e 
 
Unifier 2 
X:Magma --> #1:Magma a 
Y:Magma --> #1:Magma
     

Maude> irredundant unify in LEFTID-UNIFICATION-EXAMPLE : 
       X:Magma a =? Y:Magma a a . 
 
Unifier 1 
X:Magma --> #1:Magma a 
Y:Magma --> #1:Magma
     

Maude> unify in LEFTID-UNIFICATION-EX : a X:Magma =? a a Y:Magma . 
No unifier.
     

Consider now a similar module but for the right identity.

mod RIGHTID-UNIFICATION-EX is 
 sorts Magma Elem . 
 subsorts Elem < Magma . 
 op __ : Magma Magma -> Magma [gather (e E) right id: e] . 
 ops a b c d e : -> Elem . 
endm
   

When we unify two terms where variables of sort Magma are at the left of the terms, there is clearly no unifier, since the term Y:Magma a a is parsed as Y:Magma (a a) in module RIGHTID-UNIFICATION-EX due to the attribute gather (e E) (see Section 3.9).

Maude> unify in RIGTHID-UNIFICATION-EX : X:Magma a =? Y:Magma a a . 
No unifier.
     

Maude> unify in RIGHTID-UNIFICATION-EX : a X:Magma =? a a Y:Magma . 
 
Unifier 1 
X:Magma --> a 
Y:Magma --> e 
 
Unifier 2 
X:Magma --> a #1:Magma 
Y:Magma --> #1:Magma
     

Maude> irredundant unify in RIGHTID-UNIFICATION-EX : 
       a X:Magma =? a a Y:Magma . 
 
Unifier 1 
X:Magma --> a #1:Magma 
Y:Magma --> #1:Magma
     

Consider now a similar module but with the identity attribute (no left or right restriction).

mod ID-UNIFICATION-EX is 
 sorts Magma Elem . 
 subsorts Elem < Magma . 
 op __ : Magma Magma -> Magma [gather (E e) id: e] . 
 ops a b c d e : -> Elem . 
endm
   

When we unify two terms where variables of sort Magma are at the left of the terms, we have both a syntactic unifier and a unifier modulo identity:

Maude> unify in ID-UNIFICATION-EX : X:Magma a =? Y:Magma a a . 
 
Unifier 1 
X:Magma --> a 
Y:Magma --> e 
 
Unifier 2 
X:Magma --> #1:Magma a 
Y:Magma --> #1:Magma
     

Maude> irredundant unify in ID-UNIFICATION-EX : X:Magma a =? Y:Magma a a . 
 
Unifier 1 
X:Magma --> #1:Magma a 
Y:Magma --> #1:Magma
     

Maude> unify in ID-UNIFICATION-EX : a X:Magma =? a a Y:Magma . 
 
Unifier 1 
X:Magma --> a 
Y:Magma --> e
     

And finally, when we add commutativity, we obtain slightly different results.

mod COMM-ID-UNIFICATION-EX is 
 sorts Magma Elem . 
 subsorts Elem < Magma . 
 op __ : Magma Magma -> Magma [gather (E e) comm id: e] . 
 ops a b c d e : -> Elem . 
endm
   

When we unify two terms where variables of sort Magma are at the left of the terms, we have both a syntactic unifier and a unifier modulo identity and commutativity, but the latter is duplicated:

Maude> unify in COMM-ID-UNIFICATION-EX: X:Magma a =? Y:Magma a a . 
 
Unifier 1 
X:Magma --> a 
Y:Magma --> e 
 
Unifier 2 
X:Magma --> a #1:Magma 
Y:Magma --> #1:Magma 
 
Unifier 3 
X:Magma --> a 
Y:Magma --> e