# Lambda Calculus: Recursion

“When preceded by its quotation yields falsehood” when preceded by its quotation yields falsehood.

Willard Van Orman Quine

Before we start, recursion is a tricky subject. I suggest you read this article before continuing. Also, you’re going to need at least version 1.3.1 of the lambda calculator to try out the examples. This version allows variable names to contain symbols like `+` and more importantly, fixes a nasty bug exposed by recursive application with functions as arguments.

### Interlude

Also, before we start: let’s discuss the liar’s paradox and the quotation at the beginning of this article. The liar’s paradox – in one form – says this:

This sentence is false

It’s a paradox because, if it is true then what it says must be true but what it says is that it is false, so it must be false, which contradicts the assumption that it is true. Similarly, if it is false, the fact that it says its false means it must be true, also a contradiction. In the liar’s paradox, the phrase “this sentence” is doing quite a lot of work. You kind of have to know that it is referring to itself rather than some other sentence. For example, I might write: “The Pope is a Hindu. This sentence is false”. In that case, we could still have a paradox, but “this sentence” might actually refer to the previous sentence, which I believe may be false.

Is there a way of constructing the liar’s paradox without the self referential “this sentence”. The answer is yes. Consider the sentence fragment “when preceded by its quotation yields falsehood“. What happens if we precede it by its quotation? We get

“When preceded by its quotation yields falsehood” when preceded by its quotation yields falsehood.

What we have here is a sentence that gives us some instructions on how to build a new sentence and then tells us something about the new sentence i.e. that it is false. If we follow the instructions, we take the fragment “when preceded by its quotation yields falsehood” and precede it by it’s quotation i.e. we put it in quote marks and put it on the front. That gives us

“When preceded by its quotation yields falsehood” when preceded by its quotation yields falsehood.

which the original sentence says is false. But lo! It is the original sentence. So the original sentence must be false, which means the thing it tells you how to construct must be true. Contradiction! And all without any explicit self reference.

### Recursion in the Lambda Calculus

In the last post, we tried to implement a `last` function for lists as follows:

`let naiveLast = λl.(isEmpty (tail l)) (head l) (naiveLast (tail l))`

This failed because the variable `naiveLast` in the right hand side of the `let` statement is a free variable and will not be replaced recursively with the right hand side of the statement. We can do recursion in the Lambda Calculus, but it requires a more indirect approach, which we are going to talk about in this post.

The function `last` that gets the last element of a list is a useful function, but it is also a little bit too complicated for our purposes, containing lots of stuff not directly related to recursion. Instead, we’ll talk about a function that counts the number of elements in a list. Th naive count function is defined as follows:

`let naiveCount = λl.(isEmpty l) 0 ((naiveCount (tail l)) + 1)`

The first point here is that we don’t know how to do addition in the Lambda Calculus yet. So what we are going to end up with is a list of instructions for a human to do the addition i.e.

`count nil`β `0`

`count (λf.f banana nil)`β `0 + 1`

`count (λf.f pear (λf.f banana nil))`β `0 + 1 + 1`

and so on.

The second point is that `naiveCount` has the same problem as `naiveLast`. It works correctly for the non recursive case, but stops prematurely for any other case because `naiveCount` is free in the right hand side of the `let` statement.

