SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/endofunctions

Endofunctions, closures, cycles and chains

Introduction

Motivation

Endofunctions are functions f of type A->A where A can be any type. Since all functions are partial functions we can use endofunctions to model linked structures. E.g. if we have an object which has an optional reference to an object of the same type the optional reference can be viewed as a partial function f of type A->A. If the reference to the next object is void (there is no next object because we are at the end of a linked list or we have reached the root of a tree following the parent links) then the corresponding function f is undefined for this specific object.

Sequences and closures

If we have an element a of type A and an endofunction f of type A->A we can start at the element a, apply the function to a (if a is in the domain of the function) getting f(a), reapply the function to f(a) (provided that f(a) is in the domain of f), ... I.e. we get the set

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

We call a set p of elements of type A closed under f if the image of p under f is a subset of p, i.e. f applied to any element of p results in an element within p. I.e. we define the predicate

  is_closed(p:A?, f:A->A): ghost BOOLEAN
          -- Is the set `p' closed under the function `f'?
      ensure
          Result  =  p.image(f) <= p
      end
 

and remember the definition of image as

  image(p:A?, f:A->B): ghost B?
          -- The image of the set `p' under `f'.
      ensure
          Result = {b: some(a) a in p and a in f.domain and f(a) = b}
      end
 

With this we get an equivalent definition of a closed set as

  all(p:A?, f:A->A)
      ensure
          p.is_closed(f) = all(x:A)
                               require
                                   x in p
                                   x in f.domain
                               ensure
                                   f(x) in p
                               end
      end
 

The proof of the equivalence of both definitions is a standard exercise.

The set of all sets which are closed under an endofunction f form a closure system. Therefore we can close any set p under a function f by finding the least set which is closed under f and contains the set p.

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

Since the set {q: q.is_closed(f)} is a closure system the above used infimum is guaranteed to be closed under f (for details on closures see the article "Complete lattices and closure systems"). We often need the closure of the singleton set {a} under f and therefore define the closure of an element a by

  closed(a:A, f:A->A): ghost A?
          -- The singleton set {a} closed under the function `f'.
      ensure
          Result = {a}.closed(f)
      end
 

With this definition we can write the above set in a closed form

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

The function 'closed' is a closure operator, i.e. it is monotonic, ascending and idempotent on the first argument.

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

Furthermore the function closed is monotonic in the function argument

  all(a:A, p:A?, f,g:A->A)
      ensure
          f <= g  =>  p.closed(f) <= p.closed(g)
 
          f <= g  =>  a.closed(f) <= a.closed(g)
      end
 
   -- Note: f<=g iff f.domain <= g.domain and the values of f and g
   --                coincide on f.domain
 

Induction

Since p.closed(f) is the least set which contains all elements of p and is closed under f all other sets which contain p and are closed under f must be supersets of p.closed(f). We can use this property of the closure to prove that all elements of a closure x satisfy a certain property e. In order to do this we put all elements which satisfy e into the set q = {x: e}. If we can prove that the initial set p is a subset of q and q is closed under f then we can conclude that all p.closed(f) is a subset of q i.e. that all elements of p.closed(f) satisfy the property e.

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

This theorem is a direct consequence of the fact that the function closed is monotonic, ascending and idempotent.

We can use a similar induction law if the start set is the singleton set {a}.

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

Cycles and chains

If we start from an element a and repeatedly apply f forever or until we reach an out of domain element our intuition tells us that there are three possibilities. Either we can continue reapplying f forever without reaching an out of domain element and without reaching an element which has already been passed or we reach some out of domain element or we reach an element which we have already passed.

  infinite chain: a -> b -> c -> ....
 
  finite chain:   a -> b -> c -> .... -> z      z /in f.domain
 
  with cycle:     a -> b -> c -> .... -> z
                            ^           /
                            \........../
 

In order to deal with these structures we introduce the following definitions.

  is_cycle(p:A?, f:A->A): ghost BOOLEAN
          -- Does the set `p' form a cycle under the function `f'?
      ensure
          Result = some(a)
                       a.closed(f) = p
                       and a in f.domain
                       and a in f(a).closed(f)
      end
 
  has_cycle(p:A?, f:A->A): ghost BOOLEAN
          -- Does the set `p' contain a cycle under `f'?
      ensure
          Result = some(a) a in p and a.closed(f).is_cycle(f)
      end
 
  is_connected(p:A?, f:A->A): ghost BOOLEAN
          -- Is the set `p' connected under `f'?
      ensure
          Result = all(x,y:A)
                       require
                           {x,y} <= p
                       ensure
                           x in y.closed(f) or y in x.closed(f)
                       end
      end
 
  is_chain(p:A?, f:A->A): ghost BOOLEAN
          -- Does the set `p' form a chain under `f'.
      ensure
          Result = (p.is_closed(f)
                    and p.is_connected(f)
                    and not p.has_cycle(f))
      end
 

Simple properties

Predecessor

In any closure of the form p.closed(f) it is guaranteed that all elements except the elements of the initial set have predecessors within the closure.

