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:

– Each chain which has no out of domain elements is infinite.

– Each chain which has an out of domain element is finite.

– Each cycle is finite.

– Each closure which has a cycle is finite.

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

Advertisements
  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

%d bloggers like this: