index.md

• title : Untied fixed points
• description : A hands-ons introduction to fixed point semantics
• author : Rasmus Lerchedahl Petersen
• theme : night
• transition : default

---

Untied Fixed Points

A hands-ons introduction to fixed point semantics

Rasmus Lerchedahl Petersen - [@yoff](https://yoff.github.io)

---

"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

y = f(x) y = x x = f(x)

---

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

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

---

Coding without recursion

So, when we write

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

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

and then define fib as the fixed point

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

---

Try it now

• Hands-on
  • F# script
  • Solutions
• Online ways to try
  • http://fable.io/repl
  • http://www.tryfsharp.org/Create

---

Links

• Blog post
  • https://eiriktsarpalis.wordpress.com/2013/02/13/parametric-open-recursion-pt-1/
  • https://eiriktsarpalis.wordpress.com/2013/02/14/parametric-open-recursion-pt-2/
• Code
  • https://github.com/rgrig/barista
  • (see https://github.com/rgrig/barista/blob/master/src/common/utils.ml#L208)
• Video
  • https://www.youtube.com/watch?v=4DdUEHOhAB4
• Presentation
  • https://yoff.github.io/untied