In order to prove this claim we assume the opposite that for a certain element x in p.closed(f)-p all elements a of p.closed(f) are not predecessors of x. Since x has no predecessor we can prove that the set p.closed(f)-{x} is closed under f and contains p. This set is strictly smaller than p.closed(f) which contradicts the fact that p.closed(f) is the least set which contains p and is closed under f.

  some_predecessor:
  all(x:A, p:A?, f:A->A)
      require
          r1: x in p.closed(f)-p
      check
          c1: require
                  r2: all(a) a in p.closed(f) => a in f.domain => f(a)/=x
              check
                  c2: all(a:A)
                      require
                          r3: a in p.closed(f)-{x}
                          r4: a in f.domain
                      check
                          c3: a in p.closed(f)     -- r3
                          c4: a /= x               -- r3
                          c5: f(a) /= x            -- c3,r4,r2
                          c6: f(a) in p.closed(f)  -- c3,r4
                      ensure
                          f(a) in p.closed(f)-{x}  -- c5,c6
                      end
 
                  c7: p <= p.closed(f)-{x}             -- r1
 
                  c8: (p.closed(f)-{x}).is_closed(f)   -- c2
 
                  c9: p.closed(f) <= p.closed(f)-{x}   -- closure is least
 
                  c10: x in p.closed(f)-{x}            -- r1,c9
 
                  c11: x /in p.closed(f)-{x}           -- general law
              ensure
                  False                                -- c10,c11
              end
      ensure
          some(a)
              a in p.closed(f)
              and a in f.domain
              and f(a)=x
      end
 

All elements of cycles

By definition the set p is a cycle under f if there is one element a in the domain of f such that p=a.closed(f) and a is in f(a).closed(f).

We claim that all elements of a cycle satisfy this property. We prove this with a two step approach. First we prove the lemma that each element of a cycle transfers this property to its successor f(a). Then we use induction to prove that all elements of a.closed(f) and therefore all elements of p have this property.

feature {NONE}
      lemma:
      all(a:A, p:A?, f:A->A)
          require
              r1: a.closed(f) = p
              r2: a in f.domain
              r3: a in f(a).closed(f)
          check
              c1: f(a).closed(f) <= a.closed(f)  -- general property
              c2: a.closed(f) <= f(a).closed(f)  -- r3, closure is monotonic
 
              c3: a = f(a)  or  a /= f(a)
              c4: require
                      r4: a /= f(a)
                  check
                      c5: {f(a)} < f(a).closed(f)
                      c6: a in (f(a).closed(f)-{f(a)})  -- r3,r4
 
                      c7: f(a).closed(f) - {f(a)} <= f(f(a)).closed(f)
                                        -- general property of closure
                  ensure
                      f(a) in f.domain              -- c5
                      a in f(f(a)).closed(f)        -- c6,c7
                  end
          ensure
              f(a).closed(f) = p                 -- r1,c1,c2
              f(a) in f.domain                   -- c3,c4,r2
              f(a) in f(f(a)).closed(f)          -- c3,c4,r3
          end
 

Having this lemma it is easy to prove that all elements of a cycle under f are in the domain of f and their closure is the cycle and they can be reached by their successor.

  cycle_all:
  all(x:A, p:A?, f:A->A)
      require
          r1: p.is_cycle(f)
          r2: x in p
      local
          r3: q = {x:A: x.closed(f)=p
                        and x in f.domain
                        and x in f(x).closed(f)}
      check
          c1: some(a:A)
                  a.closed(f)=p and a in f.domain and a in f(a).closed(f)
                                               -- r1
          c2: all(a:A)
              require
                  r4: a.closed(f) = p
                  r5: a in f.domain
                  r6: a in f(a).closed(f)
              check
                  c3: a in q                   -- r3,r4,r5,r6
                  c4: q.is_closed(f)           -- lemma
                  c5: a.closed(f) <= q         -- c3,c4
                  c6: p <= q                   -- c5,r4
              ensure
                  x.closed(f) = p              -- r2,c6,r3
                  x in f.domain                -- r2,c6,r3
                  x in f(x).closed(f)          -- r2,c6,r3
              end
      ensure
          x.closed(f) = p                      -- c1,c2
          x in f.domain                        -- c1,c2
          x in f(x).closed(f)                  -- c1,c2
      end
 

Domain restrictions

Definitions

If f is a function and b is an element of f's domain then f-b is the function f without b in its domain. We can subtract a set p from the domain of f. Furthermore we can restrict the domain of a function. In order to express these domain restrictions we use the following definitions.

  - (f:A->B, p:A?): ghost A->B
          -- The function `f' without the elements of the set `p' in
          -- its domain.
      ensure
          Result.domain = f.domain - p
          Result <= f
      end
 
  - (f:A->B, a:A): ghost A->B
          -- The function `f' without the element `a' in its domain.
      ensure
          Result = f - {a}
      end
 
  | (f:A->B, p:A?): ghost A->B
          -- The function `f' with its domain restricted to `f.domain*p'.
      ensure
          Result.domain = f.domain * p
          Result <= f
      end
 

Out of domain elements are unique

