More on the Basic Datatypes

[till@informatik.uni-bremen.de]

Dear Peter,

thanks for your comments on our specification of the natural numbers.

After having thought about the points you have made, we have decided
to propose the following:

- The natural numbers (and also integers and rationals) will be
  specified in a very simple, easily readable way. Even if this
  does not follow an optimal exploitation of structure in all cases,
  you have convinced us that readability is essential here.
  The new specification Nat can be obtained unter
  
  http://www.informatik.uni-bremen.de/cofi/CASL/lib/BD_Discussion.html

  Note that Nat is now entirely self-contained, and PreNat (and
  together with it the library PreNumbers) has vanished.
  The reason is that numbers and algebra are no longer specified
  in an interleaved way.

- The simple and structured datatypes, machine numbers and
  number representations remain structured as they are. Compared to our
  original numbers (which have used a deliberate interleaving between
  numbers and algebra), they are of a different nature.
  In particular, we believe that the structuring is very natural
  here (e.g. List[Elem]) and thus can and should be shown
  to the general audience.

- Therefore, "documentation views" are a useful supplement in any case
  (and we are going to include the signatures plus some text as
  important and useful explanation of the specifications),
  but they should not replace the original specifications.
  For demonstrational purposes, we have also put the flattened
  version of our older Nat specification under the above URL,
  and we think that they are not presentable as "standalone".

- The RelationsAndOrders and algebra libraries will be simplified
  in the following way: all the Ext-versions of the specifications
  (they contain derived operations for the respective algebraic
  structure) are moved towards the end. This makes the first part
  of these libraries more readable, while the second part can be
  skipped at first reading. Moreover, besides the (paramtererized)
  Ext-versions of the specifications, there are also non-parameterized
  versions ("Rich-xxx"), which are easily obtained from the Ext-versions.

We believe that in this way, the basic datatypes become simple enough
to be usable for the non-specialist.

We would like the readers of this list to comment on this proposal
until

        *** February 17th ***

since we are afterwards going to produce a new (hopefully nearly final)
version of the basic datatypes.

> DETAILS
> 
> > In accordance with the suggestions made in Berlin,
> >
> > -> the only sorts are now Nat and Pos
> > -> partial functions are not totalized by subsorting any more.
> 
> Is the latter simplification essential?  Perhaps the provision of the
> totalized functions might be useful for standardizing the interfaces
> to CASL libraries from sub-languages?

No, it is not essential.
The objection raised in Berlin was that there should not be too many 
overloaded profiles, and that subsorts should be used only as an 
auxiliary device. Hence, in the new specifications, subsorting generally 
plays a less prominent role (e.g. the generation of Nat does not involve 
subsorts - this also leads to easier induction principles).


> > II. The Signature of Nat
> > ========================
> >
> > Sorts and subsorts:
> >
> > Nat >= Nat,Pos
> > Pos >= Pos
> 
> It may be less confusing to present the above lines using CASL syntax.

We have adjusted the CATS output now to be in accordance with the CASL syntax.

> In the present version of Note L-12, the specs for Relations and
> Orders, PreNumbers, Algebra_I, and Numbers are found in separate
> libraries.  Hypertext presentations of the libraries would allow
> users to go directly to referenced specs, but it might still be
> preferable to show users everything involved in the Nat spec in a
> single library (as the whole specification text referenced above
> indeed does itself).

Nat is now self-contained.


> > (In fact, unlike in the case of libraries for programming
> > languages, there is not much of a point in writing separate interface
> > definitions for specification libraries, since these would not really
> > look very different from the specifications themselves. [...].)
>
> I don't agree with the last sentence above.  While writing a library
> that uses natural numbers, I'd reference the Nat spec, and bear the
> exact signature in mind - but I probably wouldn't want to even look at
> the axioms of Nat unless I was in doubt about the details of some
> particular operation or predicate.  (Similarly for a generic spec: I'd
> want to see any axioms that the parameter spec might have, but
> probably not those specified in the body.)  I found the signature
> listed under II above to be very helpful (read: essential) to get a
> real overview of the Nat spec - if it hadn't been provided, I'd have
> had to construct it for myself.  I trust the authors to get the axioms
> right!
> 
> A related point is that the development of further libraries may
> suggest changes in the modular structure of the present libraries -
> but such changes shouldn't affect the normal use of the present
> libraries.

Agreed. Thus we suggest to include, besides the original specifications,
also the signatures of specifications together with some explanatory 
text as part of the publication of the basic datatypes in the CASL book.


Greetings,
   Till, Markus, and Lutz

-- 
Till Mossakowski                Phone: +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax:   +49-421-218-3054
University of Bremen            EMail: till@tzi.de           
P.O.Box 330440, D-28334 Bremen  WWW:   http://www.informatik.uni-bremen.de/~till