Primitive recursive functions and fixpoints

Introduction

Recursion and fixpoint equations

The mathematical content of the definition of a recursive function is a
fixpoint equation. Let us demonstrate this statement with a simple example.

The textbook example of a recursive function is the factorial function. In our
programming language it looks like

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

The keyword Result represents factorial(n) i.e. the value of the function
at the argument n. Since the postcondition is an equation the specification
of this function says

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

This specification states that the function factorial and the function n ->
if n=0 then 1 else n*factorial(n-1) end
are the same function.

From the function factorial we can extract the functional (for convenience
we call a function which accepts and returns functions a functional)

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

and then the specification of the function factorial reads like

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

i.e. the function factorial has to satisfy the fixpoint equation

factorial = f(factorial)

From the mathematical point of view two questions arise

  1. Does the functional f have a fixpoint (i.e. existence)?
  2. Is the fixpoint of the functional f unique?

If the answer to both question is yes then we can say that the functional
f defines uniquely a function.

In this article we study this question for primitive recursive functions over
natural numbers of the form

G: ANY

gr(n:NATURAL): G
    ensure
        Result = if n=0 then c            -- c: constant (function)
                 else h(gr(n-1),n)        -- h: total function
                 end
    end

where the constant (function) c and the function h:[G,NATURAL]->G are well
defined. For the factorial function we have c=1 and h = ([a,b] -> b*a).

Outline of the paper

We restrict our investigation about primitive recursive functions in this
paper to primitive recursive functions on natural numbers.

We do not use a specific type NATURAL but an abstract class
ABSTRACT_NATURAL. This is convenient because we can have different
implementations of natural numbers. One possible implementation is to use a
machine word (e.g. 32 or 64 bit) to implement natural numbers or to use a
sequence of numbers to implement arbitrary sized natural numbers. Since the
basic properties and assertions of all implementations are identical it is
sufficient to derive them once in an abstract module.

In the first chapter we introduce the module abstract_natural, give the
basic definitions, prove the induction law, show that there are infinitely
many natural numbers, introduce an order relation on the abstract natural
numbers and show that the order is a wellorder.

In the second chapter we introduce a general format of recursive functions and
show that typical recursive functions fit into this pattern.

In the third chapter we scrutinize the functional which represents a primitive
recursive function. We proof that the functional is monotonic, continuous and
has a unique fixpoint.

The number zero, the empty set and the undefined function

In our programming language we can use constants like 0 as names of
functions. In the class of natural numbers the constant 0 specifies the
number zero. In the class of sets 0 represents the empty set and 1
represents the universal set. In the class of partial functions (type A->B
where A and B are arbitrary types) the constant 0 represents the
completely undefined functions i.e. the function with an empty domain.

In this article the constant 0 appears with all these meanings. Usually it
is clear from the context whether the number zero, the empty set or the
undefined function is meant. Sometimes type annotations like 0:G? are used
to annotate that 0 is of type G? and represents therefore the empty set of
elements of type G.

Abstract natural numbers

Basic definitions

In the module abstract_natural we want to use axioms which are equivalent to
the five peano axioms. The five peano axioms are:

  1. Zero is a natural number

  2. All natural numbers have successor

  3. Zero is not the successor of a natural number

  4. Two natural numbers which have the same successor are identical

  5. Any property which is valid for the number zero and whose validity for any
    number implies its validity for the successor of this number is valid for all
    natural numbers.

The basic definition of the module abstract_natural looks like:

deferred class
    ABSTRACT_NATURAL
end

feature    -- Basic functions and axioms
    0: CURRENT                                              -- peano 1
        deferred end

    succ(n:CURRENT): CURRENT                                -- peano 2
        deferred end

    1: CURRENT
        deferred ensure Result = succ(0) end

    all(n,m:CURRENT)
        deferred
        ensure
            zero_not_succ:  n.succ /= 0                     -- peano 3
            succ_injective: n.succ=m.succ => n=m            -- peano 4
            closed:         (0).closed(succ) = (1:CURRENT?) -- peano 5
        end
end

In order to represent the first peano axiom we use the constant function
0. The second peano axiom is represented by the successor function
succ.

The third and forth peano axiom are represented by the assertions
zero_not_succ and succ_injective.

The assertion closed says that we can reach all natural numbers by starting
from the number 0 and applying the successor function succ an arbitrary
number of times. It will be shown in the next chapter that the assertion
closed is equivalent to the fifth peano axiom.

Induction law

We are going to demonstrate that the assertion closed is sufficient to prove
the classical induction law. Let us translate the fifth peano axiom
(induction) into our programming language

induction:
all(e:BOOLEAN)
    require
        r1: e[n:=0]
        r2: all(n:CURRENT) e => e[n:=n.succ]
    ensure
        all(n:CURRENT) e      -- r1,r2, induction_lemma (see below)
    end

Because (0).closed(succ) is a closure we get the general law

closure_induction_1:
all(p:CURRENT?)
    require
        0 in p
        p.is_closed(succ)
    ensure
        (0).closed(succ) <= p   -- See "Closures and fixpoints"
    end

which have already been proved in the paper “Closures and fixpoints”. From
this law using closed we can immediately derive the following assertion

closure_induction_2:
all(p:CURRENT?)
    require
        r1: 0 in p
        r2: p.is_closed(succ)
    check
        c1: (0).closed(succ) <= p     -- r1,r2,closure_induction_1
        c2: (1:CURRENT?) <= p         -- c1,closed
    ensure
        p = (1:CURRENT?)              -- c2, 1 is greatest set
    end

Now it is easy to derive the classical induction law.

induction_lemma:
all(e:BOOLEAN)
    require
        r1: e[n:=0]
        r2: all(n:CURRENT) e => e[n:=n.succ]
    local
        l1: p:CURRENT? := {n: e}
    check
        c1: 0 in p                -- l1,r1
        c2: p.is_closed(succ)     -- l1,r2
        c3: p = (1:CURRENT?)      -- c1,c2,closure_induction_2
        c4: all(n:CURRENT) n in p -- c3
    ensure
        all(n:CURRENT) e          -- l1,c4
    end

Range of the successor function

We claim that the range of the successor function contains all natural numbers
except zero.

range:
all
    ensure
        succ.range = {n: n/=0}             -- lemma_range
    end

In order to convert this into a valid proof we have to prove that succ.range
and {n:n/=0} are the same set. Two sets are the identical if they contain
the same elements i.e. we have to prove all(n) n in {n:n/=0} = n in
succ.range
. Since this is a statement about all natural numbers we prove this
assertion by induction (Note that n in {x:e} = e[x:=n] i.e. n in {n:n/=0} =
n/=0
).

lemma_range:
all(n:CURRENT)
    check
        c1: 0 /in succ.range             -- zero_not_succ
        c2: (0/=0) = 0 in succ.range     -- c1
        c3: all(n:CURRENT)
                require
                    (n/=0) = n in succ.range
                check
                    c4: n.succ /= 0             -- zero_not_succ
                    c5: n.succ in succ.range    -- trivial
                ensure
                    (n.succ/=0) = n.succ in succ.range   -- c4,c5
                end
    ensure
        (n/=0) = n in succ.range         -- c2,c3,induction
    end

Infinity

One of the immediate consequences of the basic definitions is that the set of
natural numbers must be infinite. We can see this by the following reasoning.

Since the successor function is defined as a total function (no preconditions)
its domain is the set of all natural numbers.

 succ.domain = (1:CURRENT?)

In the previous chapter we have proved succ.range = {n:n/=0}. This implies
that the range of the successor function is a proper subset of its domain.

succ.range < succ.domain

Because of the axiom succ_injective the successor function is injective

succ.is_injective

