Views - a correction

[hubert@mpi-sb.mpg.de]

[Apologies: I have forwarded the previous message from Hubert to the
cofi-semantics just before reading a next message where he introduced
some corrections. So, here is the corrected version. See also some
comments from Peter Mosses in the version forwarded to
cofi-language. --- AT]

[I have taken over moderating of the cofi-semantics list from Don ---
many thanks to him for taking care of this so far --- so AT in the
above stands for Andrzej Tarlecki, tarlecki@mimuw.edu.pl --- AT]

Dear all,

I just checked the new design of views and tried to give it a
semantics, however, I have some problems to understand the intended
semantics of generic views.

Given

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

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

Given an instantiation of a generic view

view VN [FA1] ... [FAn]

how are source and target specifications defined and what is the
symbol map of the resulting view? I would guess that SP' is viewed as
defining a generic specification with parameters the SPi's and as body
Sp'.  The source of the result of the instantiation of a generic view
is SP and the target is SP' instantitated by the FA1 ... FAn,
yielding the following diagram:

   sm'
 +------->SP'[SPa] <--- SPa
 |          ^            ^
 |      fm' |    po      | fm
 |   sm     |            |
 SP -----> SP' <------- SPp

where SPp is the union of the parameters SPi and SPa the union of the
corresponding argument specifications determined by FAi.

However, 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 46 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 to 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.

It is a pitty that I haven't been to Lisbon and couldn't take part in
the discussions.  Maybe someone can summarize the discussions dealing
with views?

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/

------- End of forwarded message -------