Why does the fixed point theorem justify the existence of the factorial function?

Question

I was learning about fixed point theorem in the context of programming language semantics. In the notes they have the following excerpt:

Many recursive definitions in mathematics and computer science are given informally, but they are more subtle than they appear to be. The fixed-point theorem can be used to formally argue that such definitions are indeed correct. Consider, for example, the following common definition of the factorial: $$ f(n) = \left\{ \begin{array}{ll} 1 & \mbox{if } n = 0 \\ n * f(n-1) & \mbox{if } n > 0 \end{array} \right. $$ How can we know whether such a mathematical object, i.e., a function f satisfying the above property, actually exists and is unique, as tacitly assumed?

then it moves one to claim that somehow the fixed point theorem magically justifies this definition to be valid. Thats the part I don't understand. Why is that true?

I think they proceed to try to justify the fixed point theorem justifies it but I don't think I understand what in particular makes the fixed point theorem make this work. Any ideas?

---

Excerpt (from here) for more context (page 89):

---

$f(0)=0$ unambiguously exists because we said the symbol $f(0)$ means $1$ when $n$ is zero. $f(1)=f(0)*1=1*1$ because $f(0)$ exists, continue by induction... so $f(n)$ exists because its defined everywhere in its domain. I don't see what the fixed point theorem contributes to the discussion. I wish to understand of course.

Answer 1

As the function $f$ is defined in terms of itself, you have a priori no guarantee that it is defined at all or uniquely defined.

Now the function $\mathcal F$ is such that it extends the known values of $f(n)$ (from a given subset of naturals) by applying the definition.

Then the fixed-point theorem guarantees that $\mathcal F$ has a fixed-point, which corresponds to $f$ defined over the whole of $\mathbb N$. Uniqueness of the fixed-point guarantees that $f$ is uniquely defined.

Answer 2

Why is the fixed point theorem actually important here?

Well, let's think about why we believe that there is a function $f$ satisfying [recursive description of $!$]. It comes down to the following two (quite correct) beliefs:

• We can use the recursive description of $!$ to "deduce" what the value of $!$ should be on each specific natural number.

• We cannot use the recursive description of $!$ to deduce two contradictory things about $!$ (e.g. we can't use it to prove that $2!$ should be $7$).

With both claims in hand, we can then define $!$ by saying "$n!$ is the unique $m$ such that "$n!=m$" is implied by the recursive description." (In fact, only the second claim is needed to justify the existence of $!$ as a partial function.) But these claims need to be justified, and while in the case of the factorial function they are pretty obvious, $(i)$ the second claim is actually not as trivial to prove as one might hope and $(ii)$ certainly in general we want a theorem that lets us handle problems like these.

The fixed point theorem is basically a machine for getting around this issue: given a recursive description of a function, the fixed point theorem can (often) construct functions which actually satisfy that description in a precise, controlled way.

---

How we use it here (part $1$)

We can pass from the recursive description of the factorial function to a (perfectly good) definition of an operator on (partial) functions. The fixed point theorem shows that there is a fixed point, $f$, for this operator (once we've shown that this operator is in fact continuous); we then argue by induction that in fact this $f$ actually is the factorial function.

In detail:

From our self-referential "definition" of the factorial function, we can extract a perfectly good non-self-referential definition of an operator on partial functions $\mathcal{F}$: given a partial function $g:\mathbb{N}\rightarrow\mathbb{N}$, $\mathcal{F}(g)$ is the partial function given by

$$ \mathcal{F}(g):n\mapsto \left\{ \begin{array}{ll} 1 & \mbox{if } n = 0 \\ n * g(n-1) & \mbox{if } n > 0\mbox{ and } g(n-1)\downarrow\\ \uparrow & \mbox{if $n>0$ and $g(n-1)\uparrow$} \end{array} \right. $$

where "$\uparrow$" means "is undefined" and "$\downarrow$" means "is defined." (Note that I've written "$\mathcal{F}(g):n\mapsto...$" instead of "$\mathcal{F}(g)(n)=...$" for clarity, but there's no actual difference.) Intuitively, think of $\mathcal{F}$ as taking in a "partial computation" of $!$ - say, the first seventeen bits of the factorial function - and "going a bit further." The function we want is the "limit" of this process. This is exactly what the fixed point theorem says exists.

---

A quick example

Suppose $g$ is the partial function which sends $3$ to $7$, sends $10$ to $2$, sends $11$ to $11$, and is otherwise undefined. Then what partial function should $\mathcal{F}(g)$ be?

In no particular order:

• $\mathcal{F}(g)$ is certainly defined at $0$: by definition of $\mathcal{F}$, we'll always have $\mathcal{F}(g):0\mapsto 1$ regardless of what $g$ is.

• On the other hand, since $g(0)$ isn't defined, we know that $\mathcal{F}(g)(1)$ isn't defined.

• What about $11$? Well, $11>0$ and $g(11-1)$ is defined, so the second clause of the definition of $\mathcal{F}$ tells us that $$\mathcal{F}(g)(11)=11\cdot g(11-1)=11\cdot g(10)=11\cdot 2=22.$$ So $\mathcal{F}(g)(11)\downarrow =2$.

Exercise: Convince yourself that in fact the domain of $\mathcal{F}(g)$ is precisely $\{0,4,11,12\}$ and calculate the values of $\mathcal{F}(g)(4)$ and $\mathcal{F}(g)(12)$.

---

How we use it here (part $2$)

Having defined our operator $\mathcal{F}$, we now need to use it somehow.

Claim $1$: $\mathcal{F}$ is continuous.

The text you've quoted doesn't actually prove this, but it's not hard to check. If this is an issue, though, let me know and I'll add details.

With the continuity of $\mathcal{F}$ in hand, we can now invoke the fixed point theorem to get a function $f$ such that $$\mathcal{F}(f)=f.$$ In fact, the fixed point theorem gives us a least fixed point of $\mathcal{F}$, but we don't even need that in the current situation. We now show:

Claim $2$: This $f$ is in fact the factorial function. That is, we have $(i)$ $f$ is defined on all of $\mathbb{N}$, $(ii)$ $f(0)=1$, and $(iii)$ $f(n+1)=(n+1)f(n)$.

Parts $(i)$ and $(iii)$ are proved by induction: get a contradiction from looking at the putative first $n$ on which $f$ is undefined, and the putative first $n$ on which $f(n+1)\not=(n+1)f(n)$, respectively. Part $(ii)$ doesn't require any induction, and is just a quick observation.

Specifically, here's how we prove $(i)$ and $(ii)$ (I'll leave $(iii)$ as an exercise). The key point is that the equality $$\mathcal{F}(f)=f$$ (this is what it means for $f$ to be a fixed point of $\mathcal{F}$) lets us prove things about $f$ by proving them about $\mathcal{F}(f)$.

• To prove $(ii)$, we know by definition of $\mathcal{F}$ that $\mathcal{F}(g)(0)\downarrow=1$ for any partial function $g$. In particular, we have $$\mathcal{F}(f)(0)\downarrow=1.$$ But since $f$ is a fixed point for $\mathcal{F}$ we can turn this into $$f(0)\downarrow=1.$$

• To prove $(i)$, we've just shown that $f(0)$ is defined. Now suppose $f(n)$ is defined. By definition of $\mathcal{F}$, we know $\mathcal{F}(f)(n+1)$ is defined (namely, it's $(n+1)f(n)$). But again since $f$ is a fixed point of $\mathcal{F}$, this tells us that $f(n+1)$ is defined. So by induction, $f$ is total.

Answer 3

$$ \DeclareMathOperator{\fst}{fst} \DeclareMathOperator{\snd}{snd} \DeclareMathOperator{\succ}{succ} \DeclareMathOperator{\z}{zero} \DeclareMathOperator{\fact}{fact} $$ There is also another way to formally define such recursive functions without fixpoint operators. I think it might be interesting for you since it is probably also covered in a course for semantics of progrmming languages!
We will define the factorial function as a function acting on the inductive data type of natural numbers.

Define the natural numbers as the inductive data type $Nat$ using the following signature $\Sigma$:

data Nat = zero | succ: Nat -> Nat

For example, we represent 0 as $\z$, 1 as $\succ 0$ and 3 as $\succ (\succ (\succ \z))$. $\z$ and $\succ$ are called constructors and effectively describe all valid terms induced by this definition.

You can now define $every$ primitive recursive function on Nat by specifying an interpretation of $\z$ and $\succ$. I will explain it below in more mathematical terms, but for now think of a computer program:

// JavaScript syntax
const z = function() {
    // Zero arguments because zero is a constructor taking 0 arguments
    // in our signature \Sigma
    return ???;
};

const succ = function(x) {
    // One argument because succ is a constructor taking exactly 1 argument
    // in our signature \Sigma
    return ???;
};

// The above defines a primitive recursive function on Nat
// We now evaluate it on 3
const result = succ(succ(succ(z())));

For example, if you insert return 0; and return x + 1, respectively, then this will define the "identity" function from our inductive data type into 64-bit numbers baked into JavaScript. See it live at http://jsfiddle.net/v9L0x5ef.
Using return 0; and return x + 2 will define a function doubling its argument.

Exercise: Define a function multiplying the argument by 3. Do the same with 4 (in your mind). How does a function look like multiplying the argument by $y \in \mathbb{N}$?

const y = 3; const z = function() { return 0; } const succ = function(x) { return x + y; }
Live at http://jsfiddle.net/v9L0x5ef/1/.

Now consider the following functions defining the desired factorial function (live version):

const z = function() {
    // Mathematically, this could be expressed as a simple pair
    return {
        // We remember at which number we currently are: we are now at 0.
        prevNumber: 0,

        // Our current factorial result
        currentResult: 1
    };
};

const succ = function(x) {
    // Remember: x is the evaluation of inner succ()s and z() calls!
    return {
        // Remember to keep track!
        prevNumber: x.prevNumber + 1,

        // The factorial definition would usually be f(n) = n * f(n-1)
        // and this is exactly what we are doing here
        currentResult: (x.prevNumber + 1) * x.currentResult
    }
};

// This would give
// {
//   prevNumber: 3
//   currentResult: 6
// }
const result = succ(succ(succ(z())));
const finalResult = result.currentResult;

I lied "a little bit" above. You can only define every primitive recursive function if you allow the result being served inside a pair. Here, we have the desired result under the currentResult key.

We have now uniquely (obviously) (well-)defined the factorial function by specifying a function ("interpretation") for every constructor. We could now prove the claimed property (which was your definition):

Defining $f: \mathbb{N} \to \mathbb{N}$ by $f := \snd \circ h$, we have $f(n) = n f(n-1)$ for all $n \ge 1$ and $f(0) = 0$.

I leave this to the reader.

Mathematically, we have defined a function $h$ from all valid Nat terms to pairs:

$$h(\z) := (\z, 1)\\ h(\succ n) := (\mathrm{prev} \mapsto ((\fst \mathrm{prev}) + 1, (\snd \mathrm{prev}) \cdot ((\fst \mathrm{prev}) + 1))) (h(n))\\ \\ \fact n := \snd h(n)\\ \mathrm{Alternatively: } \fact := \snd \circ h $$ Do note that in the definition for $h(\succ n)$ we do not use $n$ at all except as $h(n)$. This ensures that the resulting morphism is actually a homomorphism in the theory behind it.

All in all, you can define many recursive functions you see in the wild this way.

Exercise: What does the inductive data type for trees with values of type $T$ at every inner node look like? Which constructors does it have?

A generic tree data type with values of type T would look like data Tree T = leaf | node: T -> Tree -> Tree -> Tree node receives a value, the left and the right subtree.

Exercise: Specify interpretations of the tree constructors to sum all values in a tree with values of type $\mathbb{N}$.

$leaf \mapsto = 0, node \mapsto (x, l, r) \mapsto x + l + r$
node adds the current value to the accumulated value of both subtrees.

---

The theory

One considers algebras $\mathfrak{M} = (\Sigma, M, \mathfrak{M}[[\z]]: M, \mathfrak{M}[[succ]]: M \to M)$. They are triples consisting of the signature $\Sigma$, a universe $M$ and interpretations of all the constructors.
Naturally one can define the so-called term algebra $[[\ldots]$$ (e.g. called $[[Nat]]$ in case of Nat) induced by every inductive data type definition:

• Choose $\Sigma$ as from the inductive data type definition
• Choose $M$ as the set of all constructible valid terms, here $M := \{\z, \succ \z, \succ (\succ \z), \succ (\succ (\succ \z)), \ldots\}$
• Interpret every term as itself, e.g. $\mathfrak{M}[[\z]] = \z$, $\mathfrak{M}[[succ]](n) = \succ n$.

The term algebra is in fact the most general one — up to isomorphism — and it turns out that we can define every primitive recursive functions on inductive data types by specifying a homomorphism from it into a target algebra over the same signature. If the target algebra is $\mathfrak{N} = (\Sigma, N, \mathfrak{N}[[\z]]: N, \mathfrak{N}[[succ]]: N \to N)$, then a homormophism $h: M \rightarrow N$ is a function which commutes with the interpretation of the target algebra:

$$h(\mathfrak{M}[[\z]]) = \mathfrak{N}[[\z]]\\ h(\mathfrak{M}[[\succ]](n)) = \mathfrak{N}[[\succ]](h(n)) $$

Concretely with $\mathfrak{M} = [[Nat]]$: $h(\succ (\succ \z)) = \mathfrak{N}[[\succ]](\mathfrak{N}[[\succ]] (h(\z)))$

Above we exactly specified the interpretations $\mathfrak{N}[[\z]]$ and $\mathfrak{N}[[\succ]]$. We also explicitly stated such a homomorphism $h$. Have a look at $h(\mathfrak{M}[[\succ]](n)) = \mathfrak{N}[[\succ]](h(n))$. You see that the result $h$ computes is our interpretation (independent of $n$!) applied to $h(n)$. Here you see why we needed to restrict ourselves to only use $h(n)$ and not $n$ alone.
Actually, that restriction is unneeded since you can rewrite the interpretations to drag the terms along they are being applied to. Let's say you have an algebra with interpretations $\mathfrak{N}$ (which unfortunately depend on $n$!), then you can construct an algebra $\mathfrak{P}$ with these interpretations to formally solve the problem:

$$ \mathfrak{P}[[\z]] = (\mathfrak{N}[[\z]], \z)\\ \mathfrak{P}[[\succ]](n) = (\mathfrak{N}[[\succ]](\fst n, \succ (\snd n), \succ (\snd n)) $$

The universe of $\mathfrak{P}$ is (possibly a subset) of $N \times M$, where $N$ is the universe of $\mathfrak{N}$ and $M$ the universe of all constructible terms. You can see that $\mathfrak{N}[[\succ]]$ can now indeed be passed the term it is applied on.