functions We have chosen to illustrate the underlying body of formal mathematics on a fragment of the basic theory of functions. The fragment commonly appears in textbooks on discrete mathematics CHECK:[2][37][36]. This is a topic for which very good formalizations exist in the sense that informal methods can be faithfully formalized without prematurely introducing distracting details of logic. COMPARE WITH OLD
Nuprl library example A Nuprl library is a sequence of various kinds of objects, including definitions, theorems and comments. Libraries are divided into sections called theories. Here we give a partial listing of a Nuprl theory covering covering basic facts about functions, showing the definitions and theorems. Below we shall show how a student would access this material via explanatory material; here we just show the kind of formal data in which such material is grounded.
We begin with a few fundamentals before introducing new concepts. In the lines below, the T at the line start indicates that this object is a (potential) theorem. The * before the T shows that the theorem has been completely proven. (If the proof is not complete, the * is replaced by a # character).
The first of these expresses the fact that identity on functions depends only on input/output, the second is the axiom of choice, and the third is the weaker claim that a function is determined by describing how a unique output is related to each input. The definition of two functions being `inverses' is:
Here, the * shows that the object is complete and the A shows that this is an abstraction, Nuprl's name for a definition. Next are a couple of basic theorems about inverse functions, namely that an inverse of a function has that function as its inverse, and that a function can have at most one inverse.
Here are the definitions of `injection', `surjection', and `bijection', and some standard theorems:
The concept of one-to-one correspondence is defined in terms of inverse, and is shown equivalent to bijection.
A lesson about one-to-one correspondence and these definitions may be found below. We'll end this sampling of the library with the concept of function composition. These definitions define a function symbol by showing how to rewrite the application of the function symbol to a generic argument.
= 1\>EDIT COM Divisibility program*
Let us examine what a mixed formal and informal hypertext lesson is
like. This is the essence of the new courseware. It is intended to
be read with Nuprl's interactive editor, which will be described in
section 
. A typical lesson consists of pages linked
together by hypertext pointers and refers to various expressions,
definitions, and theorems.
As is usual for a hypertext-style document, links to other document pages are embedded in the text. For example, the buttons indicated by NEXT and LAST will raise the next and last pages of this document for viewing. Other buttons link to various supplemental documents.
A particularly useful variation of these links is exemplified by the line
Each operator definition is stored in an object. The author could simply have copied the contents of the definition into the lesson, but it would be unreliable to do so since the object might be changed later. Instead the author inserted a link to the definition and selected a kind of link that would display the contents of the object in place. Like the buttons mentioned above, this is simply a reference to an object, in this case the object that defines divisibility, and if the user really needs to view the object directly, clicking on this link will raise the object. Similarly clicking on a link to a theorem opens the indicated proof for viewing.
But there is another kind of link, or inter-object reference, between objects of the system, which we call implicit. The definition of any operator is accessible through any occurrences of the operator throughout the system. This is true not only for the formally meaningful objects of the system, such as definitions and proofs, but also for objects such as document pages. If you were to examine an occurrence of ``a | b'' with the interactive browser, you would find that it is not simply text, but rather, is actually a term of the formal language, namely, the same divisibility predicate whose definition is shown in the document, applied to the mathematical variables ``a'' and ``b''. So, the mere fact that this operator appears in the document means there is an implicit link to the definition of the operator.
It is also possible to informally discuss an equation such as
However, although the text about the equation is informal, the equation itself is fully formal - the user can interactively examine it, and view any definitions of the operators used in it by clicking appropriately on their occurrences. (Of course, the equation could have been proved formally had the author found it worthwhile.)
The point is that one can be as formal as desired in a document, and when formally defined operators are used, access to their definitions is automatic. (Conversely, it is possible to annotate formally meaningful expressions with hypertext commentary which makes no formal contribution to the meaning.)
We'll conclude this discussion with some observations about other easily realized techniques. Assuming that the student has gone beyond interactive reading, and has learned to edit Nuprl objects, the instructor can not only assign exercises in the text, but can also provide a link to worksheets prepared for the exercises. Further, students would be able to create their own documents, such as homework, formalizing what they are able to and explaining the rest informally.
Also, since Nuprl is implemented in a way that lets it start up non-Nuprl processes, it is possible to effectively refer to on-line documentation that is not part of Nuprl, such as technical reports and manuals. By effective here we mean that clicking on it will initiate an appropriate independent reader of the external document. For instance, a document may refer to a page of an on-line document in such a way that clicking on it would initiate an independent reader such as xdvi on that document. For a class, a suitable application would be references to an on-line textbook to which we want to relate our formal material.