Unique-sort order-sorted theories: A description as monad morphisms

Abstract

We present an apparently novel definition of order-sorted theory with the intention of clarifying various approaches to order-sorted algebra used in existing work on term rewriting and unification. If S is a poset we take an S-sorted theory to be a morphism between two monads, one in a category of S-sorted sets and one in Set. We describe various categories of S-sorted sets, but we concentrate on one appropriate for describing theories where the terms have unique sorts. One motivation for this work is to determine an appropriate category in which the existing category-theoretic description of unsorted non-equational unification may be extended to the order-sorted context. We use our notion of theory to relate two superficially different ways of describing a collection of order-sorted terms and substitutions, which have appeared in the literature on order-sorted unification. This both clarifies the relationship between these two approaches and shows how far our definition accommodates existing approaches.