Affordable Access

Publisher Website

Order-sorted unification

Authors
Journal
Journal of Symbolic Computation
0747-7171
Publisher
Elsevier
Publication Date
Volume
8
Issue
4
Identifiers
DOI: 10.1016/s0747-7171(89)80036-7
Disciplines
  • Computer Science
  • Linguistics
  • Mathematics

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

Order-sorted feature theory unification

on The Journal of Logic Programmi... Jan 01, 1997

Regular expression order-sorted unification and ma...

on Journal of Symbolic Computatio...

Regular expression order-sorted unification and ma...

on Journal of Symbolic Computatio...
More articles like this..