From this we can conclude that the set of natural numbers is
infinite. Remember the definition of infiniteness of a set: A set p is
infinite if there is an endofunction f whose domain is the set p and
whose range is a proper subset of its domain. The successor function is such a
function for the natural numbers.

I.e. we get

(0).closed(succ).is_infinite

and because of closed

infinite: (1:CURRENT?).is_infinite

Predecessor function

Every injective function f has an inverse function g=f.inverse such that
f.domain=g.range and f.range=g.domain. The successor function is an
injective function. The range of the successor function is
{n:n/=0}. Therefore the following predecessor function is uniquely defined.

pred(n:CURRENT): CURRENT
    require
        n /= 0
    deferred
    ensure
        Result = (succ.inverse)(n)
    end

Order relation

We define an order relation on natural numbers by defining n<=m if and only
if the number m can be reached by starting at the number n and applying
the successor function zero or more times.

<= (n,m:CURRENT): BOOLEAN
    deferred
    ensure
        Result = m in n.closed(succ)
    end

all(a,b:CURRENT)
    ensure
        (<=).is_reflexive        -- consequence of closure
        (<=).is_transitive       -- consequence of closure
        a<=b => b<=a => a=b      -- lemma_anti (see below)
        a<=b or b<=a             -- lemma_linear (see below)
    end

The reflexivity and transitivity of the relation <= are direct consequences
of its definition as a closure. The proofs of the antisymmetry and the
linearity of <= need a little bit more reasoning. In order to prove these
properties we need some definitions and laws given in the article
“Endofunctions, closures, cycles and chains”.

Let A be any type.

is_connected(p:A?, f:A->A): ghost BOOLEAN
        -- Is the set p connected under the function f? 
    ensure
        Result = all(a,b) 
                     require
                         {a,b}<=p
                     ensure
                         b in a.closed(f) or a in b.closed(f)
                     end
    end

is_cycle(p:A?, f:A->A): ghost BOOLEAN
        -- Does the set p form a cycle under 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
        -- Has the set p a subset which forms a cycle under f?
    ensure
        Result = some(q:A?) q<=p and q.is_cycle(f)
    end

is_chain(p:A?, f:A->A): ghost BOOLEAN
        -- Is the set p a chain under f?
    ensure
        Result = (p.is_closed(f)
                  and p.is_connected(f)
                  and not p.has_cycle(f))
    end

With these definitions the following laws have been derived within the article
“Endofunctions, closures, cycles and chains”:

all(a:A, f:A->A)
    ensure
        connected:       a.closed(f).is_connected(f)
        infinite_chain:  
            a.closed(f).is_infinite => a.closed(f).is_chain(f)
    end

Having these laws it is easy to prove the linearity of the order relation.

lemma_linear:
all(a,b:CURRENT)
    check
        c1: (0).closed(succ).is_connected(succ)  -- connected
        c2: b in a.closed(succ) or a in b.closed(succ)
                                                 -- c1, def is_connected
    ensure
        a<=b or b<=a                             -- c2
    end

The antisymmetry of the order relation requires all(a,b) a<=b => b<=a =>
a=b
. We prove this law by contradiction and assume that a/=b is
inconsistent with the assertions a<=b and b<=a. The inequality a/=b
implies that the set of natural numbers contained a cycle. This contradicts
the fact that the natural numbers form a chain which cannot contain a cycle.

lemma_anti:
all(a,b:CURRENT)
     require
         r1: a<=b
         r2: b<=a
     check
         c1: require
                 r3: a/=b
             check
                 c2:  b in a.closed(succ)              -- r1
                 c3:  a in b.closed(succ)              -- r2
                 c4:  b in a.succ.closed(succ)         -- c2,r3
                 c5:  a in a.succ.closed(succ)         -- c3,c4
                 c6:  a.closed(succ).is_cycle(succ)    -- c5
                 c7:  a.closed(succ)<=(0).closed(succ) -- closed
                 c8:  (0).closed(succ).has_cycle(succ) -- c6,c7
                 c9:  (0).closed(succ).is_infinite     -- infinite,closed
                 c10: (0).closed(succ).is_chain(succ)  -- c9,infinite_chain
                 c11: not (0).closed(succ).has_cycle(succ)  
                                                       -- c10,def chain
             ensure
                 false                                 -- c8,c11
             end
     ensure
         a=b                                           -- c1
     end

