Order-sorted unification

Jose Meseguer, Joseph A. Goguen, Gert Smolka

Research output: Contribution to journalArticlepeer-review


This paper studies unification for order-sorted equational logic. This logic generalizes unsorted equational logic by allowing a partially ordered set of sorts, with the ordering interpreted as set-theoretic containment in the models; it also allows overloading of function symbols, such as + for integer and rational number addition, with the overloaded functions of greater rank interpreted in the models as extensions of those of smaller rank. Our presentation emphasizes semantic aspects, and gives a categorical treatment of unification that has substantial advantages in this context over the usual treatment of unifiers as endomorphisms of a single free algebra. Given system Γ of equations and a set E of axioms that is sort-preserving and does not impose restrictions on the sorts of its variables, the main results characterize when an order-sorted signature has a minimal (or finite, or most general when Γ is solvable) family of order-sorted E-unifiers for Γ. In addition, for unitary signatures, where each solvable system of equations has a most general unifier, we give a quasi-linear algorithm for syntactic unification (i.e., for E= ) a la Martelli-Montanari, that is more efficient than the unsorted one for failures.

Original languageEnglish (US)
Pages (from-to)383-413
Number of pages31
JournalJournal of Symbolic Computation
Issue number4
StatePublished - 1989
Externally publishedYes

ASJC Scopus subject areas

  • Algebra and Number Theory
  • Computational Mathematics


Dive into the research topics of 'Order-sorted unification'. Together they form a unique fingerprint.

Cite this