Re: Minutes of Berlin meeting

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

Dear friends,

here are the proposals of the necessary changes (or better: clarifications)
of the summary according to the discussion in Berlin, apart
from the change of architectural specifications, which was already
treated by Andrzej in his mail from Tue, 18 Apr 2000.
Aha, and apart from the necessary changes to Appendix C
concerning the positions of comments and annotations.

Greetings,
Till

(i) meta-foundations: axiom of choice.

In chapter 5, after the paragraph

The semantics of structured specifications involve signature morphisms
and the corresponding reducts on models.  For instance, hiding some
symbols in a specification corresponds to a signature morphism that
injects the non-hidden symbols into the original signature; the
models, after hiding the symbols, are the reducts of the original
models along this morphism.  Translation goes the other way: the
reducts of models over the translated signature back along the
morphism give the original models.

add the following:

For the semantics of structured specifications, the
axiom of choice is assumed (in particular, the semantics of 
specifications involving hiding may depend on the axiom of choice).


(ii) default mechanisms for symbol maps

Concerning the last two paragraphs of chapter 5:

A mapping of symbols in $|\Sigma|$ determines the morphism from
$\Sigma$ that extends this mapping with identity maps for all the
remaining symbols...

>>> here, change "symbols" to "names"

... in $|\Sigma|$.  In the case that the signature
morphism does not exist, the enclosing construct is ill-formed.

Given another signature $\Sigma'$, a mapping of symbols in $|\Sigma|$
to symbols in $|\Sigma'|$ determines the unique signature morphism
from $\Sigma$ to $\Sigma'$ that extends the given mapping, and then is
the identity, as far as possible, on common symbols
...

>>> here, change "symbols" to "names"

...  of $\Sigma$ and
$\Sigma'$.  (Mapping an operation or predicate symbol implies mapping
the sorts in the profile consistently.)  In the case that the
signature morphism does not exist or is not unique, the enclosing
construct is ill-formed.


(v) signature unions

In 6.1.3, add after:

When the current local environment is empty, each \Metasub{SP}{i} must
determine a complete signature $\Sigma_i$.  The signature of the union
is obtained by the ordinary union of the $\Sigma_i$ (not their
disjoint union).  Thus all (non-localized) occurrences of a symbol in
the \Metasub{SP}{i} are interpreted uniformly (rather than being regarded
as homonyms for potentially different entities).

the following:

The union specifications in which both a partial
and a total function symbol with the same profile are declared
is undefined.

[BKB: shouldn't this be rejected by static analysis?]

-----------------------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till@informatik.uni-bremen.de           
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------