``````> naiveCount nil
: (λl.(λl.l (λh.λt.λx.λy.y)) l 0 (naiveCount ((λl.l (λx.λy.y)) l) + 1)) (λf.λx.λy.x)
>
: (λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: (λf.λx.λy.x) (λh.λt.λx.λy.y) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: (λx.λy.x) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: (λy.0) (naiveCount ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: 0
> naiveCount (λf.f banana nil)
: (λl.(λl.l (λh.λt.λx.λy.y)) l 0 (naiveCount ((λl.l (λx.λy.y)) l) + 1)) (λf.f banana (λf.λx.λy.x))
>
: (λl.l (λh.λt.λx.λy.y)) (λf.f banana (λf.λx.λy.x)) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1)
>
: (λf.f banana (λf.λx.λy.x)) (λh.λt.λx.λy.y) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1)
>
: (λh.λt.λx.λy.y) banana (λf.λx.λy.x) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1)
>
: (λt.λx.λy.y) (λf.λx.λy.x) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1)
>
: (λx.λy.y) 0 (naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1)
>
: (λy.y) (naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1)
>
: naiveCount ((λl.l (λx.λy.y)) (λf.f banana (λf.λx.λy.x))) + 1
>
: naiveCount ((λf.f banana (λf.λx.λy.x)) (λx.λy.y)) + 1
>
: naiveCount ((λx.λy.y) banana (λf.λx.λy.x)) + 1
>
: naiveCount ((λy.y) (λf.λx.λy.x)) + 1
>
: naiveCount (λf.λx.λy.x) + 1
>
: naiveCount (λf.λx.λy.x) + 1
``````

So how can we fix this? What if we try abstracting out the problematic function

`let count = (λf.λl.(isEmpty l) 0 ((f (tail l)) + 1)) F`

Without worrying too much about what `F` is, let’s try it out. It’s trivial to figure out that `count nil` is still `0`, but

`count (λf.f banana nil)`β `F nil + 1`

and in general

`count l`β `F (tail l) + 1`

Clearly we want `F` to somehow be the same as `count`. It can’t be `count` because that would involve an infinite regress. However, it could be something that β reduces to `count`. To make it a bit more clear, if we let `count'` be the abstraction of our original `naiveCount` i.e.

`let count' =` `λf.λl.(isEmpty l) 0 ((f (tail l)) + 1)`

Then `count = (count' F)` for some `F`. However the bound `f` in `count'` that will be replaced by `F` needs to reduce to `count` so that it can give us the count of elements in `(tail l)`, so, in some sense

`F = count' F`

Or, in a very specific sense `F`β `count' F`. `F` needs to be a lambda expression that β reduces to itself or “makes a copy” of itself. How can we make such an expression without invoking explicit recursion. Let’s first consider a function that returns two copies of its argument. We’ll call it `double`.

`let double = λx.x x`

``````> double apple
: (λx.x x) apple
>
: apple apple``````

What happens if we apply `double` to itself.

``````> double double
: (λx.x x) (λx.x x)
>
: (λx.x x) (λx.x x)
``````

The first line is simply the expansion of `double`, the second line is the result of the application of `double` to itself. As you can see, they are identical. `double double` is an application that makes a copy of itself.

What happens if we make the application `x x` in `double` the argument to a function. In particular, what if we make it the argument to the function `count'`.

`let countq = λx.count' (x x)`

``````> countq apple
: (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) apple
>
: (λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (apple apple)
``````

This could reduce further, but what we have got at this point is the same as `count' (apple apple)`. What about `countq countq`?

``````> countq countq
: (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x))
>
: (λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)))
>
: λl.(λl.l (λh.λt.λx.λy.y)) l 0 ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) ((λl.l (λx.λy.y)) l) + 1)
``````

That’s a bit of a mess, but, `countq` is

`λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)`

and you’ll see it’s embedded in the last expression twice (it’s actually easy to find if you look for the `(x x)`).

`λl.(λl.l (λh.λt.λx.λy.y)) l 0 ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) ((λl.l (λx.λy.y)) l) + 1)`

The bold bit and the underlined bit are both `countq`. If we replace them with `countq` (and remove some redundant parentheses we get:

`λl.(λl.l (λh.λt.λx.λy.y)) l 0 (countq countq ((λl.l (λx.λy.y)) l) + 1)`

This is what we want. Evaluating `countq countq` gives us an expression that returns 0 for an empty list or applies `countq countq` to the tail of a non empty list and returns the result `+ 1` (remember application is left associative: `countq countq foo `is the same as `(countq countq) foo`). This is what we want. Let’s try it on some lists.

``````> (countq countq) nil
: (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λf.λx.λy.x)
>
: (λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x))) (λf.λx.λy.x)
>
: (λl.(λl.l (λh.λt.λx.λy.y)) l 0 ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) l 0 (f ((λl.l (λx.λy.y)) l) + 1)) (x x)) ((λl.l (λx.λy.y)) l) + 1)) (λf.λx.λy.x)
>
: (λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: (λf.λx.λy.x) (λh.λt.λx.λy.y) 0 ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: (λx.λy.x) 0 ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: (λy.0) ((λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) (λx.(λf.λl.(λl.l (λh.λt.λx.λy.y)) (λf.λx.λy.x) 0 (f ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)) (x x)) ((λl.l (λx.λy.y)) (λf.λx.λy.x)) + 1)
>
: 0
``````

That’s encouraging, the `nil` case works. Let us try it for a list containing one element. What about non empty lists?

``````let l1 = λf.f banana nil
let l2 = λf.f pear l1
let l3 = λf.f apple l2

> (countq countq) l1
: (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λf.f banana (λf.true))
>
: (λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine))) (λf.f banana (λf.true))``````

… Lots of pressing of the return key …

``````
>
: (λf.true) (λh.λt.false) 0 ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) ((tail) ((tail) (λf.f banana (λf.true)))) + 1) + 1
>
: (true) 0 ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) ((tail) ((tail) (λf.f banana (λf.true)))) + 1) + 1
>
: (λy.0) ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) ((tail) ((tail) (λf.f banana (λf.true)))) + 1) + 1
>
: 0 + 1``````

Let’s go for broke – count the elements in a three element list.

``````> (countq countq) l3
: (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λf.f apple (λf.f pear (λf.f banana (λf.true))))
>
: (λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine))) (λf.f apple (λf.f pear (λf.f banana (λf.true))))
>
: (λl.(λl.l (λh.λt.false)) l 0 ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) ((tail) l) + 1)) (λf.f apple (λf.f pear (λf.f banana (λf.true))))
> ``````

… even more pressing of the return key …

``````>
: (true) 0 ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) ((tail) ((tail) ((tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true)))))))) + 1) + 1 + 1 + 1
>
: (λy.0) ((λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) (λquine.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (quine quine)) ((tail) ((tail) ((tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true)))))))) + 1) + 1 + 1 + 1
>
: 0 + 1 + 1 + 1``````

Now we know how to calculate the number of elements in a list (or we would if we knew how to do addition). What about other recursive functions? What about finding the last element of a non empty list? If a list has one element, its last element is its head. If it has more than one element, its last element is the same as the last element of its tail. Our naive implementation of `last` is

`let last = λlist.(isEmpty (tail list)) (head list) (last (tail list))`

This works for `l1`, returning `banana` and for longer lists, it reduces to the point where we are trying to get `last (tail list)` and gets stuck there because `last` isn’t bound inside its own definition. For example `last l2`β `last (λf.f banana (λf.true))`.

As before, we produce a new function that abstracts out the recursive function call:

`let last' = λf.λlist.(isEmpty (tail list)) (head list) (f (tail list))`

Then we do the “q” function:

`let lastq = λq.last' (q q)`

And run the application:

``````> (lastq lastq) l2
: (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λf.f pear (λf.f banana (λf.true)))
>
: (λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) ((λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q))) (λf.f pear (λf.f banana (λf.true)))

``````

… many, many presses of return …

`````` (true) ((head) ((tail) (λf.f pear (λf.f banana (λf.true))))) ((λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) ((tail) ((tail) (λf.f pear (λf.f banana (λf.true))))))
>
: (λy.(head) ((tail) (λf.f pear (λf.f banana (λf.true))))) ((λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) ((tail) ((tail) (λf.f pear (λf.f banana (λf.true))))))
>
: (head) ((tail) (λf.f pear (λf.f banana (λf.true))))
>
: (tail) (λf.f pear (λf.f banana (λf.true))) (λx.λy.x)
>
: (λf.f pear (λf.f banana (λf.true))) (λx.λy.y) (λx.λy.x)
>
: (λx.λy.y) pear (λf.f banana (λf.true)) (λx.λy.x)
>
: (λy.y) (λf.f banana (λf.true)) (λx.λy.x)
>
: (λf.f banana (λf.true)) (λx.λy.x)
>
: (λx.λy.x) banana (λf.true)
>
: (λy.banana) (λf.true)
>
: banana
``````

And, just to be sure, let’s do `l3`

``````> (lastq lastq) l3
: (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λf.f apple (λf.f pear (λf.f banana (λf.true))))
>
: (λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) ((λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q))) (λf.f apple (λf.f pear (λf.f banana (λf.true))))``````

… many happy returns …

``````>
: (λy.(head) ((tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true))))))) ((λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) (λq.(λf.λlist.(λl.l (λh.λt.false)) ((tail) list) ((head) list) (f ((tail) list))) (q q)) ((tail) ((tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true))))))))
>
: (head) ((tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true))))))
>
: (tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true))))) (λx.λy.x)
>
: (tail) (λf.f apple (λf.f pear (λf.f banana (λf.true)))) (λx.λy.y) (λx.λy.x)
>
: (λf.f apple (λf.f pear (λf.f banana (λf.true)))) (λx.λy.y) (λx.λy.y) (λx.λy.x)
>
: (λx.λy.y) apple (λf.f pear (λf.f banana (λf.true))) (λx.λy.y) (λx.λy.x)
>
: (λy.y) (λf.f pear (λf.f banana (λf.true))) (λx.λy.y) (λx.λy.x)
>
: (λf.f pear (λf.f banana (λf.true))) (λx.λy.y) (λx.λy.x)
>
: (λx.λy.y) pear (λf.f banana (λf.true)) (λx.λy.x)
>
: (λy.y) (λf.f banana (λf.true)) (λx.λy.x)
>
: (λf.f banana (λf.true)) (λx.λy.x)
>
: (λx.λy.x) banana (λf.true)
>
: (λy.banana) (λf.true)
>
: banana
``````

An unexpected discovery from running this function is that it doesn’t work in the way I expected. Were the naive version to work, it would discard each element of the list, one after the other, head first until it got to a one element list and then it would reduce to the head of that list. `(lastq lastq)` doesn’t do that: it composes a sequence of applications of `tail` wrapped in a single application of `head` and applies that composition right at the end.

One last point to note is that the creation of the “q” function is the same in every case. For example, we have:`let lastq = λq.last' (q q)`

• `let countq = λx.count' (x x)`
• `let lastq = λq.last' (q q)`

The doubling up is very similar in each case too.

• `(countq countq)` is `(λx.count' (x x)) (λx.count' (x x)`)
• `(lastq lastq)` is `(λq.last' (q q)) (λq.last' (q q))`

`count'` and `last'` fulfil a similar role in each expression, so we can create a new lambda expression that abstracts out the function from the doubled expression i.e.

`λf.(λy.f(y y)) (λy.f(y y))`

This is known as the Y combinator and it can be used to build a recursive function from any abstraction where you want a recursive application. For example:

``````> let Y = λf.(λy.f (y y)) (λy.f (y y))
: defined Y as λf.(λy.f (y y)) (λy.f (y y))
> Y count' l3
: (Y) (λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (λf.f apple (λf.f pear (λf.f banana (λf.true))))``````

… snip …

``````: (λy.0) ((λy.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (y y)) (λy.(λf.λl.(λl.l (λh.λt.false)) l 0 (f ((tail) l) + 1)) (y y)) ((tail) ((tail) ((tail) ((tail) (λf.f apple (λf.f pear (λf.f banana (λf.true)))))))) + 1) + 1 + 1 + 1
>
: 0 + 1 + 1 + 1``````

That’s recursion done. It was a bit of a trial to be honest, partly because I didn’t understand the source article on about the first ten readings and my apologies if this post is incomprehensible. The other reason is that it has taken several hours of work spread over several weeks to track down a fairly subtle bug in the Lambda Calculator. Anyway, next time, we’ll look at numbers.

This site uses Akismet to reduce spam. Learn how your comment data is processed.