Functions and Complete Partial Orders

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.