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 language||English (US)|
|Number of pages||31|
|Journal||Journal of Symbolic Computation|
|State||Published - 1989|
ASJC Scopus subject areas
- Algebra and Number Theory
- Computational Mathematics