Re: comments on v.0.96 [300 lines]

[pdmosses@brics.dk]

This message consists entirely of Peter's own reactions to Andrzej's
more serious comments.

[But I'm not sure whether Peter's reactions are as a language design
task group participant, or as editor of the language summary... --PDM]

> **********************************************************************
> More serious comments
> **********************************************************************
> 1. p. 6, just before sect. 2.1.1:
> 
> We permit overloading of identifiers across various kinds of entities:
> fine. But what about variables, which are not mentioned here?
> Overloading variables and constants might lead to strange ambiguities
> in the syntax of terms, so maybe they should be kept separate.

If parsing is context-free, one (presumably) can't see any difference
between constants and variables, they are just IDs.

If parsing is context-sensitive, one can see whether an ID is a
(possibly-overloaded) constant or a (non-overloaded) variable; if both
are allowed by the context, the enclosing atomic formula is surely
illegal in any case.

Please give an example of a "strange ambiguity" - I don't see the problem.  

> 2. sect. 2.1.2 and elsewhere.
> 
> I must admit, i do not like too much the changes related to the
> introduction of constants as separate things. I think that what was
> here before, forcing the application of a zero-ary function to the
> empty list of arguments, was okay and was quite readable (and any
> potential inconveniences might be resolved at the level of a concrete
> syntax then). Moreover, this was quite uniform throughout the
> language, and everything (e.g. partiality) was nicely symmetric.

Agreed!

> Okay: I also buy some of Bernd's arguments about the
> possible future interaction with a higher-order extension.

This was the ONLY reason that I switched style i v0.96: I couldn't see
how to give a smooth extension of the AS from CASL to HO-CASL with
v0.95 AS.

> However, if constants are to be treated separately in the language,
> differently than functions, then I think we should do this
> systematically throughout the entire formalism in a "proper" way.
> Otherwise we loose some sense of uniformity of the language.

Agreed.  Although one might also argue that constants have just as
much right to be uniform with variables as with functions, perhaps?

> For instance:
>  ... etc, etc, etc ...
> (Peter: please let me know if you really want me to write all this in
> detail --- maybe I would withdraw this comment then :-)
> 
> Can we please consider going back to what was there before, with
> constants as a special case of functions?
> 
> I think Michel shares the feeling, anybody else?

Andrzej, please talk with Bernd about this, and let me know if you can
agree on a compromise.  I'll look again at the possiblity of extending
to HO from the old-style treatment of constants (over the weekend).
I need to resolve this issue by Monday if I'm to have a chance of
producing v0.97 on schedule.

> 3) sect. 2.5, last sentence:
> 
> In the case of open datatypes, it makes little sense to presume that a
> selector is total if there is only one clause in a datatype
> declaration --- after all, further constructors may be added later,
> and moreover, there may be values of a datatype which are not built
> using any constructor at all...

Agreed!

> 4) sect.2.6:
> 
> As it is now: ATTRIBUTIONs are treated just as certain abbreviations
> for axioms -- and I like this. However, as far as i can see, there is
> then no decent way to allow them to influence the possible syntax of
> terms: stating that a binary "plus" is associative does not introduce
> to the abstract syntax legal applications like "application plus
> TERM+" (with arbitrarily long list of argument terms). If the
> intention was to allow such syntactic consequences to be drawn, then I
> believe attributions would have to be attached directly to function
> declarations.

You seem to be suggesting that properties such as associativity should
be incorporated in signatures, attached to the function symbols
somehow.  This would be an unwelcome complication, IMHO.

But I could imagine (context-sensitive) parsers exploiting an
attribution of associativity for "+" to justify disregarding the
harmless ambiguity in "a+b+c", mapping to some particular binary
abstract syntax tree.  Then there is surely no need for attaching the
attribution to the function declaration.

One final point, which I'll amplify in a later message: it might be
convenient (again, just for conciseness) to allow PROPERTY* also as a
component of a FUN-DECL, as in OBJ3.

> 5) sect.4.1, p. 13:
> 
> It is stated here that an embedding declaration cannot lead to
> implicit (other than imposed by ISO-DECLs) cycles in the sort
> ordering. I believe that in Paris/Lille we were discussing a stronger
> requirement: that in no context a new cycle can appear, except for an
> explicit declaration in ISO-DECL. I do not think this is ever
> mentioned now in the summary.
> 
> However, I think now that perhaps this was a suggestion which goes a
> bit contrary to the overall language design. If I recall right, the
> only reason for this was that "if a new cycle is introduced
> implicitly then this is probably an error". In other similar cases
> (e.g. name clashes, notably in instantiations of generic specs) we
> have taken the opposite view: "okay, this might have been an error, so
> perhaps a tool should warn the user, but since this makes perfect
> semantic sense, we do not throw this out as a possibility for the
> user".
> 
> Perhaps the similar philosophy should be applied here, and we should
> allow cycles to be introduced by language constructs?

Should we then eliminate ISO-DECL altogether?

> 6) This is more a question to the subsorting group than a comment: do
> we have a decent "type-checking" algorithm to type terms and formulae
> and check if they are well-formed? (sorry if this was written
> somewhere and I missed this among the tones of CoFI material).

