4.1 The Structure of the Specifications

For real numbers we give a loose specification DefineBasicReal in terms of an ArchimedianField, which is algebraically closed and complete for Cauchy sequences. An ordered field is Archimedian if each element is bounded by a natural number. It is algebraically closed if all positive square roots exist and each polynomial of odd degree has a solution. A Cauchy sequence is a sequence the elements of which get arbitrary close to each other.

The main difficulty when specifying the reals is to write down the completeness axiom. Instead of the usual forms (each Dedekind cut has a cut number, or each bounded set has a supremum), we here use the form

"Every Cauchy sequence converges."

Sequences of reals (i.e. functions from the naturals to the reals) are not directly available in CASL. We therefore introduce a sort Sequence, an access operation __ ! __ (where a!n gives the nth element of the sequence a), and some operations on sequences (mainly those gained by lifting operations pointwise from reals to sequences). The latter is necessary for getting enough sequences.¹

In order to define this algebraic structure we give specifications DefineOrderedField, OrderedField, and DefineArchimedianField. The specification BasicReal completes the real numbers by standard functions of real analysis. Adjoining the two elements -infty and infty and defining the value of the standard operations on real numbers at these points leads to the specification CompactBasicReal.

There is no need for a special literal syntax for elements of the sort Real. As we declare the rational numbers as a subsort of the real numbers, the literal syntax of rational numbers, which we described in section 2.3, carries over.

The choice of the name "BasicReal" reflects the fact that the specification is strong enough to develop the basics of reals as far as it is needed for those real functions that occur in programming languages. We shortly discuss the mathematical background of the specification DefineBasicReal in section 5.

Thus for now² the specifications of this note complete the list of specifications from Note M-6 [RM99a] as follows:

Algebra:

DefineOrderedField, OrderedField,
DefineArchimedianField, ArchimedianField.

Numbers:

DefineBasicReal, BasicReal, CompactBasicReal.