Closures and fixpoints

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
About these ads

, ,

  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 32 other followers

%d bloggers like this: