- The natural numbers (and also integers and rationals) have been
specified in a very simple, easily readable way. Even if this
does not follow an optimal exploitation of structure in all
cases,
readability is more essential here.
The new specification Nat, together with its signature, can be obtained here.
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.
The flattened
version of our older Nat
specification
shows that these are not presentable as "standalone".
- The RelationsAndOrders
and Algebra
libraries have been 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 to obtain any comments on this proposal until
*** end of May 2001 ***
since we are afterwards going to produce a new (hopefully nearly final)
version of the basic datatypes.