# 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)) c`_{0}

## “Manual” recursion

We’d like to define a factorial function recursively:

`fac ≡ λn. if iszro n then c`_{1} 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 c`_{1} 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 c`_{1} 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 c
```_{1} else times n (h h (prd n))) fac"
⟶ λn. if iszro n then c_{1} 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 c`

:_{3} = c_{6}

`fac c`_{3} ≡ fac" fac" c_{3}
≡ (λh. λn. if iszro n then c_{1} else times n (h h (prd n))) fac" c_{3}
⟶ (λn. if iszro n then c_{1} else times n (fac" fac" (prd n))) c_{3}
⟶ if iszro c_{3} then c_{1} else times c_{3} (fac" fac" (prd c_{3}))
⟶* if fls then c_{1} else times c_{3} (fac" fac" (prd c_{3}))
⟶* times c_{3} (fac" fac" (prd c_{3}))
⟶_{v}* times c_{3} (fac" fac" c_{2})

(The `⟶`

is because the next redex is _{v}`times c`

, but we don’t want to expand the definition of _{3}`times`

.) The recursion happens similarly two more times:

` ⟶`_{v}* times c_{3} (times c_{2} (fac" fac" c_{1}))
⟶_{v}* times c_{3} (times c_{2} (times c_{1} (fac" fac" c_{0})))

And now the base case:

` ≡ times c`_{3} (times c_{2} (times c_{1} ((λh. λn. if iszro n then c_{1} else times n (h h (prd n))) fac" c_{0})))
⟶_{v} times c_{3} (times c_{2} (times c_{1} ((λn. if iszro n then c_{1} else times n (fac" fac" (prd n))) c_{0})))
⟶_{v} times c_{3} (times c_{2} (times c_{1} (if iszro c_{0} then c_{1} else times c_{0} (fac" fac" (prd c_{0})))))
⟶_{v}* times c_{3} (times c_{2} (times c_{1} (if tru then c_{1} else times c_{0} (fac" fac" (prd c_{0})))))
⟶_{v}* times c_{3} (times c_{2} (times c_{1} c_{1}))
⟶_{v}* times c_{3} (times c_{2} c_{1})
⟶_{v}* times c_{3} c_{2}
⟶_{v}* c_{6}

## 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 c`_{1} else times n (f (prd n))
fac" ≡ λh. λn. if iszro n then c_{1} else times n (h h (prd n))

How about:

` 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 c
```_{1} else times n (f (prd n))) (λv. fac" fac" v)
⟶ λn. if iszro n then c_{1} 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 c`

:_{3} = c_{6}

`fac c`_{3} ⟶ fac" fac" c_{3}
⟶² (λn. if iszro n then c_{1} else times n ((λv. fac" fac" v) (prd n))) c_{3}
⟶ if iszro c_{3} then c_{1} else times c_{3} ((λv. fac" fac" v) (prd c_{3}))
⟶* if fls then c_{1} else times c_{3} ((λv. fac" fac" v) (prd c_{3}))
⟶* times c_{3} ((λv. fac" fac" v) (prd c_{3}))
⟶_{v}* times c_{3} ((λv. fac" fac" v) c_{2})
⟶_{v} times c_{3} (fac" fac" c_{2})

The recursion happens two more times:

` ⟶`_{v}* times c_{3} (times c_{2} (fac" fac" c_{1}))
⟶_{v}* times c_{3} (times c_{2} (times c_{1} (fac" fac" c_{0})))

And now the base case:

` ⟶`_{v}² times c_{3} (times c_{2} (times c_{1} (λn. if iszro n then c_{1} else times n ((λv. fac" fac" v) (prd n))) c_{0}))
⟶_{v} times c_{3} (times c_{2} (times c_{1} (if iszro c_{0} then c_{1} else times c_{0} ((λv. fac" fac" v) (prd c_{0})))))
⟶_{v}* times c_{3} (times c_{2} (times c_{1} (if tru then c_{1} else times c_{0} ((λv. fac" fac" v) (prd c_{0})))))
⟶_{v}* times c_{3} (times c_{2} (times c_{1} c_{1}))
⟶_{v}* times c_{3} (times c_{2} c_{1})
⟶_{v}* times c_{3} c_{2}
⟶_{v}* c_{6}

**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.