Practical Foundations of Mathematics

Paul Taylor

3.3  Fixed Points and Partial Functions

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 non-termination 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³(^) º T(T(T(^))).

In general, Tⁿ⁺¹(^) 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

(a)

The empty relation is the least partial function, called ^.

(b)

Any total function is maximal (Definition  3.2.1(e)), but not greatest (unless X = Æ or Y = 1). Total functions at higher types, as in Convention  2.3.2, are not, however, characterised by maximality.

(c)

Any inhabited set of partial functions has a meet; its support is the set of elements on which all the partial functions are defined and agree, and it takes the agreed values there.

(d)

Any set of partial functions which pairwise agree on their common support has a join in the extension order; its support is the union of the supports and it takes the same value at an argument as any (and hence all) of the partial functions which are defined there. See Exercise  3.21 for a notion of domain based on this fact. []

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) = {y|x 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. Function-types 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₁\sqsubseteq x₂. Otherwise providing the information that x₂ does beyond that provided by x₁ would result in retracting the guarantees which f(x₁) 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 sub-program 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_nTⁿ(^) 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ⁿ is monotone it follows that

DEFINITION 3.3.9 A poset X is w-complete 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 w-complete posets is w-continuous if it preserves all such joins.

EXAMPLE 3.3.10 The poset [N® LiftN] of partial endofunctions of N is w-complete, by Lemma  3.3.5(d). Any functional T:[N® LiftN]® [N® LiftN] which codes a recursive program is, in fact, w-continuous.

PROPOSITION 3.3.11 Let X be an w-complete poset which has a least element ^ and let T:X® X be an w-continuous function. Then the join Ú_nTⁿ(^) exists, is a fixed point of T and is indeed the least such.

PROOF:

(a)

We have already observed that n® Tⁿ(^) is an w-sequence, so the join exists.

(b)

The sequence n® T(Tⁿ(^)) = Tⁿ⁺¹(^) is the same as n® Tⁿ(^), apart from the missing T⁰(^) = ^, but this does not affect the join.

(c)

Since T preserves joins of w-sequences, T(Ú_nTⁿ (^)) = Ú_nTⁿ⁺¹(^), so this is a fixed point.

(d)

If T(q) = q then Tⁿ(^) £ q by induction on n (since if Tⁿ(^) £ q then Tⁿ⁺¹(^) £ T(q) = q), so Ú_nTⁿ(^) £ q. []

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)] ² = {(x,y)|x²+y² £ 1} Ì R² 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.