Wellorder

We claim that the order relation is a wellorder i.e. each nonempty set p has
a minimal element.

wellorder:
all(p:CURRENT?)
    require
        p /= 0
    ensure
        some(n) n.is_least(p)
    end

Before proving this theorem we first prove the related theorem all(n:CURRENT)
all(p:CURRENT?) p*{m:m<=n}/=0 => some(m) m.is_least(p)
which says that for
all natural numbers n and for all sets p the nonemptiness of the
intersection of p with the downward closure of n implies that there is a
least element of p. Since this is a statement about all natural number we
can use induction to proof it.

lemma_wo:
all(n:CURRENT, p:CURRENT?)
    check
        c1: require
                r1: p*{m:m<=0} /= 0
            check
                c2: 0 in p              -- r1
            ensure
                some(m) m.is_least(p)   -- c2, witness 0
            end

        c3: all(n:CURRENT)
            require
                r2: p*{m:m<=n}/=0 => some(m) m.is_least(p)
                r3: p*{n:m<=n.succ}/=0
            check
                c4: p*{m:m<=n}=0 or p*{m:m<=n}/=0
                c5: require
                        r4: p*{m:m<=n}=0
                    check
                        c6: n.succ in p             -- r3,r4
                        c7: n.succ.is_least(p)      -- c6,r4
                    ensure
                        some(m) m.is_least(p)       -- c7, witness n.succ
                    end
            ensure
                some(m) m.is_least(p)               -- c4,c5,r2
            end
    ensure
        p*{m:m<=n}/=0 => some(m) m.is_least(p)
    end

Having this we can prove the wellorder theorem.

wellorder:
all(p:CURRENT?)
    require
        r1: p /= 0
    check
        c1: some(n:CURRENT) n in p
        c2: some(n:CURRENT) p*{m:m<=n}/=0   -- c1
        c3: all(n:CURRENT)
            require
                 r2: p*{m:m<=n}/=0
            ensure
                 some(m) m.is_least(p)   -- r2, lemma_wo
            end
    ensure
        some(n) n.is_least(p)            -- c2,c3
    end

Recursive functions

Examples of recursive functions on natural numbers

Let us look at some primitive recursive functions on natural numbers. First we
can define addition of two natural numbers n+m. We use a definition
which is recursive in the first argument (an equivalent definition being
recursive in the second argument is possible as well).

+ (n,m:CURRENT): CURRENT
        -- The sum of the numbers n and m.
    deferred
    ensure
        Result = if n=0 then m 
                 else (n.pred+m).succ
                 end
    end

Then we can define multiplication of two natural number n*m.

* (n,m:CURRENT): CURRENT
        -- The product of the numbers n and m.
    deferred
    ensure
        Result = if n=0 then 0
                 else (n.pred*m) + m
                 end
    end

As a third typical primitive recursive function we define n^m which
represents the number n raised to the m-th power.

^ (n,m:CURRENT): CURRENT
        -- The  number n raised to the m-th power.
    deferred
    ensure
        Result = if m=0 then 1
                 else
                    n^(m.pred) * n
                 end
    end

Transformation into a general form

Now we want to transform the definition of a recursive function into the
general form

gr(n:CURRENT): G
    ensure
        Result = if n=0 then c
                 else h(gr(n.pred),n)
                 end
    end

where

c: CURRENT->G
h: [G,CURRENT]->G

Let us look at the function +

+ (n,m:CURRENT): CURRENT
    deferred
    ensure
        Result = if n=0 then m            -- (m->m)(m)
                 else (n.pred+m).succ     -- (m->(n.pred+m).succ)(m)
                 end
    end

