This approach to partial functions has not been retained in standard Nuprl developments. See Recursive Functions for more current practice.


next up previous contents index
Next: Details of the Up: Recursive Definition Previous: Example Proof

Partial Function Types

We handle partial functions by viewing them as total functions over their domains of convergence. To do so we introduce dom terms, which capture the notion of a domain of convergence. Thus, for a partial function application to be sensible one must prove that the domain of convergence predicate is true for the argument, i.e., that the argument is in the domain of convergence of the function. The introduction of dom terms introduces additional proof obligations into the rules for reasoning about partial functions.

As an example, the partial function producing the smallest root of f,

has a domain of convergence defined by the predicate as follows.
Thus is a total function in .

In our notation the type of partial  

functions from A to B is A> B , the application of partial function f to a is written f[a], recursive functions are expressed as terms of the form fix(f,x.b), so function of the preceding example is

     MU == fix(mu,x. int_eq(f(x); 0; x; mu[x+1])),
and is dom(MU)  , an elim form which turns out to have value
     \x.rec(mu',x. int_eq(f(x); 0; true; mu(x+1)); MU; x).
The domain  predicate is derived later; in general, if A> B then \[x] {x :A |dom(f)(x)}->B.

As a second example, the ``91'' function,

has domain
In our notation F and are
     91== fix(F,x. less(100; x; x-10; F[F[x+11]])

     \x.rec(F',x. 
        less(100; x; true; c:F'(x+11)#F'(F[x+11]); 91; x)
Notice that the rec forms defined in the preceding section must be extended to include the simultaneous definition of the recursive function. The new proof rules for these rec terms are only slight variants of the given rules, so they are not listed here.



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