Also see Evaluation for supplementary material.


next up previous contents index
Next: The Type System Up: Semantics Previous: Substitution

The Computation System

Figure gif 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.gif 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 gif 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 gif gives the relative  precedences and associativities  of operators.

  
Figure: Operator Precedence

 

The closed terms above the dotted line in figure gif 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 gif 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 up previous contents index
Next: The Type System Up: Semantics Previous: Substitution



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