A subsorted signature Sigma=(S, TF, PF,P, < S) consists of a many-sorted signature (S, TF, PF,P) together with a pre-order < S of subsort embedding on the set S of sorts. < S is extended pointwise to sequences of sorts. We may drop the subscript S when obvious from the context.
For a subsorted signature, we define overloading relations for operation and predicate symbols. Let f in (TFw1,s1 union PFw1,s1) n (TFw2,s2 union PFw2,s2) and p in Pw1 n Pw2. Two qualified operation symbols fw1,s1 and fw2,s2 are in the overloading relation (written fw1,s1 ~ F fw2,s2) iff there exists a w in S* and s in S such that w < S w1, w2 and s1, s2 < S s. Similarly, two qualified predicate symbols pw1 and pw2 are in the overloading relation (written pw1 ~ P pw2) iff there exists a w in S* such that w < S w1, w2. We say that two profiles of a symbol are in the overloading relation if the corresponding qualified symbols are in overloading relation.
Note that two profiles of an overloaded constant declared with different sorts are in the overloading relation iff the two sorts have a common supersort.
A subsorted signature morphism sigma: Sigma -> Sigma' is a many-sorted signature morphism that preserves the subsort relation and the overloading relations.
With each subsorted signature Sigma=(S, TF, PF,P, < S) a many-sorted signature Sigma# is associated, extending (S, TF, PF,P) for each pair of sorts s < S s' by a total embedding operation (from s into s'), a partial projection operation (from s' onto s), and a membership predicate (testing whether values in s' are embeddings of values in s). The symbols used for embedding, projection, and membership are chosen arbitrarily so as not to be in Sigma.
Any subsorted signature morphism sigma: Sigma1 -> Sigma2 expands to a many-sorted signature morphism sigma#: Sigma1# -> Sigma2#, preserving the symbols used for embedding, projection, and membership.