**Go up to** 3 Subsorting Concepts

**Go forward to** 3.2 Models

## 3.1 Signatures

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 ***e*** (**TF*_{w1,s1} **u*** **PF*_{w1,s1}) **n*** (**TF*_{w2,s2} **u*** **PF*_{w2,s2}) and *p ***e*** P*_{w1} **n*** P*_{w2}. Two qualified operation symbols *f*_{w1,s1}
and *f*_{w2,s2} are in the *overloading relation* (written
*f*_{w1,s1} ~ _{F} f_{w2,s2}) iff there exists a *w ***e*** S*^{*} and
*s ***e*** S* such that *w *__<__ _{S} w_{1}, w_{2} and *s*_{1}, s_{2} __<__ _{S} s.
Similarly, two qualified predicate symbols *p*_{w1} and *p*_{w2} are
in the overloading relation (written *p*_{w1} ~ _{P} p_{w2}) iff
there exists a *w ***e*** S*^{*} such that *w *__<__ _{S} w_{1}, w_{2}. 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: Sigma*_{1} -> Sigma_{2}
expands to a many-sorted signature morphism *sigma*^{#}:
Sigma_{1}^{#} -> Sigma_{2}^{#}, preserving the symbols used for
embedding, projection, and membership.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk