Re: More comments on 1.0

[Peter Mosses <mosses@csl.sri.com>]

Dear Till,

Just a few queries - all that I've omitted to cite below looks OK to
me: 

> Date: Mon, 12 Oct 1998 16:51:11 +0200 (MET DST)
> ... 
> I have some questions concerning implicit fitting morphisms.
> The current reading in the summary is (end of section 5):
> 
> Given another signature Sigma', a mapping of symbols in
> |Sigma| to symbols in |Sigma'| determines the set of
> all morphisms from Sigma to Sigma' that both extend
> the given mapping, and are identity on common symbols of
> Sigma and Sigma', other than those already in the
> domain of the mapping.  (Mapping an operation or
> predicate symbol implies mapping the sorts in the profile
> consistently.)
> ...
> My second question is:
> Consider
> 
> spec FORMAL = sorts s,t
>  ops f:s, f:t->t
> 
> spec ACTUAL = sorts s,t
>  ops g:s, f:t->t
> 
> Is the fitting map f |-> g illegal?
> I would say yes, because it expands to
> f:s |-> g:s, f:t->t |-> g:t->t, which does not work.
> This assumes that symbol maps get their qualification
> only in dependency of the source signature (otherwise,
> the semantics would be more complicated).
> 
> In any case, f:s |-> g would be o.k.

I see now that v1.0-DRAFT says:

  SYi |-> SY'i denotes the map that takes the symbol SYi to the symbol
  SY'i. The mapped symbols in the list must be distinct. Overloaded
  operation symbols and predicate symbols may be disambiguated by
  explicit qualification; when SYi is not qualified, the effect is that
  all operation or predicate symbols with the same name are mapped
  uniformly to SY'i.

Would you like to propose a wording consistent with your answer to the
above question?

BTW, I think that an analogous comment about overloading should be
added 6.4.1, since hiding or revealing an unqualified overloaded
symbol presumably affects all its qualifications too?

> Date: Thu, 15 Oct 1998 15:12:50 +0200 (MET DST)
> ...
> Unit specifications (8.2)
> -------------------
> The last paragraph on p. 55 explains the use of named unit
> specifications
> for synonym definition. But this is only a very restricted form
> of use - named UNIT-SPECs may also be used in unit declarations,
> for example. The general use should be explained like:
> 
> " A UNIT-SPEC can also be just a SPEC-NAME, referring to a
> unit specification definition in the global environment.
> (Such a reference cannot, however, be distinguished context-freely
> from a unit type without argument specifications. Therefore,
> the abstract syntax contains no extra clause for this case.)"

See my reply to Andrzej's message, concerning reinstating SPEC-NAME in
the abstract grammar.

> Anonymous mixfix operator
> -------------------------
> I suggest to mention that the anonymous mixfix operator
> might/will be reserved for application in the higher-order extension
> (and therefore first-order specifications using it cannot
> be used verbatimly in the higher-order extension).

Perhaps add the following to Sect. 2.3.4.3 Operation Application:

  (The operation symbol `__ __' is allowed, and regarded as an infix,
  although in higher-order extensions of CASL, it is likely to be
  treated differently.)

Perhaps HO-CASL will allow reserved symbols such as `__ __' to be
renamed, even if they can't be declared, so as to use all first-order
specs.

> Editorial comments and typos
> ----------------------------
> ...
> p.7, last paragraph:
> Logically, this paragraph would belong to section 2.3.4.
> I guess that it was placed here in order to stress it as an
> important general point. But I found that it rather abruptly
> starts to talk about terms. What about
> "While well-formedness of terms occurring in sentences of the
> language ..."?

Oops, well-formedness of terms is not even a CASL concept...  
How about:

  While well-formedness of specifications of the language can be checked
  statically, the question of whether the value of a term that occurs in
  a specification is necessarily defined in all models or not may depend
  on the specified axioms (and it is not decidable in general).
  
> p.9, 2.1.1.1
> ...
> Insert a "sort" keyword before the last "sn".

> p.11, line -7
> V1m1 looks a bit funny in my printout (but maybe the paper
> was a bit dirty)

Ok on mine.

> p. 17, 2.2.2 and 2.3
> The last semicolon is optional in both cases.

Explained at the top of page 8.

> p.42, 6.2.1
> Perhaps swap "imports" with "paramemters" because this order
> is also used in the syntax?

I need a decision on whether to revert to the v0.99 order or not!

> ...
> Library names
> -------------
> What is the relation between the LIB-NAME in a LIB-DEFN
> and in a DOWNLOAD-ITEM? The latter specifies a directory
> giving access to the library, while the former seem to be just
> a name for documentation but irrelevant for the semantics.
> If this is correct, the irrelevance for the semantics
> should be explicitly stated.

No, that wasn't the intention, I think.  I'll try to clarify that the
LIB-ID here must be consistent with the actual location of (at least
one mirror of) the library.  It indicates the canonical way to refer
to the library.

> Qualified ids in a symbol map
> -----------------------------
> I am still not sure which abstract syntax tree is associated
> to
>         SP with c:s
> I can see two ASTs. Both have the form
>         renaming SP (symb-map-items implicit (qual-id c t))
> where t is either
>         total-op-type (sorts ()) s
> or
>         pred-type (sorts s)
> What do parser writers say (the Bremen parser is for basic
> specs only, so far).

Let's add SORT as an alternative, cf. SPEC-NAME qua UNIT-SPEC
discussion raised by Andrzej.

> Reserved tokens
> ---------------
> p. C-9
> Is the reservation of {, }, [, and ] really necessary?
> Probably it is necessary for LALR(1) parsers, but what
> about ASF+SDF? It would be nice to have {__} and [__],
> and {, }, [, and ] could be forbidden for parsers not
> supporting mixfix.

I'm not aware of a link between "LALR(1)" and "not supporting mixfix"
since the mixfix analysis is beyond any context-free parser, see my
reply to Frederic.

> Examples
> --------
> The N.B. paragraph on p. E-1 should be deleted or 
> reformulated. We should give examples that are as elegant
> and concise as possible. Each feature of CASL can be
> illustrated by such an example (otherwise, we have designed
> a bad language).

I was intending to do this, but ran out of time...

> Examples for views and arch specs are still missing!

Would someone please supply nice exmaples of views?  I can steal a
couple of arch specs from M-4, I guess.
 
> Editorial comments/typos
> ------------------------
> ...
> p. C-7/C-8
> What is the precedence of TOKEN __ ... __ TOKEN ?

Does it need one?

> p. D-2, 2nd last paragraph
> Why are semantic annotations not displayed?

We'll need to be able to switch between showing or not.  By making the
minimum display the default, it allows minimal formatters that don't
know or care about fancy semantic annotations.

Many many thanks for all your careful bug reports!

-- Peter
_________________________________________________________
Dr. Peter D. Mosses             International Fellow  (*)

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-2200 ! CHANGED
333 Ravenswood Avenue           fax:   +1 (650)  859-2844
Menlo Park, CA 94025, USA       http://www.brics.dk/~pdm/

(*) on leave from DAIMI & BRICS, University of Aarhus, DK
    also affiliated to CS Department, Stanford University
_________________________________________________________