Collaborative Mathematics Environment
Paul Chew, Robert L. Constable, Keshav Pingali, Steve Vavasis, Richard Zippel
Department of Computer
Science
Cornell University
Ithaca, New York 14853
Computational science will be the dominant paradigm for science in the next century. This proposal addresses one of the major challenges facing this new kind of science—the demand for better software support for computational mathematics. The task of providing this support is sufficiently central to the national interest and sufficiently comprehensive that it could serve as a Grand Challenge problem for computer science.
A strategy for meeting this challenge has evolved from inter-project cooperation at Cornell on the elements of scientific computing. This proposal represents a collaboration among five computer scientists with diverse backgrounds: scientific computing, computational geometry, computer algebra, applied logic, and programming languages. In various combinations, these people have worked together, and software from their separate projects has been linked. Their experience with the difficulty of this linking process has led to the identification and to the prospective solutions of three major problems: the connectivity problem, the code generation problem, and the explanation problem. The problems and their solutions are briefly explained below. This proposal outlines a plan to design and implement an open system architecture that will integrate a variety of computational science tools into an environment that supports collaborative activity.
Many interesting and powerful tools exist to support computational mathematics (for example, Matlab, Lapack, Mathematica, Axiom, Ellpack, PLTMG, Autocad, and LEDA), but most of these are focused on one specific area or on one specific style of computation. These systems are largely self-contained and closed, connecting to other software only at a very low level of abstraction, using, for instance, string-to-string communication. They do not have a common semantic base that would allow one system to ‘‘collaborate’’ with another. This is the connectivity problem. To address the connectivity problem, a common mathematical bus (the MathBus) will serve as the backbone of the system. Its communication protocols will be based on a typed formal language which provides the semantics for collaboration. A major design objective is to raise the level of communication among software tools, allowing the communication of mathematical objects instead of being restricted to simple strings.
Although existing software has contributed substantially to scientific programming productivity, the time taken to generate code remains a major impediment to progress in computational science. This is the code creation problem. In part, this problem is due to the difficulty of expressing certain mathematical techniques as subroutines. The problem of code creation is addressed with a method of transformation and refinement, allowing the transformation of high-level mathematical expressions into more-traditional code.
One of the reasons that sharing code with a colleague is difficult is because there is no common language for explaining what a program does and for precisely giving the conditions necessary to apply it. This is the explanation problem. The solution to the connectivity problem also provides an approach to explanation, namely to provide formal and semi-formal semantic standards for communications and linkage on the proposed MathBus.
The problem solutions outlined here lead to an additional opportunity. Once tools can inter-operate and mathematical models can be shared, it becomes possible to create collections of mathematical theorems, explanations, and examples and counterexamples. Such a mathematical database could capture an important part of mathematical knowledge that is at best poorly represented by books and journals.
Vision
The essence of scientific understanding is the creation of mathematical models—models for natural phenomena like the progression of the seasons or the creation of the universe, or models for artifacts like bridges, aircraft, or financial markets. To a large degree mathematics is the study of abstract tools that facilitate understanding these models. This was the role of arithmetic among the early merchants and traders, of geometry and logic among the early Greeks, and it is the role of differential equations in much of modern engineering.
In the second half of this century, our success in using computers to perform mathematical calculations has greatly increased our ability to predict many phenomena and has deepened our understanding of them. This success has created a new paradigm for scientific experiment—computational science. While it cannot replace the two existing scientific approaches of (1) experiment and (2) theory, we see computational science as a third scientific approach, one that will become dominant in the next century.
This proposal addresses one of the major challenges facing this new kind of science—the demand for better software support for computational mathematics. The task of providing this support is sufficiently central to the national interest and sufficiently comprehensive that it could serve as a Grand Challenge problem for computer science.
To frame the existing difficulties, consider the engineering computations involved in a large-scale design project such as the design of a new automobile. In a large design effort involving dozens of engineers, each group or department typically has its own set of favorite mathematical software tools. For example, we can suppose that the group designing the body has a parametric surface modeler such as ACIS, the group designing the engine and valve system has a combustion simulator and the research group is using Matlab to prototype new algorithms. This division of labor among multiple tools is very natural because the effective use of any one of these tools requires a fair amount of engineering experience. Two groups that want to combine results, however, face a major stumbling block because mathematical software tools are, at present, unlikely to be compatible. In many cases, the different tools actually make use of the same underlying mathematical objects (e.g., matrices, flow fields, surfaces), but are still incompatible, a situation that can be especially frustrating.
Even when one focuses on a single engineering activity, a wide variety of mathematical tools may come into play. Consider a research group developing a radically new internal combustion engine. In such a situation, simulation tools used for previous combustion studies must often be discarded, and new tools must be written by the group. Designing such a tool requires pieces of software that cut across many mathematical disciplines: initial boundary value problems, dynamical systems, geometry, and statistics. Often some of these pieces of software will come from packages—the numerical method will probably be prototyped in Matlab, for example. Other pieces will be copies from existing tools.
Merging together existing tools with new routines to create a new tool for a complex simulation like combustion is an extremely difficult task. The task is often made more difficult by flaws in the software itself: the type definitions for mathematical objects may be left unspecified, preconditions for mathematical routines are not stated, and different aspects of the numerical computation may be blended in the same subroutine in a way that makes it difficult to disentangle distinct mathematical procedures.
We envision an open architecture that will address these difficulties. Within this environment, an engineer’s ability to combine and create mathematical software is significantly enhanced.
Introduction
The investigators on this proposal come from a wide range disciplines within Computer Science: numerical analysis, computational geometry, symbolic computing, compilation, and applied logic. While each of our research interests are different, we have always found a common language for explaining our interests to each other—the language of computational mathematics. As we have started to look at larger scale computations and problems, we have found a need to combine the ideas and techniques we each developed. This process has led us to the observation that the software tools we have created cannot communicate and collaborate as readily as we can. As a matter of fact, in general, these tools cannot interoperate at all, except at the most primitive level, without significant design and coding effort.
Through discussions over the past two years, we have developed a coordinated plan to resolve what we believe are the basic problems of software collaboration. The resolution we advocate can be summarized as: Raise the semantic level of communications between programs from the level of text to the level of mathematics.
In section 2.1 we briefly discuss the basic problems and relate them to our experiences. A summary of the research plan we intend to pursue to resolve these problems is given in section 2.2. Each of the three basic problems and the research program that addresses each of those problems is presented in sections 3. 4, and 5. Additional detail on the database opportunity and the research required to undertake this project is given in section 6.
Connectivity/Interoperability Problem: Scientific computations involve an increasingly wide range of disparate tools. Problems often involve computations using combinations of numerical subroutine libraries, plotting and graphing packages, geometric modelers, symbolic computing systems and other tools. The engine design scenario discussed in the previous section illustrates the need to combine mathematical computation tools from a wide range of disciplines.
While some systems try to serve as comprehensive platforms for mathematical computation, they have not been sufficiently flexible to be satisfactory. In particular, no tool has a sufficiently expandable type system to deal with foreign mathematical objects. Those tools that have some provision for collaboration with other tools expect to be the master of the environment, not an equal with other tools. Finally, the semantics of the tools themselves is not specified precisely enough to support automated inter-operation.
Code Creation Problem: Packages are not always appropriate for solving computationally intensive scientific problems. For example, Matlab is extremely effective for certain problems like singular value decompositions, but it is not so appropriate for finite element stiffness matrix assembly, which involves a fair amount of pointer-chasing. In these cases, we must resort to a general purpose programming language such as Fortran or C and take advantage of subroutine libraries to minimize the coding required.
However, many aspects of creating mathematical software are not well captured by subroutine libraries. An example arises when coding iterative solvers for sparse matrices. An iterative solver typically requires some information about the underlying matrix A, such as matrix-vector products of the form Ax or A*x, or information about the diagonal entries of A (to construct a preconditioner). There are many different such iterative solvers [3], and there are also many different formats for representing sparse matrices [28]. It is difficult to code an efficient, modular iterative linear equation solving routine in Fortran or C that encapsulates the sparse matrix representation separately from the iterative method itself. Nonetheless, this type of modularization is very desirable to preserve the generality of the Fortran or C program. This encapsulation problem is exacerbated when working with parallel computers. It would be better to develop a transformation that starts from a separate specification of the iterative method and a specification of the sparse matrix representation and produces Fortran or C code.
We expect a dramatic increase in software productivity when scientists and engineers generate Fortran or C code for sequential and parallel computers by taking advantage of both libraries of subroutines and libraries of high level mathematical program transformations. The transformational approach allows preservation of encapsulation and allows generality as the program is developed.
Explanation problem: Sharing code with colleagues is difficult because there is no common language for explaining what programs do and precisely giving the conditions necessary to apply them. We need some assurance that the modules provided actually do meet the specifications provided. This assurance can be achieved either by verifying the code meets the indicated specification or by deriving aspects of the specification directly from the code. We call the combination of creating the specification and assurance of the specification the explanation problem.
Sharing/Mathematical Database Opportunity: Once tools can inter-operate, mathematical models can be shared and all aspects of mathematical study can be accessible to computation, a new opportunity arises. It is then possible to create collections of mathematical theorems, explanations, examples and counterexamples. When properly indexed, annotated and linked such databases can capture an important part of mathematical knowledge that is at best poorly captured via books and journals.
The resolution of these problems, coupled with the rapid technological advances in computer hardware, communications and software will allow us to create a truly collaborative environment—one in which both people and software tools can work together.
It is partially through these experiences that we have come to recognize the three main problems discussed above. The following sections describe occurrences of these problems more concretely.
Our plan is to build on our experience with mathematical software to create an integrated software environment for scientific/mathematical problem-solving. The important ideas behind our approach can be summarized as follows:
These four points are discussed in detail in the remaining sections of the proposal.
Our diverse team is uniquely qualified to achieve these goals. Constable brings his extensive experience with formal logic tools to bear on the proposed research. His group’s Nuprl system [16] 1has been used for verifying hardware [2][1], formalizing mathematical theories [36]and as an aid in the study of constructive mathematics [17][55].
Chew and Zippel have both worked on the SimLab project, which is an attempt to build a comprehensive environment for engineering computation. Chew’s area of expertise is computational geometry, and he has developed an advanced tool for mesh generation. Zippel’s work addresses symbolic computation and transformation based programming. Zippel has developed the Weyl language for symbolic algebra.
Pingali’s research area is restructuring compiler technology, and specifically, transformation based parallel programming for scientific problems. His research group has developed the Lambda loop transformation tool-kit, which can be used to transform loops in FORTRAN programs with the goal of increasing parallelism or of enhancing locality of reference. This technology has been transferred to Hewlett-Packard’s FORTRAN compiler for the HP-PA architecture. Pingali’s group has also worked on fast algorithms for control dependence problems, and this technology has been incorporated into a production compiler by Flavors Inc; it is also being used at Microsoft.
Finally, Vavasis’s area is scientific computing and numerical algorithms. He has developed algorithms for numerical solution of partial differential equations and also optimization. He is currently developing a mesh-generation software package.
The combined expertise of the five investigators covers all aspects of the proposed research. Moreover, we have already begun to collaborate on projects that extend each of our own individual expertise into the overlapping area defined by this proposal. Examples of these collaborations are described below.
In addition, we plan to continue to coordinate our activities with Cornell work on programming languages and environments [24][23][33][48][71][64][75]. In particular, the work being developed in support of the NSF proposal Software Engineering with a Transformational System by Gries and Teitelbaum is likely to supply a homogeneous user interface to the MathBus.
The basic connectivity problem is making software inter-operate. Over the past two years we have integrated a number of locally built tools with other local tools and with tools developed outside of Cornell. This experience has increased our understanding of the issues that arise in the connectivity problem, especially those issues that are specific to mathematical computation. The most apparent problem is the absence of common representations for many mathematical concepts. Such representations are needed to transmit mathematical objects between packages running in the same process and between programs running in separate address spaces. Persistent representations are also needed to store mathematical objects in databases and knowledge bases (which could then be made widely available, e.g., on the World Wide Web [7]). Those representations that do exist often lack precise semantic specifications, do not accurately model their underlying mathematical concepts and do not provide adequate mathematical flexibility, all of which inhibits their use as interchange formats between programs. Finally, previous attempts to meet all of the above desiderata have not yielded systems with adequate performance. Some of these same concerns have been recognized earlier [27].
In sections 3.1, 3.2, and 3.3 we discuss some of our experiences, which focus on the connectivity problem in more detail. In section 3.4 we discuss our approach to resolving the connectivity problem.
Meshers serve as intermediaries between the modelers used to define the geometric regions to be studied, and the tools that actually solve the differential equations governing a system’s behavior. Meshers convert the geometric descriptions produced by geometric modelers into collections of small, well shaped polyhedral pieces that cover the geometric region and that are the basis for the numerical equation solving techniques.
Mesh generators are an interesting example of a mathematical software package because they must solve the connectivity problem to be at all useful. In particular, they must accept geometric regions as input, and produce simplicial complexes in a format compatible with a finite element package. This connectivity problem is made difficult by the lack of standard representations for n-dimensional geometric objects and simplicial complexes.
A second peculiarity is that one of the arguments of a mesh generator is a mesh-grading function that indicates the required size of the elements of the mesh for different parts of the geometric region. Sometimes the user wants to specify this real-valued function interactively.
Currently, Vavasis is attempting to connect his C++ n-dimensional mesh generation program [54] to external software packages using interfaces written in Tcl [56]. Tcl is also used to overcome the problem of specifying new functions at run-time. Nevertheless, Vavasis’s solution is problematic; for instance, there is no way to specify (automatically) the preconditions on the user’s geometric domain as required by the mesher. Similarly, there is no way to specify (let alone verify) that the user’s mesh-grading function must be positive. Vavasis has hard-coded his types (for domains, meshes, and mesh-grading functions) into his C++ programs, along with some ad hoc type-checking routines.
Matlab [52] contains a number of features that make it a much higher-level language for specifying mathematical computation than conventional programming languages (like Fortran), and it has been an invaluable tool for exploring many issues in numerical analysis. Vavasis uses a Matlab program as his differential equation solving tool in conjunction with his mesher. For this, Matlab’s sparse Cholesky factorizer [29] is invaluable.
Indeed, it is the phenomenal growth of Matlab that partly inspired us to write this proposal. Scientists who used to write their own software or use subroutine libraries are switching in droves to Matlab.
Nonetheless, for some complex problems, the use of Matlab has been problematic. The main difficulty is the lack of support for data structures more general than matrices. For example, there is no easy way to represent geometric objects, which is why Vavasis’s mesher is written in C++. Furthermore, due to excessive operator overloading, the semantics of Matlab, even for matrix operations, are complex.
It might be possible to ‘‘fix" Matlab by adding a powerful type system, but this would defeat the appealing interactive feature that variables don’t have to declared. Instead, we are proposing to accept Matlab as it is, but design convenient semantics for connecting it to other software. Matlab already provides the C-language hooks for this purpose, so our job is the higher-level semantics of the Matlab/MathBus connection.
In addition to the usual algebraic objects manipulated by computer algebra systems (polynomials, power series, vectors and matrices), our mathematics substrate Weyl [76], can represent objects from a variety other mathematical domains. For instance, using Weyl’s ability to represent and perform arithmetic with functions (including those specified via their values at points), we were able to synthesize high dimensional dynamical systems from the Navier-Stokes equations using the Galerkin projection using only a page of code (compared to over fifty pages required using other techniques). Weyl’s framework is general enough to support objects like simplices, simplicial complexes and other objects from geometry and topology as ‘‘first class" objects. Mesh generation software that takes advantage of these tools have been developed using Weyl.
The domains of which these objects are elements are also represented in Weyl. That is, not only are elements of rings, fields and vector spaces representable in Weyl, but the rings, fields and vector spaces themselves are Weyl objects. This facility provides a natural home for many mathematical properties that arise in computations. For instance, one can specify the algebraic extension over which to factor a polynomial by explicitly providing the algebraic number field. Determining which of several polynomial greatest common divisor routines should be used depends on properties of the coefficient domain of the polynomial (e.g., coefficient growth, characteristic, presence of zero divisors, etc.). In Weyl, this type of information can be managed and maintained in the rings themselves.
Increasingly, we are seeing that sophisticated mathematical computations involve a non-trivial amount of deductive inference in addition to calculation. For instance, an algebraic extension will be free of zero divisors if a certain ideal is a prime. Deductions of this type and management of the vast array of mathematical theorems involved in these deductions are more appropriately handled by a proof development system like Nuprl [16]. With some success, we have recently conducted some experiments that combine the facilities of Weyl and Nuprl [36][37]. Nuprl was able to axiomatize the domain structures used in Weyl, and create accurate and effective semantic models for many issues that had previously been treated in an ad hoc manner.
This broad coverage, and the fidelity with which we manipulate mathematics has made Weyl/Nuprl attractive as a platform for developing meshing algorithms, as an intermediary between geometric modeling programs and finite element solvers, and as the foundation of program transformation tools that synthesize numerical programs from specifications of mathematical computations [75].
However, this flexibility and fidelity has come at a cost in performance. Experiments have shown that the cost of repeated run-time dispatching for low level arithmetic operations, and the constant ‘‘re-boxing’’ of objects to provide a place to attach the mathematical domain can be excessive. While clever use of the ‘‘template’’ and ‘‘RTTI’’ mechanisms in C++ can resolve some of these problems, additional research is needed to develop methodologies for using these ideas in maintainable code.
To address the issues raised in this section, as well as to provide a common base on which to address the problems described in the following sections, we propose to create a software bus [63] specially designed for mathematical objects, which we call the MathBus. Conceptually the MathBus is similar to Polylith [62], but our concerns about persistence, mathematical soundness and special needs of mathematical computations lead to some important differences.
The MathBus consists of four components. First, there is a transport mechanism that enables efficient transmission of mathematical data structures from one process to another regardless of the machines on which the processes reside. A number of transport mechanisms are currently available from which we can choose, e.g., ToolTalk, OLE and OpenDoc. Due to the large size of some objects these mechanisms may need to be extended or enhanced. On top of the chosen transport mechanism we will specify a reference set of data formats for dealing with common mathematical structures—real and complex numbers, vectors, matrices, polynomials, asymptotic expansions, differential equations, manifolds, simplices, graphs, trees, etc.
The MathBus is used to communicate mathematical information between two tools. In order to ensure that the parties to a communication understand each other we will provide ‘‘customs houses’’ at the entrance ramps to the MathBus. These customs houses will be responsible for translating data between the applications’ data formats. In the simplest scenario, the customs house on the ‘‘on ramp’’ will translate an application’s data format into the MathBus reference standard data format, while the customs house on the ‘‘exit ramp’’ will translate from the reference standard to the applications data format. (The customs house’s specifications will given in a formal manner as described in section 5.)
To avoid the cost of constantly translating data from one format to another, the ‘‘customs inspectors’’ can negotiate ‘‘free trade zones,’’ through which data can be transmitted without inspection or translation. Once a free trade channel has been negotiated between two applications data can be transmitted at the underlying transport substrate’s data rate.
Finally, we plan to develop a generic mathematics substrate that has the flexibility and fidelity of Weyl, but which is efficient and lightweight enough for general use. This substrate will have easy access onto and off of the MathBus since its data formats will closely match the reference standard data formats. It will probably be easiest to write the customs house software in this substrate.
While increasingly powerful mathematics packages like Matlab, Maple and Mathematica have dramatically reduced the effort required to perform some mathematical experiments, it is often still necessary to retreat to conventional programming languages, augmented by standard subroutine libraries, for complex or multi-domain problems. A few of the issues that arise were described in the context of mesh generation in section 3.1.
However, even with the programming tools and subroutines libraries now available, far more effort is required to code a complex mathematical computation than is required to explain the computation to a colleague. This is largely due to (1) the semantic gap between mathematics and conventional programming languages, and (2) the difficulty in expressing certain mathematical techniques as subroutines.
We feel that these issues can be effectively addressed by using transformations to convert high level mathematical expressions into more traditional code (in Fortran or C, for instance). A library of such transformations would also include routines that verify the mathematical validity of the transformations before they are applied as well as verifying the pre- and post-conditions of conventional subroutines. These tools could also support parallel versions of these languages such as Split-C [18] or Fortran-90 [26].
In section 4.1 we illustrate why a transformation based programming methodology requires a system with a rigorous mathematical substrate. In section 4.2 we give an example of an application of transformation based software development that could have a broad impact on scientific computing.
As a simple example of the transformational approach, consider writing a program to solve the quadratic equation, x2 + bx + c = 0. Mathematically, it is most natural to write the solutions as:
From this mathematical specification, we can produce two different types of solvers: numerical solvers where the coefficients of the polynomial are expressed as floating point numbers and semi-numerical solvers for use when b and c are expressed exactly or in terms of symbolic expressions.
In the first case, we
know that direct use of (1) is unacceptable for three reasons.
First, the computation of b2 can overflow even
when the value of 
and 
can be
expressed as floating point numbers. To deal with this (1) should
be coded as:
.
Second, if 4c/b2 is small then the subtraction case above will involve subtracting two nearly equal quantities. Thus, a better way to compute these two roots is
, 
.
If the
computer’s arithmetic does not deal with underflow
gracefully then an additional modification may be needed. Third,
if 
is negative,
then the square root will return a complex number which must be
dealt with properly.
For each of the problems that arose, a suitable transformation could be defined to convert the original formula into one that does not have the indicated problem. Furthermore, these transforms could be reused to deal with numeric errors that arise in other calculations. These transformations, however, cannot be easily encoded in a subroutine library.
In the exact case, the formula (1) is satisfactory, however the square root must be dealt with carefully to avoid running afoul of branch cut problems.
From the perspective of creating a comprehensive problem solving environment, the transition from the numeric solvers to semi-numeric solvers needs to be seamless, since, for instance, the mathematician rarely feels that introducing into a computation a small (symbolic) e increases the difficulty significantly. By encouraging the development of mathematical programs via program transformations and by providing a library of transforms, like those discussed above, we expect to ameliorate the problem.
The transformational approach and the MathBus will be used in a restructuring compiler that will generate highly optimized parallel code for sparse matrix problems. Sparse matrix computations are ubiquitous in computational science since they arise whenever differential equations are solved using numerical techniques such as the finite element and finite difference methods. It is therefore ironic that almost all of the work to date on automatic program restructuring and parallelization, such as the HPF effort, has focused on dense matrix problems. The main reason for this is that restructuring compilers cannot analyze sparse matrix programs. Sparse matrices are stored in special formats, such as compressed row or column storage (CRS, CCS), and these formats complicate dependence analysis. Consider matrix-vector multiplication, which is a key step in conjugate gradient solvers, as well as in other iterative matrix algorithms [30]. If A is a sparse matrix in CCS form, the following code computes Ax, storing the result in vector v.
This small code fragment illustrates two key points regarding sparse matrix programs and their parallelization using automatic code restructuring tools. First, there is substantial parallelism in sparse matrix problems. A sparse matrix program performs a subset of the operations performed by the corresponding dense program; if two operations can be done in parallel in the dense program, they can be done in parallel in the sparse program. In the matrix-vector product, this means that different rows of the matrix can be multiplied with the vector in parallel; for each row, the partial products can be accumulated in parallel. In fact, in algorithms like the multi-frontal algorithm for sparse Cholesky factorization, the zero entries in sparse matrices can be exploited to extract more parallelism than is there in the corresponding dense program [47].
Secondly, the parallelism in sparse matrix programs is obscured by the storage scheme for sparse matrices. In particular, the use of indirection arrays, such as row-index in CCS, can foil the ability of a restructuring compiler to generate parallel code. These compilers perform dependence analysis to determine a partial order on loop nest iterations, but the analysis techniques work only when array subscripts are linear functions of loop index variables, allowing standard tests like the GCD and Banerjee tests to be used [74][60][11]. When complicated subscripts such as those involving indirection arrays are used, dependence analysis fails. With conventional compiler technology, the matrix-vector product code shown above is doomed to run sequentially.
The Bernoulli project at Cornell is addressing this problem through the use of program transformations to generate sparse matrix codes from dense matrix programs. Intuitively, this process can be viewed as a form of partial evaluation in which the compiler exploits information about zero/nonzero elements of matrices to eliminate unnecessary computations, and then chooses an appropriate representation for the sparse matrices. Since the input to the compiler is a dense matrix program, the ability to analyze and restructure programs, for example by using the Lambda loop transformation tool-kit developed at Cornell [43], is retained. However, the transformation to sparse code requires information about the sparsity structure of arrays. To get this information, we are integrating our compiler with a discretization system being written by Rich Zippel. This system uses Paul Chew’s mesh generator, and incorporates symbolic and numerical routines for implementing the weighted residual method of discretizing differential equations. The discretization system has complete knowledge of the sparsity structure of matrices since this is fully determined by the meshing and discretization process. This information will be passed on the MathBus to the restructuring compiler to generate parallel code. Any bottlenecks detected by the restructuring compiler can be passed back to the synthesizer so that a revised mesh or different set of basis functions can be used for better parallel performance. The two-way flow of information between the discretization system and the restructuring compiler is an instance of the synergy which results from an integrated system, a synergy that is absent in current approaches. Distribution of sparse matrices across the nodes of the parallel machine is done using standard methods like recursive spectral bisection [61] and geometric partitioning [53].
To summarize, the compiler generates efficient, parallel sparse code by partial evaluation of the dense program relative to the sparsity structure of matrices which is obtained over the MathBus from the discretization system.
Ongoing Activities
Collectively the investigators have a significant amount of experience with transformation technologies. As mentioned above, the Bernoulli project (Pingali and Zippel) includes both high level program transformations (discretizations) and the transformations required by compiler optimizations. The Nuprl proof development system (Constable) has at its core a powerful transformation system. Each of the transformation systems mentioned deals with different types of expressions. Already in the Bernoulli project, we have seen how cooperation between the discretization transformations and the code restructuring transforms used by the compiler can produce significant benefits for parallel computations. While it is not likely to be practical to create a single transformation system that is appropriate for all of these activities, we plan to combine the technologies being developed to strengthen our individual efforts. Furthermore, adapting the term structures used by the different transformation systems to the MathBus will facilitate more closely coupling the systems.
In addition, our colleagues in the Computer Science Department (Gries and Teitelbaum) are developing user interface technologies that simplify the use of expression transformation systems (see their NSF proposal Software Engineering with a Transformational System). We will take advantage of the ideas, techniques and tools they develop.
One of the characteristic features of a scientific theory is that it can explain natural phenomena and predict events. When we produce a list of numbers that indicate the direction, velocity and time for the launch of a spacecraft intended to intercept an asteroid, behind the generation of these numbers is a detailed explanation that the intercept will actually occur based on mechanics and its mathematics. But when the line of reasoning from the heavenly bodies to the decimal digits reaches the computer software and hardware used to generate these numbers, the explanation loses clarity and conviction. We come to need principles that govern the numerical approximation, the programming languages, the compilers and the hardware. These principles are not currently as well understood as those used in the physics and mathematics.
As we try to build more sophisticated software tools to solve the code creation problem and the connectivity problem, we run the risk of making the explanation of results unmanageably complex. This proposal is concerned with providing tools to manage explanations in computational science as well. The first step is to identify the new issues. We do this based on our experience and we confine the account here to matters with which we are directly familiar, but many more examples come readily to mind. After raising three kinds of problems, we focus on one kind of solution that we have explored and which we intend to pursue in more detail. We will be looking for other compatible approaches as well.
The problems we cite all have the character that they reveal a need to be more careful about the mathematical assumptions underlying the use of software. Since the computer is carrying out a wider variety of steps than just numerical evaluation, a wider variety of conditions must be generated and many more of them must be checked than is customary in derivations done by hand.
The solution we propose is the one used in mathematics when validity is an issue—be rigorous. The way to keep up with the computer’s generation of conditions is to use a computer to manipulate them as well. This leads to formal methods and tools from applied logic.
Symbolic Computations and the Explanation Problem
Symbolic computations incur for a number of subtle problems that do not arise in numeric computations. These problems arise in a number of ways, many of which have been enumerated in informal announcements and talks by Kahan [39]and Fateman. One of the paradigmatic sources of error arises when the different levels of abstraction are used in the computation. Resolving this problem is one of the foundations of the Axiom system [38][19] and is addressed by our own Weyl system [76].
A simpler, but just as serious problem is illustrated below. Consider the issues that arise in trying to write a subroutine that produces the value of the parameterized integral
.
Because the integrand is a simple rational function, and might have poles in the interval [0, 1], we find it preferable to compute the indefinite integral symbolically, and then transform the symbolic form into a numerical program. When a symbolic computing system like Maple is asked to compute the indefinite integral, it returns something like
The transcendental function is expected since it is the sum of two logarithms and the denominator has two zeroes. Unfortunately, the resulting numerical program will fail whenever b2 – 4c vanishes.
This problem arises because the integration routines had assumed that the denominator was square free—a reasonable assumption since x2 + bx + c and its derivative with respect to x are relatively prime as elements of Z[b, c, x]. However, when b and c are given numeric values, this assumption is invalid and the result is erroneous. This is an example of two pieces of software not clearly communicating their assumptions. The problem is not a simple question about polynomials in Z[b, c, x]. Additional assumptions are involved.
Geometry and the Explanation Problem
The subject of geometry has not been ‘‘computerized’’ in the same way as algebra, in that there are no Computer Geometry Systems analogous to existing Computer Algebra Systems such as Axiom, Maple, Weyl, and Mathematica. The closest thing to Computer Geometry Systems are commercial Computer Aided Design (CAD) packages such as AutoCad.
This emphasis on CAD (and on producing pictures of objects) has led to another problem with existing geometric software packages: these packages typically provide a severely limited set of possible geometric representations. The provided representations are useful for CAD, but are too restrictive for more general mathematical applications. Clearly, no single representation can support all possible geometric objects, but consider one popular (abstract) way to represent such objects: boundary representation. In a boundary representation, the geometric object is stratified; zero-dimensional elements of its boundary are described, then these are linked to one-dimensional boundary elements, and so on, for as many dimensions as needed. There are no widely-supported and fully general realizations of boundary representations in current mathematical software. Instead, existing software typically imposes limitations such as geometric objects can be three-dimensional only, coordinates are required to be represented in floating-point (as opposed to allowing additional numeric systems such as rational or algebraic numbers), and only certain kinds of parametric surfaces are allowed.
Access to Libraries
One of the common problems of using an algorithm written by someone else is knowing exactly what it does and under what conditions it works. These problems are compounded when we use large libraries of programs or complex systems.
One example of the importance of providing better access to libraries is illustrated by the Amphion project at NASA Ames led by M. Lowry [50]. Amphion helps users compose software from SPICELIB, a Fortran-77 library for computations in solar system geometry. Even though the routines in SPICELIB are well documented, users were reluctant to invest the effort required to learn to use the library by reading the documentation. So, Amphion users can pose problems by drawing planets, spacecraft, etc. using a graphical user interface, e.g., they can position Voyager to observe the shadow of the moon Io on Jupiter.
One difficulty with this approach is that Amphion might compose routines without regard for their pre-conditions. To solve this problem, formal methods are being used to synthesize simple routines and ensure that they are correctly connected [70].
A similar example problem arises with the opportunity to synthesize special purpose routines from specifications. For instance, scientific subroutine libraries currently contain a variety of Fast Fourier Transform (FFT) routines. Among the parameters of these routines are the number of points in the FFT, the radix used and how the FFT matrix is factored. However, it is not difficult to synthesize FFT routines directly from a specification [6][59], which leads to more flexibility. In addition, synthesized routines that use various parameters explicitly can often be better optimized than more general, parameterized routines.
A software library that uses synthesized software, as we are suggesting, has rather different characteristics from the existing approaches. In particular, a language is needed to specify the desired parameters of the FFT routine to be synthesized, and some checks need to be provided to ensure that the delivered software matches the specification.
Value of Precise Mathematical Language
The three examples of the explanation problem discussed above all arose in our work. They are representative of problems that have faced applied mathematicians and engineers for years. One solution pursued by the scientific community has been to be more precise and careful. The algorithm’s pre-conditions are specified carefully, e.g., the fact that b2 – 4ac must be nonzero for (2) to be valid. Theorems that characterize the applicability of an algorithm, for example that a particular meshing algorithm is only valid for piece-wise smooth 2-manifolds. Finally, reference books have been developed that precisely document the standard library algorithms in terms of the communal database of mathematical knowledge [40][34][35]. Indeed, it is the elaborate knowledge base that characterizes the domain in which we work.
The emergence of applied logic and formal methods has opened new opportunities for computers to help in more effectively employing the methodology of mathematics. We now know how to specify algorithms rigorously and how to create semi-formal databases. We look at how two specific examples are treated.
Conditions on Transformations
The problem of section 5.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 [36][37].
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
.
But this numerical routine is only valid when b2 – 4c 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:
{f : [a1, a2] ® R ½ RiemannIntegrable(f, a1, a2)} .
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 
.
Geometry
A general way to describe a geometric object in b-rep format is as a layered directed graph with the description of each face associated with a node. (The base layer of the graph is the 0-dimensional faces, i.e., vertices, and successive layers specify higher-dimensional faces.) For polyhedral objects, the information associated with each node is a system of linear equations that define the affine hull of the face. S. Allen showed how to define this layered structure in Nuprl with a few lines of Nuprl terms with bindings. Allen’s type definition also yields a notation for specifying any particular instance of an n-dimension polyhedral object. The notation is a simple recursive nesting with the 0-dimensional faces defined by the outermost layer of nesting, and then higher dimensions are nested inside.
Vavasis has adopted Allen’s notation to describe the geometry of the input domain for his n-dimensional mesh generator. There are many correctness properties associated with a polyhedral region that could be completely captured by theorems in Nuprl.
For Chew’s surface mesher, the layered structure can also be used, but the faces are now defined by nonlinear equations, typically algebraic. The correctness properties for a boundary-rep object with nonlinear faces are much more difficult to verify, but fortunately, Nuprl and Weyl provide exactly the right environment for this problem. (The heart of the correctness testing involves checking for intersections between algebraic surfaces.)
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
and 
then
will imply
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. [70] 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 [65][13][20][21][66][51][15][16] 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 [12][25]. Using the theorem prover in a ‘‘shallow mode,’’ the system has been able to glue together algorithms [37].
The Mathematical Database Opportunity
In our description of the Mathematical Bus up to now, we have regarded objects shared between packages as ephemeral—objects are translated to the common mathematical language and then back again as packages inter-operate. Nevertheless, once the data types and definitions are in place for some subset of interesting mathematical objects, it becomes possible to make objects permanent.
The permanent objects are not just the ‘‘data’’ but also the ‘‘definitions’’ and ‘‘theorems’’ themselves. This is because the formal system we envision treats data, definitions, theorems, and so on with a uniform notation. Nuprl is an example of such a system.
Indeed, a major component of our envisioned collaborative mathematics environment will be a database of definition, display forms, facts, algorithms, theorems, explanations, transformations, system-level (meta) functions, and methods. We expect these to be linked by a user interface that will provide natural ways to browse, as with Mosaic on the Nuprl library browser. Moreover, there will be system-level functions to automatically access data and use it. A model for this is the Weyl transformation and Nuprl tactics.
When one thinks of mathematical repositories, one usually thinks of software libraries like Netlib [22] or GAMS [9]. These libraries are enormously successful, having made a large body of numerical software widely available twenty-four hours a day. However, when software synthesis becomes more widely accepted the structure of these libraries will change and new problems will arise.
As a simple example of such a library, consider the problem of selecting elements (shape functions) to use as a basis in a finite element method. A typical finite element package such as ANSYS offers the user dozens of elements, documented by many pages of the ANSYS manual. In our imagined library, these shape functions could be stored together with all their attributes such as order, degree of continuity, and nodal coordinates. This information could then be used in synthesis of a numerical method, with pre- and post- conditions automatically checked. This kind of database entry is considerably different from the traditional subroutine-library approach, because most of the useful information about a shape function takes the form of specification rather than executable code.