[CoFI] CASL v0.99 - Views

[hubert@mpi-sb.mpg.de]

Dear all,

I just checked the new design of views and I am very much
surprised. It is a pity that I haven't been to Lisbon and couldn't
take part in the discussions.

[Right!  And as I wrote yesterday to cofi-semantics:
 "The syntax and semantics of views are still quite tentative, since the
  changes agreed in Lisbon had an impact on the way that generic views
  had been provided.  (The discussion of the detailed design better be
  on the cofi-language mailing list, I suppose.)"  --PDM]

At the moment I have severe problems to understand from the 0.99
summary how the new generic views are supposed to work and thus
write their semantics.

[I must apologize personally for the vagueness in this revised part of
 the Summary, which indeed reflects some doubt about how the semantics
 should be.  I think the changes to the ordinary views worked out OK -
 now relying on signatures of specs instead of their names - but in
 Lisbon I hadn't realized how much this might complicate having views
 whose targets are generic.  Anyway, this is the essentially the only
 part of CASL v0.99 still open to discussion, and anyone should feel
 free to propose how best to deal with this issue!  Any changes needed
 in the syntax would surely be limited to one or two of the given
 productions for views, and not affect the rest of CASL at all. --PDM]

Given

view VN [SP1] ... [SPn] : SP to SP' = SM 

what is the relationship between SPi (1 <= i <= n) and SP? Is SP
intended to be an extension of the union of the SPi's? Then, I would
guess that the local environment given to SP (but not to Sp'?) is
the union of the SPi's, similar to generics?

What is the result of instantiating a generic view? Given

view VN [FA1] ... [FAn]

what is the resulting view, that is, how are source and target
specifications defined and what is the symbol map? I would guess
that SP (and SP' also?) are viewed a defining a generic specification
with parameters the union of the SPi and as body Sp (SP') and the
source and target of the result of the instantiation of a generic view
are the SP and SP' instantiated by the same fitting morphism? Another
possibility would be that SP' is instantiated by SP instantiated by
the argument. Ie,
                     sm'
SPa ------> SP[SPa] -----> SP'[SP[SPa]]
 ^           ^                 ^
 | fm po     |       po        |
 |           |    sm           |
SPp -------> SP -------------> SP'


However, in both cases, I would expect similar problems to those that
led to the introduction of imports to generic specifications, ie.,
instantiations that should be pushouts are not pushouts.

On page 44 [Sec. 6.3] of the summary it reads:

"Generic parameters in a view definition allow the same view to be
instantiated with different fitting arguments, giving compositions of
the morphism defined by the view with other fitting morphisms."

I would expect here that a fitting morphism defines a translation of
the symbol maps of the generic view. That is, if the symbol map of the
view maps s to s' and the fitting morphism maps s to a then I would
expect as a result a map mapping a to s'. 

On page 46 [Sect. 6.3.2] of the summary it reads:

"Generic views can also be implicitly instantiated: if there is a
unique definition of a generic view VN which for some instantiation
of its parameters is from SP to SP' ... "

This seems to imply that searching for a matching generic view requires 
guessing the appropriate arguments of the generic view?

It seems that the requirement that the reduct of the models of the
target of a view are contained in the source is not needed anymore,
since application of views only depend on the signatures of the
involved specifications and thus checking that the models of the
argument of an instantitation of a generic specification are contained
in the parameter has to be done regardless whether the fitting
argument is a view or not.

Maybe someone can summarize the discussions in Lisbon dealing with views.

[In fact I'm still hoping to find time to send a brief summary of *all*
 the significant changes made since the draft of v0.99, but I may not
 manage it before I leave for a (10-day, net-less) trip early tomorrow.  
 I realize that this must make it difficult to understand the
 motivations for some of the changes - sorry!  --PDM] 

Thanks,
	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/