Semantical domain for SPEC

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear semantics group members,

the work for task B1 has been divided into five parts.
To ensure that the outcomes, especially of part 1/2 and 3,
are compatible, I propose to fix the semantical domain
for SPECs as follows:

[SPEC] = {f:SigMod -o-> SigMod |
          f is a partial function,
          f(\Sigma,M) defined ==>
               f(\Sigma,M) is an extension of (\Sigma,M)  }

SigMod = {(\Sigma,M) | \Sigma is a signature
                       M \subseteq Mod(\Sigma) }

(\Sigma',M') \in SigMod is an extension of (\Sigma,M) \in SigMod                             iff there exists an inclusion \sigma:\Sigma-->\Sigma'
		and Mod(\sigma)(M') \subseteq M

A naive choice for [SPEC] of course would be SigMod itself.
The reason for the more complicated domain is explained on
page 21 of the annotated tentative design, it has to do
with incomplete parts of specifications, which must have
a semantics, too.

Please use this domain for SPECs (or propose another one),
and, more importantly, already for BASIC-SPECs (or describe a 
way of constructing an element of [SPEC] from an element of [BASIC-SPEC].
I see no way how to do this if [BASIC-SPEC]=SigMod).

Greetings,
Till