This section presents Nuprl formalizations of constructive versions of some of the most familiar concepts of real analysis. The account here is brief; more on this subject will be found in the forthcoming thesis of Howe [Howe 86].

We begin with a basic type of the positive integers, two definitions that
make terms involving ` spread` more readable and an alternative
definition of ` some` which uses the set type instead of the product.

Pos == {n:int|0<n}

let <x:var>,<y:var>=<t:term> in <tt:term> == spread(<t>;<x>,<y>.<tt>)

let <w:var>,<x:var>,<y:var>,<z:var>= <t1:term>,<t2:term> in <t3:term> == let <w>,<x>=<t1> in let <y>,<z>=<t2> in <t3>

Some <x:var>:<T:type> where <P:prop> == { <x>:<T> | <P> }Figure lists a few of the standard definitions involved in the theory of rationals . Note that the rationals,

**Figure:** Defining the Rational Numbers

We adopt Bishop's formulation of the real
numbers as * regular* (as opposed to * Cauchy*)
sequences of rational numbers. With the regularity approach a real
number is just a sequence of rationals, and the regularity
condition (see the definition of ` R` below) permits the
calculation of arbitrarily close rational
approximations to a given
real number. With the usual approach a real number would actually
have to be a pair comprising a sequence * and* a function giving the
convergence rate.
Figure lists the definition of the reals and functions
and predicates involving the reals.
The definition of **<** is a little different than
might be expected, since
it has some computational content, i.e., a positive lower
bound to the difference of the two real numbers.

**Figure:** Defining the Real Numbers

The definition of (` <_`) in figure is
squashed since it is a predicate over a quotient type.
However, in the case of the real numbers the use of the squash
operator does not completely solve the problem with quotients.
For example,
if ` X` is a discrete type (i.e., if equality in
` X` is decidable) then there are no nonconstant functions
in ` R/= -> X`. In particular, the following basic facts * fail* to
hold.

All x:R/=. All n:int. Some a:Q. |x-a| <_ 1/n in Q

All x,y,z:R/=. x<y in R/= => ( z<y in R/= | x<z in R/=)We are therefore precluded from using the quotient type here as an abstraction mechanism and will have to do most of our work over

Consider the computational aspects of the next two definitions.
Knowing that a sequence of real
numbers converges involves
having the limit and the function which gives the convergence
rate. Notice that we have used the set type (in the
definition of ` some where`) to isolate the computationally
interesting parts of the concepts.

<x:Pos->R> is Cauchy == All k:Pos. Some M:Pos where All m,n:Pos. M <_ m in int => M <_ n in int => |<x>(m)-<x>(n)| <_ (1/k)* in R/=

<x:Pos->R> converges == Some x:R/=. All k:Pos. Some N:Pos where All n:int. N <_ n in int => |(<x>)(n)-x| <_ (1/k)* in R/=Figure defines the ``abstract data type'' of compact intervals.

**Figure:** Defining Compact Intervals

Following is the (constructive) definition of continuity
on a compact interval. A function in ` R+ -> R+`
which inhabits the type given as the definition of continuity
is called
a * modulus of continuity* .

R+ == { x:R | 0<x in R/= }

<f:|I|->R> continuous on <I:CompactIntervals> == All eps:R+. Some del:R+ where All x,y:|<I>|. |x-y| <_ del in R/= => |<f>(x)-<f>(y)| <_ epsIt is now a simple matter to state a constructive version of the intermediate value theorem.

>> All I:CompactIntervals. All f:|I|->R. f continuous on I & f(a_of I) < 0 in R & 0 < f(b_of I) in R => All eps:R+. Some x:|I|. |f(x)| < eps in RA proof of the theorem above will yield function resembling a root--finding program.

Thu Sep 14 08:45:18 EDT 1995