Re: [CoFI] Proposal for named morphisms in CASL

[Didier Bert <Didier.Bert@imag.fr>]

   Dear all,

   Here is my comments on the proposal of Peter for the introduction of a
very "basic framework" for named morphisms.

  Many thanks to Hubert who explains very well what is the intended use of
morphisms (views) in my proposal. Views are names for symbol mappings
between named specifications. His example of instantiation with a view
is ok. This replies to the Andrzej's objection (because a morphism is
applied only if the source of the fitting view and the parameter are the
same specification name (or via an injective translation, in my proposal):

AT>I think that the current proposal goes for 2, and least at the
AT>surface.  But then I have a number of semantic doubts: it seems that
AT>it would be logical to check whether the specification morphisms when
AT>used to transform a specification (e.g. as a fitting morphisms, or as
AT>a morphism used in translation) is "semantically applicable", that is,
AT>whether the source or target specification of the morphism is a
AT>(semantic) subspecification of the one we transform. I do not think
AT>that this is the intention here.

  I agree that problems may arise for the determination of the global
fitting arguments when there are several parameters with various kinds of
instantiations (views and explicit/implicit symbol mappings). But I do not
see why it is so different from the combination of several symbol mappings
given from several generic parameters.

  For translation and reduction (source and target), the proposal of L-6
is useless because we deal only with constant morphism. So, the source or
the target of a morphism is always an explicit specification which can be
written down instead. The notion would be useful if unknown morphisms
(variables) were used. The corresponding syntactic rules can be dropped.

Andrzej claimed:

AT>In addition, I do not like (if I understand this at all) the use of a
AT>VIEW as a fitting argument without any actual parameter specification
AT>(which I guess then implicitly is given as the target of the view).
AT>This seems like another, quite different use of the specification
AT>morphism, which to me feels like going against the basic intuitions we
AT>put into CASL.

OK, the actual parameter specification is the target of the view as
usual. So, a view is a fitting argument CONTAINING an actual parameter
specification. Like Peter, I don't understand the last sentence at all.
Be careful in the definition of the views if the target is a generic
specification. In that case, the view is generic too.

At last, I do not see the advantage for declaring symbol maps only.
About the semantics of views, I think that it should be the same as for
fitting morphism of instantiations. We should have a signature morphism
(checking the right symbol correspondence (well-definedness)) together
with verification conditions (correctness).

Abstract syntax :

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

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

  VIEW	           ::=  ...| GEN-VIEW-INST
  GEN-VIEW-INST    ::=  gen-view-inst GEN-VIEW-NAME FITTING-ARG+ SYMB-MAP*

  FITTING-ARG      ::=  fitting-spec SPEC SYMB-MAP*
		     |  fitting-view VIEW

  GEN-VIEW-NAME    ::=  SIMPLE-ID

With respect to generic specifications, a generic view (GEN-VIEW rule)
does not contain the IMPORTS part because all the entities needed for the
view definition are either in PARAMS, or in the first SPEC or in the
second SPEC. I am not sure that the view instantiation must be renamed
after instance, but I let it there for sake of orthogonality with
GEN-SPEC-INST. Obviously the notion FITTING-ARG is common with the
instantiation of specifications. Are you not pleased by the regularity of
the view definitions and specification definitions ?

  I am ready for any kind of reactions (even that of removing the notion
of views!).

Regards
Didier

----------------------------------------------------------------------------
Dr. Didier Bert			   http://www-lsr.imag.fr/users/Didier.Bert/
CNRS, Laboratoire LSR-IMAG	   Tel: 04 76 82 72 16	    +33 476 82 72 16
681, rue de la Passerelle 	   Fax: 04 76 82 72 87	    +33 476 82 72 87
BP 72 
38402 Saint-Martin-d'Heres CEDEX, France
----------------------------------------------------------------------------