The Eiffel Compiler / Interpreter (tecomp)

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

- Does the functional
`f`

have a fixpoint (i.e. existence)? - 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)`

.

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.

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`

.

In the module `abstract_natural`

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

Zero is a natural number

All natural numbers have successor

Zero is not the successor of a natural number

Two natural numbers which have the same successor are identical

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.

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

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

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

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

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

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

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

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

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

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

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

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

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`

.

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