Re: [CoFI] Comments on CASL v0.99 DRAFT

["Don Sannella" <dts@dcs.ed.ac.uk>]

This is in response to Till's proposal on empty carriers.

[REMINDER: the DEADLINE for comments on v0.99 is TOMORROW! --PDM] 

> Horst Reichel came up with an example specification using empty
> carriers. [...]

[In fact the example is a particularly natural way of specifying the
 datatype of Graphs.  By coincidence, it also appears in the CafeOBJ 
 Report: paths through such graphs are used to illustrate the CafeOBJ
 treatment of partiality.  And in my paper on CASL for CafeOBJ Users
 (already sent to Japan, and to be installed  as a tentative CoFI
 document later today) I've actually included this example when
 showing how nicely one can translate CafeOBJ specifications to CASL...  
--PDM]

> My proposal to include empty carriers is the following:
>  
> We have two kinds of sorts, normal sorts, and
> possibly-empty carrier-sorts. [...]
> The semantics is straightforward: collect all sorts into
> the signature as usual, use possibly-empty-carrier-semantics
> for all sorts, but add an implicit axiom
>       exists x:s.true
> for all normal sorts s. (In the present version of CASL,
> this implicit axiom is there for *all* sorts, destroying
> initial semantics if there are no ground terms.)

Till's proposal seems to be an elegant compromise.

But honestly I think this is a case where we shouldn't compromise: we
should either decide that sorts cannot be empty and then Horst's
example is ruled out, 

[Taking into account also the referees' views on this point, it seems
 to me a bit difficult to motivate "ruling out" the Graphs example.  
--PDM]

or decide that sorts can be empty and then deal
with the well-known problems that this causes.  (I would vote for the
simplest solution, which is what we have now -- no empty sorts -- but
would be satisfied with the other solution too.)  The additional
complication of allowing the user to decide isn't worth the tiny
amount of added flexibility.

[Perhaps the main virtue of Till's proposal is not so much catering
 for flexibility per se, but more that one gets our current version of
 CASL (i.e., forbidding empty sorts) by simply removing the extra
 empty-sort-declaration production.  Looking at in the other way round,
 Till has proposed a simple way of providing an *extension* of CASL to
 cater for empty sorts.  Whether "CASL" should refer to the current
 language or to this extension is mainly a matter of politics...
 (except for those who are writing the "CASL" semantics, of course!)  
--PDM]

Regards, Don