Institution independence

[till@Informatik.Uni-Bremen.DE]

Dear semanticists,

concerning the institution-independence of structured
and architectural specifications, I have written a
study note

Institution-independent semantics for CASL-in-the-large

which can be found under URL

   http://www.informatik.uni-bremen.de/~till/inst.ps  (or .ps.gz)

I also will send the note to cofi-semantics, after
I have got some initial reactions.

The purpose of the note is the following (citing Andrzej):
>For structured and architectural specifications, Till is to prepare a
>vocabulary of concepts to be used (mainly to deal with signatures and
>their morphisms: how symbol sets determine subsignatures and how
>symbols maps determine signature morphisms --- this has been already
>partly smuggled into the current summary v.0.99, except for the part
>on compound identifiers).

Andrzej continues:
>These are defined now specifically for the
>institution of CASL. However, they can also be defined in an arbitrary
>institution with identifiers, so that other such institutions might be
>plugged into CASL structuring and architectural mechanisms in the
>future. There should be a separate note presenting the exact
>definition of institutions with identifiers and discussing their use
>in the definition of CASL, with a pointer to this from the semantics
>document.

Actually, the note is a first version of this "separate note".
But as a side-effect, it also defines the abovementioned
vocabulary of concepts.

As I can see, the responsibilty for defining
the CASL instance of this vocabulary of concepts
is Don's and mine's. I would propose that Don just defines 
those notions he needs, and I define the rest.

The responsibility of the writers of the structured
and architectural semantics (i.e. Hubert, Andrzej and me)
is to rely on this vocabulary of concepts only.
The following table, relating the old vocabulary
of concepts in S-6, p.48ff., with the new one, might
help here:

S-6                           New study note
---                           --------------
Signature extension           signature extension
Union of signature with       Target of signature extension
   signature extension
Signature extension morphism  Symbol map
Sub-(signature extension)     Subset (of symbols)
Constructing a signature      Signature morphism from \Sigma
  morphism out of a             induced may symbol map h
  signature extension
  morphism
Union of signature            Union of signature extensions
  extensions
Union of signature            Union of symbol maps
  extension morphisms
Intersection of two           Intersection of two
  signature extensions          sets of symbols
Generation of an              Signature generated by a set
  extension                     of symbols
Translation of a              Extending a signature morphism 
  signature extension           along a signature extension
  along a signature
  extension morphism

In some cases, the replacement is not literally.
For example, signature extension morphisms are not in
one-one-correspondence with symbol maps, but it is more
sensible to work with symbol maps instead of signature
extension morphisms.

Greetings,
Till