# Recursion

Reading: TAPL Section 5.2, pages 65-67.

TAPL doesn’t attempt to explain the fixed-point combinator and says (p. 65, fn. 8) that such explanations are “fairly intricate.” Here’s an attempt at one.

## Conditionals

The book defines a function called `test` which always evaluates both of its arms (under call-by-value evaluation). This is often not what we want, especially when recursion is involved.

Exercise 5.2.9 shows how to rewrite the factorial function using `test`; here’s a definition of `if` that works the same way. Note that it’s not a function, but a “macro”.

``if l then m else n ≡ (test l (λz. m) (λz. n)) c0``

## “Manual” recursion

We’d like to define a factorial function recursively:

``fac ≡ λn. if iszro n then c1 else times n (fac (prd n))``

But this definition is circular. So, let’s make `fac` available to itself as a local variable:

``fac' ≡ λf. λn. if iszro n then c1 else times n (f (prd n))``

Then we promise that whenever `fac'` is invoked, it will receive itself as its first argument. It may seem like we could just define `fac ≡ fac' fac'`, but we need to keep this promise even for the recursive call as well. So we modify `fac'` into:

``fac" ≡ λh. λn. if iszro n then c1 else times n (h h (prd n))``

Now we can define

``fac ≡ fac" fac"``

To see how this works, note that

``````fac ≡ fac" fac"
≡ (λh. λn. if iszro n then c1 else times n (h h (prd n))) fac"
⟶ λn. if iszro n then c1 else times n (fac" fac" (prd n))``````

So whenever you self-apply `fac"`, it unrolls one step of recursion – only one, because the new occurrence of `fac" fac"` is buried deep in the term and self-applies just before the actual recursive call is made.

Check that `fac c3 = c6`:

``````fac c3 ≡ fac" fac" c3
≡ (λh. λn. if iszro n then c1 else times n (h h (prd n))) fac" c3
⟶ (λn. if iszro n then c1 else times n (fac" fac" (prd n))) c3
⟶ if iszro c3 then c1 else times c3 (fac" fac" (prd c3))
⟶* if fls then c1 else times c3 (fac" fac" (prd c3))
⟶* times c3 (fac" fac" (prd c3))
⟶v* times c3 (fac" fac" c2)``````

(The `⟶v` is because the next redex is `times c3`, but we don’t want to expand the definition of `times`.) The recursion happens similarly two more times:

``````   ⟶v* times c3 (times c2 (fac" fac" c1))
⟶v* times c3 (times c2 (times c1 (fac" fac" c0)))``````

And now the base case:

