The Eiffel Compiler / Interpreter (tecomp)

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.

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.

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

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

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

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

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 pigeons where 'm>0'. If all the n+m pigeons are in the n pigeonholes 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

Furthermore 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

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.

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

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

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

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.

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

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

Now we switch from partial orders to upcomplete partial orders.

```
-- module: upcomplete_partial_order
```

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

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

Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: