# Introduction

Recursive definitions of functions (and processes as we well see later) are

fixpoint equations. The simple example of the recursive definiton of the

factorial function can be used to illustrate this fact.

fact(n:NATURAL): NATURAL ensure Result = if n=0 then 1 else n*fact(n-1) end end

This definition is equivalent to the following assertion.

fact_all: all(n:NATURAL) ensure fact(n) = if n=0 then 1 else n*fact(n-1) end end

This shows the function ‘fact’ appearing on the left hand side and the right

hand side of an equation. In order to see the fixpoint equation better we

derive the function ‘f’ from the definition of ‘fact’.

f(g:NATURAL->NATURAL): NATURAL->NATURAL ensure Result = (n -> if n=0 then 1 else n*g(n-1) end) end

The function ‘f’ transforms any function of type NATURAL->NATURAL to a

function of the same type. Using ‘f’ we can see that the function ‘fact’ has

to satisfy the fixpoint equation

fact_fix: fact = f(fact)

Expanding the definition of ‘f’ and using equality of functions it is evident

that ‘fact_fix’ and ‘fact_all’ are the same assertion.

Mathematically the following question arises: Does the function ‘f’ have

fixpoints? If yes, is the fixpoint unique? If the answer to both questions is

yes, then the fixpoint equation ”fact=f(fact)’ defines the function ‘fact’.

In this article we investigate the question if a function ‘f’ has

fixpoints. The outline of the developed thoughts is the following.

Having a function ‘f’ we can try any element ‘a’ in its domain (in the case of

the example the element is itself a function) and feed it into the function to

get ‘f(a)’. As long as the result is within the domain of ‘f’ we can iterate

this procedure getting the set

cl = {a, f(a), f(f(a)), f(f(f(a))), ... }

The procedure stops if we encounter a fixpoint or an element not in the domain

of ‘f’. The set ‘cl’ is obtained by the closure operation

cl = a.closed(f)

If we are in the domain of a partial order (and the type A->B is a partial

order) and we start at an element ‘a’ where the function ‘f’ is increasing,

then the sequence ‘a, f(a), f(f(a)), …’ is increasing. If ‘a’ is the least

element and is in the domain of ‘f’ this condition is satisfied.

I.e. if we feed the completely undefined function ‘0:NATURAL->NATURAL’ into

‘f’ we get the sequence

cl = {0, f(0), f(f(0)), f(f(f(0))), ... }

For the above example of the factorial we get the following set of functions

(representing functions as a set of key-value pairs).

cl = { {} -- The undefined function {0 -> 1} -- Function defined for one argument {0 -> 1, 1 -> 1} {0 -> 1, 1 -> 1, 2 -> 2} {0 -> 1, 1 -> 1, 2 -> 2, 3 -> 6} {0 -> 1, 1 -> 1, 2 -> 2, 3 -> 6, 4 -> 24} ... }

At each iteration we get a ‘better’ approximation of the factorial

function. It is intuitively clear that this set ‘coverges’ in some sense to the

desired factorial function.

In the following chapters we are going to prove the following facts about such

a closure for the domain of a partial order.