If a closure a.closed(f) has an element which is not in the domain of f then this element is unique.

  out_of_domain_unique:
  all(a,b,c:A, f:A->A)
      require
          {b,c} <= a.closed(f)
          {b,c} * f.domain = 0
      ensure
          b = c            -- lemma below
      end
 

Proof: Assume that b and c are different, i.e. there are two out of domain elements in the closure. We put all objects whose closure contains b and c into the set p. Clearly a is in the set p. Furthermore the set p is closed under f. Assume that x is an element of p and in the domain of f. Thus x is neither b nor c. Therefore f(x).closed(f) must contain b and c as well and is therefore an element of p. So we have that all elements of a.closed(f) are in p. This contradicts the fact that b and c are in a.closed(f) which cannot be in p.

  feature {NONE} -- Proof of 'out_of_domain_unique'
      lemma:
      all(a,b,c:A, f:A->A)
          require
              r1: {b,c} <= a.closed(f)
              r2: {b,c} * f.domain = 0
              r3: b /= c
          local
              r4: p = {x:A: {b,c} <= x.closed(f)}
          check
              c1: a in p              -- r4,r1
              c2: all(x:A)
                  require
                      r5: x in p
                      r6: x in f.domain
                  check
                      c3: x /= b                  -- r6,r2
                      c4: x /= c                  -- r6,r2
                      c5: {b,c} <= f(x).closed(f) -- r5,r4,c3,c4
                  ensure
                      f(x) in p                   -- c5
                  end
              c6: p.is_closed(f)                  -- c2
              c7: a.closed(f) <= p                -- c1,c6
              c8: b /in p                         -- r4,r2,r3
              c9: b /in a.closed(f)               -- c8,c7
              c10: b in a.closed(f)               -- r1
          ensure
              False                               -- c9,c10
          end
  end
 

Sequencing

If we have a closure of the form a.closed(f) and two elements b and c within this closure then starting from a we either first encounter b or c. This intuitively clear fact can be expressed by the claim

  sequence:
  all(a,b,c:A, f:A->A)
      require
          {b,c} <= a.closed(f)
      ensure
          b in a.closed(f-c) or c in a.closed(f-b)
      end
 

We prove this claim by a series of intermediate lemmas.

First we show that all b in the closure a.closed(f) are also in the closure of a.closed(f-b) (f-b is the function f with b removed from its domain). We prove this claim by contradiction.

  sequence_1:
  all(a,b:A, f:A->A)
      require
          r1: b in a.closed(f)
      check
          c1: require
                  r2: b /in a.closed(f-b)
              check
                  c2: b in f.domain or b /in f.domain
                  c3: require
                          r3: b in f.domain
                      check
                          c4: a.closed(f-b) = a.closed(f-b+{b->f(b)})
                                        -- r2,r3,
                                        -- modification of a function outside
                                        -- the closure has no effect on the
                                        -- closure
                          c5: a.closed(f-b) = a.closed(f)     -- c4
                          c6: b /in a.closed(f)               -- r2,c5
                      ensure
                          False                               -- r1,c6
                      end
                  c7: require
                          r4: b /in f.domain
                      check
                          c8: f-b = b
                          c9: b /in a.closed(f)         -- r2,c8
                      ensure
                          False                         -- r1,c9
                      end
              ensure
                  False                                 -- c2,c3,c7
              end
      ensure
          b in a.closed(f-b)    -- c1
      end
 

Next we show that for any c in a.closed(f) and b in a.closed(f-c) that the closure of a.closed(f-b) is a subset of the closure a.closed(f-c).

  sequence_2:
  all(a,b,c:A, f:A->A)
      require
          r1: c in a.closed(f)
          r2: b in a.closed(f-c)
      check
          c1: b=c or b/=c                        -- first trivial
          c2: c in f.domain or c /in f.domain    -- second trivial
          c3: require
                  r3: c in f.domain
                  r4: b /= c
              check
                  c4: b in a.closed(f-c-b)       -- r2, sequence_1
                  c5: c /in a.closed(f-c-b)      -- c4, out_of_domain_unique
                  c6: f-b = f-c-b + {c->f(c)}    -- r3, general law
                  c7: a.closed(f-c-b) = a.closed(f-b)
                          -- c5,c6,modify_out_of_closure
                  c8: a.closed(f-c-b) <= a.closed(f-c)  -- monotonic
              ensure
                  a.closed(f-b) <= a.closed(f-c)        -- c7,c8
              end
      ensure
          a.closed(f-b) <= a.closed(f-c)                -- c1,c2,c3
      end
 

Consider an element b and an element c which is not in the closure a.closed(f-b). From this we can conclude that a.closed(f-b) is a subset of a.closed(f-c).

  sequence_3:
  all(a,b,c:A, f:A->A)
      require
          r1: c /in a.closed(f-b)
      check
          c1: a.closed(f-b) = a.closed(f-b-c)   -- r1
          c2: a.closed(f-b) = a.closed(f-c-b)   -- c1
          c3: a.closed(f-c-b) <= a.closed(f-c)  -- monotonic
      ensure
          a.closed(f-b) <= a.closed(f-c)        -- c2,c3
      end
 
 

