disjointness of sorts of a many sorted algebra

98 Views Asked by At

Given a many-sroted signature sig with the sorts S1, S2, ..., Sn.

A many sorted algebra alg of signature sig comprises a carrier set Ai for each sort Si, i.e., A1 is the carrier set of S1, etc.

Questions

  1. Do A1, A2, ..., An have to be pairwise-disjoint? I have been reading through many definitions and none explicitly excludes this possiblity. If that is not allowed; what is the reasoning/implications behind that?

  2. Is there any reason that prevents a sort Si from being a composite sort, e.g., assume A1 to be natural numbers N and A2 to be the power set of N (the set of all sets the can be constructed from the natural numbers N).

  3. Do you recommend some introductory references?

EDIT 1

As an example of question (1), consider that we have two sorts: NATURALS and INTEGERS, which, in some algebra, have the carrier sets N (natural numbers) and Z (integral numbers). I think that this is a very natural requirement. For example, assume we are interested in subtraction of natural numbers which then will be expressed as function: subtract : NATURALS x NATURALS -> INTEGERS