S-1 -- 1.1 Signatures

Go up to 1 Basic Concepts
Go forward to 1.2 Models

1.1 Signatures

A many-sorted signature Sigma= (S,TF,PF,P) consists of:

a set S of sorts;
sets TF_w,s, PF_w,s, of total function resp. partial function symbols, such that TF_w,s n PF_w,s = Ø, for each function profile (w,s) consisting of a sequence of argument sorts w e S^* and a result sort s e S ( constants are treated as functions with no arguments);
sets P_w of predicate symbols, for each predicate profile consisting of a sequence of argument sorts w e S^*.

[TM] Can the sets of sorts, function symbols and predicate symbols be infinite? (No)

Discharged: It doesn't seem to matter much, but let's say that they must be finite.

Note that symbols may be overloaded, occurring in more than one of the above sets. To ensure that there is no ambiguity in sentences at this level, however, symbols are always qualified by profiles when used (the language considered in a later section allows the omission of such qualifications when these are unambiguously determined by the context).

A many-sorted signature morphism sigma: (S,TF,PF,P) -> (S',TF',PF',P') consists of a mapping from S to S', and for each w e S^*, s e S, a mapping between the corresponding sets of function, resp. predicate symbols. A partial function symbol may be mapped also to a total function symbol, but not vice versa.

[DTS] The last few words are potentially ambiguous, but I think it is clear that what is meant is that sigma has four components: sigma^S : S -> S'; <sigma^TF_w,s : TF_w,s -> TF_{sigma^S(w),sigma^S(s)}>_we S^*, s e S; <sigma^PF_w,s : PF_w,s -> TF_{sigma^S(w),sigma^S(s)} u PF_{sigma^S(w),sigma^S(s)}>_we S^*, s e S; <sigma^P_w : P_w -> P_sigma^S(w)>_we S^*.

Discharged: Yes, but the text is probably clear enough as it stands.

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk