Details

Terms are implemented in the current Nuprl system in Lisp. You should rarely have to work with terms at the Lisp level. Rather you either use the term editor to view and edit terms, or a set of term-related functions in ML.

We describe here the the current parameter types  , the acceptable strings for opids, parameters, and variables, and the implementation of these strings from the ML point of view.

The current parameter types and associated values are:

natural

natural  numbers (including 0). Implemented using ML type int. Acceptable strings are generated by the regular expression .

token

character strings.  Implemented using ML type tok. Acceptable strings can draw from any non-control characters in Nuprl's font.

string

character strings.  Implemented using ML type string. Acceptable strings can draw from any non-control characters in Nuprl's font.

variable

Names of variables  .  Implemented using ML type var. Acceptable strings draw on the alphabet a-zA-Z0-9_-% . The % character

has a special use. See Section . The empty string is not an acceptable name for a variable parameter.

level-expression 

Universe level expressions . These are used to index universe  levels in Nuprl's type theory. Implemented using ML type level_exp . The syntax of level expressions is described in Section .

The names of parameter types are usually abbreviated to their first letters.

Opids are character strings drawn from the alphabet a-zA-Z0-9_-! . (Here - is the ASCII 

character, x-y indicates the characters from x to y inclusive.) An ! at the start of a character string indicates that the term does not belong to Nuprl's object language. Opids are implemented using ML type tokindexML type tok .

Binding variables  are character strings drawn from the same alphabet as variable parameters. In addition, the empty string  can be used. We call the binding variable with the empty string as its name, the null variable . Null variables can never bind. Binding variables are implemented using ML type var .

Earlier, when we described the term type, we said that variables were considered to be terms. This was a slight simplification of the actual state of affairs; In Nuprl, we consider variables and terms to be distinct. We have a special term kind, variable{v}  for injecting  variables into the term type. So when we talk of the variable foo as a term, we are really thinking of the term variable{foo:v}. When we write terms, this injection if often implicit. So for example, we write bar(x;y) instead of bar(variable{x:v}; variable{y:v}).

We often assume a similar implicit injection for natural numbers. So for example, the term bar(10;11) when written out in full is the term bar(natural_number{10:n}; natural_number{11:n}).

Some examples of terms in both pretty and plain notation are shown in Table .

  
Table: Examples of term notation