Instantiation of Generics and Well-formedness

[Hubert Baumeister <hubert@mpi-sb.mpg.de>]

Dear all,

At present the semantics of instantiation of generics is defined 
even if for some actual parameter models their reduct to the 
formal parameter signature is not a model of the formal 
parameter. 

The reason, as far as I understood, is that it should be easy to 
check well-formedness of instantiation, i.e., well-formedness in 
general, and that checking that the actual parameter is included 
in the formal parameter is undecidable in general and thus should 
not be used in the definition of well-formedness.

While I agree that well-formedness should be decidable, I 
disagree that well-formedness always implies the definedness of a 
construct.

I would compare this to the situation in programming languages. I 
would consider a program accepted by a compiler a well-formed 
program. However, such a program can still produce a run-time 
error, meaning it has no "model-semantics". Checking if a program 
creates a runtime error is undecidable.

I think that with the separation of static- and model semantics 
in CASL, we have a similar distinction between "compile"-time and 
"run"-time.
 
My suggestion would be to have well-formedness refer to 
definedness of the static semantics, while definedness of the 
model semantics is separated. 

In the case of instantiation I would write that instantiation is 
well-formed if the fitting arguments extend to a signature 
morphism from the union of the formal parameter specifications to 
the union of the actual parameter specifications and that the 
semantics of instantiation is defined if the models of the actual 
parameter models are also models of the formal parameter and undefined
if not. 

I think in CASL 0.97 we have a similar situation with terms. A 
well-formed term may be undefined.

 From a methodological point of view a formal parameter can be 
viewed as a typing constraint and then I would expect that the 
semantics is undefined if the typing is not satisfied. Otherwise 
one is forced to think about the semantical consequences if the 
actual parameter does not satisfy the formal parameter 
specification. (Is it always inconsistent?) 

Also, a user might deliberate write specifications to take 
advantage of this semantics.

Though we might expect that tool writers warn the user about such 
situations or generate proof obligations, our intend to have the 
tool writers do this is in my view best reflected if the 
semantics is undefined in the problematic cases. 

Following a similar line, I would argue that the semantics of a 
conservative extension is undefined if the extension is not 
conservative wrt. the current local environment and not the 
empty class of models as it is currently. 

I am willing to write a note of dissent about this, if I find 
someone who supports my view :-)  

This is from http://www.brics.dk/Projects/CoFI/Documents/CASL/Dissent/:

>For each separate topic of dissent, a CoFI Note of Dissent on Language Design should be provided, with the
>following contents: 
>[..]
>   - the names of some participants (at least two) who support this view; 
>[..]

Regards,   
	Hubert

- -- 
           Hubert Baumeister
           MPI Informatik, Im Stadtwald, D-66123 Saarbr"ucken, Germany
    Phone: (x49-681)9325-220  Fax: -299
   e-mail: hubert@mpi-sb.mpg.de  
      WWW: http://www.mpi-sb.mpg.de/~hubert/