Re: More comments on 1.0 - compound ids

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

[Bernd: please add a reminder about the imminent deadline for comments
on CASL v1.0-DRAFT! --PDM]
[sorry to be late: the deadline is only a few hours away now!! -BKB]

Till wrote:

> here are some more comments on CASL 1.0 draft.
> 
> Contents
> --------
> - Compound ids versus translation and reduction
> - Institution independence
> - Redeclaration
> - Unit declarations
> - Unit specifications
> - Anonymous mixfix operator
> - Editorial comments and typos
> 
> Greetings,
> Till
> 
> Compound ids versus translation and reduction
> ---------------------------------------------
> The 2nd last paragraph on page 49 reads:
> 
>   Instantiation, however, does preserve subsorts: if in a generic
>   specification we have \Symb{Elem} declared as a subsort of
>   \Symb{Seq[Elem]}, where \Symb{Elem} is a parameter sort,
>   then in the result of instantiation of \Symb{Elem} by \Symb{Nat}, one
>   does get \Symb{Nat} automatically declared as a subsort of
>   \Symb{Seq[Nat]}.  Similarly for translation and reduction.
>  
> The last sentence is new!

I seem to recall that I'd pencilled this in on my print of v0.99 in
response to a comment in some cofi-semantics or private e-mail this
summer - but now I can't locate it... :-(

> It suggests that not only instantiations of generics, but also
> translations and reductions interact with compound ids.
> 
> An argument in favour of this would be that then the semantics
> of institation can be really explained in terms of the
> semantics of renaming, union and extension.

...as it always has been, at least in the Summary!  I guess that this
must have been what led me to add the offending sentence after all.

> The main contra argument is that compound ids are specially
> constructed for instantiations, in order to avoid name clashes
> between two different instantiations of the same generic spec.
> Is it methodologically useful to think of two different translations
> of the same spec, which are then united? Surely, for example
> when we want to get a generic spec with two similar but independent
> parameters. But is a special treatment of compound ids useful in 
> this context?
> 
> Technically, it is not possible to introduce this interaction
> only at the level of interaction with subsorting (i.e. in the above 
> quoted paragraph).  Either, we have to introduce it from scratch (i.e. 
> translation and reduction interacts in the same way with compound
> ids as instantiation, cf. the first paragraph on p. 49), or we 
> have to leave it out entirely.

I was definitely not intending to change the language design on my own
initiative.  Sorry that ithe sentence crept in; I'll remove it again
(unless there is immediate general agreement to keep it...).  But then
I guess the wording at the end of 6.2.2 Specification Instantiation
will have to expanded: to add a caveat, with a reference to 6.5?

Thanks for your careful reading of v1.0, and for all the proposed
amendments so far!

Best regards,

-- 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
_________________________________________________________