to derive the transformation.

The function gr is a function of one argument and the function + has two
arguments. Therefore the result type G of the function gr has to be a
function of type CURRENT->CURRENT so that n+m = gr(n)(m) i.e. the function
gr is the curried version of +. If we uncurry the definition of gr we
get the generic form

gr2(n,m:CURRENT): CURRENT
    ensure
        Result = if n=0 then c(m)
                 else h((m->gr2(n.pred,m)),n)(m)
                 end
    end

-- where

gr(n.pred) = (m->gr2(n.pred,m))

If we match the definition of + with the generic definition of gr2 we get
the following correspondences:

c   =    (m -> m)
h   =    ([g,n] -> m -> g(m).succ)

For the functions * and ^ we get the following:

* (n,m:CURRENT): CURRENT
    deferred
    ensure
        Result = if n=0 then 0
                 else (n.pred*m) + m
                 end
    end

c   =  (m -> 0)
h   =  ([g,n] -> m -> g(m) + m)



^ (n,m:CURRENT): CURRENT    -- '^' is recursive in the second argument!!
    deferred
    ensure
        Result = if m=0 then 1
                 else
                    n^m.pred * n
                 end
    end

c   =  (n -> 1)
h   =  ([g,m] -> n -> g(n) * n)

-- Note: because '^' is recursive in the second argument we get
--       gr2(m,n) = n^m !!

Functional of a recursive function

Definition

The general definition of a (primitive) recursive function on natural numbers
looks like:

gr(n:CURRENT): G
    ensure
        Result = if n=0 then c
                 else h(gr(n.pred),n)
                 end
    end

with c:G and h:[G,CURRENT]->G where h is a total function. From this
definition we extract the functional f

f(g:CURRENT->G): CURRENT->G
    ensure
        Result = (n -> if n=0 then c
                       else h(g(n.pred),n)
                       end)
    end

so that the function gr is a fixpoint of the functional f.

gr = f(gr)                -- gr is fixpoint of f

The functional f depends only on c and h. Therefore we define a function
functional which given c and h returns the functional.

functional(c:G, h:[G,CURRENT]->G): (CURRENT->G)->(CURRENT->G)
    require
        h.is_total
    ensure
        Result = (g -> n -> if n=0 then c 
                            else h(g(n.pred),n)
                            end)
    end

Domain transformation

The functional f=functional(c,h) transforms the domain of any function
g:CURRENT->G according to the formula f(g).domain = {0} +
g.domain.image(succ)
. I.e. zero is contained in f(g).domain as well as all
elements of g.domain shifted one up. We prove this claim by the following
reasoning:

fdtrans:
all(c:G, h:[G,CURRENT]->G, f:(CURRENT->G)->(CURRENT->G), g:CURRENT->G)
    require
       r1: f = functional(c,h)
       r2: h.is_total
    check
       c1: g.domain.image(succ) = {n: some(m) m.succ = n and m in g.domain}
                                         -- def image
       c2: g.domain.image(succ) = {n: n/=0 and n.pred in g.domain}
                                         -- c1, def pred

       c3: f(g).domain = {0} + {n: n/=0 and n.pred in g.domain}
                                         -- r1, def functional
    ensure
       f(g).domain = {0} + g.domain.image(succ)   -- c3,c2
    end

Monotonicity

Any functional f=functional(c,h) is monotonic i.e. for all pairs of
functions a,b:CURRENT->G with a<=b we get f(a)<=f(b). Note that the
category of functions of type CURRENT->G forms a complete partial order. The
relation a<=b states that the domain of a is a subset of the domain of
b and that a and b restricted to the domain of a (i.e. b|a.domain)
are the same function.

We give a formal prove of the monotonicity of the functional f.

