Also see Evaluation for supplementary material.

Figure shows the terms of
.
Variables are terms, although since they are not closed they are not executable.
Variables are written as identifiers, with
distinct identifiers indicating distinct variables.
Nonnegative integers are written
in standard decimal notation. There is
no way to write a negative
integer in
; the best one can do is to write a noncanonical
term, such as ` -5`, which evaluates to a negative integer.
Atom constants are written as character strings enclosed in
double quotes, with distinct strings indicating distinct atom constants.

The free occurrences of a variable **x**
in a term **t** are the occurrences
of **x** which either * are* **t** or are free in the immediate subterms of **t**,
excepting those occurrences of **x** which become * bound*
in **t**. In figure
the variables written below the terms indicate which variable
occurrences become bound; some examples are explained below.

- In
**x**:**A**#**B****x**in front of the colon becomes bound and any free occurrences of**x**in**B**become bound. The free occurrences of variables in**x**:**A**#**B****A**and all the free occurrences of variables in**B**except for**x**. - In
`<`no variable occurrences become bound; hence, the free occurrences of variables in**a**,**b**>`<`are those of**a**,**b**>**a**and those of**b**. - In
`spread(`the**s**;**x**,**y**.**t**)**x**and**y**in front of the dot and any free occurrences of**x**or**y**in**t**become bound.

Parentheses may be used freely around terms and often must be used to resolve ambiguous notations correctly. Figure gives the relative precedences and associativities of operators.

The closed terms above the dotted line in figure are the
canonical terms, while the closed terms below it
are the noncanonical terms. Note that
carets appear below most of the noncanonical forms; these indicate the
* principal argument places* of those
terms. This notion is used in the
evaluation procedure below. Certain terms are
designated as * redices* , and each redex has a
unique * contractum* .
Figure shows all redices and their contracta.

The evaluation procedure is as follows.
Given a (closed) term **t**,

- If
**t**is canonical then the procedure terminates with result**t**. - Otherwise, execute the evaluation procedure on each
principal argument of
**t**, and if each has a value, replace the principal arguments of**t**by their respective values; call this term**s**. - If
**s**is a redex then the procedure for evaluating**t**is continued by evaluating the contractum of**s**. - If
**s**is not a redex then the procedure is terminated without result;**t**has no value.

Thu Sep 14 08:45:18 EDT 1995