Comments on CASL 1.0 draft

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

Dear Peter,

thank for for all the efforts towards the long-awaited 1.0!

Here are my (first) comments to 1.0-draft:

4.1.2.1 (Free datatypes with subsorts)
--------------------------------------
I suggest to replace 

"Finally, a free datatype must be conservative with
respect to the overloading relations. ..."
(until the end of the paragraph)

with

  Finally, the constructors of a free datatype must neither be
  in the overloading relation with each other nor with functions
  in the local environment. In particular, this condition is fulfilled 
  if the operation names introduced by the free datatype construct 
  are new and distinct from each other.

The reason is the following:
I tried to avoid the introduction of any axioms by free types
in order to have the absolute free semantics. But this is too strict.
It is no problem to introduce axioms over the signature of the
local environment. This is because the semantics of structured free
specs is the restriction to those models which are free over their
own reduct (to the signature of the local environment).
Thus, imposing axiom over the signature of the local environment
within a free type has the same effect as imposing them directly
on the local environment. This also means that we can drop the
restriction that free types must not lead to new overloading 
relation between functions from the local environment.
(cf. my mail from 30 Aug)

End of section 6.2.2, instantiation as push-out
-----------------------------------------------
I suggest to replace (or at least explain) the condition
that the instantiation must be a push-out by the following
two conditions:

   If 
                { SP' with FM }             (the translated body)
   and 
                SP'_1 and ... and SP'_n     (the actual paramemter)
   share any symbols, these symbols have to be translations (along FM) 
   of symbols that share in the extension of the imports by the generic
   parameters
                {SP''_1 and... and SP''_m} then {SP_1 and ... and SP_n}.
   Here, two sorts share if they are identical, and two
   function or predicate symbols share if they are in the
   overloading relation.

   Compound identifiers must not be identified through the
identification
   of components by the fitting morphism. E.g. if the body of a generic 
   specification contains both list(elem1) and list(elem2), the fitting
   morphism must not map both elem1 and elem2 to nat.

The latter condition of course should appear in the section
about compound identifiers.
Together, the two conditions are equivalent to the pushout property.
at least for the CASL institution. I am not sure if I manage
to extend the notion of institution by an abstract form of overloading
relations in order to give an institution-independent semantics to
the above explanations. In any case, the institution-
independent semantics can always be the pushout property.


Greetings,
Till