The Eiffel Compiler / Interpreter (tecomp)

Why study complete partial orders?

Let us look at some simple examples. Everybody knows the recursive definition of the factorial function. In our programming language the definition looks like:

factorial(n:NATURAL): NATURAL ensure Result = if n=0 then 1 else n*factorial(n-1) end end

But this is not a classical definition. A classical definition of a function defines a function in terms of simpler functions. This is a recursive definition, i.e. we use the function to define the function.

From our intuition we know that this recursive function is well behaved. If we call the function 'factorial' and enter the recursive branch, we know that the recursive call is with a smaller argument. Finally the recursion will terminate and the function returns some value.

From a mathematical point of view the above recursive definition is a property which the function 'factorial' has to satisfy. I.e. the definition says that the function 'factorial' has to satisfy the following property.

all(n:NATURAL) ensure factorial(n) = if n=0 then 1 else n*factorial(n-1) end end

Two questions arise naturally from such a property.

- Is there a function which satisfies this property?
- Is this function unique?

The property states that the function 'factorial' and the function 'n -> if n=0 then 1 else n*factorial(n-1) end' are the same function. We can express this better if we define the mapping

g(f:NATURAL->NATURAL): NATURAL->NATURAL ensure Result = (n -> if n=0 then 1 else n*f(n-1) end) end

which maps one function of type NATURAL->NATURAL to another function of the same type. Now the property which 'factorial' has to satisfy reads

all(n:NATURAL) ensure factorial(n) = g(factorial)(n) end

or simpler

factorial = g(factorial)

I.e. the function 'factorial' has to be a fixpoint of the function 'g'.

We can feed any function as an argument into the function 'g'. For any function 'f' we get

all(f:NATURAL->NATURAL) ensure g(f).domain = {0} + f.domain.image(n->n+1) end

i.e. 'g(f).domain' is zero plus the domain of 'f' shifted one up. I.e. 'g(f).domain' has more elements than 'f.domain' (but is not necessarily a superset).

If we feed the completely undefined function '0' into 'g' we get a function whose domain has one element. We can iterate this

g(0).domain = {0} g(g(0)).domain = {0,1} g(g(g(0))).domain = {0,1,2} ...

i.e. the set

(0).closed(g) = {0, g(0), g(g(0)), g(g(g(0))), ... }

is a chain. Any chain of functions has a supremum as we will see below. The supremum of this chain is the fixpoint of 'g'.

The theory behind complete partial order gives a lot of mathematical tools to decide if a fixpoint of a function exists, if it is unique etc. In order to apply the theory to functions we have to verify that the category of functions is a complete partial order. In this paper we prove that functions form a complete partial order. The properties of a complete partial order will be studied in a different article.

The content of this article is based on the results of the articles

- Predicates as sets
- Complete lattices and closure systems
- Binary relations, endorelations and transitive closures.

Let us recall shortly the basic definitions of a partial order.

-- module: partial_order deferred class PARTIAL_ORDER end feature -- Basic definitions and axioms <= (a,b:CURRENT): BOOLEAN deferred end < (a,b:CURRENT): BOOLEAN ensure Result = (a<=b and a/=b) end >= (a,b:CURRENT): BOOLEAN ensure Result = b<=a end > (a,b:CURRENT): BOOLEAN ensure Result = b<a end all deferred ensure (<=).is_reflexive (<=).is_transitive (<=).is_antisymmtric end end -- Basic definitions

Two elements 'a' and 'b' of a partial order are related if either 'a<=b' or 'b<=a' is valid.

feature -- Related elements is_related(a,b:CURRENT): BOOLEAN ensure Result = (a<=b or b<=a) end end

For two related elements the maximum (and the minimum) is defined

maximum(a,b:CURRENT): CURRENT require a.is_related(b) ensure Result = if a<=b then b else a end end end -- Related elements

An element 'a' is an upper bound of a set 'p' if it dominates all elements in 'p'. An element 'a' is a lower bound of a set 'p' if all elements of 'p' dominate 'a'.

feature -- Upper and lower bounds <= (p:CURRENT?, a:CURRENT): ghost BOOLEAN -- Is `a' an upper bound of the set `p'? ensure Result = all(x) x in p => x<=a end <= (a:CURRENT, p:CURRENT?): ghost BOOLEAN -- Is `a' a lower bound of the set `p'? ensure Result = all(x) x in p => a<=x end end -- Upper and lower bounds

A set is directed if it is nonempty and contains for each pair of elements an upper bound of this pair.

feature -- Directed sets and chains is_directed(p:CURRENT?): ghost BOOLEAN -- Is the set `p' nonempty and has for each pair -- of elements an upper bound for these elements? ensure Result = (p/=0 and all(a,b) {a,b}<=p => some(c) {a,b}<=c and c in p) end -- Note {a,b}<=p means that {a,b} is a subset of p -- {a,b}<=c means that c is an upper bound of {a,b}

