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 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

`>`

`\`

`[`

`]`

`{`

`}->`

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

has domain

In our notation

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

Thu Sep 14 08:45:18 EDT 1995