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!