``````       ≡ times c3 (times c2 (times c1 ((λh. λn. if iszro n then c1 else times n (h h (prd n))) fac" c0)))
⟶v times c3 (times c2 (times c1 ((λn. if iszro n then c1 else times n (fac" fac" (prd n))) c0)))
⟶v times c3 (times c2 (times c1 (if iszro c0 then c1 else times c0 (fac" fac" (prd c0)))))
⟶v* times c3 (times c2 (times c1 (if tru then c1 else times c0 (fac" fac" (prd c0)))))
⟶v* times c3 (times c2 (times c1 c1))
⟶v* times c3 (times c2 c1)
⟶v* times c3 c2
⟶v* c6``````

## The fixed-point combinator

This works. But, it’s still not very convenient for the programmer to define recursive functions this way. We previously discarded `fac'` as incorrect, but it’s simple, so it would be convenient to have a function `fix` such that we can define `fac ≡ fix fac'`.

Let’s look at `fac'` and `fac"` again and think about how we might express `fac"` (or something equivalent) in terms of `fac'`:

``````fac' ≡ λf. λn. if iszro n then c1 else times n (f (prd n))
fac" ≡ λh. λn. if iszro n then c1 else times n (h h (prd n))``````

``     fac" ≡ λh. fac' (h h)``

Unfortunately, that leads to infinite recursion before we even apply `fac" fac"` to a number:

``````fac" fac" ≡ (λh. fac' (h h)) fac"
⟶ fac' (fac" fac")
⟶ fac' (fac' (fac" fac"))
⟶ fac' (fac' (fac' (fac" fac")))
⋮``````

To delay the recursion, wrap the self-application `h h` inside a `λv. … v` (known as an η-expansion):

``````     fac" ≡ λh. fac' (λv. h h v)
fac" fac" ≡ (λh. fac' (λv. h h v)) fac"
⟶ fac' (λv. fac" fac" v)
≡ (λf. λn. if iszro n then c1 else times n (f (prd n))) (λv. fac" fac" v)
⟶ λn. if iszro n then c1 else times n ((λv. fac" fac" v) (prd n))``````

Good – now the self-application `fac" fac"` happens just before the recursive call, as before.

Now we want a function `fix` such that `fix fac' = fac" fac"`:

``  fix ≡ λg. (λh. g (λv. h h v)) (λh. g (λv. h h v))``

This function is known as the call-by-value fixed-point combinator, and is also written as `Z`. If we define `fac ≡ fix fac'`, it reduces to `fac" fac"` as desired:

``````fac ≡ fix fac'
≡ (λg. (λh. g (λv. h h v)) (λh. g (λv. h h v))) fac'
⟶ (λh. fac' (λv. h h v)) (λh. fac' (λv. h h v))
≡ fac" fac"``````

We can check that `fac c3 = c6`:

``````fac c3 ⟶ fac" fac" c3
⟶² (λn. if iszro n then c1 else times n ((λv. fac" fac" v) (prd n))) c3
⟶ if iszro c3 then c1 else times c3 ((λv. fac" fac" v) (prd c3))
⟶* if fls then c1 else times c3 ((λv. fac" fac" v) (prd c3))
⟶* times c3 ((λv. fac" fac" v) (prd c3))
⟶v* times c3 ((λv. fac" fac" v) c2)
⟶v times c3 (fac" fac" c2)``````

The recursion happens two more times:

``````     ⟶v* times c3 (times c2 (fac" fac" c1))
⟶v* times c3 (times c2 (times c1 (fac" fac" c0)))``````

And now the base case:

``````     ⟶v² times c3 (times c2 (times c1 (λn. if iszro n then c1 else times n ((λv. fac" fac" v) (prd n))) c0))
⟶v times c3 (times c2 (times c1 (if iszro c0 then c1 else times c0 ((λv. fac" fac" v) (prd c0)))))
⟶v* times c3 (times c2 (times c1 (if tru then c1 else times c0 ((λv. fac" fac" v) (prd c0)))))
⟶v* times c3 (times c2 (times c1 c1))
⟶v* times c3 (times c2 c1)
⟶v* times c3 c2
⟶v* c6``````

Question. What would happen if we had used the better-known `Y` combinator (namesake of the startup incubator), shown below, instead of `Z`? What is the `Y` combinator good for?

``  Y ≡ λg. (λh. g (h h)) (λh. g (h h))``

## Turing-completeness

Here’s a sketch of how a Turing machine might be simulated in the lambda calculus.

We’ll represent the tape as two lists (Exercise 5.2.8). We can represent both tape symbols and states using Church numerals, with a designated tape symbol `blank` and designated start and accept states `q0` and `qf`. We need a definition of `equal` that works on both tape symbols and states (Exercise 5.2.7).

Then, given a Turing machine, construct a function `f`:

``````f ≡ λf. λq. λl. λa. λr.
if equal q qf then tru

# for each transition (Q, A, Q', A', N):
else if and (equal q Q) (equal a A) then
f Q' l A' r

# for each transition (Q, A, Q', A', L):
else if and (equal q Q) (equal a A) then
if (isnil l) then
f Q' (tail l) (head l) (cons A' r)
else
f Q' l A' r

# for each transition (Q, A, Q', A', R):
else if and (equal q Q) (equal a A) then
if isnil r then
f Q' (cons A' l) blank nil
else
f Q' (cons A' l) (head r) (tail r)

...

else fls``````

Then `λw. fix f q0 nil (head w) (tail w)` simulates the Turing machine.