Skip to main content
PRL Project



next up previous
Next: Mathematical Bus Up: The Connectivity Problem Previous: Numerical Linear Algebra

Weyl/Nuprl

 

In addition to the usual algebraic objects manipulated by computer algebra systems (polynomials, power series, vectors and matrices), our mathematics substrate Weyl [128], 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 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 [26]. With some success, we have recently conducted some experiments that combine the facilities of Weyl and Nuprl [53,54]. 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 [127].

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 can resolve some of these problems, additional research is needed to develop methodologies for using these ideas in maintainable code.



next up previous
Next: Mathematical Bus Up: The Connectivity Problem Previous: Numerical Linear Algebra



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