Skip to main content
PRL Project

next up previous
Next: The Mathematical Database Up: The Explanation Problem Previous: Geometry.


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



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 up previous
Next: The Mathematical Database Up: The Explanation Problem Previous: Geometry.

nuprl project
Tue Nov 21 08:50:14 EST 1995