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)| <_ 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.