SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/closures fixpoints

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

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

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
 

Emacs suffix

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

- Introduction

- Closed sets and induction

- Basics

- Subclosure

- Decomposition of a closure

- Induction

- Fixpoints

- Injections and finite sets

- Closures in partial orders

- Prefixpoints

- Start element is least element

- Split the closure

- Closure is chain

- Closures with greatest elements are finite

- Greatest elements

- Closures in complete partial orders

- Continous maps

- Fixpoints

- Emacs suffix


ip-location