As you probably already now, recursive function are those that call them self. For instance, you can define the factorial function as:
fact(0) = 1
fact(n) = n*fact(n-1)
This doesn't look like something you can say with the small syntaxis of the λ-calculus. That is right, but I will prove that you can say something a bit different -but with the same meaning. By doing so, I will prove that it's possible to create recursive functions in this calculus.
Let's try to transform the factorial function into λ-calculus sintax.
First of all, we have to get rid of the different cases. That's easy:
fact(n) = if (n = 0) then 1 else n*fact(n-1)
I invite the reader to read the post "Arithmetics with λ-calculus". Because in λ-calculus there is no if, nor booleans, we have to create them. I will use the same technique for the numbers:
true = (λx y. x)
false = (λx y. y)
if = (λx.x)
true is the function that given two parameters, returns the first one. false is similar to true, but it returns the second parameter. That sounds much like the if and else part of the if structure, respectively. That's why if is just the identity function. So
if condition s t → condition s t
and if condition → ... → true
then true s t → s
(and the oposite for false)
Just for fun, let's make some examples:
and = (λx y. if x y false)
or = (λx y. if x true y)
not = (λx y z. if x z y)
Why does not receive more parameters than and??? Because for and we need just to return the correct boolean, and the boolean will make the "if" thing. But for the not, we've to change the order of the parameters in the "if".
So know we've got the booleans. Now, let's define a useful function for our factorial:
iszero = (λx. x alwaysfalse true)
alwaysfalse = (λx.false)
Remember that a number n is the n-ary application of a function in a parameter. In this case, if the number x is greater than 0, then it will apply x times the function that always returns false. So
iszero 1 → ... → false
and
iszero 0 → ... → true
So we have almost everything for our factorial function. We have the functions mult, iszero, pred, if.
fact = (λn. if (iszero n) 1 (mult n (fact (pred n))))
Now, as I said before, when we use the name iszero, we are meaning the function written above, with all the parenthesis, λ's, etc. So, we still have something to change in our fact expression. Supose that we change the fact label in the body of the fact definition... it will be changed by another expression with a fact inside it, so we change it again... And we continue until we hang ourselves, or until we got killed by bore.
As the bride says: "how do we solve this dilema". And, as Bill answers "Well, It just happens I've got the solution!".
If we find a function (let's call it Fix) like this:
Fix f → ... → f (Fix f)
then we are done. Let's change the fact function so it also take a function as a parameter:
fact = (λf n. if (iszero n) 1 (mult n (f (pred n))))
So, (for simplicity, I will write fact instead of the term above)
Fix fact 3 → ... → fact (Fix fact) 3 = (λf n. if (iszero n) 1 (mult n (f (pred n)))) (Fix fact) 3
putting the (Fix fact) parameter inside the term:
→ (λn. if (iszero n) 1 (mult n ((Fix fact) (pred n)))) 3
putting the 3 parameter inside the term:
→ if (iszero 3) 1 (mult 3 ((Fix fact) (pred 3))))
iszero 3 is false, and pred 3 is 2, so
→ mult 3 ((Fix fact) 2))
And, again Fix fact is fact (Fix fact)
→ mult 3 (fact (Fix fact) 2))
We now how the story ends: →...→ mult 3 (mult 2 (mult 1 1))) → ... → 8
No, just checking if you're still with me. The number is, of course, 6.
Again, if you don't understand anything, try writting it down in a paper, and follow the ideas.
You can see the Fix function as something that feeds the original function (fact) with the next step to execute. Fix exists:
Fix = (λf. (λx. f (x x)) (λx. f (x x)))
Fix g = (λf. (λx. f (x x)) (λx. f (x x))) g → (λx. g (x x)) (λx. g (x x))
→ g ((λx. g (x x)) (λx. g (x x))))
and that exactly:
g (Fix g)
That's it for pure λ-calculus. The next step is to see different calculus that will address implementation problems that arises when trying to make a λ interpreter. 'Till next post!