next up previous contents index
Next: Domain Predicate Up: Details of the Previous: Details of the

Computation System Modification

The domain predicate captures a call--by--value order of computation, so the entire computation system must be adjusted slightly to reflect this. In particular, computing the value of a function application (total or partial) dictates that function and argument are normalized before beta reduction, both subterms in pairs are normalized, and for injections into disjoint sums the subterm is normalized. In this extension direct computation rules are not present.

To add > types to the logic we add terms

A> B
where f and x range over variables and a,b,t,A and B range over terms. When closed, the first two kinds of terms are canonical, and the last two are noncanonical.

Let stand for fix(f,x.b) henceforth. Each closed term [a]\ is a redex with contractum , and each closed term dom()\ is a redex with contractum

\x. rec(,x.b; ;x),
where is defined below. The rule for binding variables is as follows.

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