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, Q, are
a quotient type ; therefore, as explained in the
section on
quotients in chapter 10, we must use the squash operator
( ||...||) in the definition of < over Q.
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 R. R/= can still be used, however, to gain access to the substitution and equality rules, and it is a convenient shorthand for expressing concepts involving equality.
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)| <_ eps
It 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 R
A proof of the theorem above will yield function resembling a
root--finding program.