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
