next up previous contents index
Next: Denotational Semantics Up: Mathematics Libraries Previous: Regular Sets

Real Analysis

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 ==
     let <x:var>,<y:var>=<t:term> in <tt:term> ==
     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 gif 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 gif 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 gif 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 gif 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.

next up previous contents index
Next: Denotational Semantics Up: Mathematics Libraries Previous: Regular Sets

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995