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.
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.
Figure: Operator Precedence
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.
Figure: Redices and Contracta
The evaluation procedure is as follows. Given a (closed) term t,