From these intermediate lemmas it is easy to prove the main theorem.

  sequence_4:
  all(a,b,c:A, f:A->A)
      require
          r1: {b,c} <= a.closed(f)
      check
          c1: require
                  r2: c /in a.closed(f-b)
              check
                  c2: a.closed(f-b) <= a.closed(f-c)    -- r1, r2, sequence_3
                  c3: b in a.closed(f-b)                -- r1, sequence_1
              ensure
                  b in a.closed(f-c)                    -- c3,c2
              end
      ensure
          b in a.closed(f-c) or c in a.closed(f-b)      -- c1
      end
 

Cycles

In this chapter we concentrate on closures which have cycles or which are a cycle.

Two cycles are identical or disjoint

If we have two sets p and q which form a cycle under f then they are either identical or disjoint.

  cycle_disjoint_or_identical:
  all(p,q:A?, f:A->A)
      require
          r1: p.is_cycle(f)
          r2: q.is_cycle(f)
      check
          c1: require
                  r3: p*q /= 0
              check
                  c2: some(a:A) a in p and a in q      -- r3
                  c3: all(a:A)
                      require
                          r4: a in p
                          r5: a in q
                      check
                          c4: p = a.closed(f)          -- r4,r1,cycle_all
                          c5: q = a.closed(f)          -- r5,r2,cycle_all
                      ensure
                          p = q                        -- c4,c5
                      end
              ensure
                  p = q                                -- c2,c3
              end
      ensure
          p*q=0  or   p=q                              -- c1
      end
 

Cycles are unique

A closure of the form a.closed(f) cannot have two different cycles.

  cycle_unique:
  all(a:A, p,q:A?, f:A->A)
      require
          r1: p.is_cycle(f)
          r2: q.is_cycle(f)
          r3: p <= a.closed(f)
          r4: q <= a.closed(f)
      check
          c1: require
                  r5: p /= q
              local
                  r6: s = {a:A: not a.closed(f).is_cycle(f)
                                and p+q<=a.closed(f)}
              check
                  c2: p*q = 0      -- r1,r2,r5,cycle_disjoint_or_identical
                  c3: not a.closed(f).is_cycle(f)
                                   -- r1,r2,r5,r3,r4 if a.closed(f) were a
                                   -- cycle it would have to be identical to
                                   -- p and q which contradicts r5
                  c4: a in s       -- c3,r3,r4
                  c5: all(x:A)
                      require
                          r7: x in s
                          r8: x in f.domain
                      check
                          c6: x /in p          -- r7,r6,r1
                          c7: x /in q          -- r7,r6,r2
                          c8: p+q <= f(x).closed(f)  -- c6,c7
                          c9: not f(x).closed(f).is_cycle(f)
                              -- if it were a cycle it would have to be
                              -- identical to p and q which contradicts r5
                      ensure
                          f(x) in s            -- c8,c9
                      end
                  c10: s.is_closed(f)           -- c5
                  c11: a.closed(f) <= s         -- c4,c10
                  c12: not p.is_cycle(f)        -- c11,r3
              ensure
                  False                         -- r1,c12
              end
      ensure
          p = q         -- c1
      end
 

All elements of a cycle have predecessors

In some previous chapter we have already proved that each element in a.closed(f) except a is guaranteed to have a predecessor. In a cycle each element is guaranteed to have a predecessor.

  cycle_all_predecessor:
  all(p:A?, f:A->A)
      require
          r1: p.is_cycle(f)
      check
          c1: all(y:A)
              require
                  r2: y in p
              check
                  c1: y in f.domain         -- r1,r2
                  c2: y in f(y).closed(f)   -- r1,r2,cycle_all
                  c3: f(y).closed(f)=p      -- r1,r2,cycle_all
                  c4: y=f(y) or y/=f(y)
                  c5: y=f(y) => some(x) x in p and f(x)=y  -- witness y
                  c6: y/=f(y) => some(x) x in p and f(x)=y
                            -- c2,c3,some_predecessor
              ensure
                  some(x:A) x in p and f(x)=y           -- c4,c5,c6
              end
      ensure
          all(y) y in p => some(x) x in p and f(x)=y    -- c1
      end
 

All elements of a cycle have unique predecessors

If the set p is a cycle under f we claim that each element in p has a unique predecessor. In order to prove this claim we assume that a, b and c are three elements of the cycle where b and c are different predecessors of a and lead this to a contradiction. As a first step we assume additionally that b is in a.closed(f-c).