A set is a chain if each two elemens 'a' and 'b' are releated

is_chain(p:CURRENT?): ghost BOOLEAN ensure Result = all(a,b) {a,b}<=p => a.is_related(b) end

Clearly every nonempty chain is a directed set because for each pair the maximum of both elements is an upper bound for both.

all(p:CURRENT?) require r1: p /= 0 r2: p.is_chain check c1: all(a,b:CURRENT) require r3: {a,b}<=p check c2: a.is_related(b) -- r2,r3 c3: {a,b}<=maximum(a,b) -- definition 'maximum' ensure some(c:CURRENT) {a,b}<=c -- c3 end ensure p.is_directed -- r1,c1 end end -- Directed sets and chains

An element 's' is a supremum of a set 'p' if it is the least upper bound of 'p'. In order to define a supremum we need the following definitions.

feature -- Supremum upper_bounds(p:CURRENT?): ghost CURRENT? -- The set of upper bounds of the set `p'. ensure Result = {x: p<=x} end is_least(a:CURRENT, p:CURRENT?): ghost BOOLEAN -- Is `a' the least element of the set `p'? ensure Result = (a in p and a<=p) end is_supremum(a:CURRENT, p:CURRENT?): ghost BOOLEAN -- Is `a' the supremum of the set `p'? ensure Result = a.is_least(p.upper_bounds) end

The least element of a set (if it exists) is unique.

all(a,b:CURRENT, p:CURRENT?) require a.is_least(p) b.is_least(p) ensure a=b end

This implies that a supremum is unique if it exists

all(a,b:CURRENT, p:CURRENT?) require a.is_supremum(p) b.is_supremum(p) ensure a=b end end -- Supremum

The dual notions like 'is_greatest, 'is_infimum' etc. can be defined in a similar manner.

A function of type A->B where A and B are partial orders is monotonic or orderpreserving if 'a<=b' implies 'f(a)<=f(b)'.

local A: CURRENT B: CURRENT feature -- Maps is_monotonic(f:A->B): ghost BOOLEAN -- Is the function `f' order preserving ensure Result = all(a,b:A) {a,b}<=f.domain => a<=b => f(a)<=f(b) end

Monotonic maps preserve upper/lower bounds and least elements

all(a:A, p:A?, f:A->B) require f.is_monotonic a in f.domain check -- Proof: expand the definitions of '<=' and 'image' and -- use the elimination law of existential quantification ensure a<=p => f(a)<=p.image(f) p<=a => p.image(f)<=f(a) end

all(a:A, p:A?, f:A->B) require f.is_monotonic a in f.domain a.is_least(p) check -- Proof: expand the definitions of 'is_least' and 'image' and -- use the elimination law of existential quantification ensure f(a).is_least(p.image(f)) end

end -- Maps

A set of elements of a partial order may have a supremum or not. Furthermore a least element of a partial order may exist or not.

In a complete partial order each directed set has a supremum. We call this order and upcomplete partial order because the dual notion of a downcomplete partial order is possible as well (where filtered set/infimum is used instead of directed set/supremum).

An upcomplete partial order has the following basic definition.

-- module: upcomplete_partial_order deferred class UPCOMPLETE_PARTIAL_ORDER inherit PARTIAL_ORDER end feature -- Basic functions and axioms supremum(p:CURRENT?): ghost CURRENT require p.is_directed deferred end all(a:CURRENT, p:CURRENT?) deferred ensure least: 0 <= a supremum: p.is_directed => p.supremum.is_supremum(p) end end

The type FUNCTION[A,B] defines the partial functions from objects of type A to objects of type B. The type A->B is a shorthand for FUNCTION[A,B]. Tuples can be used to specify functions with multiple arguments and return values (e.g. [A1,A2,...]->[B1,B2,...] which is a shorthand for FUNCTION[ [A1,A2,...],[B1,B2,...] ]).

-- module: function A: ANY B: ANY immutable class FUNCTION[A,B] inherit ghost UPCOMPLETE_PARTIAL_ORDER end

Each function 'f' has a domain 'f.domain' and for arguments 'a' within its domain (i.e. 'a in f.domain') the value 'f(a)' is defined (instead of 'f(a)' we can use the notation 'a.f' as well).

feature domain(f:CURRENT): ghost A? -- The domain of the function. note built_in end () (f:CURRENT, a:A): B -- The value of the function at `a' (written f(a) or a.f). require a in f.domain note built_in end range(f:CURRENT): ghost B? -- The range of the function `f'. ensure Result = {b: some(a:A) a in f.domain and f(a)=b} end end

