Spec <--> Basic-Item*

[cerioli@disi.unige.it (Maura Cerioli)]

Since this Monday (at least in the morning) our local network will be
disconnected from the word (black-out in Genoa, the rest of the world
isolated! ;-), I decided to send my comments on the Part I before reading
the Part II, to be sure that I was to send through at least a part of my
comments.
This has caused the misunderstanding on the unability of expressing
local-declarations to axioms.
For this I'm sorry.

However, I thought that in Paris we decided
1) specs were going to be self contained
2) extensions were going to involve the spec to be extended and a basic-item
   list as extending elements
3) generic specs body were going to have two parts: a list of basic items
   and a (self-contained) spec and their semantics was roughly speaking
   the extension of the union of the spec with the parameters by the
   list of basic items.
Thus, I assumed that this would have been implemented and didn't think to
check that some construct in the "structured spec" could be used somehow to
generate a different kind of formulae, belonging imho in the "basic" part.

I'm not sure that I'm correctly remembering the "last" decision, as on
Sunday morning we were switching decisions at a quite high speed.

But I think that Michel said something about having always assumed in his
intuition that specs were closed (and hence that he was happy to have them
in such a way) and Bernd was doubtful that such form of generic specs was
sufficient.

[Your recollections of the Paris meeting, and of Bernd and Michel's views,
appear to be accurate.  But you should have come to Lille: the speed of
decision-switching there would have impressed you even more!  :-(  --PDM]

I think that having specs as self-contained objects would both simplify the
semantics (avoiding to have the local environments around)

[The semantics for v0.95 in Note S-4 deals with such open specs; it seems
that eliminating them would not lead to a significant simplification.
--PDM]

and help in writing/reading specs.

[In practice, a SPEC is almost always structured as an extension of some
named specifications (BOOL, NAT) so one has to take a local environment
into account when writing/reading the extending part anyway. --PDM]

If the only reason to have "open" specifications is to write the body of
generics, I would reconsider the design of the generic specs.

[It appears that the situation is not so simple.  Some of us had intense
discussions in Lille (and afterwards) about the methodological aspects of
persistent extension, where the simple form of extension that you mention
above does NOT behave so nicely - the problem being essentially that
  extension (extension persistent SP1 by BIT1) by BIT2
does not ensure that models of SP1 are protected in the result.  Perhaps
you don't regard that as a problem, but those who make `light-weight' use
of extension (when presenting in several steps extensions that you might
prefer to write as a single list of basic items) would surely find it
problematic.  This motivated the new syntax for EXTENSION in v0.96.  I see
that the comment in the CASL Rationale on this point is misleading, it's
not entirely a matter of `convenience'; I'll try and amplify on it in the
next version.  --PDM]

Indeed, it seems to me, that either there is a clear pattern for the body
of a generic spec satisfied from most examples (like extends
(parameters+fixed part) by...), or it's better to have a "standard" (say
lambda-calculus) approach.

[There is no time left to reach agreement on a major change to the
treatment of generics before the submission of the CASL design to IFIP WG
1.3.  The current design appears to be consistent, and it (mostly) already
has a formal semantics. Clearly, the treatment of generics is a point where
opinions in the Language Design group are somewhat divergent - as we know
from many previous meetings and messages...

However, it would surely help IFIP WG 1.3 in assessing the treatment of
generics in the submitted CASL design, if you could give a concise summary
of the case for the lambda-calculus approach to generics - condensing the
previous messages on this point by you and others, and relating the
discussion explicitly to the submitted design.  If the summary is longer
than about 200 lines, please format it in LaTeX, so that I can install it
as a Note; otherwise, just send it directly to cofi-language.  If you could
find time to do it straight away, that would be ideal, as we should give
the IFIP WG 1.3 members as much time as possible to assess all aspects of
the submitted design.  --PDM]

If the former hypothesis is correct, then we can have all the parts of the
"standard" expression forming the body.

[From Bernd's messages on this topic, this appears not to be the case. --PDM]

Otherwise, I don't think appropriate to complicate the semantics and the
presentation of both specs and generic specs, apparently for the sake of
restricting the expressive power of our language.

[My understanding is that keeping to the simple form of extension that you
propose would also be a significant restriction on the expressive power of
the language.  And personally, I prefer the current treatment of generics -
although as Summary Editor, I will of course have to write whatever
reflects the general consensus of the Language Design task group.  --PDM]

Maura

[Sorry, my comments ended up almost as long as Maura's message!  --PDM]