final comments on v0.96

[Till Mossakowski <till@informatik.uni-bremen.de>]

[Thanks to all those who have commented on CASL v0.96.  I am now
trying to finalize the abstract syntax for v0.97, based on the
comments that I have received.  I hope to send a draft of the revised
grammar to this list later today, in the hope that any remaining
infelicities might be noticed in time...  --PDM]

Dear friends,

concerning the

Treatment of constants and functions in CASL
--------------------------------------------
I fully agree with Don's proposal for the higher-order extension:

>  b ::= bool | int | ...
>  t ::= b | t1*...*tn | t -> t' | t -p-> t' | pred(t)
>  decl ::= id:t

but not with his conclusion that there are no problems
with the extension of V0.95 to this.
Namely, it would be nice to have product types already
in the first-order fragment, instead of having special
function spaces with n argument sorts, which have
no *direct* counterpart in the above proposal.

Thus, for the first-order fragment, I would propose something like:

DECL  ::= decl NAME TYPE
TYPE  ::=   TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE 
TOTAL-FUN-TYPE    ::= total-fun-type PRODUCT-TYPE SORT
PARTIAL-FUN-TYPE  ::= partial-fun-type PRODUCT-TYPE SORT
PRODUCT-TYPE      ::= product-type SORT*

>[This change seems quite innocuous.  How about APPLICATION, should we
>replace TERM* by TERMS there?  --PDM]

Yes, I would call it something like PRODUCT-TERM indeed, because
there has to be a tupling constructor from TERM* to PRODUCT-TERM
in the higher-order extension, but now
it plays a role only at the application position.

Say:

APPLICATION   ::= application FUN-SYMB PRODUCT-TERM
PRODUCT-TERM  ::= product-term TERM*

[OK, but I'd prefer to use SORTS and TERMS as non-terminals, to avoid
people getting the impression that CASL has already gone HO... --PDM]

>With Maura's removal of total/partial distinctions from TYPE we might take:
>
>        CONST-DECL  ::=  const-decl NAME FUN-TYPE TOTALITY
>        FUN-TYPE    ::=  fun-type SORT* SORT
>        TOTALITY    ::=  total | partial
>
>and the generalization to HO-CASL could be by adding to the above:
>
>        CONST-DECL  ::=  ... | const-decl NAME TYPE TOTALITY
>        TYPE        ::= BASIC-TYPE | FUN-TYPE
>        BASIC-TYPE  ::= basic-type SORT
>        FUN-TYPE    ::= ... | fun-type TYPE* TYPE
>
>where with order-sorted abstract syntax the first-order case is still
>there as subsorts.  --PDM]

This does not work!
How do we epxress, written in Don's notation, 
f: (t-p->t')->t'' ?
Only in the first-order case we can globalize the TOTALITY,
but this is not compatible with the higher-order extension.

[Ah, I guess you want to regard t->t' as a subtype of t-p->t',
treating it properly when type-checking terms?  OK, the the
total/partial distinction does need building into the TYPE.  --PDM]


Compound ids and subsorting
---------------------------
>The anomaly mainly was in the example
>
>spec LIST (ELEM) =
>sorts Empty < Stack(Elem)
>...
>
>Then, we would have both Empty < Stack(Int) and Empty < Stack(Bool),
>which makes the axiom D(Empty) ill-formed.
>But of course this example can be repaired by making Empty into
>a compound sort, too.
>
>[Presumably you mean D(empty), where empty:Empty.  I must admit that I
>find it a bit disconcerting that D(empty) is ill-formed, and cannot be
>easily disambiguated...  One could make Stack(Elem) < Stack, I
>suppose, which would ensure that all stack functions were in the
>overloading relation - isn't there an easier way?  --PDM]

Sorry, I have to distinguish between the following two:

spec LIST1 (ELEM) = 
sorts Empty(Elem) < Stack(Elem)
opns empty:Empty(Elem)
...

spec LIST2 (ELEM) = 
sorts Empty < Stack(Elem)
opns empty:Empty
...

Now in LIST1 there is the peculiarity that within
LIST(NAT) + LIST(BOOL), D(empty) is ambigous, but it may
be disambiguated by taking either D(empty:Empty(nat))
or D(empty:Empty(bool)).

In LIST2, the empty lists for all instantiations are collapsed
into one element. And empty denotes this single element,
so D(empty) is *not* ambiguous.

[Fine, that is what I was hoping for!  --PDM]

Historical remark:
I used examples like the above in an argument against the
introduction of compound ids, in favour of waiting for
a truely polymorphic extension, where problems as above
do not occur.
But all this has nothing special to do with the interaction
of compound ids and subsorting.

So altogether I see no severe problem at all.


Greetings,
Till