**Next:**Summary

**Up:**Value of Precise

**Previous:**Conditions on Transformations.

#### Geometry.

A fairly 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.)

*nuprl project*

Tue Nov 21 08:50:14 EST 1995

Tue Nov 21 08:50:14 EST 1995