The principal syntactic units of Nuprl are terms of an
extensible, general purpose binding syntax. The data base the user
works with is a library of objects, to which they may add.
Other than proofs, all objects are terms that have been given names in
the library, and proofs are special structures built from terms.
Objects may be classified according to which of four roles they play:
formally meaningful, informally meaningful, ``utility'', and display
specification.
An operator definition, sometimes called an abstraction, is one kind of object, e.g., the definition of ``fog.'' Proofs of theorems constitute another kind of formally meaningful object. A third kind of object is used to declare the basic inference rules, in terms of which all other more complex inferences are defined. Another kind of object defines procedures in the programming language ML for use in the proof tactics. Finally, the user may simply create objects to be used as data by tactics. These various kinds of objects constitute the formally meaningful part of the system about which precise semantic claims are made; ultimately, our claims about the truth of theorems depend upon them.
The informally meaningful objects are the various documents, such as lessons and notes, which typically refer to the formally meaningful components. Although these objects have no formal significance, they are essential to practical use of the library, providing the explanatory interface to the formal components. It is by means of such documents that one is guided through what could otherwise be a formal thicket whose significance is unclear; we call a document used as such a guide a reading of the library.
A third class of objects might be called utilities, which make using the system easier, such as menus for edit commands.
Finally, there are the objects that tell the system how to display terms. A fundamental design principle for Nuprl is this: the formal content of an object is independent of the way it is to be displayed.
This means that you never need commit to a particular notational decision since your changes to the display specification objects have automatic effect on viewing any objects of the system. For example:
There is an editor built into Nuprl, which we call the resident
editor, and this is what the class would use. As was explained in the
previous section, all library objects other than proofs are terms, and
this includes hypertext documents. To represent text in the Nuprl
term language, we have simply declared some new terms and operators
without assigning them any mathematical meaning, and have specified
display forms for them that make them look like ordinary text. These
display methods together with a few utilities defined in the editor
constitute a simple word processor. This is why formal expressions
can be easily embedded in informal documents; a document is just a big
term which may have subterms with formal meaning.
Similarly, ``hypertext'' links were also built the same way, and associated in the editor with actions such as ``clicking on this link raises the referenced object.'' Basically, we get the word processor and hypertext links almost for free given the general purpose term editor, and the user's general term editing skills apply as well to informal documents. Notice that no rigid form for documents is enforced; the author is free to use whatever document creating utilities have been provided, and to innovate as needed. So our discussion reduces to one about term editing generally.
structure editing The resident editor is a visually oriented structure editor [63]. It is a structure editor rather than a text editor because we edit the abstractly represented term directly rather than a string of characters that gets parsed into a term. The editor is visually oriented in that the interpretation of most edit commands depends not only upon the abstract term structure, but also, of course, on the display forms in use.
some conventional notational devices supported by Nuprl It often happens that when you develop a body of mathematics, you find you have implicitly parameterized it by one or more variables held fixed throughout large expressions. In Nuprl, these implicit parameters would fill actual argument places in the underlying term, but you would be able to declare contexts in which these argument places would be elided during display when the places are filled by the implicit variable, and would show if filled by some other expression.
Another conventional notational device is to abbreviate the display of certain iterated operators.
The last conventional device we shall describe here is for notations where a single variable is, in a sense that can be made precise, both free and bound. We call it the ``ddx'' device since it is most familiar in the Leibniz notation for derivative, as in the expression df(x)/dx + x. In the expression df(x)/dx, the variable x is clearly binding the scope f(x), but the value of df(x)/dx is the derivative evaluated at whatever value x has. In Nuprl, df(x)/dx is explained as a notational abbreviation for the special case of df(x)/dx|x=E in which the variable x itself fills the place of E, and df(x)/dx|x=E is defined as the value of the derivative evaluated at E. In df(x)/dx|x=E, x is simply used as a binding variable, and E is just an ordinary argument.
Just to demonstrate that the ``ddx'' device is not unique to derivative notation, consider the proposition
As in the derivative example, the variable f binds the scope
P(f), and yet it is free in the expression
``f is the only such that P(f)'' as a
whole.
Again, we explain this expression as an abbreviation for
in the special case that the variable f itself occurs in the place of E. The larger point is that we respect conventional notations, which we must suppose have often developed for good reason. When we can, and can afford to, we try to adopt conventional devices into our system. The obstacles in any case are figuring out how the notation works, and determining whether it is compatible with prior systematic constraints on formal expression we have established for Nuprl.