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):

enter image description here

$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.

  • $\begingroup$ I would check out the well-ordering principle. This is very much related to this $\endgroup$ Oct 3, 2018 at 22:13
  • $\begingroup$ What page is it on? $\endgroup$
    – Ovi
    Oct 3, 2018 at 22:19
  • $\begingroup$ @Ovi page 89 of the notes fsl.cs.illinois.edu/images/c/ca/… $\endgroup$ Oct 3, 2018 at 22:20
  • 3
    $\begingroup$ 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. $\endgroup$ Oct 3, 2018 at 23:06
  • 1
    $\begingroup$ @NoahSchweber In this case, can't we give the following proof of the existence and uniqueness of $f$? Base case: $f(0)$ is uniquely defined. Now suppose for some $k \in \mathbb{N} \cup \{ 0 \}$ $f(k)$ is defined and unique. Then $f(k+1) = k f(k)$, so $f(k+1)$ is defined and unique? $\endgroup$
    – Ovi
    Oct 4, 2018 at 0:13

3 Answers 3


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.

  • $\begingroup$ is taking in a....seems you missed out a part of your sentence. $\endgroup$ Oct 3, 2018 at 23:07
  • $\begingroup$ my previous comment is important because I am failing to understand how continuity holds. $\mathcal F$ maps partial functions $g(n)$ to either the partial constant function 1, or $n*g(n-1)$ or undefined. So $\mathcal F$ itself is a partial function because it maps partial functions to undefined? I'm really confused... $\endgroup$ Oct 3, 2018 at 23:12
  • $\begingroup$ @Pinocchio Good catch, I've fixed that bit. Re: your second comment: no, $\mathcal{F}$ is total as an operator on partial functions: it takes in partial functions and outputs partial functions. Saying that $\mathcal{F}$ is total is to say that $\mathcal{F}(g)$ is always a well-defined partial function whenever $g$ is a partial function, not that $\mathcal{F}(g)$ is always a total function whenever $g$ is a partial function. (Unfortunately the phrase "$\mathcal{F}(g)$ is always defined" may indeed suggest the latter!) $\endgroup$ Oct 3, 2018 at 23:13
  • $\begingroup$ sorry to be a complainer but it makes it harder to read, usually $\bot$ i.e. bottom means undefined. So seeing arrows going up instead of down for undefined is confusing me. I'm trying to parse your answer. I still don't get it :( $\endgroup$ Oct 3, 2018 at 23:19
  • 1
    $\begingroup$ What is the topology on the space of partial functions, which makes $\mathcal F$ continuous? $\endgroup$
    – Jack M
    Oct 4, 2018 at 9:21

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.

  • 1
    $\begingroup$ I'm failing to appreciate what the role of $\mathcal F$ is. $\mathcal F(g(n))$ is equal to the definition of factorial function plus a condition of undefined when the funciton is undefined. Conceptually $\mathcal F$ is just the same as $g(n)$. So I don't see what role its suppose to be playing. $\endgroup$ Oct 3, 2018 at 22:57
  • 1
    $\begingroup$ like we could have done induction on the original definition of $f(n)$ that didn't refer to any fixed points to show it was defined everywhere...what did $\mathcal F $ contribute? $\endgroup$ Oct 3, 2018 at 22:59
  • $\begingroup$ @Pinocchio First of all, the notation $\mathcal{F}(g(n))$ is wrong: $\mathcal{F}$ turns a partial function into a partial function, but you give it $g(n)$ as an argument which is a natural number (or undefined). The right thing to write is $\mathcal{F}(g)(n)$ by which we mean $(\mathcal{F}(g))(n)$. So $\mathcal{F}$ is applied to $g$, giving you a new partial function $\mathcal{F}(g)$ and this function is then applied to $n$. Understanding this difference might already help. $\endgroup$ Oct 4, 2018 at 11:18
  • $\begingroup$ @Pinocchio Second, $\mathcal{F}$ is not the same as $g(n)$! If you have a fixed point $h$ of $\mathcal{F}$ then $\mathcal{F}(h) = h$. But you can apply $\mathcal{F}$ to non fixed points as well and in that case $\mathcal{F}(g)$ is not the same as $g$. See the “quick example” in the other answer to see that happening. $\endgroup$ Oct 4, 2018 at 11:21

$$ \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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .