Definition 2.5.1 described the paradigm for recursive programs, which we studied assuming that they terminate and so define total functions. Because of the Halting Problem there is no way to guarantee this by imposing conditions on programming languages without destroying their expressive power.
Taking a different attitude, we may accept nontermination as a first class value. By extending the domain of mathematical values which the two sides may be understood to have, we may then treat recursive definitions of programs as equations.
EXAMPLE 3.3.1 Consider the program


REMARK 3.3.2 Any recursive program nevertheless has a well defined, albeit partial, de facto meaning. When the program is given a particular argument, say 2, what the machine actually executes is
fact 2 = if2 = 0 then1 else2*(if1 = 0 then1
else1*(if0 = 0 then1 else u fi ) fi ) fi
where u never gets called. So it may be anything  for example the program
whileyesdoskipod which goes straight into a tight unending loop. The latter is interpreted as the empty (totally undefined) partial function ^, and the version of the factorial function as executed for the argument 2 is T^{3}(^) º T(T(T(^))).
In general, T^{n+1}(^) suffices to give fact(n). Intuitively, the programs

The poset of partial functions Agreement of total functions is all or nothing, but two partial functions (Definition 1.3.1(b)) may agree on the intersection of their supports, whilst one offers more information than the other on some other values.
DEFINITION 3.3.3 Let f,g:X\rightharpoonup Y be partial functions between sets. We write f\sqsubseteq g and say that g extends f if

Partial functions may be expressed by spans of total ones:
DEFINITION 3.3.4 The subset suppf = {x$y.xf® y} Ì X is called the support of f.
omitted diagram environment
Then f\sqsubseteq g iff suppf Ì suppg and f is the restriction of g to suppf. So the inclusion k:suppf\hookrightarrow suppg satisfies i = k;j and f = k;g.
LEMMA 3.3.5 Partial functions X\rightharpoonup Y between sets form a poset under the extension relation. Moreover
Instead of modifying the source of a function we can change its target. The trick we employ to do this is applicable to any relation:
LEMMA 3.3.6 There is a bijection between relations R:X\leftharpoondown \rightharpoonupY and functions \expx R:X® P(Y), defined by \expx R(x) = {yx Ry}. If the relation R is functional, then each subset \expx R(x) has at most one element. []
DEFINITION 3.3.7 The lift or partial function classifier of a set Y is the set of subsets with at most one element:

^ = Æ Î Lift Y.
We tend to identify y Î Y with lifty Î Lift Y. (Classically, Lift Y = YÈ{^}, and we put f(x) = ^ for x Ï supp f.) The lemma restricts to a bijection between partial functions X\rightharpoonup Y and total functions X® Lift Y.
LiftY is the set of partial functions {*}\rightharpoonup Y, and the extension order for these agrees with the inclusion order on subsingleton subsets of Y; we call it the information order. It is rather sparse, being discrete when restricted to Y itself, with ^\sqsubseteq y. Example 3.9.8(c) extends the definition of the lift to the case where there is already an order on Y, Exercise 3.71 shows how to construct it for topological spaces and locales, and Example 9.4.11(a) explains its significance in type theory. Functiontypes in Section 3.5 are typically less ``flat'' than LiftY is.
LEMMA 3.3.8 Partial functions X\rightharpoonup Y extend to functions LiftX® LiftY by

We expect computable functions to be monotone with respect to the information order x_{1}\sqsubseteq x_{2}. Otherwise providing the information that x_{2} does beyond that provided by x_{1} would result in retracting the guarantees which f(x_{1}) has already given about the output.
On the other hand, strictness of a program means that it tries to use the input ( cf Remark 2.3.4 and Example 6.1.10). The input of T is the subprogram u in Remark 3.3.2, which, as we saw, need not be called (used), so in general T(^) ¹ ^.
The fixed point theorem We may define fact as the join \bigsqcup_{n}T^{n}(^) in the poset of partial functions N\rightharpoonup N. It is important to appreciate that the order implicit here is the extension or information order, not the arithmetical one.
Now the poset N\rightharpoonup N does not have all joins, so how can we be sure that this particular join exists? We have ^\sqsubseteq T(^) since ^ is the least element, and then since T^{n} is monotone it follows that

DEFINITION 3.3.9 A poset X is wcomplete if any w sequence, ie any diagram x_{()}:w® X where w is N with the arithmetical order, has a join. A monotone function f:X® Y between wcomplete posets is wcontinuous if it preserves all such joins.
EXAMPLE 3.3.10 The poset [N® LiftN] of partial endofunctions of N is wcomplete, by Lemma 3.3.5(d). Any functional T:[N® LiftN]® [N® LiftN] which codes a recursive program is, in fact, wcontinuous.
PROPOSITION 3.3.11 Let X be an wcomplete poset which has a least element ^ and let T:X® X be an wcontinuous function. Then the join Ú_{n}T^{n}(^) exists, is a fixed point of T and is indeed the least such.
PROOF:
This is often (inaccurately) called Tarski's theorem: the result that Alfred Tarski actually proved (1955, Exercise 3.39) is that any monotone endofunction of a complete lattice has a least fixed point, and indeed a complete lattice of fixed points (see also Proposition 3.7.11ff).
REMARK 3.3.12 Algebraic topology gives other, quite different, reasons why continuous endofunctions of certain spaces must have fixed points: the closed interval [0,1] Ì R and disc [`(B)] ^{2} = {(x,y)x^{2}+y^{2} £ 1} Ì R^{2} are the simplest examples (the former is essentially the intermediate value theorem). The latter is due to Jan Brouwer, which is ironic because such results rely on excluded middle, and the fixed points do not depend continuously on the given endofunction.
Tarski's theorem does assign fixed points continuously  a fact which is crucial to denotational semantics. A traditional fixed point theorem which is more closely related to what we require is that for contraction mappings on a complete metric space (X,d), ie functions f:X® X such that "x, y.d(f(x),f(y)) £ k d(x,y) for some constant 0 £ k < 1. This analogy is closer if the symmetry law, d(x,y) = d(y,x), for metric spaces is dropped, since certain concrete domains can be equipped with such a (pseudo)metric.
We shall return to partial functions in Sections 5.3 and 6.3.