SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/functions and cpos

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.

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

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

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.

Emacs suffix

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

- Motivation

- Partial order

- Basic definitions

- Related elements

- Upper and lower bounds

- Directed sets and chains

- Supremum

- Maps between partial orders

- Complete partial order

- Functions

- Basic definitions

- Partial order

- Bottom element

- Connection to relations

- Union of functions

- Supremum

- Emacs suffix


ip-location