A paper including this has been written, but not released yet.  It
works on AS trees, adding qualifications where missing.  I don't know
whether it can be combined with parsing.  [Till? --PDM]

> 7) sect. 6.1.1.
> 
> I must say that again, i do not like the simplification of the
> abstract syntax for SYMB-MAP, which now pushed some of the
> requirements previously given in the grammar in a context free way
> (that things of the same categories are mapped to the things of the
> same category) to the semantics (context checking...).

Here, I support Bernd's view: the impact on Semantics is relatively
minor, and we shouldn't complicate the AS unduly.  Also, I'd like
SYMB-MAP and NAME-MAP to be analogous in the AS, for uniformity, but
NAME now has so many sub-categories, following your own suggestion... 

> Also, this introduces here some questions about what happens when a
> symbol overloaded between various categories (say, identifier that is
> both a function and a sort) is used? Do we need a way to indicate that
> an identifier is used as a sort, or is it implicit in the abstract
> syntax already?

FUN-SYMB and PRED-SYMB are definitely distinguished from SORT in the AS.

> 8) sect. 6.1.2.
> 
> EXTENSIONs should have at least two SPECs in the chain, right?
> 
> In fact, since the role of the first SPEC is different (at least
> w.r.t. CONSERVATISM), we should perhaps separate it out, so:
> 
>    EXTENSION ::= extension SPEC CONSERVATISM? SPEC+

I suppose we could, for better suggestiveness, and to allow the
Summary to refer more easily to the "first SPEC".

> Aha: just above: maybe we should require that there are at least two
> SPECs in a union (just as we did for some reason --- mysterious to me
> --- for disjunctions and conjunctions).

I don't see the reason for such restrictions either: it doesn't hurt
for the AS to allow a few extra things (unless we require the concrete
syntax to map ONTO the AS, of course!) if their semantics is uniform.

> 9) p.20, sect. 6.2:
> 
> Just a tiny complaint: we have removed multiple SPECs as things to be
> extended in EXTENSIONs, but we have retained this possibility for
> generic specs. This is a bit un-uniform: I think I understand the
> reason for the latter, without fully appreciating the reason for the
> former.

The reason for the latter is purely allowing for positional notation
in instantiations - otherwise, the generic parameters could simply be
a single union, and the argument spec could be fitted directly to it.
(I'd prefer this, but my impression was that others were very much
attached to positional notation...)

The removal from EXTENSION was because there, one can always write the
list of specs to be extended as a UNION.  Perhaps it would be nicer to
take

   EXTENSION ::= extension SPEC+ CONSERVATISM? SPEC+

for uniformity with generics?  Do we have implicit union other places?
- ah yes, in UNIT-TYPEs.  OK.

> Anyway: one nice side-effect is that conservatism is now always
> required uniformly on all the extended SPECs. A nice semantic
> consequence of this is that in the cases when an instantiation of
> generic specs leads to a pushout signature (no unintended name clashes
> between the body and the actual parameter) then both persistency and
> freeness of the body over the formal parameter are preserved (I think).

That's a nice surprise!

> 10) p.27, sect.9, 2nd paragraph:
> 
> I'm afraid this is not "quite true": if my understanding of things is
> correct, we do not have referential transparency now (see trivial
> examples below).
> 
> The point is that, as rightly explained in sect.6.2, p.20, just after
> the first group of clauses, naming a specification is a semantically
> meaningful operation, which fixes the "local environment" for the
> specification expression to be empty. Consequently, the structure of
> the expression is not "visible" anymore.
> 
> Overall though I do not think that this is so terrible, and we can
> live with this --- just dropping this paragraph...

OK, point taken.

> 11) I am running out of steam, 

Good!  

(I don't really mean that, of course, but it's been a tough day...)

> so the last one will be sketchy :-)
> 
> can somebody re-raise the issue of linear vs. non-linear visibility of
> declarations within lists of basic item, please...

I'll be drafting the Rationale (probably FOR non-linearity) this weekend...

> If the proposal from my earlier message would be accepted, and
> consequently type-declaration groups would be back, 

The same goes for my new proposal for a SORT-GEN, I guess.

> then any real need
> for non-linear visibility would disappear. As far as I can see, in all
> other cases we can (and in my view, we should) write basic specs so
> that linear visibility is maintained.

What is the motivation for linear visibility: methodology, semantics,
tools, other languages, ...?

> And a related issue: once linear visibility would be restored then
> perhaps we could go back to the idea of local declarations (SIG-DECLs)
> within basic specs only, rather than locality introduced only at the
> level of structured specs?

By putting them in at the BASIC-GROUP level, we could also avoid
nesting them.

But I really don't see much advantage to

  basic-spec ... (local-decls ... in ...) ...

over

  extension (basic-spec ...) (local-spec ... in ...) (basic-spec ...)

assuming sensible concrete syntax, of course.

> That's all, more than enough I'm afraid: apologies for too much of
> text and for reviving some of the issues again, but 

No need to apologize!  Thanks enormously for the considerable time and
effort that you have found for this (not only) while in Paris...

> I just want to be sure I like what we submit to WG1.3...

Me too (referring to what I like, not what you like, of course :-)

Cheers

Peter