The partial functions from A to B form a partial order. The function 'f' is less or equal than the function 'g' if the domain of 'f' is a subset of the domain of 'g' and the values of 'f' and 'g' are the same within the common domain.

feature <= (f,g:CURRENT): ghost BOOLEAN -- Is the domain of `f' contained within the domain of `g' and -- have both functions the same values within the common domain? ensure Result = (f.domain<=g.domain and all(a:A) a in f.domain => f(a)=g(a)) end = (f,g:CURRENT): ghost BOOLEAN -- Do `f' and `g' define the same function. ensure Result = (f<=g and g<=f) end all ensure -- Proofs: expansion of definitions (<=).is_reflexive (<=).is_transitive (<=).is_antisymmetric end end

It is easy to prove that '<=' is reflexive, transitive and antisymmetric.

The bottom element of the type A->B is the function which is has an empty domain, i.e which is not defined for any argument.

feature -- Bottom element 0: CURRENT ensure Result.domain = 0 end

It is evident that '0' is the least function with respect to the defined order.

all(f:CURRENT) ensure 0 <= f -- trivial end end -- Bottom element

We can map each function of type A->B to a relation of type [A,B]?.

feature -- relations relation(f:CURRENT): ghost [A,B]? -- The relation defined by the function `f'. ensure Result = {a,b: a in f.domain and b=f(a)} end

Clearly the relation defined by the function 'f' is functional and the domain of the function conicides with the domain of the relation and the range of the function conicides with the range of the relation. Furthermore the function 'relation' which maps functions to relations is monotonic

all(f:CURRENT) ensure f.domain = f.relation.domain f.range = f.relation.range f.relation.is_functional relation.is_monotonic end

For any functional relation 'r' we can reconstruct the corresponding function. A relation is functional if the image of each element in its domain is unique. By expanding the definition of 'is_functional' we get the following assertion.

all(r:[A,B]?, a:A) require r1: r.is_functional r2: a in r.domain ensure exist: some(b:B) [a,b] in r -- r2, def 'domain' unique: all(x,y:B) [a,x] in r => [a,y] in r => x=y -- r1, def 'is_functional end

I.e. for each object 'a' in the domain of 'r' there exists an image under 'r' and the image is unique. Having this we can define a function 'value' which returns this unique value.

value(r:[A,B]?, a:A): ghost B -- The unique image of `a' under the functional relation `r'. require r.is_functional a in r.domain ensure [a,Result] in r end

With this function we can define another function which maps a functional relation 'r' back to its function.

function(r:[A,B]?): ghost CURRENT -- The function defined by the functional relation `r'. require r.is_functional ensure Result = (a -> r.value(a)) end

Clearly 'function' is the inverse of 'relation'. Furthermore 'function' is monotonic.

all(f:CURRENT?, r:[A,B]?) ensure f = f.relation.function r.is_functional => r.function.relation=r function.is_monotonic end

end -- relations

A function is greater than another function if it has a greater domain and within the common domain both functions have the same values for the same arguments. If we have two functions 'f' and 'g' we might want to build the union of the two functions so that the union has the union of the domains of 'f' and 'g'. It is intuitively clear that such a union is possible only if 'f' and 'g' do not have different values for arguments within their common domain.

In order to define union of functions we first define the domain restriction for a function.

feature -- Union of functions <: (d:A?, f:CURRENT): ghost CURRENT -- The function `f' restricted to the domain `d*f.domain'. ensure Result <= f Result.domain = d*f.domain end

With a domain restriction we can split the relation of a function into two disjoint parts.

all(d:A?, f:CURRENT) ensure (d<:f).relation * ((-d)<:f).relation = 0 end

Furthermore two subsequent domain restrictions are equivalent to the domain restriction of the intersection (this implies that two subsequent domain restrictions are commutative).

all(d,e:A?, f:CURRENT) check c1: (d<:e<:f).domain = d*e*f.domain ensure e1: d<:e<:f = (d*e)<:f -- c1 e2: d<:e<:f = e<:d<:f -- e1 end -- Note: The operator '<:' is right associative because it ends with -- a colon.

We say that two functions 'f' and 'g' are consistent if their restriction to the intersection of their domains define the same function.

is_consistent(f,g:CURRENT): ghost BOOLEAN ensure Result = (g.domain<:f = f.domain<:g) end

