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

[Till Mossakowski <till@informatik.uni-bremen.de>]

Didier Bert wrote:

> A- On the modification of the CASL summary (part: PROPOSED CHANGES
> TO THE CASL SUMMARY):
> 
> A.1- The sentence just before 6.3:
>         The instantiation is also undefined whenever the result is
>         not a push-out.
> Have we a characterization which avoid to refer to the "push-out"
> notion?
> I am afraid that the reader is discouraged to write and use any generic
> specification if such conditions are required.

There is a subsection ("Extending a signature morphism along a signature
extension") in the study note S-8 explaining in detail conditions
that imply the instantiation being a pushout. These conditions
are also used in the semantics.
The following is an attempt to reformulate these conditions
in natural language:
 
1. SP' with FM and SP"1 and ... and SP"n 
   (i.e. the extension of the fitting morphism to the body
    and then its union with the actual parameters)
   exists (this is already required in the summary, section 6.2.1)

2. If two symbols are identified by the fitting morphism,
   this must not lead to identifications of compound
   identifiers in the body.
   E.g. if the fitting morphism maps both elem1 and elem2 to nat,
   the body must not contain both list(elem1) and list(elem2).

3. If the actual parameter and the translated body share any symbols,
   these symbols have to be translations of symbols
   from the formal parameter or the import
   (where translation is along the fitting morphism).

Greetings,
Till