Untied Fixed Points

A hands-ons introduction to fixed point semantics

Rasmus Lerchedahl Petersen - @yoff

"When we define a recursive function, we are asking the compiler to compute a fixed point"

Fixed points

Q:
What is a fixed point?

A:
A point that is not moved
(by some function)

Formally:
\(x\) is a fixed point for \(f\) iff \[f(x) = x\]

Example

Recursive functions

Q:
What is a recursive function?

A:
A function that calls itself

Actually:
The solution to a functional equation in which the function to solve for appears on both sides

Usually of the form \[f(x) = e[f,x]\]

Example

\(f(x) = f(x-2) + f(x-1)\)

More complete

\[f(x) = \begin{cases} \ 0 & ,\ x = 0 \\ \ 1 & ,\ x = 1 \\ \ f(x-2) + f(x-1) & ,\ x > 1 \end{cases}\]

Solutions are fixed points

The right hand side can be viewed as a functional \[e: (\mathbb{N} \rightarrow \mathbb{N}) \rightarrow (\mathbb{N} \rightarrow \mathbb{N})\]
\[e(f)\ =\quad x \mapsto\ f(x-2) + f(x-1)\]

Fixed point

\(f\) is a fixed point for \(e\) iff \[e(f) = f\]
That is \[f = e(f) = f(x-2) + f(x-1)\]

The fixed point combinator

\(x\) is a fixed point for \(f\) iff \[f(x) = x\]
So a fixed point combinator must satisfy \[f(\ fix(f)\ ) = fix(f)\]
We can use the left hand side as a definition

1: 

let rec fix f x = f (fix f) x

Coding without recursion

So, when we write

1: 
2: 
3: 

let rec fib x =
  if x < 2 then x
  else fib (x-2) + fib (x-1)

we are asking the compiler to compute the fixed point of

\[e(f) = x \mapsto\ \begin{cases} \ 0 & ,\ x = 0 \\ \ 1 & ,\ x = 1 \\ \ f(x-2) + f(x-1) & ,\ x > 1 \end{cases}\]

\[e(f) = x \mapsto\ \begin{cases} \ 0 & ,\ x = 0 \\ \ 1 & ,\ x = 1 \\ \ f(x-2) + f(x-1) & ,\ x > 1 \end{cases}\]

We can write this function explicitly

1: 
2: 
3: 

let fibU fibR x =
  if x < 2 then x
  else fibR (x-2) + fibR (x-1)

and then define fib as the fixed point

1: 

let fib = fix fibU

Does this work?

With normal recursion

\[\begin{aligned} fib\ 3 & \mapsto fib\ 2 + fib\ 1 \\ & \mapsto (fib\ 1 + fib\ 0) + 1 \\ & \mapsto (1 + 0) + 1 \\ & \mapsto 2 \end{aligned}\]

With explicit fixed point

\[\begin{aligned} fib\ 3 & \mapsto \underline{fix\,\, fibU\ 3} \\ & \mapsto fibU\ (fix\,\, fibU)\ 3 \\ & \mapsto (\underline{fix\,\, fibU\ 2}) + (\underline{fix\,\, fibU\ 1}) \\ & \mapsto (fibU\ (fix\,\, fibU)\ 2) + (fibU\ (fix\,\, fibU)\ 1) \\ & \mapsto ((\underline{fix\,\, fibU\ 1}) + (\underline{fix\,\, fibU\ 0})) + 1 \\ & \mapsto ((fibU\ (fix\,\, fibU)\ 1) + (fibU\ (fix\,\, fibU)\ 0)) + 1 \\ & \mapsto (1 + 0) + 1 \\ & \mapsto 2 \end{aligned}\]