Also see Evaluation for supplementary material.     Next: The Type System Up: Semantics Previous: Substitution

## The Computation System

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. Figure: Terms

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 the 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 are all the free occurrences of variables in A and all the free occurrences of variables in B except for x.
• In <a,b> no variable occurrences become bound; hence, the free occurrences of variables in <a,b> are those of a and those of b.
• In spread(s;x,y.t) the 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. 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,

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.     Next: The Type System Up: Semantics Previous: Substitution

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995