# Motivation

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.

# Partial order

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

## Basic definitions

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

## Related elements

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

## Upper and lower bounds

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

## Directed sets and chains

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

## Supremum

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.

## Maps between partial orders

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

# Complete partial order

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

# Functions

## Basic definitions

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

## Partial order

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.

## Bottom element

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

## Connection to relations

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

## Union of functions

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

## Supremum

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.

#1 by Asma Al-Harbi on November 29, 2012 - 5:47 am

nice article 🙂

excuse me i jst wanna ask u how could u put ur codes as blocks in ur blog?

#2 by helmutbrandl on December 1, 2012 - 10:48 pm

I just use preformatted blocks i.e. I put the code between a <pre> and a </pre> html tag. The fusion theme highlights the code blocks.

#3 by Asma Al-Harbi on December 14, 2012 - 3:46 am

thx ! 😀