fmono:
all(c:G, h:[G,CURRENT]->G, f:(CURRENT->G)->(CURRENT->G))
    require
        r1: h.is_total
        r2: f = functional(c,h)
    check
        c1: all(a,b:CURRENT->G)
            require
                r1: a <= b
            check
                c2: a.domain <= b.domain         -- r1
                c3: {0} + a.domain.image(succ) <= {0} b.domain.image(succ)
                                                 -- c2
                c4: f(a).domain <= f(b).domain   -- c3,fdtrans

                c5: all(n:CURRENT)
                    require
                         r2: n in f(a).domain
                    check
                         c6: n in f(b).domain
                         c7: n=0 or n/=0
                         c8: f(a)(0) = f(b)(0)   -- = c
                         c9: require
                                 r3: n/=0
                             check
                                 c10: n.pred in a.domain      -- r2
                                 c11: n.pred in b.domain      -- c10,c2
                                 c12: a(n.pred)=b(n.pred)     -- r1,c10,c11
                                 c13: f(a)(n) = h(a(n.pred),n)  -- def f
                                 c14: f(b)(n) = h(b(n.pred),n)  -- def f
                             ensure
                                 f(a)(n) = f(b)(n)       -- c12,c13,c14
                             end
                    ensure
                         f(a)(n) = f(b)(n)               -- c7,c8,c9
                    end

                c15: f(a) = f(b)|f(a).domain     -- c4,c5
            ensure
                f(a) <= f(b)                     -- c4,c15
            end
    ensure
        f.is_monotonic
    end

Continuity

We claim that the functional f=functional(c,h) is continuous. Continuity
requires that the suprema of directed sets are maintained. I.e. if d is a
directed set and s=d.supremum its supremum then we have to prove that
d.image(f).supremum = f(s).

Since f is monotonic it is guaranteed that d.image(f) is a directed set
and that upper bounds of all sets are mapped to upper bounds. This implies
d.image(f) <= f(s).

In order to prove that f(s) is the least upper bound of d.image(f) we show
that the assumption of another upper bound g with d.image(f)<=g and
g<f(s) leads to a contradiction.

If there exists such an upper bound g then there has to be one element n
in the domain of f(s) which is not in the domain of g. In the case n=0
the contradiction is evident because all functions in d.image(f) have zero in
their domain and therefore g cannot be an upper bound. In the case n/=0 we
get n.pred in s.domain because n in f(s).domain. This implies that there
has to be one function a within d so that n.pred in a.domain otherwise
s would not be a supremum. This implies that there is another function a in
d.image(f)
so that n in a.domain. Therefore n has to be in the domain of
g because g is an upper bound of d.image(f). This contradicts the fact
that n /in g.domain.

fconti:
all(c:G, h:[G,CURRENT]->G, f:(CURRENT->G)->(CURRENT->G))
    require
        r1: h.is_total
        r2: f = functional(c,h)
    check
        c1: all(d:(CURRENT->G)?, s:CURRENT->G)
            require
                r3: d.is_directed
                r4: s = d.supremum
            check
                c2: d <= s                -- r4
                c3: d.image(f) <= f(s)    -- c2, fmono

                c4: require
                        r5: some(g:CURRENT->G)
                                d.image(f)<=g and g<f(s)
                    ensure
                        false    -- contra_fconti (see below)
                    end
                c5: all(g:CURRENT->G)
                         d.image(f)<=g => f(s)<=g
                                -- c4
            ensure
                d.image(f).supremum = f(s)    -- c3,c5
            end
    ensure
       f.is_continuous
    end


