**Next:**The Mathematical Database

**Up:**The Explanation Problem

**Previous:**Geometry.

## Summary

What we have called the * explanation problem* in this section is
familiar to every scientist and engineer. It is the task we face in
``writing up'' a result or documenting an artifact. Software has been
helping with more and more aspects of this chore. We are all familiar
with the kind of help provided by word processors, type checkers and
other software tools that check for errors or enforce style. We
believe that for mathematics there is a deeper level on which help can
be provided, and it will offer even greater advantage in the long run
than the word processor or the programming language processor.

The idea is to write explanations in the formal languages that have been developed in the fields of applied logic and formal methods and direct those tools to providing the kind of assistance called for in our examples. We have seen four ways that these tools can help.

First, if we use an expressively rich formal system for working with mathematics, we can naturally define the actual concepts and the data to which algorithms refer, and we can precisely define the problems these algorithms solve.

Second, the type checking routines in compilers are examples of programming tools that are based on the standard elements of mathematical notation. Type checkers have been extremely successful in helping programmers find and eliminate errors in code. The type checking routines we can build based on the rich types system of mathematics will be of similar value in coding and in other manipulations of mathematical expressions.

Third, a formal language can express * pre- and post-conditions* on
algorithms. For example, given

then

will imply that

If proving a condition like (3) can be done semi-automatically with minor user assistance, then we can build a tool that will help check that algorithms are composed properly. These formulas act as glue that hold a compound piece of code together, and one can imagine tools for finding weak spots in the glue. This is what Stickel, et. al. [107] are attempting to provide for the NASA code library using simple theorem proving tools (of the kind we have available as well).

Fourth, when it is necessary to understand an algorithm in precise
detail, a person would like to have access to a complete explanation
of it. But a * good explanation* is a subtle artifact. It should
cover just enough detail to answer the educated reader's question, no
more and no less. But the level of detail needed varies from user to
user. We know from experience with Nuprl that in the presence of *
formal text*, explanations can be organized in layers of detail,
eventually down to a complete account. Furthermore, related parts of
text can be automatically linked creating hypertext. The links can be
semantic, e.g., a link points to the definition of a concept or an
example of it.

We have experience with interprocess communication of mathematical
objects using the Nuprl term structure. We have seen that Nuprl's
* typed formal language* comes close to realizing the value of
precise language in the four ways outlined above, and we see ways to
build on the basis, expanding the term structure as necessary.

First, Nuprl has been able to define all the basic concepts for number theory, finite set theory, algebra and basic analysis. We are looking at geometry and topology as well. The language was designed based on the foundational type theories studied for much of the century [97,23,33,34,100,76,25,26] and believed to be adequate for all of mathematics.

Based on this experience with Nuprl, we know that type theory is a good basis for meeting the above goals. The language can express mathematical problems and their algorithmic solutions. The Nuprl group has been able to check the type correctness of expressions in algebra and analysis [22,39]. Using the theorem prover in a ``shallow mode,'' the system has been able to glue together algorithms [54].

**Next:**The Mathematical Database

**Up:**The Explanation Problem

**Previous:**Geometry.

*nuprl project*

Tue Nov 21 08:50:14 EST 1995

Tue Nov 21 08:50:14 EST 1995