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."since we anyway need sequences to specify the exponential and trigonometric functions using Taylor power series.

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
*n*th 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.^{1}

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^{2} 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.

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.

Comments to till@informatik.uni-bremen.de