“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 appleWhat 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 + 1Let’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 + 1Now 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 + 1That’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.
Sincere Flattery 