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

wherefix(f,x.b)

A`>`

B

dom(t)

t`[`

a`]`

Let stand for ` fix( f,x.b)` henceforth.
Each closed term

where is defined below. The rule for binding variables is as follows.`\`

x.rec(,,x.b; ;x)

- In
`fix(`, the**f**,**x**.**b**)**f**and**x**in front of the dot and any free occurrences of**f**or**x**in**b**become bound.

Thu Sep 14 08:45:18 EDT 1995