Since a, b and c are elements of the cycle they are in the domain of f. b and c are different therefore b is in the domain of f-c, i.e (f-c)(b)=a because b is a predecessor of a. Together with the additional assumption that b is in a.closed(f-c) we get that b is in (f-c)(b).closed(f-c) which is sufficient to conclude that b.closed(f-c) is a cycle and therefore that a.closed(f-c) is a cycle as well. From the lemma 'sequence_1 we can conclude that c is in a.closed(f-c). In a cycle all elements are in the domain of the function, therefore c must be in the domain of f-c which contradicts the definition of f-c.

  feature {NONE}
      lemma:
      all(a,b,c:A, f:A->A)
          require
              r1: a.closed(f).is_cycle(f)
              r2: {b,c} <= a.closed(f)
              r3: f(b) = a
              r4: f(c) = a
              r5: b in a.closed(f-c)
          check
              c1: require
                      r7: b /= c
                  check
                      c2: b in (f-c).domain             -- r1,r2,r7
                      c3: (f-c)(b)=a                    -- c2,r3
                      c4: b in (f-c)(b).closed(f-c)     -- c3,r5
                      c5: b.closed(f-c).is_cycle(f-c)   -- c4
                      c6: a.closed(f-c).is_cycle(f-c)   -- c5,c3
                      c7: c in a.closed(f-c)            -- r2,sequence_1
                      c8: c in (f-c).domain             -- c6,c7,cycle_all
                      c9: c /in (f-c).domain            -- by definition
                  ensure
                      False                             -- c8,c9
                  end
          ensure
              b = c
          end
  end
 

Having this lemma we can prove that every element of a cycle has a unique predecessor.

  cycle_unique_predecessor:
  all(p:A?, f:A->A)
      require
          r1: p.is_cycle(f)
      check
          c1: all(a,b,c:A)
              require
                  r2: {a,b,c} <= p
                  r3: f(b) = a
                  r4: f(c) = a
              check
                  c2: a.closed(f) = p            -- r1,r2,cycle_all
                  c3: {b,c} <= a.closed(f)       -- c2,r2
                  c4: b in a.closed(f-c) or c in a.closed(f-b) -- c3,sequence
              ensure
                  b = c        -- c4,r2,r3,r4,lemma
              end
      ensure
          all(a,b,c) {a,b,c} <= p => f(b)=a => f(c)=a => b=c
      end
 

As a corollary we get the fact that if the set p is a cycle under f then f is injective on p.

  cycle_injective:
  all(p:A?, f:A->A)
      require
          r1: p.is_cycle(f)
      check
          c1: all(b,c:A)
              require
                  r2: {b,c} in (f|p).domain
                  r3: f(b) = f(c)
              check
                  c2: p <= f.domain          -- r1
                  c3: (f|p).domain = p       -- c2
                  c4: {b,c} <= p             -- r2,c3
              ensure
                  b = c                      -- r2,r3,c4,
                                             -- cycle_unique_predecessor
              end
      ensure
          (f|p).is_injective
      end
 
      -- Note: f|p is the function f restricted to the domain
      --       f.domain*p
 

Closures with cycles are completely in the domain

If a closure a.closed(f) has a cycle then it is guaranteed that all elements of the closure are within the domain of f. This claim is easy to prove. We put all elements of f.domain whose closure has a cycle into the set p and show that a is in p and that p is closed under f.

The element a is in p because a.closed(f) has a cycle. Therefore either a is in the cycle and is therefore in f.domain or it is not in the cycle. If it is not in the cycle and not in the domain then a.closed(f) could not contain a cycle.

Assume an arbitrary element x of p i.e. x is in f.domain and x.closed(f) has a cycle. Since x.closed(f) has a cycle f(x).closed(f) has a cycle as well. Now either f(x).closed(f) is a cycle. Then f(x) is in p as well. Or f(x).closed(f) is not a cycle. Then f(x) must be in f.domain otherwise it could not contain a cycle.

  cycles_in_domain:
  all(a:A, f:A->A)
      require
          r1: a.closed(f).has_cycle(f)
      local
          r2: p = f.domain * {x:A: x.closed(f).has_cycle(f)}
      check
          c1: a in f.domain          -- r1
          c2: a in p                 -- c1,r2
          c3: all(x:A)
              require
                  r3: x in p
                  r4: x in f.domain
              check
                  c4: x.closed(f).has_cycle(f)    -- r3,r2
                  c5: f(x).closed(f).has_cycle(f) -- c4
                  c6: f(x).closed(f).is_cycle(f)
                      or not f(x).closed(f).is_cycle(f)
                  c7: require
                          r5: f(x).closed(f).is_cycle(f)
                      check
                          c8: f(x) in f.domain
                      ensure
                          f(x) in p         -- c8,c5
                      end
                  c9: require
                          r6: not f(x).closed(f).is_cycle(f)
                      check
                          c10: f(x) in f.domain    -- r6,c5
                      ensure
                          f(x) in p                -- c10,c5
                      end
              ensure
                  f(x) in p
              end
          c11: p.is_closed(f)                      -- c3
          c12: a.closed(f) <= p                    -- c1,c11
      ensure
          a.closed(f) <= f.domain                  -- c12,r2
      end
 

Closures are connected

If we have a closure of the form a.closed(f) we can take any element b of the closure and form the subclosure b.closed(f). From the properties that 'closed' is monotonic, ascending and idempotent it is immediately evident that b.closed(f) is a subset of a.closed(f).

But there are more properties in subclosures. Suppose we pick two elements b and c of a.closed(f). Then we claim that either b is in the subclosure c.closed(f) or c is in the subclosure b.closed(f) i.e. we can reach either b from c or c from b which says that all elements of the closure are connected.

