Re: [CoFI] Revised proposal for CASL Views, Imports

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

Didier Bert wrote:
[..]
> -----
> B- On the informal explaination (First part and their consequences in
> the
> rest of the document):
> 
> About the example of generic views:
> 
>   view LISTasELEM [ELEM]: ELEM to LIST[ELEM] = Elem |-> List end
> 
> It should be clear if the source specification (ELEM) is in the scope of
> the parameter. We can interpret the instantiation:
> 
>   view LISTasELEM[view NATasELEM]
> 
> either as a view: NAT to LIST[view NATasELEM] = Nat |-> List
> or:               ELEM to LIST[view NATasELEM] = Elem |-> List
> 
> I guess that it is the second one which is the right interpretation.

You are right, the 0.99 summary was unclear about that, but Peter tried
to remedy this in the additions to section 6.3 in the revised proposal
for CASL views. Please check if the wording is still ambiguous.

> With the same example, the specification expression:
> 
>         LIST[view LISTasELEM[view NATasELEM]]
> 
> contains two instances of the sort "List", which are not distinguished.

Of course, this makes LIST[view LISTasELEM[view NATasELEM]] ill-formed,
because
the result is not a push-out anymore.

> Can we combine view instantiation and renaming? 

No. This is a good example why one would want to have the composition of
views in CASL. 

[there seems to be a serious need here. Shouldn't we introduce it? BKB]

> Must we use compound
> identifiers?

Yes.

> 
> -----
> C- About the discussion (Last part). This comment can be skipped because
> it is not developed in the (pure) CASL framework. However, it
> illustrates
> similarities and differencies between the "named specification"
> approach and the unnamed (CASL) one.

I am not sure whether this has appeared on this list. In Lisbon a design
decision was made to favour referential transparency above the "named
specification" approach. The idea is that it should be possible to
replace a named specification by its definition in a specification
expression without changing the semantics of that expression. 

Consider 

spec NAT = sorts N ...

spec ELEM = sorts E

spec LIST1[ELEM] = sorts list[E] ...

spec LIST2[sorts E] = sorts list[E] ...

view NATasELEM : ELEM -> NAT =  E |-> N

With the named specification approach, LIST1[view NATasELEM] would be
well-formed, because NATasELEM is a view from a specification named ELEM
to a specification named NAT and ELEM is also the formal parameter of
LIST1.

However, LIST2[view NATasELEM] would be ill-formed, because the formal
parameter of LIST2 is not a named-specification and thus cannot match
the source of NATasELEM.

With the approach taken in 0.99, LIST2[view NATasELEM] is still
well-formed.

> 
> Unique view expression vs. unique signature morphism.
> 
> In the framework where named morphisms are defined between named
> specifications, the second mecanism (Till's one) is easily implementable
> because source and target specification names are part of the named
> specification morphism. And we can deal with specification morphisms,
> not
> simply signature morphisms. Semantic checking are confined at some
> particular places. So, in the Andrzej's example, V, V0 and V1 have
> distinct "dependent types", namely:
>         view V : ELEM to NAT
>         view V0: SOME0 to NAT
>         view V1: SOME1 to NAT
> even if they have same source signature and same mapping.
> 
> Moreover, this example is typically a case where we could have the
> following
> possibilities (that occur very often in writing specifications):
> 
> view S0 : ELEM to SOME0 end     -- implicit identity mapping
> view S1 : SOME0 to SOME1 end
> 
> Then:
> view V1 : SOME1 to NAT = ... (as it is)...
> view V0 : SOME0 to NAT = S1;V1 end      -- morphism composition. No need
> view V  : ELEM to NAT = S0;V0 end       -- of semantic checking
>                                         -- if target(S1)= source(V1).
> Now,
> view VL [SOME0] : SOME0 -> LIST[SOME0] = ...
> needs always a view from SOME0 to something to be correctly
> instantiated.
> So, clearly:
>         view VL[view V]  is not okay,
>         view VL[view V0] is okay,
>         view VL[view V1] is not okay (excepted if we introduce again,
> the
>                          implicit view S1 at the right place!).
> 
[see above for need of morphism composition. BKB]

Best regards,
        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/