[CoFI] Re: question

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

Dear All,

In answer to the following question:

>> I have a question concerning CASL. In Section 6.5, page 48, there is 
>> the following statement:
>> 
>> "If there are two compound sorts with multiple components, and the 
>> number of components are the same, and each pair of corresponding 
>> components either consist of two identical IDs or of two sorts in
>> the subsort relationship, then there is also a subsort embedding 
>> between the compound sorts."
>> 
>> Let us now assume that we have a generic specification corresponding 
>> to the Pascal-like array type and we produce two compound sorts 
>> ARRAY(FromOneToTen, Nat) and ARRAY(FromOneToTwenty, Nat). Evidenty, 
>> we can easily specify that the sort FromOneToTen is a subsort of 
>> FromOneToTwenty. However, we cannot state for Pascal-like arrays that 
>> ARRAY(FromOneToTen, Nat) is a subsort of ARRAY(FromOneToTwenty, Nat). 
>> How do you handle this problem?
>> 

I am afraid that this issue has been overlooked so far. Indeed, I would
claim that it is much more sensible (and consistent with the rest of the
design of CASL) to never deduce anything from compound ids.
It has been argued (and adopted) by Andrzej and myself, and
independently
by Hubert if I remember correctly, that signature morphisms should not
interact with compound ids (i.e., a renaming of Nat into Num will not
entail a renaming of List[Nat] into List[Num]) ***but*** for the special
case of fitting morphims.

My claim is that the same decision should have been made w.r.t.
subsorting
relations. Of course, it is nice to deduce from Nat < Int that 
List[Nat] < List[Int]. But this may as well lead to unwanted results, as
pointed out by Zamulin.

My proposal would be to simplify CASL w.r.t. this issue, and just decide
that compound id do not interact w.r.t. subsorting relations (again,
***but*** for the special case of fitting morphism). Thus:
a) Nat < Int will not entail List[Nat] < List[Num], but the latter can
of
course be explicitly specified by the user.
b) If in one generic spec we have Elem < List[Elem], and fit Elem to
Nat,
then we have in the resulting spec Nat < List[Nat].

I believe the above suggested modification is easily implementable both
in
the summary and in the semantics.

Best regards,
Michel
-- 
Michel Bidoit
Laboratoire Specification et Verification       Tel:  +33 (0)1 47 40 28
68
CNRS URA 2236                                   Secr: +33 (0)1 47 40 24
04
Ecole Normale Superieure de Cachan              Fax:  +33 (0)1 47 40 24
64
61, Avenue du President Wilson          
94235 CACHAN Cedex France                Email:
Michel.Bidoit@lsv.ens-cachan.fr