Re: [CoFI] Proposal for named morphisms in CASL

[Hubert Baumeister <hubert@mpi-sb.mpg.de>]

Dear all,

the following is a proposal for named morphisms based on my
understanding of Didier's proposal for named morphisms (cf
note L-6). As I understand Didier's proposal, he proposes named
_specification_ morphisms and in particular only named specification
morphisms between _named_ specifications. That is

   VIEW-DEFN ::= view-defn VIEW-NAME VIEW
   VIEW ::= view SPEC-NAME SPEC-NAME SYMB-MAP*

[Right, I'd mistakenly generalized that to allow arbitrary SPECs in my
abstract syntax proposal.  Thanks for clarifying this point!  --PDM]

Applicability of a named specification morphism is determined by
identity of spec names and not by a semantic relationship between
specifications. That is, a named specification morphism can only be
used as a fitting argument if the corresponding formal parameter is a
named specification and its name is the same name as the source of the
fitting morphism. For example, if one has named specifications Nat and
Elem and a named specification morphism NatAsElem with source Elem and
target Nat then given a generic specification List:

   gen-spec List (gen-spec (params [sort Elem]) ...)

the following instantiation would be ill-formed

   gen-spec-inst List (spec-view Nat NatAsElem)

because [sort Elem] is a basic specification and not a named
specification. However, if List is defined as

   gen-spec-defn List (gen-spec (params Elem) ...)

the above instantiation is okay, since the formal parameter is a named
specification with name Elem and that is the name of the source of the
specification morphism NatAsElem.

Then it is sufficient to write "gen-spec-inst List NatAsElem" because
the actual argument is given uniquely as the target of the
specification morphism. Even "gen-spec-inst List Nat" would be okay,
because there is only one named specification morphism in the global
environment with Elem as source and Nat as target.  In case there are
several such morphisms, the instantation would be ill-formed.

A translation

   translation SPEC VIEW-NAME

is well-formed only if SPEC is a SPEC-NAME, the source of VIEW-NAME
has the same name as SPEC-NAME and the signature morphism denoted by
VIEW-NAME is the identity on the current local environment. Then the
semantics is the set of all models of the target specification such
that their reduct w.r.t. VIEW-NAME is the same as SPEC.  Note however
that "translation SPEC VIEW-NAME" is the same as the target of
VIEW-NAME and since the target of VIEW-NAME is already a named
specification one could directly write the corresponding named
specification instead of the translation.

The semantics of "derive SPEC-NAME VIEW-NAME" is similar to translate,
however this time "derive SPEC-NAME VIEW-NAME" is not the same as the
source of VIEW-NAME.

[If "translation SPEC VIEW-NAME" is completely redundant, it should
presumably be omitted from CASL.  How about "derive SPEC-NAME
VIEW-NAME", would there be much use for it in practice?  Are there
methodological grounds for including it?  If not, that would leave us
with just the OBJ-like use of views for instantiations... --PDM]

 From a semantic point of view I see only one problem integrating the
above view in CASL and this has to do with the global symbol map
applying to all fitting arguments in an instantiation. If for one
parameter the fitting morphism is a named morphism I would just ignore
the global fitting morphism for that parameter.

Greetings,
   Hubert

-- 
           Hubert Baumeister
           MPI Informatik, Im Stadtwald, D-66123 Saarbr"ucken, Germany
    Phone: (x49-681)9325-220  Fax: -299
   e-mail: hubert@mpi-sb.mpg.de  
      WWW: http://www.mpi-sb.mpg.de/~hubert/