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 pitty that I haven't been to Lisbon and couldn't
take part in the discussions.

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.

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 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 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.

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/