[CoFI] Basic specs in CASL 0.98 (FUN-DEFN, COMPONENT)

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

2.1.2, last sentence: In a FUN-DEFN for a total function, all the
function symbols used in the definition are required to be total too.

This seems unnecessarily restrictive.  One might write
  total id(x) = pred(succ(x))
and not want to be forced to declare subsorts etc. required to make
pred into a total function.  Also, there are one or two places where
we regard known total functions as partial -- e.g. in
  datatype t = construct of (select:int)
select:int->t is regarded as partial even though it is total (because
there is just one constructor).  So the restriction might well be
very annoying sometimes.

Given other design decisions, I think it would be more natural if a
total FUN-DEFN would be just like a partial FUN-DEFN with the sole
difference that the defined function is required to be total.  If
there is no such total function, then there are no models.

2.1.4, COMPONENT: This has changed to allow several selector functions
with the same result to be specified together.  (See appendix D,
points for discussion.)  This allows one to write e.g.
  datatype rational = fraction of (numerator,denominator):int
rather than
  datatype rational = fraction of (numerator:int,denominator:int)

[The current proposal for concrete syntax for the latter is actually:
   sorts rational = fraction(numerator:int,denominator:int)
--PDM]

I can live with this, and I see the motivation, which is (I think)
more for uniformity with e.g. VAR-DECL, ARG-DECL and FUN-DECL than
the need to pack still more into datatype declarations.  

[Right.  In fact the non-uniformity was shown up during the concrete
 syntax design: in those other contexts, one allows a comma-separated
 list of names followed by a single type, e.g. 
   operators rem(m,n:int):?int = abs(m-(n*div(m,n)));
   variables x,y:nat; z:int;
 The idea is now to abbreviate selectors in the same way, e.g.
   sorts rational = fraction(numerator,denominator:int)
 using a semicolon to separate COMPONENTs, e.g.
   sorts list = empty | cons(head:elem;tail:list)
 also when there are no selectors, e.g.
   sorts list = empty | cons(elem;list)
--PDM]

I would just like to note that datatypes are already by far the most
complicated construct in basic specs, at least if one looks at the
semantics, and this makes them a little more complicated.

[I must admit that I was unsure of whether to include this in v0.98 or
 not, since the burden of writing the same sort for several selectors
 is rather slight.   BTW, LSL apparently allows the abbreviated form in
 tuples - although using commas rather than semicolons.  But if there
 is no support for this change, we should simply revert to the v0.97
 abstract syntax for COMPONENT. --PDM] 

Regards,
Don Sannella