**Next:**Geometry.

**Up:**Value of Precise

**Previous:**Value of Precise

#### Conditions on Transformations.

The problem of Section 4.1 illustrates that in mathematical computations, especially those that involve symbolic aspects, a significant deductive component is needed to manage the assertions, preconditions and other logical aspects of the computation. We believe that a formal, deductive component, like Nuprl, is essential for assuring that combinations of mathematical tools will perform correctly in concert. Towards this end we have been coupling Weyl and Nuprl to address problems that arise in computations in commutative algebra [53,54].

For example, formal definitions can be given for the indefinite integral of a function, for the value of the definite Riemann integral

and the relationship between the indefinite integral and the value of the definite integral. These definitions frame the task of a numerical routine that evaluates the definite integral using the formula of QuadIntegral:Eq, viz.,

But this numerical routine is only valid when is bounded
away from **0**, as a very simple and shallow inference shows.

Once the mathematical types are given formally, there will be
cases in which static * type checking* will guarantee that the
expressions being used are sensible. Given a predicate
``RiemannIntegrable'' that determines whether a function is Riemann
integrable over an interval, one can define the * type* of Riemann integrable
functions:

The task of determining whether or not a definite integral has a well defined value can then be viewed as type checking in as much as it asks if the function belongs to the type of Riemann integrable functions for and .

*nuprl project*

Tue Nov 21 08:50:14 EST 1995

Tue Nov 21 08:50:14 EST 1995