This section introduces the approach we use for entering and displaying terms.
We distinguish between logical structure of terms , and the notation in which terms are presented. When we talk of the logical structure of a term, we are thinking of some abstract object of mathematics. We are not just thinking of the term in uniform syntax, though the regularity of the uniform syntax for a term does reflect the regularity of the underlying abstract object. When we talk of notation, we are thinking of the visual presentation of abstract objects on the printed page, or on the computer screen. When you read mathematical or logical expressions in familiar notation, you often mentally construct the abstract object in your mind so readily that you forget the distinction between abstract structure and notation.
Notation understandable by machines became a focus of study when people started to design programming languages. The languages had to not only be easily understandable by humans, but also easily parseable by machine. The study of notation became the study of regular expressions and grammars. People devised sophisticated techniques for designing parsers.
In the programming language world, source texts in ASCII files correspond to our idea of notation, and abstract-syntax-trees get close to our notion of logical structure.
In mathematics notation is crucial issue. Many mathematical developments have heavily depended on the adoption of some clear notation, and mathematics is made much easier to read by judicious choice of notation. However mathematical notation can be rather complex, and as one might want an interactive theorem prover to support more and more notation, so one might attempt to construct cleverer and cleverer parsers . This approach is inherently problematic. One quickly runs into issues of ambiguity. Often to read mathematical notation one has to be aware of the immediate context it is presented in. A simple example is that juxtaposition of symbols can mean function application in one place and multiplication in another. A notion introduced in programming languages to address ambiguity has been that of overloading operators; one assumes that the type-checker can sort out what is meant, even if the parser cannot. Closely related to this notion, is the notion of implicit coercions . There is also the question of what notation is supported by editors; mathematics presented in ASCII characters is not anywhere as easy to read as mathematics in books and papers.
A half-way solution that is sometimes taken (for example with Mathematica ), is to do what one can with a parseable syntax in ASCII characters for input, and then use pretty-printing routines for formatted output (say in Display PostScript).
The approach which we have taken 
is to
design an editor that presents terms in pretty notation, and groups the
notation in chunks that correspond to parts of the underlying tree structures.
One edits the tree structure directly, so there is no need for a parser.
Such editors are often called structured editors .
The advantages of a structured editor are:
Structured editors do have their disadvantages. The most major one is that they are quite different from conventional text editors such as vi or emacs, and so it can take a while to learn how to use them. We have tried to design the Nuprl editor to reduce this startup time. We welcome suggestions from users for further improvements. Another disadvantage is that you have less control over formatting, since all display formatting is done automatically. Again we have been working to enhance the pretty-printing algorithm that Nuprl uses so that the formatting is acceptable.