Intuitively two functions are consistent if they don't have any conflicting values.

If two functions are consistent then the union of their relations is functional.

all(f,g:CURRENT, r:[A,B]?) require r1: f.is_consistent(g) local r2: r = f.relation + g.relation check c1: all(a:A, x,y:B) require r3: [a,x] in r r4: [a,y] in r check c2: a in f.domain-g.domain or a in g.domain-f.domain or a in f.domain*g.domain ensure x=y -- r1,r2,r3,r4,c2 case split end c2: r.is_functional ensure (f.relation+g.relation).is_functional -- c2 end

Having this we can define the union of two consistent functions

+ (f,g:CURRENT): ghost CURRENT require f.is_consistent(g) ensure Result = (f.relation+g.relation).function end

On the other hand if two functions have an upper bound then they are consistent.

all(f,g,h:CURRENT) require r1: f<=h r2: g<=h check c1: f = f.domain<:h -- r1 c2: g = g.domain<:h -- r2 c3: g.domain<:f = (g.domain*f.domain)<:h -- c1 c4: f.domain<:g = (f.domain*g.domain)<:h -- c2 c5: g.domain<:f = f.domain<:g -- c3,c4 ensure f.is_consistent(g) -- c5 end

Therefore any two functions of a directed set are consistent

all(d:CURRENT?, f,g:CURRENT) require d.is_directed f in d g in d check some(h) h in d and {f,g}<=h ensure f.is_consistent(g) end

end -- Union of functions

In order to satisfy the requirements of an upcomplete partial order we have to define the supremum of a directed set of functions.

Within a directed set of functions each two functions have an upper bound within the set. In the last chapter we have proved that two functions which have an upper bound are consistent. This implies that all functions of a directed set are consistent.

In order to define the supremum of a directed set we can try the following construction.

We can map the directed set 'd' of functions to a set of relations.

d.image(relation)

As demonstrated in the article "Predicates as sets" each set of sets has a supremum. Since a relation is a set of pairs a set of relations is a set of sets. Therefore we can calculte the supremum by

d.image(relation).supremum

If we can prove that this supremum is a functional relation then we can transform this relation back to a function by

d.image(relation).supremum.function

We have to prove two assertions

- 'd.image(relation).supremum' is a functional relation
- 'd.image(relation).supremum.function' is the supremum of 'd'

As a first step we prove that 'd.image(relation).supremum' is a functional relation.

feature -- Supremum

all(d:CURRENT?) require r1: d.is_directed local r2: rr = d.image(relation) r3: r = rr.supremum check c1: all(a:A, x,y:B) require r4: [a,x] in r r5: [a,y] in r check c2: some(s:[A,B]?) s in rr and [a,x] in s -- r3,r4 c3: some(t:[A,B]?) s in rr and [a,y] in s -- r3,r5 c4: some(f) f in d and f(a)=x -- r2,c2 c5: some(g) g in d and g(a)=y -- r2,c3 c6: all(f,g) require r6: f in d; r7: g in d r8: f(a)=x; r9: g(a)=y check c7: f.is_consistent(g) -- r1,r6,r7 ensure x=y -- c7,r8,r9 end ensure x=y end ensure d.image(relation).supremum.is_functional end

Having this assertion the following function is well defined.

supremum(d:CURRENT?): ghost CURRENT -- The supremum of a directed set of functions. require d.is_directed ensure Result = d.image(relation).supremum.function end

But we still have to prove that 'd.supremum' is really the supremum of 'd'. In order to prove this we have to demonstrate that 'd.supremum' is an upper bound of 'd' and that all upper bounds of 'd' are greater equal than 'd.supremum'.

First we verify 'd<=d.supremum' i.e. that 'd.supremum' is an upper bound of 'd'.

all(d:CURRENT?) check c1: all(f:CURRENT) require r1: f in d local r2: r = d.image(relation).supremum check c2: f.relation<=r -- 'r' is supremum c3: f.relation.function<=r.function -- 'function' is monotonic ensure f<=d.supremum -- c3 end ensure d<=d.supremum -- c1 end

In a second step we prove that 'd.supremum' is the least of all upper bounds.

all(d:CURRENT?, f:CURRENT) require r1: d.is_directed r2: d<=f local r3: r = d.image(relation).supremum check c1: d.image(relation)<=f.relation -- 'relation' is monotonic c2: r<=f.relation -- c1,r3, 'r' is supremum c3: r.function<=f.relation.function -- c2, 'function' is monotonic ensure d.supremum<=f -- r3,c3 end

end -- Supremum

This completes the proof that the type A->B implements an upcomplete partial order.

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