We are going to prove this claim by induction. But before doing the induction let us split out the induction step.

Assume that b and c are in a.closed(f) and c is in b.closed(f). Then we prove that either c is in f(b).closed(f) or f(b) is in c.closed(f).

  feature {NONE}
      lemma:
      all(a,b,c:A, f:A->A)
          require
              r1: {b,c} <= a.closed(f)
              r2: c in b.closed(f)
              r3: b in f.domain
          check
              c1: b=c or b/=c
              c2: require
                      r4: b=c
                  check
                      c3: f(b) in c.closed(f)     -- r3,r4
                  ensure
                      c in f(b).closed(f) or f(b) in c.closed(f)  -- c3
                  end
              c4: require
                      r5: b/=c
                  check
                      c5: c in f(b).closed(f)      -- r2,r3,r5
                  ensure
                      c in f(b).closed(f) or f(b) in c.closed(f)  -- c5
                  end
          ensure
              c in f(b).closed(f) or f(b) in c.closed(f)    -- c1,c2,c4
          end
  end
 

Having this lemma we can prove the main theorem.

  subclosure:
  all(a,b,c:A, f:A->A)
      require
          r1: {b,c} <= a.closed(f)
      local
          r2: p = {b:A: c in b.closed(f) or b in c.closed(f)}*a.closed(f)
      check
          c1: a in p                                       -- r2,r1
          c2: all(x:A)
              require
                  r3: x in p
                  r4: x in f.domain
              check
                  c3: x in a.closed(f)
                  c4: c in x.closed(f) or x in c.closed(f)
                  c5: require
                          r5: c in x.closed(f)
                      check
                          c6: c in f(x).closed(f) or f(x) in c.closed(f)
                                   -- r4,r1,c3,r5,lemma
                      ensure
                          f(x) in p       -- c3,r2,c6
                      end
                  c7: require
                          r6: x in c.closed(f)
                      check
                          c8: f(x) in c.closed(f)    -- r6,r4
                      ensure
                          f(x) in p                  -- c8,c3
                      end
              ensure
                  f(x) in p                          -- c4,c5,c7
              end
          c9:  p.is_closed(f)                        -- c2
          c10: a.closed(f) <= p                      -- c1,c9
      ensure
          c in b.closed(f) or b in c.closed(f)       -- c10,r2
      end
 

Chains

A chain has an injective function

Whenever we have a set p which is a chain under the function f we can conclude that f is injective on p.

Remember that a function g is injective if for all pairs x and y in the domain of g the equality g(x)=g(y) implies x=y. The function g is our function f restricted to p i.e. f|p. We claim that f|p is injective if p is a chain under f.

We prove this claim by contradiction. Assume that f|p is not injective. Then there are x and y in the domain of f|p such that f(x)=f(y) and x/=y. Without loss of generality we can assume that y is in x.closed(f) (see definition of a chain).

Since y is in x.closed(f) and x/=y we get y in f(x).closed(f) and therefore y in f(y).closed(f). This implies that y.closed(f) is a cycle which contradicts the fact that p is a chain.

In order to keep the proof readable we split out the contradiction as a lemma and then prove the main theorem.

  feature {NONE}
      lemma:
      all(p:A?, x,y:A, f:A->A)
          require
              r1: p.is_chain(f)
              r2: {x,y} <= (f|p).domain
              r3: f(x) = f(y)
              r4: x /= y
              r5: y in x.closed(f)
          check
              c1: y in f(x).closed(f)         -- r5,r4
              c2: y in f(y).closed(f)         -- c1,r3
              c3: y.closed(f).is_cycle(f)     -- r2,c2
              c4: not y.closed(f).is_cycle(f) -- r2,r1
          ensure
              False                           -- c3,c4
          end
  end
 
  chain_injective:
  all(p:A?, f:A->A)
      require
          r1: p.is_chain(f)
      check
          c1: require
                  r2: not (f|p).is_injective
              check
                  c2: some(x,y:A) {x,y}<=(f|p).domain
                                  and f(x)=f(y)
                                  and x/=y               -- r2
                  c3: all(x,y:A)
                      require
                          r3: {x,y} <= (f|p).domain
                          r4: f(x) = f(y)
                          r5: x /= y
                      check
                          c4: y in x.closed(f) or x in y.closed(f)   -- r1,r3
                          c5: y in x.closed(f) => False  -- r1,r3,r4,r5,lemma
                          c6: x in y.closed(f) => False  -- r1,r3,r4,r5,lemma
                      ensure
                          False                          -- c4,c5,c6
                      end
              ensure
                  False                                  -- c2,c3
              end
      ensure
          (f|p).is_injective
      end
 

The image of a chain does not contain the first element