contra_fconti:
all(c:G, h:[G,CURRENT]->G,
    f:(CURRENT->G)->(CURRENT->G),
    d: (CURRENT->G)?, s,g:CURRENT->G,
)
    require
        r1: h.is_total
        r2: f = functional(c,h)
        r3: d.is_directed
        r4: s = d.supremum
        r5: d.image(f) <= g
        r6: g < f(s)
    check
        c1: some(n:CURRENT) n in (f(s).domain-g.domain)  -- r6
        c2: all(n:CURRENT)
            require
                r7: n in f(s).domain
                r8: n /in g.domain
            check
                c3: all(a) a in d.image(f) => 0 in a.domain  -- fdtrans
                c4: 0 in g.domain                            -- c3,r5

                c6: n=0 or n/=0
                c7: n=0 => n in g.domain and n /in g.domain  -- c4,r8
                c8: require
                        r9: n/=0
                    check
                        c9:  n.pred in s.domain   -- r7,r9,fdtrans
                        c10: some(a:CURRENT->G)
                                 a in d and n.pred in a.domain
                                                  -- c9,r4
                        c11: some(a:CURRENT->G)
                                 a in d.image(f) and n in a.domain
                                                  -- c10,fdtrans
                        c12: n in g.domain        -- c11,r5
                    ensure
                        false     -- c12,r8
                    end
            ensure
                false             -- c6,c7,c8
            end
    ensure
        false                     -- c1,c2
    end

Continuous functions and least fixpoints

We cite the central fixpoint law from the article “Closures and fixpoints”:
Whenever an endofunction f on a complete partial order is continuous and
there is an element a which is a prefixpoint of f and the set
a.closed(f) and its supremum are completely in the domain of f then
a.closed(f).supremum is the least fixpoint above a (Note that
a.closed(f) is a chain and is therefore directed so that the supremum
exists).

CPO: COMPLETE_PARTIAL_ORDER

least_fixpoint:
all(a,s:CPO, f:CPO->CPO)
    require
        f.is_continuous
        a in f.prefixpoints
        s = a.closed(f).supremum
        a.closed(f) + {s} <= f.domain
    ensure
        s.is_least(f.fixpoints * {x:a<=x})
    end

We can apply this theorem to the functions of type CURRENT->G and the
functional f=functional(c,h).

Since the functions form a complete partial order and the completely undefined
function 0 is the least function within this order we get that 0 is a
prefixpoint of the functional f and (0).closed(f).supremum is the least
fixpoint of the functional f.

Unique fixpoint

From the least_fixpoint theorem it follows that the supremum s with
s=(0).closed(f).supremum is the least fixpoint of a functional of the form
f=functional(c,h).

We claim that the supremum s is a unique fixpoint of the functional
f. We prove this claim by showing that s is a total function. If s is a
total function then there is no function above s i.e. there cannot be any
fixpoint above s (and there is no fixpoint below s because s is the
least fixpoint).

In order to demonstrate that s is a total function we look at the functions
in the closure (0).closed(f). For each natural number n there is an
element in the closure which has n in its domain. We proof this by induction
on n (see below). If this is the case then all natural numbers n must be
in the domain of the supremum s as well. Otherwise s were not an upper
bound of (0).closed(f).

all(n:CURRENT,
    c:G, h:[G,CURRENT]->G,
    f:(CURRENT->CURRENT)->CURRENT->CURRENT)
    require
        r1: f = functional(c,h)
    check
        c1: f(0) in (0).closed(f)
        c2: 0 in f(0).domain
        c3: all(n:CURRENT)
            require
                r2: some(g) g in (0).closed(f) and n in g.domain
            check
                c4: all(g:CURRENT->G)
                    require
                        r3: g in (0).closed(f)
                        r4: n in g.domain
                    check
                        c5: f(g) in (0).closed(f)        -- f is total
                        c6: f(g).domain
                            = {0}+g.domain.image(succ)   -- fdtrans
                        c7: n.succ in f(g).domain        -- r4,c6
                    ensure
                        some(g)
                            g in (0).closed(f)
                            and n.succ in g.domain -- c5,c7, witness f(g)
                    end
            ensure
                some(g) 
                    g in (0).closed(f)
                    and n.succ in g.domain    -- r2,c4
            end
    ensure
        some(g:CURRENT->G)
            g in (0).closed(f)
            and n in g.domain    -- c1,c2,c3, induction
    end
Advertisements
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: