Recursion in Lambda Calculus: The Y Combinator

In the last post I talked about how powerful lambda calculus is.  In this post I further proves the point by encoding recursion in it.  This enables you to do recursion in any languages!

If you haven’t read my last post already, please do so!  It’d be easier for you to follow this post, especially if you don’t know any lambda calculus.

The Simplest Recursion

In this video, Professor Hutton shows us the simplest recursion he can think of:

loop = loop

The function loop does only one thing: calling itself.  When you evaluate loop, you go to loop‘s definition, which is loop!  We can encode a function that behaves like loop in lambda calculus:

loop = (λx.x x)(λx.x x)

Recall that in lambda calculus, what we do with two items side by side is to apply the first item as a function to the second item as an input.  In loop, one applies the function (λx.x x) to the input (λx.x x):

(λx.x x)(λx.x x) = (λx.x x)(λx.x x)      (replace each x with the input)
                 = (λx.x x)(λx.x x)      (infinite replacements can be made)

You can see that encoding loop as above gives us a function that behaves like loop.  We got this property from the self-application of the function (λx.x x).  (λx.x x) is applied to an input like itself!

General Recursion

Self-application takes us to general recursion.  A general recursion function (named rec) takes itself as the input.  In mathematics, it looks like this:

rec f = f (rec f)
      = f (f (rec f))      (replace rec f with f (rec f))
      = f (f (f (...))...)      (infinite replacements can be made)

The general recursion function can easily become any recursive function because f can be whatever you like!

The Y-combinator

Like loop, we can encode rec in lambda calculus too!  But we call rec ‘Y’ in lambda calculus this time, because this encoding is the famous Y-combinator that lets you have recursion in any languages:

Y = λf.(λx.f (x x))(λx.f (x x))

Let’s verify that it behaves like rec by giving it an input g:

Y g = λf.(λx.f (x x)) (λx.f (x x)) g      (replace Y with its definition)
    = (λx.g (x x)) (λx.g (x x))      (replace f with input g)
    = g ((λx.g (x x)) (λx.g (x x)))      (replace x with input (λx.g (x x)))
    = g (g ((λx.g (x x)) (λx.g (x x))))      (infinite replacements can be made)

From lines 2 and 3 above, we can see that

Y g = (λx.g (x x)) (λx.g (x x)) = g ((λx.g (x x)) (λx.g (x x)))

So, we have Y g = g (Y g)!  Just like rec!

Cool right?  By now you have grasped the concepts of the Y combinator.  If you want to know more terminology and formal illustrations, this medium article and the lambda calculus wikipedia page may be a good start.  I’ll also go through some exercises in my upcoming post.