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