-- module: partial_order feature all(a,c:CURRENT, f:CURRENT->CURRENT) require f.is_monotonic a in f.domain => a in f.prefixpoints ensure a.closed(f) * f.domain <= f.prefixpoints a.is_least(a.closed(f)) a.closed(f).is_chain (some(c) c.is_greatest(a.closed(f)) => a.closed(f).is_finite all(c) c.is_greatest(a.closed(f)) = (c in f.domain => c in f.fixpoints) end -- Note: f.prefixpoints = {x: x in f.domain and x<=f(x)} end

We can phrase the content of the theorems as follows: If the function is

monotonic and the start point is either not in domain of the function or is a

prefixpoint of the function then

– all elements in the closure which are in the domain are prefixpoints as

well

– the start point is the least element of the closure

– the closure is a chain (i.e. all elements ‘a’, ‘b’ of the closure are

related in the sense that ‘a<=b or b<=a’ is valid)

– the existence of a greatest element of the closure implies that the closure

is finite

– the greatest element of the closure (if it exists) is either not in the

domain or it is a fixpoint

If we switch from partial orders to upcomplete partial orders we get the

following stronger results.

-- module: upcomplete_partial_order feature all(f:CURRENT->CURRENT) require f.is_continuous -- 'f' preserves suprema f.domain.is_limitclosed -- Domain is sufficiently large f.prefixpoints /= 0 ensure f.fixpoints /= 0 end end

This law states that any continuous function with sufficiently large domain

having prefixpoints is guaranteed to have fixpoints.

# Closed sets and induction

## Basics

If we have a function ‘f:A->A’ we can apply the function to an argument ‘a’

of type A within its domain and get ‘f(a)’ which is as well of type A. If

‘f(a)’ is in the domain of ‘f’ we can reapply the function getting

‘f(f(a))’. Iterating this procedure we get the set

{a, f(a), f(f(a)), f(f(f(a))), ... }

As long as the result remains in the domain of ‘f’ we can repeat this

procedure forever. We call a set ‘p’ closed under ‘f’ if ‘f’ applied to any of

its members does not leave the set.

Closures have been described in detail in the article “Complete lattices and

closure systems”. Let us repeat some of the results.

local A: ANY feature -- Closed sets and induction

A set ‘p’ is closed under ‘f’ if its image under ‘f’ is a subset of ‘p’.

is_closed(p:A?, f:A->A): ghost BOOLEAN ensure Result = p.image(f) <= p end

The collection of all sets closed under ‘f’ are a closure system.

all(f:A->A) ensure {p:A?: p.is_closed(f)}.is_closure_system end

Being a closure system means that the intersection (aka infimum) of any

collection of closed sets is closed. We can close any set (therefore any one

element set as well) with respect to this closure system. The closure of a set

‘p’ under the function ‘f’ is the least set containing ‘p’ which is closed

under the function ‘f’.

closed(p:A?, f:A->A): ghost A? -- The set `p' closed under the function `f' ensure Result = ({q:A?: p<=q}*{q:A?: q.is_closed(f)}).infimum end closed(a:A, f:A->A): ghost A? -- The one element set {a} closed under the function `f' ensure Result = {a}.closed(f) end

Remember that {q:A?: p<=q} is the set of all sets containing ‘p’. The

expression ‘p.closed(f)’ selects the intersection of all supersets of ‘p’ with

the closed sets. Because the closed sets form a closure system it is

guaranteed that this intersection is closed.

The function ‘closed’ has some nice properties.

all(p,q:A?, f:A->A) ensure closure_1: p.closed(f).is_closed(f) closure_2: p.is_closed(f) => p = p.closed(f) ascending: p <= p.closed(f) monotonic: p <= q => p.closed(f) <= q.closed(f) idempotent: p.closed(f).closed(f) = p.closed(f) end

These rules say that the set generated by ‘p.closed(f)’ is really closed and

every closed set can be obtained by applying the function ‘closed’. The

function ‘closed’ is ascending, monotonic and idempotent.

## Subclosure

Whenever we close any element ‘a’ under ‘f’, i.e. forming ‘a.closed(f)’ we can

be sure that the closure of any member of ‘a.closed(f)’ is completely

contained in ‘a.closed(f)’. This claim can be proved by

subclosure: all(a,b:A, f:A->A) require r1: b in a.closed(f) check c1: {b} <= a.closed(f) -- r1 c2: {b}.closed(f) <= a.closed(f).closed(f) -- c1,closure is -- monotonic ensure b.closed(f) <= a.closed(f) -- c2, closure is -- idempotent end

## Decomposition of a closure

Another quite useful law allows us to decompose a closure.

closure_decomposition: all(p:A?, f:A->A?) ensure p + p.image(f).closed(r) = p.closed(f) end

We prove the forward and backward direction separately.

closure_decomposition_fwd: all(p:A?, f:A->A) check c1: p <= p.closed(f) -- closure is increasing c2: p.image(f) <= p.closed(f) -- closure is closed and contains 'p', -- therefore p.image(f) as well c3: p.image(f).closed(f) <= p.closed(f) -- c2,monotonic,idempotent ensure p + p.image(f).closed(f) <= p.closed(f) -- c1,c3 end

closure_decomposition_bwd: all(p:A?, f:A->A) local r1: pic = p.image(f).closed(f) check c1: p <= p + pic c2: (p+pic).image(f) = p.image(f) + pic.image(f) -- image distributes over union c3: p.image(f) <= pic -- r1, closure is increasing c4: pic.image(f) <= pic -- r1, pic is closed c5: p.image(f) + pic.image(f) <= pic -- c3,c4 c6: (p+pic).image(f) <= pic -- c2,c5 c7: (p+pic).image(f) <= p+pic -- c6 c8: (p+pic).is_closed(f) -- c7, def 'is_closed' c9: p.closed(f) <= p+pic -- c1,c8, closure is -- least set ensure p.closed(f) <= p + p.image(f).closed(f) -- c9,r1 end

## Induction

In order to proof that all members of a closed set ‘p.closed(f)’ satisfy a

certain property we can use the following induction principle.

induction: all(p,q:A?, f:A->A) require p <= q q.is_closed(f) ensure p.closed(f) <= q end

We can apply this principle by defining a set ‘q’ whose elements have the

desired property. In order to prove that all elements of ‘p.closed(f)’ have

this property we need to prove that all members of ‘p’ have this property and

that the set ‘q’ is closed under ‘f’.

We can prove this induction principle with the following reasoning.

all(p,q:A?, f:A->A) require r1: p <= q r2: q.is_closed(f) check c1: p.closed(f) <= q.closed(f) -- r1, monotonic ensure p.closed(f) <= q -- c1, closure_2 end

end -- Closed sets and induction

# Fixpoints

An element ‘a’ is a fixpoint of the function ‘f’ if it is in the domain of ‘f’

and ‘a=f(a)’ is valid.

local A: ANY feature -- Fixpoints fixpoints(f:A->A): ghost A? -- The set of fixpoints of `f'. ensure Result = {a: a in f.domain and a=f(a)} end end -- Fixpoints

By definition all fixpoints are in the domain of the function.

In the domain of a partial order we can define prefixpoints and postfixpoints.

local A: PARTIAL_ORDER feature -- Pre- and postfixpoints prefixpoints(f:A->A): ghost A? -- The set of prefixpoints of `f'. ensure Result = {a: a in f.domain and a <= f(a)} end postfixpoints(f:A->A): ghost A? -- The set of postfixpoints of `f'. ensure Result = {a: a in f.domain and f(a) <= a} end end

The set of prefixpoints is the part of the domain where the function is

ascending and the set of postfixpoints is the part of the domain where the

function is descending. Clearly a fixpoint must be a prefixpoint and a

postfixpoint i.e. ‘f.fixpoints = f.prefixpoints*f.postfixpoints’.

# Injections and finite sets

local A,B: ANY feature -- Injections and finite sets

An injective function is one-to-one

is_injective(f:A->B): ghost BOOLEAN -- Is the function `f' one-to-one ensure Result = all(a,b:A) require {a,b} <= f.domain f(a) = f(b) ensure a = b end end

Clearly every domain restriction of an injective function is again an

injective function

all(p:A?, f,g:A->B) require f.is_injective ensure g <= f => g.is_injective (p<:f).is_injective end

A set ‘p:A?’ is finite if all functions mapping ‘p’ to a proper subset of ‘p’

are not injective.

is_finite(p:A?): ghost BOOLEAN ensure Result = all(f:A->A) require f.domain = p f.range < p ensure not f.is_injective end end

This definition is sometimes illustrated as the pigeonhole principle. Imagine

n pigeonholes and n+m pidgins where ‘m>0’. If all the n+m pigeons are in the

n pidgoenholes then at least one pigeonhole has more than one pigeon.

The set {i: i<n} is definitely a proper subset of {i: i<n+m}. If all pigeons

fly into the holes we have a mapping from the set of pigeons {i: i<n+m} to

the set of pigeonholes {i: i<n}. The fact that there is at least one hole

with more than one pigeon expresses the fact that the mapping cannot be

one-to-one.

Let us demonstrate that this definition of finiteness is inline with our

intuition about finiteness. First of all we expect the empty set to be finite.

all(p:A?) require r1: p = 0 check all(f:A->A) require r2: f.domain = p r3: f.range < p check c1: f.range <= 0 -- r3 c2: f.range /= 0 -- r3 c3: f.range = 0 -- c1, 0 is least element ensure not f.is_injective -- c2,c3, contradiction end ensure p.is_finite end

Furtermore we expect if we add an element ‘a’ to finite set ‘p’ that the set

remains finite.

We prove this by assuming the opposite i.e. ‘p+{a}’ is not finite. Then there

exists an injective function which maps its domain to a proper subset. The

domain restriction to ‘p’ yields an injective function which maps ‘p’ to a

proper subset of ‘p’. Since ‘p’ is finite such a map must not exist therefore

we have a contradiction.

all(a:A, p:A?) require r1: p.is_finite r2: a /in p check c0: require r3: not (p + {a}).is_finite check c1: some(f:A->A) f.domain = p+{a} and f.range < f.domain and f.is_injective c2: all(f:A->A) require r4: f.domain = p + {a} r5: f.range < f.domain r6: f.is_injective local r7: g = p<:f check c3: g.is_injective -- r7,r6 c4: g.domain = p -- r4,r7 c5: g.range = f.range - {f(a)} -- r4,r7 c6: f.range - {f(a)} < f.domain - {a} -- r4,r6 c7: g.range < g.domain -- c5,c6,r4 c8: not g.is_injective -- c4,c7,r1 ensure False -- c3,c8, contradiction end ensure False -- c1,c2 end ensure (p + {a}).is_finite -- c0 end

end -- Injections and finite sets

# Closures in partial orders

All code of this chapter is understood to be in the module ‘partial_order’,

i.e. the type CURRENT stands for any type which represents a partial order.

-- module: partial_order feature -- Generated sets

We investigate sets generated by the expression ‘a.closed(f)’ where ‘a’ is the

starting point of the generated set and ‘f’ is a function. The starting point

‘a’ is a prefixpoint of ‘f’ or not in the domain and the function ‘f’ is

monotonic.

## Prefixpoints

The first fact we prove is the statement that all elements of ‘a.closed(f)’

which are in the domain of ‘f’ are prefixpoints provided that the starting

point ‘a’ is a prefixpoint or is not in the domain of ‘f’.

The crucial point in the proof is the following: Whenever some element ‘b’ in

‘a.closed(f)’ is a prefixpoint, then by definition of a prefixpoint

‘b<=f(b)’. By monotonicity of ‘f’ we get ‘f(b)<=f(f(b))’ provided that ‘f(b)’

is in the domain of ‘f’. I.e. the property of being a prefixpoint transfers

from one element to the next as long as there is a next element.

The following proof defines a set ‘p’ which contains all elements of the

closure which are either prefixpoints or not in the domain. The proof shows

that the set ‘p’ is closed under ‘f’. Some technicalities are necessary to

treat the case that an element is not in the domain of ‘f’.

all_prefixpoints: all(a:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in (f.prefixpoints + (-f.domain)) local r3: p = s.closed(f) * (f.prefixpoints + (-f.domain)) check c1: {s} <= p -- r3,r2 c2: all(b:CURRENT) require r4: b in p r5: b in f.domain check c3: f(b) in a.closed(f) -- r4,r5,r3 c4: b<=f(b) -- r4,r5,r3 c5: require r6: f(b) in f.domain check c6: f(b) <= f(f(b)) -- c4,r1,r6 ensure f(b) in f.prefixpoints -- r6,c6 end ensure f(b) in p -- c3,c5 end c7: p.is_closed(f) -- c2 c8: a.closed(f) <= p -- c1,c7,induction c9: a.closed(f) <= f.prefixpoints + (-f.domain) -- c8,r3 ensure a.closed(f)*f.domain <= f.prefixpoints -- c9 end

## Start element is least element

In this chapter we prove that ‘a’ is the least element of ‘a.closed(f)’. In

order to prove this we have to show that all elements of ‘a.closed(f)’ are

above or equal ‘a’.

We want to use induction and define a set ‘p’ which contains all elements of

‘a.closed(f)’ which are above or equal ‘a’. We show that ‘a’ is in this set

(which is trivial) and that the set is closed under ‘f’.

feature -- Start element is least element

start_is_least: all(s:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in (f.prefixpoints + (-f.domain)) local r3: p = a.closed(f)*{x:a<=x} check c1: all(b:CURRENT) require r4: b in p r5: b in f.domain check c2: b in f.prefixpoints -- r4,r5,lemma_2 c3: b<=f(b) -- c2 c4: s<=f(b) -- r4,c3,transitivity ensure f(b) in p -- c4,r3 end c5: p.is_closed(f) -- c1 c6: a.closed(f) <= p -- c5, 'a in p', induction ensure a.is_least(a.closed(f)) -- c6,r3 end

## Split the closure

In order to prove that ‘a.closed(f)’ is a chain we need one more intermediate

step. We have seen above that for any ‘b’ within the closure the subclosure

‘b.closed(f)’ is completely contained within the closure. I.e. we can split

‘a.closed(f)’ into the two disjoint parts

a.closed(f) = b.closed(f) + a.closed(f)-b.closed(f)

Since we know that all elements of ‘b.closed(f)’ are above or equal ‘b’ we can

try to prove that all elements of ‘a.closed(f)-b.closed(f)’ are strictly below

‘b’.

In order to prove this we put all elements ‘b’ of the closure where

‘a.closed(f)-b.closed(f)’ contains only elements strictly below ‘b’ into a set

‘p’ and prove that ‘a’ is within the set and the set is closed under ‘f’.

split_closure: all(a:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in (f.prefixpoints + (-f.domain)) local r3: pa = a.closed(f) r4: p = {b: pa-b.closed(f)<={x:x<b}}*pa check c1: a in p -- r3,r4 c2: all(b) require r5: b in p r6: b in f.domain check c3: b=f(b) or b/=f(b) c4: require r7: b/=f(b) check c5: b<f(b) -- r7, r1, all elements in pa and in -- the domain of f are prefixpoints c6: f(b) in pa -- r5,r4,r6 c7: b.closed(f) = {b}+f(b).closed(f) c8: f(b).closed(f) = b.closed(f)-{b} -- c7,r7 c9: pa-f(b).closed(f) = pa-b.closed(f)+{b} -- c8, lemma_2b c10: {b} <= {x:x<f(b)} -- c5 c11: {x:x<b} <= {x:x<f(b)} -- c5 c11: pa-f(b).closed(f)<={x:x<f(b)} -- c8,r5,r4,c5,c10 ensure f(b) in p -- c11,r4 end ensure f(b) in p -- c4,c8,r3 end c12: p.is_closed(f) -- c2 c13: a.closed(f) <= p -- c1,c12,induction ensure a.closed(f) <= {b: a.closed(f)-b.closed(f) <= {x:x<b}} -- c13,r3,r4 end

## Closure is chain

Having the theorem ‘split_closure’ it is straightforward to prove that the

closure is a chain since for all elements in the closure there are only

elements above or equal or strictly below in the closure.

all(a:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in f.prefixpoints check c1: all(b,c:CURRENT) require r3: b in a.closed(f) r4: c in a.closed(f) check c2: c in a.closed(f)-b.closed(f) or c in b.closed(f) c3: require r5: c in a.closed(f)-b.closed(f) ensure c<b -- r3, split_closure end c4: require r6: c in b.closed(f) check c5: b.is_least(b.closed(f)) -- r6 ensure b<=c -- c5 end ensure b.is_related(c) -- c2,c3,c4 end ensure a.closed(f).is_chain end

Note that being a chain implies being a directed set.

## Closures with greatest elements are finite

The closure ‘a.closed(f)’ has a greatest element if it contains one element

which is either not in the domain of ‘f’ or is a fixpoint of ‘f’. We expect a

closure with a greatest element to be finite.

We prove this claim by first verifying that set of all elements of

‘a.closed(f)’ below or equal a certain element ‘b’ is finite. The proof is

done by induction. The crucial point is that for any element ‘b’ within the

closure the set of elements below or equal ‘f(b)’ has one element more than

the set of elements below or equal ‘b’, namely ‘f(b)’. If the set of elements

below or equal ‘b’ is finite then the set of elements below or equal ‘f(b)’

has to be finite as well because it contains just one more element.

all(a,b:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in (f.prefixpoints + (-f.domain)) r3: b in a.closed(f) local r4: p = {b: ({x:x<=b}*a.closed(f)).is_finite}*a.closed(f) check c1: {x:x<=a} * a.closed(f) = {a} -- r1,r2,'a' is least c2: {a}.is_finite -- '{a} = 0 + {a}' c3: a in p -- c1,c2 c4: all(b:CURRENT) require b in p b in f.domain check b in a.closed(f) f(b) in a.closed(f) {x:x<=f(b)}*a.closed(f) = {x:x<=b}*a.closed(f) + {f(b)} ({x:x<=b}*a.closed(f)).is_finite ({x:x<=f(b)}*a.closed(f)).is_finite ensure f(b) in p end c5: p.is_closed(f) ensure ({x: x<=b}*a.closed(f)).is_finite -- r3,c3,c5,induction end

## Greatest elements

As long as there is an element ‘c’ in the closure ‘a.closed(f)’ which is in

the domain of ‘f’ and which is not a fixpoint the element ‘f(c)’ is as well in

the closure and strictly above ‘c’. Therefore ‘c’ cannot be the greatest

element of the closure. On the other hand if ‘c’ is a fixpoint of ‘f’ or not

in the domain of ‘f’ then there is no next element. Therefore ‘c’ is the

greatest element of the closure.

Therefore we claim that and element ‘c’ of the closure is the greatest element

if and only if it is either not in the domain of ‘f’ or is a fixpoint of ‘f’.

In order to prove this claim we have to show the forward and the backward

direction. First the forward direction.

greatest_fwd: all(a,c:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in f.prefixpoints r3: c in a.closed(f) r4: c in f.domain => c in f.fixpoints check c0: c.closed(f) = {c} -- r4 c1: all(b:CURRENT) require r5: b in a.closed(f) check c2: b in a.closed(f)-c.closed(f) or b in c.closed(f) -- r5 c3: b in a.closed(f)-c.closed(f) => b<c -- r3,'split' c4: b in c.closed(f) => b=c -- c0 ensure b <= c -- c2,c3,c4 end ensure c.is_greatest(a.closed(f)) -- c1,r3 end

Then the backward direction.

greatest_bwd: all(a,c:CURRENT, f:CURRENT->CURRENT) require r1: f.is_monotonic r2: a in f.domain => a in f.prefixpoints r3: c.is_greatest(a.closed(f)) check c1: c in a.closed(f) -- r3 c2: a.closed(f) <= c -- r3 c3: require r4: c in f.domain check c4: f(c) in a.closed(f) -- r4,c1 c5: c <= f(c) -- r4,c1 c6: f(c) <= c -- c4,c2 ensure c in f.fixpoints -- c5,c6 end ensure c in f.domain => c in f.fixpoints -- c3 end

Combining the two assertions we get.

greatest: all(a,c:CURRENT, f:CURRENT->CURRENT) require f.is_monotonic a in f.domain => a in f.prefixpoints ensure c.is_greatest(a.closed(f)) = (c in f.domain => c in f.fixpoints) -- greatest_fwd/bwd end

end -- Generated sets

# Closures in complete partial orders

Now we switch from partial orders to upcomplete partial orders.

-- module: upcomplete_partial_order

## Continous maps

It is always interesting to look at functions which preserve the structure. In

partial orders we have monotonic maps which preserve the order structure. For

upcomplete partial orders we can define continuous maps. A function is

continuous if it preserves suprema.

local A,B: CURRENT feature -- Continuous maps

is_continuous(f:A->B): ghost BOOLEAN ensure Result = all(d:CURRENT?) require d.is_directed d+{d.supremum} <= f.domain ensure f(d.supremum).is_supremum(d.image(f)) end end

We claim that this property is strong enough to preserve the order structure

as well. I.e. we state that any continuous map is order preserving.

all(f:A->B) require r1: f.is_continuous check c1: all(a,b:A) require r2: {a,b} <= f.domain r3: a <= b check c2: b.is_supremum({a,b}) -- r3 c3: f(b).is_supremum({f(a),f(b)}) -- c2,r1 c4: {f(a), f(b)} <= f(b) -- c3, supremum is -- upper bound ensure f(a) <= f(b) -- c4 end ensure f.is_monotonic -- c1 end

end -- Continuous maps

## Fixpoints

feature -- Fixpoints

In order to study fixpoints we have to look at functions of the type

f:CURRENT->CURRENT. Let us first define sets which are closed in the sense

that they contain all directed sets completely if they have some elements in

common and that they include the suprema of contained directed sets.

is_limitclosed(p:CURRENT?): ghost BOOLEAN ensure Result = all(d:CURRENT?) require d.is_directed d * p /= 0 ensure (d + {d.supremum}) in p end end

The central fixpoint law of continuous functions reads like: Whenever a

continuous map with sufficiently large domain has prefixpoints, it has

fixpoints as well. We state this law formally.

some_fixpoints: all(f:CURRENT->CURRENT) require f.is_continuous f.domain.is_limitclosed f.prefixpoints /= 0 ensure f.fixpoints /= 0 -- least_fixpoint below end

We are going to prove this law by constructing the least fixpoint of such a

function i.e. we are going to prove

least_fixpoint: all(a:CURRENT, f:CURRENT->CURRENT) require f.is_continuous a in f.prefixpoints a.closed(f) + {a.closed(f).supremum} <= f.domain ensure a.closed(f).supremum.is_least(f.fixpoints * {x:a<=x}) -- lemma_fix_3 below end

In order to prove this claim we show first that ‘a.closed(f)’ and

‘a.closed(f).image(f)’ have the same supremum.

lemma_fix_1: all(a:CURRENT, f:CURRENT->CURRENT) require a in f.prefixpoints f.is_continuous a.closed(f) + {a.closed(f).supremum} <= f.domain ensure a.closed(f).image(f).supremum = a.closed(f).supremum end

Having this we can demonstrate that the supremum of ‘a.closed(f)’ is a

fixpoint.

lemma_fix_2: all(a:CURRENT, f:CURRENT->CURRENT) require r1: a in f.prefixpoints r2: f.is_continuous r3: a.closed(f) + {a.closed(f).supremum} <= f.domain local r4: s = a.closed(f).supremum check c1: a.closed(f).is_directed -- r1, because it is a chain c2: f(s) = a.closed(f).image(f).supremum -- r2,c1 = a.closed(f).supremum -- lemma_fix_1 = s -- r4 ensure a.closed(f).supremum in f.fixpoints end

But we want to prove that the supremum of ‘a.closed(f)’ is the least fixpoint

above ‘a’. In order to prove this we show that any fixpoint ‘z’ above ‘a’ is

an upper bound of ‘a.closed(f)’. Because the supremum is the least upper bound

it follows that the supremum is the least fixpoint. In order to show that any

fixpoint ‘z’ is an upper bound of ‘a.closed(f)’ we use induction.

lemma_fix_3: all(a:CURRENT, f:CURRENT->CURRENT) require r1: a in f.prefixpoints r2: f.is_continuous r3: a.closed(f) + {a.closed(f).supremum} <= f.domain local r4: s = a.closed(f).supremum check c1: all(z:CURRENT) require r5: z in (f.fixpoints * {x: a<=x}) local r6: p = {b: b<=z}*a.closed(f) check c2: a in p c3: all(b:CURRENT) require r7: b in f.domain r8: b in p check c4: b <= z -- r8,r6 c5: f(b) <= f(z) -- c4,r7,r2 c6: f(b) <= z -- c5,r5 c7: f(b) in a.closed(f) -- r7,r8,r6 ensure f(b) in p -- c6,c7,r6 end c8: p.is_closed(f) -- c3 c9: a.closed(f) <= z -- c2,c8,r6,induction ensure s <= z end ensure a.closed(f).supremum.is_least(f.fixpoints * {x:a<=x}) -- c1 end

end -- Fixpoints