The Eiffel Compiler / Interpreter (tecomp)

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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.

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.

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

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

- Out of domain elements are unique

- Cycles

- Two cycles are identical or disjoint

- All elements of a cycle have predecessors

- All elements of a cycle have unique predecessors

- Closures with cycles are completely in the domain

- Chains

- A chain has an injective function

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