Display Forms

We describe here our notion of a display form .

A display form definition  associates a chunk of notation with a term. For example consider the term add(x;y) for binary addition. The usual notation for this is to use an infix + . We could write the notation chunk as:

where the 's are holes for the two subterms, and the outer box shows the extent of the chunk. We call these holes term slots  because in they can be filled by terms. Later on we shall encounter text slots  which can only be filled with text strings. Usually we need to indicate how term slots correspond to the logical subterms of a term so we label term slots. For example, the definition of the notation chunk for add(x;y) can be written:

add(x; y)

Here, we read as saying that a is defined as the atomic notation chunk or display form for b. Throughout this section, we use rectangular boxes to delimit terms and term slots.

Term slots stretch to accomodate the terms inserted in them. For example say we have the term mul(1;2) which is displayed as 1 * 2 . Then the term add(mul(1;2);3) will be displayed as:

Nuprl automatically adds parentheses according to display form precedences. When a display form of lower precedence  is inserted into the slot of display form with higher precedence, parentheses are automatically inserted to delimit the slot. For example, we assign the display form for mul(x;y a higher precedence than the display form for add(x;y). The term add(mul(1;2);3) is displayed as

1 * 2 + 3

but the term mul(1;add(2;3)) is displayed as 1 * (2 + 3)

Let us move on to a more complicated display form; that for universal quantification  . The term all(T;x.P)  means that ``for all x of type T, the proposition P is true''. Note that the term all(T;x.P) binds free occurrences of x in P. We would normally write all(T;x.P) as

x:T. P

The display form definition for the all(T;x.P) could be written as:

all(T; x.P)

Here, 0pt[12pt][4pt]

is used to indicate a text slot. A text slot is filled with a text string rather than a term. Text slots are used for term parameter values, and binding variables.

A few more display form definitions are:

1. exists(T; x.P)

2. equal_int(x; y)

3. variable{x:v}

4. natural_number{i:n}

The last two display form definitions are rather special; 3 is the display form definition for variable terms, and 4 is the display form definition for natural numbers. Both the display forms defined for these terms have only a single text slot, and no other printing or whitespace  characters.

Using these display forms the term

all(int(); i.exists(int(); j.equal(int(); j; add(i;1))))

has the notation:

or leaving out the bounding boxes and circles for the slots and the term as a whole:

i: . j: . j = i + 1

In general, a display form for a term is made up of 0 or more text and term slots, interspersed with printing and space characters. We can annotate display forms with whitespace formatting  commands which specify where linebreaks  can be inserted, and how to control indentation  . Chapter describes in detail the structure and appearance of the display form definitions which are contained in display objects in Nuprl theories. Chapter also contains information on how to set precedences, and how to control how precedence affects parenthesization  .

The notation for some term tree is built up from the display forms associated with each node of the tree --- so the structure of the notation mirrors the structure of the term, and it makes sense to talk about the display form tree  of a term.

The display form tree is the tree structure that you edit with Nuprl's term editor. Nuprl takes care of translating back-and-forth between the two kinds of trees. In a display form tree, each display form and each slot is considered a node of the tree If a text (term) slot is not empty, it is identified with text string (display form) filling it. All the slots of a display form are considered to be the immediate children of the display form. The editor considers slots ordered in the order they appear, left to right, in display form definitions, not in the order in which they occur in the uniform syntax.

In most of this manual, we refer to terms by their display notation rather than their uniform syntax, unless we want to emphasize their logical structure. Also, in talking the term editor, we talk informally about nodes of terms, when we are referring to nodes of the corresponding display-form trees.

When one enters a new terms using Nuprl's structured editor, one most often enters the term in a top-down fashion, starting with the root of the term tree and working on down to the leaves. This means that one has to work with incomplete terms . For example, at an intermediate stage of entering the term

i: . j: . j = i + 1

you might be presented with term:

i: . [var]:[type]. [prop].

Here [var], [type] and [prop] are place-holders for slots. [var] is a place-holder  for a text slot, and [type] and prop are place-holders for term slots. If a slot has a place-holder, we say that the slot is empty, or uninstantiated . The labels which appear in the place-holders for a display form (the var, type or prop in the example above) are controlled by the display form's definition. If a text (term) slot contains a a text string (term) we say that slot is filled  or instantiated . If a display form has no uninstantiated slots, then it is considered complete . Placeholders re-appear when the contents of slots are removed.