Consider a closure a.closed(f) which is a chain under f. The image of the closure under f does not contain a.

  all(a:A, f:A->A)
      require
          r1: a.closed(f).is_chain(f)
      check
          c1: a in f.domain or a /in f.domain
          c2: require
                  r2: a in f.domain
              check
                  c3: a.closed(f) = {a} + f(a).closed(f)     -- general law
                  c4: a /in f(a).closed(f)                   -- r1
                  c5: f(a).closed(f) = a.closed(f) - {a}     -- c3,c4
                  c6: a.closed(f).image(f) = f(a).closed(f)  -- general law
              ensure
                  a.closed(f).image(f) = a.closed(f) - {a}   -- c5,c6
              end
          c7: require
                  r3: a /in f.domain
              check
                  c8: a.closed(f) = {a}   -- r3
                  c9: {a}.image(f) = 0    -- r3
              ensure
                  a.closed(f).image(f) = a.closed(f) - {a}   -- c8,c9
              end
      ensure
          a.closed(f).image(f) = a.closed(f) - {a}           -- c1,c2,c7
      end
 

Finiteness

In this chapter we want to prove the following facts:

In this chapter we don't do all proofs in full formality. Some proofs will be given with textual arguments only. However it is an easy exercise to construct the formal proofs.

Definitions

Let us recall the definition of infiniteness of a set.

  is_infinite(p:A?): ghost BOOLEAN
         -- Is the set `p' infinite?
     ensure
         Result = some(f:A->A) 
                      f.is_injective
                      and p <= f.domain
                      and p.image(f) < p
     end
 

I.e. a set p is infinite if there is an injective map f mapping all elements of p to a proper subset of p.

A set is finite if it is not infinite.

  is_finite(p:A?): ghost BOOLEAN
         -- Is the set `p' finite?
     ensure
         Result = not p.is_infinite
     end
 

This gives us an equivalent definition of finiteness.

  all(p:A?)
      ensure
          p.is_finite = all(f:A->A)
                        require
                            f.is_injective
                            p <= f.domain
                            p.is_closed(f)   -- i.e. p.image(f)<=p
                        ensure
                            p = p.image(f)
                        end
      end
 

From the definitions we can immediately conclude that the empty set is finite since there is no proper subset of the empty set (and therefore not any function mapping to a proper subset).

Furthermore we can prove that p+{a} is a finite set provided that p is a finite set. Without loss of generality we can analyze the case that the element a is not in p (if a is in p then p+{a}=p which is a trivial case).

Let's assume the opposite that p+{a} is infinite. Then there is a injective function f which maps p+{a} to a proper subset. We analyze the case where a is in the image and where a is not in the image.

If a is not in the image then (p+{a}).image(f) <= p. This implies p.image(f)<p because f(a) is missing in the image. Thus p must be infinite which contradicts the fact that p is finite.

If a is in the image then there is a unique element b in p+{a} with f(b)=a because of the injectivity of f. We define a new function g which is f with the values for a and b swapped. g is still injective with g(a)=a and (p+{a}).image(g)<p+{a}. Thus p.image(g)<p which says that p is infinite and therefore contradicts the assumption that p is a finite set.

  all(a:A, p:A?)
      require
          r1: (p+{a}).is_infinite
          r2: a /in p
      check
          c1: all(f:A->A)
              require
                  r3: f.is_injective
                  r4: p+{a} <= f.domain
                  r5: (p+{a}).image(f) < p+{a}
              check
                  c2: a /in (p+{a}).image(f) or a in (p+{a}).image(f)
                  c3: require
                          r6: a /in (p+{a}).image(f)
                      check
                          c4: (p+{a}).image(f) <= p                 -- r5,r6
                          c5: p.image(f) = (p+{a}).image(f)-{f(a)}  -- r2
                          c6: p.image(f) < p                        -- c4,c5
                      ensure
                          p.is_infinite       -- r3,r4,c6
                      end
                  c7: require
                          r7: a in (p+{a}).image(f)
                      local
                          r8: b = (-f)(a)      -- -f is the inverse of f
                          r9: g = f <+ {a->f(b),b->f(a)}
                      check
                          c8: g.is_injective            -- r3,r9
                          c9: g(a) = a                  -- r8,r9
                          c10: (p+{a}).image(g) < p+{a} -- r5,r9
                          c11: p.image(g) < p           -- c9,c10
                          c12: p <= g.domain            -- r4,r9
                      ensure
                          p.is_infinite                 -- c8,c11,c12
                      end
              ensure
                  p.is_infinite       -- c2,c3,c7
              end
      ensure
          p.is_infinite               -- r1,c1
      end
 
  all(a:A, p:A?)
      require
          r1: p.is_finite
      check
          c1: a in p or a /in p
          c2: a in p => (p+{a}).is_finite   -- trivial
          c3: require
                  r2: a /in p
                  r3: (p+{a}).is_infinite
              check
                  c4: p.is_infinite         -- r2,r3,previous theorem
              ensure
                  False                     -- r1,c4
              end
      ensure
          (p+{a}).is_finite                 -- c1,c2,c3
      end
 

Infinite chains

Let a.closed(f) be a chain under the function f and all elements of the chain are in the domain of f. This implies that the set p is infinite.

