# Unfolding Fix

In pure lambda calculus (untyped or typed) the `fix` combinator is used to encode recursion. `fix` represents the least fixed point of a function `f` i.e the least defined `x` for which `f x = x`. An important concept is that a function need not have a least fixed point. But for those functions which do, the least fixed point is the base case for recursion. An intuition about the least fixed point is :

``````f (f (f ( f x))) = x
``````

This is a convenient way to represent recursion in a language which doesn’t support naming functions. The base case of the recursion is determined by the actual least point of the function. Here we will take the most popular example of encoding fix which is a factorial function :

``````factorial n = if n <= 1
then 1
else n * factorial (n - 1)
``````

and demonstrate the stack trace of how the fix function unfolds this recursion. First lets define `fix` in Haskell.

``````fix :: (a -> a) -> a
fix f = f (fix f)
``````

Owing to the laziness of Haskell we can define such an expression which doesn’t fully evaluate the `fix f` call in the right hand side but rather creates a thunk.

Now writing the `factorial` function using `fix` :

``````factorial = fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1))
``````

or

``````factorial x =
(fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1))) x
``````

Lets try calculating `factorial 3`

Unfolding:

``````(f (fix f)) 3

-- substituting f

((\fac n -> if n <= 1
then 1
else n * fac (n-1))
(fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1))))
3

-- beta reduction

(\n -> if n <= 1
then 1
else n * ((fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1))) (n - 1))
) 3

-- beta reduction

if 3 <= 1
then 1
else 3 * ((fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1))) 2)

-- evaluating if

3 * ((fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1))) 2)

-- substituting f

3 *
(\fac n -> if n <= 1
then 1
else n * fac (n-1))
(fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)))
2)

-- beta reduction

3 *
((\n -> if n <= 1
then 1
else n * (fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)) (n - 1))) 2)

-- beta reduction

3 *
if 2 <= 1
then 1
else 2 * (fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)) 1)

-- evaluating if

3 * 2 * (fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)) 1)

-- substituting f

3 * 2 *
(((\fac n ->
if n <= 1
then 1
else n * fac (n-1))
(fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)))) 1)

-- beta reduction

3 * 2 *
((\n -> if n <= 1
then 1
else n * ((fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)) ) (n - 1))) 1)

-- beta reduction

3 * 2 *
if 1 <= 1
then 1 -- hit the base case
else n * ((fix (\fac n ->
if n <= 1
then 1
else n * fac (n-1)) ) (n - 1)))

-- evaluating if

3 * 2 * 1 = 6
``````
Written on December 20, 2019