Terms

Recall that terms have the form

$$op(\bar{v}_1.t_1; \ldots; \bar{v}_n.t_n)$$

where op is an operator. Operators actually have structure because some of them come in families. For example, universes (displayed as ${\sf U_i}$) are nullary operators indexed by natural numbers. Generally an operator has the form

$$o\{i:f\}$$

where o is an operator name, and i:f is a tagged parameter consisting of $index f\!amily, f$. For universes, the operator is

$${\sf univ\{i:nat\}.}$$

To reflect operators, we need to reflect operator names and index families. The $index f\!amilies$ include opname, ifname, var, nat. There are others. In order to specify the type representing these families, we need the new type constructor IFam(x); if x represents an index family name, then IFam(x) is a type representing the corresponding family. For example, IFam(ifid(nat)) is the type $\{z:{\sf int} \vert 0\leq z\}$.

Notice, we need an operator to represent the index family name; this operator is ifid (``index family id''). It produces an operator name inside Nuprl corresponding to the various index families. In the Nuprl literature, we use these definitions

$$IF\!Name =$$

The primitive type OpName is used to represent the operator names. Its elements look like $opid\{p\}$ for some tagged parameter p. For example, the representation of the opname univ is opid{univ:opname}.

To illustrate the level of precision that we achieve with this machinery, let us look at the official definition of variables. The terms called variables are

$${\sf var\{v:var\}}$$

These are formed with the var operator name indexed by elements from a mathematical class, an index family (also named var). At this level, we could choose any discrete mathematical class for var, say character strings. To be precise, we say that var is the class of finite sequences of variable characters. We require a subset of the ASCII characters as specified in the Nuprl manual.

Now to represent the variables inside Nuprl, we choose one of the Nuprl types that will represent this index family, and axiomatize it to be equal to IFam(ifid(var)). We have chosen to represent the variable characters by the type N₂₅₆, natural numbers from to 256. Variables are lists of these. The definition and axioms are

Let us take a closer look at OpName. This is a new type. What are its elements? Intuitively the elements are the terms that represent the actual operator names. Here are some of those names.

operator           representation   

We use the convention that opid{x} stands for opid{x:opname}. This can be done for any fixed number of operator names because we can specify in the definition which index family is associated with which parameter. So in practice, we can eliminate the tags. They are needed to deal with the open-ended nature of the class OpName. This type must be open-ended because the mathematical class of actual operator names is open-ended.

The operator opid{x} produces canonical values. These are terms that evaluate to themselves.

Here is the official definition of Term.

Definition

$$\times$$

This tells us everything we need to know about terms. From the inductive type definition we get a recursor defining objects inductively over Term and we get an induction principle.

The small theory of the lambda calculus can be seen as a special case of a theory of Term if we just take these definitions and display forms.

$$<<{\sf opid\{var\}}, [a_1, \ldots, a_n]\gt, {\sf nil}\gt as \ implode([a_1, \ldots, a_n])$$ Display

where $[a_1, \ldots, a_n]$ is a notation for lists and implode takes a list of characters to an atom.