editorial comments on v.0.96

[Tarlecki <tarlecki@lsv.ens-cachan.fr>]

Then, perhaps just to Peter as the editor of the summary, a bunch of
specific editorial comments which seemed obvious to me.

[I'm forwarding these mainly so that others can see what has already
 been noticed and reported.  I don't expect it to provoke reactions.
 Thanks for your careful reading!  --PDM]

**********************************************************************
Editorial comments
**********************************************************************
i) p.ii, in the middle. The sentence on datatypes does not seem
appropriate anymore, after all the changes to the datatype concept. In
fact it may be removed entirely, since essentially datatypes now do
not introduce anything especially new, they really are just
abbreviations. Alternatively, it might be changed to something like
"Datatype declarations are provided for concise introduction of new
sorts together with some constructors and selectors."?

ii) p.1, 1st sentence: a brief reminder (rather than: an brief...)

iii) p.1 after the itemize: somehow, I do not think that the concept
of a local environment belongs here at all. After all we are talking
here about institution, where it does not occur. This should be moved
somewhere to sect.2 perhaps. Moreover, the explanation now is not
adequate, since with non-linear visibility within basic specs, the
local environment is always the entire signature in fact...

iv) p.2, 1st boldface phrase: CASL (rather than Casl)

[Somehow the small-caps effect disappears in boldface.  But the
 highlighting will be removed in the version to be submitted, so this
 should correct itself. --PDM]

v) p.3, at the bottom: fully-qualified terms, rather than
explicitly-sorted terms (twice), right?

vi) p.7, end of sect.2.2: perhaps add, just for clarity, something
like: "due to the assumption that all carriers are non-empty".

vii) p.8, bold face about "primitive sentences": should be the same
phrase for true and for false.

viii) sect. 2.3.3:

All these well-formedness issues here and in sect.4.2 are actually
quite delicate and not so easy to grasp. It took me while to realise
that you're defining in fact a meta-property of a term being
well-sorted for a specific sort. This later part of the phrase ("for a
sort") disappeared in the later paragraphs in the section. Things are
rather obvious there, I think, but perhaps we should stick to the same
phrase everywhere, or add explicitly "for which sort" the well formed
terms as described there are well-formed...

ix) sect. 2.5.

CONSTANT is no good for ALTERNATIVE: it may expand to a FUN-NAME with
a FUN-TYPE, which makes no sense. If the separation from constructors
with arguments is to be maintained, perhaps FUN-NAME is better here,
but in fact this calls for CONST-NAME.

x) sect. 2.5: there is only one sentence here mentioning constants,
and only for the case where all ALTERNATIVEs are CONSTANTs. There
should be some obvious comment added (e.g., that the clause for
CONSTANTs should in fact be viewed in the same way as a clause for
CONSTRUCT with an empty list of components :-)

xi) p.13, the last line: it does not seem clear what "they" here
are. Perhaps just say "... when the terms are identical up to...".

xii) p.14,in the middle, I would drop "noon-equivalent" into:

"...a well-sorted atomic formula or term may have several
non-equivalent expansions..."

xiii) p. 19, in the middle:

The first SPEC in an EXTENSION gets... (rather than get)

xiv) sect.6.2, p.20:

the clause for GEN-SPECs occurs twice.

xv) p.21, 5th line:

I think "the inclusion morphism" rather than "the identity morphism".
Or was the any reason why inclusions would have to be spelled out?

xvi) Few small comments on sect. 8:

a) SPEC can now be a ARCH-SPEC-NAME. Fine. I can see no special reason
to limit this to the use of names arch specs only, so I think it could
be 

   SPEC ::= ... | ARCH-SPEC

as well. But i guess that this does not really matter in practice.

b) perhaps some more explicit explanation of the use of this
construct, towards the end of the paragraph following it:

"... whereas its use as a SPEC is interpreted as a specification with
the signature and the class of models that consists of all the
possible result units built within the referenced ARCH-SPEC (of
course, in this case the result usint must not be parameterised)."

c) thanks for adding UNIT-DEFNs:

In the sentence after the clause for BASIC-ARCH-SPEC:
"... consists of a list of unit declarations and definitions
UNIT-DECL-DEFN+".

And then at the end of the paragraph after the clause for UNIT-NAME:
"No UNIT-NAME may be introduced..." (rather than "declared" since this
should apply also to unit definitions).

d) the last two sentences of sect. 8.1 seem to suggest a contradictory
interpretation of a UNIT-TYPE. In the first of them I believe you mean
that the result SPEC is viewed as an extension to be added to the
argument specs (as in the GENERIC-SPECs) while the last sentence seems
to impose a requirement which is then always satisfied (given the
restrictions on the ways extensions are formed) which might suggest
that the result SPEC should explicitly contain the specification of
the parameters.

I thought we have agreed ages ago on the first interpretation in the
"extension style", so the last sentence should be removed...

**********************************************************************

Best regards,

Andrzej