Proof: Since f is an injection on a.closed(f) and a.closed(f) is completely contained in the domain of f and f maps the chain to a proper subset (a.closed(f).image(f) does not contain a) we have a witness for the injective function required in the definition of infiniteness.

  all(a:A, f:A->A)
      require
          r1: a.closed(f).is_chain(f)
          r2: a.closed(f) <= f.domain
      check
          c1: (f|a.closed(f)).is_injective              -- r1
          c2: a.closed(f) <= (f|a.closed(f)).domain     -- r2
          c3: a.closed(f).image(f|a.closed(f))
              = a.closed(f).image(f)                    -- general law
          c4: a.closed(f).image(f) = a.closed(f)-{a}
          c5: a.closed(f).image(f) < a.closed(f)        -- c4
          c6: a.closed(f).image(f|a.closed(f) < a.closed(f) -- c3,c5
          c7: some(g:A->A)
                  g.is_injective
                  and a.closed(f) <= g.domain
                  and a.closed(f).image(g) < a.closed(f)
                  -- c1,c2,c6, witness f|a.closed(f)
      ensure
          a.closed(f).is_infinite    -- c7
      end
 

This theorem implies in the contrapositive that any finite chain of the form a.closed(f) must have one out of domain element.

  all(a:A, f:A->A)
      require
          a.closed(f).is_chain(f)
          a.closed(f).is_finite
      ensure
          some(x:A) x in a.closed(f) and x /in f.domain
             -- contrapositive of the above theorem
      end
 

Finite chains

In the previous chapter we have proved that all finite chains of the form a.closed(f) must have some out of domain element. In the following we prove that the existence of an out of domain element in a chain of the form a.closed(f) is sufficient to conclude that the chain is finite.

We first prove that for all elements x in a.closed(f) the closure a.closed(f-x) is finite. We do this by induction. We put all elements x with a.closed(f-x).is_finite into a set p. The start element a is in this set because a.closed(f-a) is the one element set {a} which is definitely finite. Now assume that a.closed(f-x) is finite and x is in the domain of f. The set a.closed(f-f(x)) is equal to the set a.closed(f-x) + {f(x)}. Since a.closed(f-x) is finite a.closed(f-f(x)) is finite as well and therefore p is closed under f. Thus for all x in a.closed(f) we have a.closed(f-x) is finite.

Now assume that there is one element e in a.closed(f) which is not in the domain of f. Therefore f = f-e. Since e is in a.closed(f) we have a.closed(f-e) is finite and therefore a.closed(f) is finite as well.

Cycles are finite

Let's assume that a.closed(f) is a cycle. From this we conclude that a is in f(a).closed(f) and f(a).closed(f) = a.closed(f) by definition of a cycle. By induction we can prove that all elements of f(a).closed(f) are in f(a).closed(f-a). Since f-a <= f and the closure is monotonic in the function we get the equality f(a).closed(f) = f(a).closed(f-a). Since f(a).closed(f-a) is a chain with an out of domain element it is finite. Therefore a.closed(f) is finite as well.

Closures with cycles are finite

Let's assume that a.closed(f) has a cycle. Then we claim that a.closed(f) is finite.

From our intuition we know that there is an element e in a.closed(f) so that a.closed(f-e) is a chain which contains all elements of a.closed(f). Since a chain with one out of domain element is finite we can conclude that a.closed(f) is finite. It remains to be proved that an element e exists within a.closed(f) such that a.closed(f) = a.closed(f-e).

We prove this claim by contradiction. We assume that for all elements e of a.closed(f) we have a.closed(f-e) < a.closed(f). We define a set p = {x: all(e) e in x.closed(f) => x.closed(f-e)<x.closed(f)}. From our assumption we conclude that a is in this set. Furthermore we can prove that p is closed under f. Assume an element x in p and in the domain of f. x.closed(f) does not contain an element e so that x.closed(f-e)=x.closed(f). Since f(x).closed(f) is a subset of x.closed(f) the same applies to f(x). Therefore f(x) is in p as well.

But a.closed(f) has a cycle. I.e. there is an element b in a.closed(f) so that b.closed(f) is a cycle. f is injective on b.closed(f) therefore there is a unique predecessor e of b which is also in a.closed(f). By the same reasoning as in the previous chapter we can conclude that b.closed(f-e)=b.closed(f) which contradicts the assumption that there is no element a.closed(f) which has this property. Therefore the assumption must be wrong that there is no element e in a.closed(f) so that a.closed(f-e)=a.closed(f).

Emacs suffix

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

- Introduction

- Motivation

- Sequences and closures

- Induction

- Cycles and chains

- Simple properties

- Predecessor

- All elements of cycles

- Domain restrictions

- Definitions

- Out of domain elements are unique

- Sequencing

- Cycles

- Two cycles are identical or disjoint

- Cycles are unique

- All elements of a cycle have predecessors

- All elements of a cycle have unique predecessors

- Closures with cycles are completely in the domain

- Closures are connected

- Chains

- A chain has an injective function

- The image of a chain does not contain the first element

- Finiteness

- Definitions

- Infinite chains

- Finite chains

- Cycles are finite

- Closures with cycles are finite

- Emacs suffix


ip-location