Unification is the solving of equations, either in free algebras of the form TΣ(X), or in relatively free algebras modulo a set E of equations, that is, in algebras of the form TΣ∕E(X). The first case is sometimes called syntactic unification. The second case is sometimes called E-unification, or, if E is not explicitly mentioned, 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 to the equation, is called a unifier. For example, if we are solving the above
equation in the free algebra TΣ(X) with X a countable set of variables and with Σ having a single
sort (unsorted unification), the substitution σ = {x
g(y),z
h(y)} is a unifier, and indeed the
so-called most general unifier, so that for any other unifier ρ there exists a substitution μ such that
ρ = σ;μ, where σ;μ 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
σ.
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Σ(X). It does, however, have a solution in TΣ∕C(X), where C is the commutativity axiom f(x,y) = f(y,x). Indeed, the exact same substitution σ 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)) = Cf(g(y),h(y)).
Unification is a fundamental deductive mechanism used in many automated deduction tasks (see Section 12.6 for a discussion of some of them). 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, as explained in Section 12.6.2, about rewrite theories (system modules or theories).
Therefore, it is very useful to have an efficient implementation of unification available in Core Maude, which is what this chapter describes. Specifically, we explain how order-sorted unification modulo frequently occurring equational axioms is currently supported in Maude 2.4.
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. Furthermore, for an arbitrary set of equations E no unification algorithm may be known; even if one is known, the number of solutions may be infinite.
This suggests 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 confluent and terminating modulo Ax. We can then consider order-sorted equational theories of the form (Σ,E ∪ Ax) and decompose the E ∪ Ax-unification problem into two problems: one of Ax-unification, and another of E ∪Ax-unification that uses an Ax-unification algorithm as a subroutine. This decomposition, as well as a similar one for membership equational theories, are explained in Section 12.6. The point is that only Ax-unification needs to be built-in at the level of Core Maude’s C++ implementation for efficiency purposes. Instead, E ∪ Ax-unification can then be implemented in Maude itself. 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.
We can, however, define the basic concepts of order-sorted E-unification in full generality, even though in the Core Maude implementation E will always be a particular combination of equational axioms declared as equational attributes in a module or a theory.
Given an order-sorted equational theory (Σ,E), an E-unification problem consists of a nonempty
set of unification equations of the form t
t′, written in the notation
where n ≥ 1 and the “conjunction” operator ∧ is assumed to be associative and commutative.
Given such an E-unification problem, an E-unifier for it is an order-sorted substitution1 σ : Vars(t1,t′1,…,tn,t′n)-→TΣ(X) (where we assume that the set of variables X contains a countable number of variables for each sort) such that, for all i = 1,…,n,
where Y i = Vars(σ(ti),σ(t′i)), that is, all the equations (∀Y i) σ(ti) = σ(t′i) can be deduced in (membership) equational logic from the set of equations E.
A set of unifiers 
is called a complete set of E-unifiers for a given E-unification problem
t1
t′1 ∧… ∧ tn
t′n iff for any other E-unifier ρ of the same E-unification problem there exists a
substitution μ and a unifier σ ∈ such that ρ = Eσ;μ, that is, for each variable x in the domain of ρ
we have E ⊢ ρ(x) = μ(σ(x)). A complete set of E-unifiers is called minimal if any proper subset of
fails to be complete.
For an order-sorted equational theory (Σ,E), unification is said to be finitary if for any
E-unification problem there is always a finite complete set of unifiers . Similarly, unification for
(Σ,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 (Σ,E) has a unification algorithm if there is an algorithm generating a complete set of E-unifiers for any E-unification problem in (Σ,E).
Unlike unsorted syntactic unification, which always either fails or has a single most general unifier, order-sorted syntactic unification is not unitary, that is, there is in general no single most general unifier. What exists (if Σ 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. However, for other theories, such as commutativity or associativity-commutativity, unification is finitary, both when Σ is unsorted and when Σ is order-sorted (and finite).
As mentioned in Section 12.2, a practical way of dealing with order-sorted equational unification is to consider order-sorted theories of the form (Σ,E ∪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 ∪Ax-unification problem into an Ax-unification problem and an E ∪Ax-unification problem that uses an Ax-unification algorithm as a subroutine. In such a decomposition, only the Ax-unification algorithm needs to be built-in for efficiency purposes.
Maude 2.4 currently provides an order-sorted Ax-unification algorithm for all order-sorted theories (Σ,E ∪ Ax) such that:
Explicitly excluded are theories with binary function symbols having either: (i) the id:, left id:, or right id: attributes; or (ii) the assoc attribute without the comm one; or (iii) a combination of (i) and (ii) (for example, a binary symbol with only assoc and id: attributes). The reason for excluding the assoc attribute without comm is the already-mentioned fact that associative unification is not finitary. The reason for excluding for the moment the id:, left id:, and right id: attributes is that they are collapse equations (one of the terms in the equation is a variable), requiring a more complex way of combining their unification algorithms than the combination method supported by the current Maude implementation. However, such id:, left id:, and right id: attributes may be supported in a future release. Moreover, as explained in Section 12.6, they can currently be supported in a non-built-in way.
If we give to Maude a unification problem in a functional module of the form fmod (Σ,Ax) endfm where Σ and Ax satisfy the above requirements, we get a complete set of order-sorted unifiers modulo the theory (Σ,Ax). If, instead, we give the same problem to Maude in the functional module fmod (Σ,E ∪ Ax) endfm, then the equations E are ignored and we still get a complete set of order-sorted unifiers modulo the theory (Σ,Ax). Similarly, if we provide the same unification problem in a functional theory fth (Σ,E ∪ Ax) endfth, a system module mod (Σ,E ∪ Ax,R) endm or a system theory th (Σ,E ∪ Ax,R) endth, we again get a complete set of order-sorted unifiers modulo the theory (Σ,Ax). All this is consistent with the decomposition idea mentioned above: to deal with order-sorted E ∪ Ax-unification, other methods, that use the Ax-unification algorithm as a component, can later be defined as we explain in Section 12.6.
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 (Σ,E ∪ M ∪ Ax ∪ Ax′) endfm (or the analogous specification in the other cases), where (Σ,Ax) satisfies the conditions mentioned above, but M is an optional set of membership axioms (that is, (Σ,E ∪M ∪Ax∪Ax′) can be a membership equational theory and not just an order-sorted theory), and the axioms Ax′ violate those requirements (as explained in conditions (i)–(iii) above). Then what will happen is:
Furthermore, the functional module fmod (Σ,E ∪ M ∪ Ax ∪ Ax′) 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.
Given a functional module or theory, or a system module or theory, ⟨ModId⟩, the user can give to Maude a unification command of the form:
] in ⟨ModId⟩ :
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 ⟨ModId⟩ can be any module or theory declared in the current Maude session (as usual, if no module is mentioned, the current module is used).
For a simple example of syntactic order-sorted unification problem illustrating:
and then give to Maude the following command:
The next example on the same module illustrates the use of the unify command with a unification problem consisting of two unification equations:
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
so that, if we give again the same unify commands above, we will obtain exactly the same sets of order-sorted unifiers as for the UNIFICATION-EX1 module.
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:
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 7.2), plus the fact that even small AC-unification problems can generate a large number of unifiers are all illustrated by the following command:
The following unification command in the predefined CONVERSION module (see Section 7.9) 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.
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:
As already mentioned, a unification problem using such an associative function symbol f in a non-ground subterm will mean that the unification attempt fails and a warning is issued:
Instead, if all symbols satisfying unsupported equational axioms Ax′ only appear in ground subterms of the unification problem, the unification attempt succeeds with the correct set of order-sorted Ax ∪ Ax′-unifiers:
We finish this section with an example illustrating the efficiency of order-sorted unification modulo the iter theory (in this example in combination with the comm theory). Consider the following module:
We can then give the unification commands:
and
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 12.3. However, there is no guarantee that the computed set of unifiers is minimal, 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.
Following the general Maude philosophy, all Maude functionality is as much as possible moved up to the metalevel, so that it becomes available by reflection (see Chapter 11). This is particularly important for unification for two reasons:
In Maude 2.4, unification is reflected in the META-LEVEL module (see Section 11.5) by two descent functions:
These two metalevel functions work on unification problems constructed by means of the following signature:
The key difference between metaUnify and metaDisjointUnify is that the latter assumes that the variables in the left and righthand unificands are to be considered disjoint even when they are not so, and it generates each solution to the given unification problem not as a single substitution, but as a pair of substitutions, one for left unificands and the other for right unificands. This functionality is very useful for applications, such as critical-pair checking or narrowing, where a disjoint copy of the terms or rules involved must always be computed before unification is performed. The metaDisjointUnify operation avoids the explicit computation of such disjoint copies. The need for two substitutions in each solution is then obvious, since the terms in the given unification problem need not be made explicitly disjoint, but their (accidentally) common variables must be treated differently, as if they were disjoint.
Since it is convenient to reuse variable names from unifiers in new problems, for example in narrowing, this is allowed via the third argument, which is the largest number n appearing in a unificand metavariable of the form #n:Sort. Then the fresh metavariables in the computed unifiers will all be numbered from n + 1 on.
As is usual for descent functions, the last argument in the function is used to select which result is wanted, starting from 0. Caching is used so that if unifier i has just been returned, requesting unifier i + 1 gives rise to an incremental computation.
Results are returned using the following constructors:
as appropriate for the descent function. The final Nat component is the largest n occurring in a fresh metavariable of the form #n:Sort. In this way, when we want to reuse variable names from unifiers, the next invocation of the function can use this parameter to make sure that the new variables generated are always fresh.
When no unifier with a given index exists the constant
or, respectively, the constant
is returned as appropriate for the corresponding descent function.
We can illustrate the use of these metalevel functions with a few examples. The first one comes from the previous section, but moved up at the metalevel:
The second example shows that we can request fresh variables with arbitrarily large numbering:
The following example shows a similar unification problem but with much smaller numberings in fresh variables, and now involving an invocation of metaDisjointUnify.
Yet another example shows how using variable names in unification problems with larger numbers than declared by the third argument generates a warning and no reduction.
In this section we review briefly some applications that can be developed using a unification infrastructure like the one described in this chapter. We begin by discussing narrowing and narrowing-based unification algorithms. We also explain how narrowing modulo an equational theory can be used for reachability analysis of concurrent systems described by rewrite theories, and, more generally, for symbolic temporal logic model checking of such systems. We then discuss briefly other automated deduction applications, including theorem proving ones.
Chapter 16 contains more information about an implementation of narrowing in Full Maude following the ideas introduced here.
If we have a dedicated algorithm (as the one supported by Maude) to solve unification problems in an order-sorted theory (Σ,Ax), then we can use it as a component to obtain a unification algorithm for theories of the form (Σ,E ∪ Ax), provided the equations E are coherent,2 confluent and terminating modulo Ax [69].
The technique used under such conditions to obtain an E ∪ Ax-unification algorithm
from an Ax-unification algorithm is called narrowing, and is the obvious generalization
of term rewriting to handle logical variables and perform a kind of symbolic rewriting.
In ordinary term rewriting, if we want to apply a rewrite rule, say l → r, to a term t at
position p, the subterm tp must be an instance of the lefthand side l, that is, there must be a
substitution σ such that tp = σ(l). Instead, in narrowing we can apply the rule l → r at a
non-variable position p in t, provided the unification problem tp
l (where the variables of
l and t are assumed disjoint) has a nonempty set of unifiers. For any such unifier θ we
then narrow the original term t to the substitution instance under θ of t[r]p. We then
write
![t ↝ θ(t[r])
p](maude-manual112x.png)
for such a narrowing step. For example, in the standard, unsorted specification of the natural
numbers, we can use the equation x + s(y) = s(x + y) as a rewrite rule to narrow the term
x′* (y′ + z′) at position 2 with substitution θ = {x
y′′,y
z′′,y′
y′′,z′
s(z′′)} to get the
narrowing step
In this example, θ is the most general unifier for the syntactic unification problem y′ + z′
x + s(y).
However, in the same way as we can perform rewriting modulo a set of axioms Ax if we have an
Ax-matching algorithm, we can likewise perform narrowing modulo a set Ax of axioms if we have an
Ax-unification algorithm. That is, the unification problems tp
l are now solved, not by syntactic
unification, but by Ax-unification.
If a theory (Σ,E ∪ Ax) satisfies the above coherence, confluence, and termination modulo Ax requirements, we can systematically reduce E ∪ Ax-unification problems to narrowing problems as follows:
t′ to the narrowing reachability problem
modulo Ax in the theory extending (Σ,E ∪ Ax) with these new sorts, operators, and equations, where E and the new equations are used as rewrite rules.
That is, we search for all narrowing paths modulo Ax from eq(t,t′) to tt. Each such path then gives us a
unifier of the equation t
t′, just by composing the unifiers of each narrowing step in the path. As
explained in [12], narrowing can be performed not only in order-sorted equational theories, but also in
membership equational theories.
The just-described computation of E ∪Ax-unifiers by narrowing modulo Ax yields a complete but in general infinite set of E ∪ Ax-unifiers. For the case when Ax = ∅, some sufficient conditions are known ensuring termination of the basic narrowing strategy (see, e.g., [68, 5, 3]), and therefore ensuring that the complete set of E ∪Ax-unifiers computed by basic narrowing is finite. However, for commonly occurring sets of axioms Ax, such as associativity-commutativity (AC), it is well-known that narrowing modulo AC “almost never terminates” and, furthermore, that narrowing strategies facilitating termination such as basic narrowing are incomplete [106, 27]. Based on the idea of “variants” in [27], a complete, yet quite efficient in terms of its search space, narrowing strategy modulo Ax called variant narrowing has been proposed in [56]. Furthermore, in [55] sufficient checkable conditions on (Σ,E ∪ Ax) have been given ensuring that the E ∪ Ax-unification algorithm provided by variant narrowing modulo Ax is finitary, even though variant narrowing modulo Ax may still not terminate in spite of such conditions. A Maude-based narrowing library that uses the current built-in unification algorithm of Maude 2.4 as a component has been developed by Santiago Escobar and, as explained in Section 12.6.2, is used as a key component in the Maude-NPA tool [53] for analyzing cryptographic protocols.
The above discussion has a direct bearing on the issue of how to support in Maude 2.4 unification modulo “forbidden” axioms (i.e., axioms not supported by the current Maude unification algorithm) such as the id:, left id:, and right id: equational attributes in the context of other allowed axioms Ax. In a future Maude implementation, such axioms may also be supported in a built-in way, but currently they are not. The idea is that for Ax′ axioms of the form id:, left id:, and right id:, we can consider a theory decomposition (Σ,Ax′∪ Ax), where Ax are axioms currently supported by Maude’s unification algorithm. As it turns out, the sufficient conditions in [55] do apply to such equations Ax′ modulo Ax, and we can get a finitary Ax′∪ Ax-unification algorithm by variant narrowing modulo Ax.
A rewrite theory3 ,
say 
= (Σ,E ∪Ax,R), specified in Maude as a system module, describes a concurrent system whose
states are E ∪ Ax-equivalence classes of ground terms, and whose local concurrent transitions are
specified by the rules R. When formally analyzing the properties of , an important problem
is ascertaining for specific patterns t and t′ the following symbolic reachability problem:
with X the set of variables appearing in t and t′, which for this discussion we may assume are a disjoint union of those in t and those in t′. That is, t and t′ symbolically describe sets of concurrent states [[t]] and [[t′]] (namely, all the ground substitution instances of t, resp. t′, or, more precisely, the E ∪ Ax-equivalence classes associated to such ground instances). And we are asking: is there a state in [[t]] from which we can reach a state in [[t′]] after a finite number of rewriting steps?
For example, may specify a cryptographic protocol, t may symbolically describe a set of initial
states, and t′ may likewise describe a set of attack states. Then, if the above reachability question can
be answered in the affirmative, the protocol is insecure against the kinds of attacks described by t′.
Furthermore, if the way of answering the reachability question is somehow constructive, we should
be able to exhibit a concrete attack as a rewrite sequence violating the security of the
protocol.
As explained in [89], provided the rewrite theory = (Σ,E ∪ Ax,R) is topmost (that is, all
rewrites take place at the root of a term), or, as in the case of AC rewriting of object-oriented
systems, is “essentially topmost,” and the rules R are coherent with E modulo Ax, narrowing with
the rules R modulo the equations E ∪Ax gives a constructive, sound, and complete method to solve
reachability problems of the form (∃X) t-→*t′, that is, such a problem has an affirmative answer if
and only if we can find a finite narrowing sequence modulo E ∪Ax of the form t ↝*θ(t′) for some θ.
The method is constructive, because instantiating t with the composition of the unifiers for each step
in the narrowing sequence gives us a concrete rewrite sequence witnessing the existential
formula.
Of course, narrowing with R modulo E ∪ Ax requires performing E ∪ Ax-unification at each
narrowing step. As explained in Section 12.6.1, E ∪ Ax-unification can itself be performed by
narrowing with the equations E modulo Ax, provided E is coherent, confluent, and terminating
modulo Ax. Therefore, in performing symbolic reachability analysis in a rewrite theory
= (Σ,E ∪Ax,R) there are usually two levels of narrowing and two levels of unification: narrowing
with R modulo E ∪ Ax for reachability, and narrowing with E modulo Ax for unification purposes.
Similarly, unification modulo E ∪ Ax is performed by narrowing, while unification modulo Ax is
usually performed in a built-in way.
This is exactly the approach taken in the Maude-NPA protocol analyzer [53], where cryptographic
protocols are formally specified as rewrite theories of the form = (Σ,E ∪ Ax,R), and the formal
reachability analysis is performed in a backwards way, from an attack state to an initial state. This
just means that we perform standard (forwards) reachability analysis with the rewrite theory
-1 = (Σ,E ∪Ax,R-1), where R-1 = {r-→l∣(l-→r) ∈ R}. The equational theory E ∪Ax typically
specifies the algebraic properties of the cryptographic functions used in the given protocol, for
example, public key encryption and decryption, exclusive or, modular exponentiation, and so on.
Reasoning modulo such algebraic properties is very important to gain high levels of assurance, since it
is well-known that some cryptographic protocols that can be proved secure under the standard
Dolev-Yao model, in which the cryptographic functions are treated as a “black box,” can
actually be broken by an attacker that makes clever use of the algebraic properties of
the cryptographic functions of the protocol. Besides using narrowing with rules modulo
equations, the Maude-NPA tool uses several state space reduction techniques, including
grammars that can describe sets of unreachable states that need not be explored [53],
to drastically reduce the narrowing search space, often from an infinite set of states to
a finite set of them, so that finite failure to find an attack becomes an actual proof of
security.
Given a rewrite theory = (Σ,E ∪ Ax,R), we may be interested in verifying properties more
general than existential questions of the form (∃X) t-→*t′. Note that we can view such questions as
questions about the violation of an invariant, because we can regard the set of states [[t′]] as
the complement of an invariant set of states, say I, which can be easily specified by an
equationally-defined predicate. That is, proving the existential formula (∃X) t-→*t′ is the same thing
as finding a counterexample for the assertion ,t
□I. This is just a temporal logic satisfaction
assertion (see Chapter 10), but with the following nonstandard features: (i) the term t does not
describe a single initial state, but a possibly infinite set [[t]] of initial states; and (ii) there is no
guarantee that the set of reachable states is finite. Therefore, standard model-checking
techniques may not be usable, because of a possible double infinity: in the number of initial
states, and in the number of states reachable for each of those initial states. One can also
generalize the above reachability question ,t
□I to questions of the form ,t
φ, with φ a
temporal logic formula. The paper [54] shows how narrowing can be used (again, both at the
level of transitions with rules R and at the level of equations E) to perform a kind of
symbolic model checking to verify such temporal logic formulas, not in the binary decision
diagram sense of “symbolic,” which still remains finite-state, but in a much more general
sense in which possibly infinite sets of states are finitely described by patterns with logical
variables.
The automated deduction application par excellence, and the one that historically, thanks to Alan Robinson, gave rise to the unification notion is resolution-based theorem proving [99]. Subsequent work by Gordon Plotkin [94] made it clear that not just syntactic unification, but unification modulo a set of equational axioms Ax is a very useful mechanism supporting theorem proving. Indeed, state-of-the-art resolution-based theorem provers routinely support unification modulo commonly occurring equational theories such as AC. Of course, the use of equational unification need not be restricted to resolution-based theorem provers. For example, the paper [100] shows how narrowing with sequent rules and equational unification can be used in a sequent-based theorem prover in which one can reason modulo both the equivalences given by the structural rules for sequents and also Boolean equivalences between formulas.
Yet another important application area is that of formal reasoning methods such as Knuth-Bendix equational completion (and its associated “inductionless induction” theorem-proving methods), checking local confluence of rewrite rules, and checking coherence of a set of rewrite rules with respect to a set of equations [107]. In all these formal reasoning methods one needs to compute critical pairs by unification of a term with a subterm of another term. In particular, tools such as the Maude Church-Rosser Checker (CRC) and Coherence Checker (ChC) were up to now restricted to theories where the only equational axiom supported was commutativity. Thanks to the present built-in support for unification modulo a wide set Ax of axioms (further extensible to identity axioms by narrowing as explained in Section 12.6.1), it will be possible in the near future to have much more general versions of the Maude Church-Rosser Checker and Coherence Checker tools to reason about the confluence and coherence of Maude specifications modulo equational axioms specified as equational attributes in Maude modules and theories.
The current Maude order-sorted unification algorithm modulo axioms Ax is what we might call an endogenous algorithm, in the sense that the computation of order-sorted unifiers is intimately integrated with the order-sorted reasoning process, so that unifiers that do not type under the order-sorted typing restrictions are never generated. This makes such an algorithm typically more efficient, because the order-sorted typing restrictions may drastically cut the number of generated unifiers, particularly modulo axioms such as AC where the number of unsorted unifiers can be very large. That is, order-sorted unification, even though it lacks the unitary property of unsorted syntactic unification and is more expensive than unsorted unification in the syntactic case, can often be more efficient in the modulo Ax case because of the drastic reductions that can be achieved by order-sorted typing restrictions in the number of Ax-unifiers. Moreover, even in the syntactic case, the efficiency of deductive processes that use order-sorted unification can substantially increase, because order-sorted unification will fail more often than unsorted unification, leading to smaller search spaces.
However, from the early papers on order-sorted unification such as, e.g., [101, 87, 102] a more modular, although typically less efficient, approach to order-sorted unification, which we might call exogenous has been known. The basic idea is to reuse an unsorted unification algorithm modulo some axioms Ax (under some conditions on Ax) to compute order-sorted Ax-unifiers in the following way:
For a state-of-the art study of the exogenous approach, allowing very general axioms Ax and proving the correctness of an order-sorted inference system to generate the order-sorted unifiers from the unsorted ones, see [66].
Both the endogenous and the exogenous approaches have their own advantages and disadvantages. The endogenous approach is more efficient, but it requires dedicated algorithms and implementations, so that unsorted unification algorithms and tools cannot be reused. The exogenous algorithms are less efficient because: (i) they can generate many unifiers that may later be discarded; (ii) a separate order-sorted filtering process is needed; and (iii) changes of representation, and even parsing, are required between unsorted and order-sorted representations (particularly when existing unsorted algorithms are reused). However, they are more modular and flexible, so that one can with relatively little effort obtain an order-sorted unification algorithm from an unsorted one.
In Maude we have experimented with, and benefited from, both an exogenous algorithm and the current endogenous one. The exogenous algorithm was developed in collaboration with Evelyn Contejean and Claude Marché from Université Paris-Sud, and involved also the efforts of Prasanna Thati and Joe Hendrix at UIUC. It reused the rich library of unsorted unification algorithms modulo axioms of the CiME system [29], which could be called from Maude in an experimental version. Inside Maude, it used the order-sorted inference system to compute order-sorted unifiers developed by Joe Hendrix and described in [66].
This exogenous algorithm has been extensively used in a previous version of the Maude-NPA tool, and has been shown effective in finding attacks to cryptographic protocols modulo nontrivial equational theories of the form E ∪ Ax [52]. The exogenous algorithm has also been extremely useful in testing the endogenous one. Because of the large number of unifiers generated and the complex nature of semantic unification algorithms, their testing is a nontrivial matter, and the automation of such testing is quite difficult. Thanks to the exogenous algorithm, and through the efforts of Ralf Sasse and Santiago Escobar, it has been possible to generate large numbers of random unification problems of different sizes in which the sets of unifiers generated by the exogenous and endogenous order-sorted unification algorithms have been automatically compared. This testing uncovered several bugs in an earlier alpha version of the Maude endogenous algorithm, and has also served to evaluate in practice the greater efficiency of the endogenous algorithm developed by Steven Eker.
Order-sorted unification is NP-complete in general because Boolean algebra can be encoded as an order-sorted free theory signature and hence satisfiability can be reduced to an order-sorted free theory unification problem. In practice, reasonable performance can be obtained using a binary decision diagram technique to compute sorts for free variables occurring in unsorted unifiers. Furthermore in the AC case, sort information can be pushed into the unsorted unification algorithm and used to prune the Diophantine basis and the choice of subsets drawn from such a basis [50].
The unification theory combination framework and AC-unification algorithm are based on [11] while the Diophantine system solver used by the AC algorithm is based on [28]. The unification algorithm has been thoroughly tested by Santiago Escobar and Ralf Sasse using CiME [29] as an oracle, and has shown better average performance than CiME on the same problems.