Notes (TILC 04/05): Recursion
4 Recursion
recursion: A pattern where a function calls itself.
The basic idea behind recursion in lambda calculus is that we want to build an expression that regenerates itself as we reduce it. What I mean by that is if a function F
is going to apply itself inside itself, it’s reduction needs to somehow build a new copy of F
. We’re going to want to end up with some function that transforms F
into a sequence of repeated applications of F
:
F (F (F ....)))
Imagine we want to apply an expression F
to itself once. If F
is the identity function id
:
id id => (\x.x) (\x.x) => \x.x
Let’s say we want a function that does this self-application, that we’ll call M
:
M = \f. f f
Now supppose we apply M
to M
:
M(M) = (\f. f f) (\f. f f) =>
(\f. f f) (\f. f f) => \dots
This is an infinite loop! M(M)
regenerates itself perfectly, so that any reduction just goes M(M) => M(M) ...
. M(M)
is in fact the classic case of a non-terminating lambda expression, and is usually called Ω).
Infinite loops are cool, but what we really want is to modify M(M)
so that we add an application of a function R
at every loop:
M (\f. R (f f)) = (\f. f f) (\f. R (f f)) =>
(\f. R (f f)) (\f. R (f f)) =>
R ((\f. R (f f)) (\f. R (f f)) =>
R ( R ((\f. R (f f)) (\f. R (f f)))) =>
...
When we abstract over R
, this becomes the famous Y
combinator:
Y = \r. (\f. f f) (\f. r (f f)) => \r. (\f. r (f f)) (\f. r (f f))
combinator: A lambda abstraction with no free variables.
Another way to think about the Y
combinator is as a fixed-point combinator.
fixed-point. If x = (f x)
, x
is a fixed-point of the function f
.
Suppose we have a function fix
such that(fix f)
that returns a fixed-point of f
. Then, by the definition of a fixed-point,
(fix f) = f (fix f)
This can be expanded indefinitely as
fix f => f (fix f) => f (f (fix f)) => ...
Which is precisely the same as the Y
combinator:
Y f => f (Y f) = f (f (Y f))
so we can say that Y
is the lambda expression that implements the function fix
for lambda functions.
We know know how to recurse a function R
an infinite number of times:
Y R => R (Y R) => R (R (Y R)) => ...
But suppose we want to only recurse R
a finite number of times:
Y R => R (Y R) => R (R (Y R)) => R ( R ( ... (R B)) ...)
We’re going to have to bottom-out at some base-case B
.
But how do we structure our function R
so that it generates a base case, if YR => R(Y R)
? Won’t that generate more copies of R
no matter what we do?
Watch what happens if we apply Y
to 0_
:
Y 0_ => Y (\s z. z) -> (\s z. z) Y (\s z. z) -> (\s z. z) -> 0_
0_
throws away its first argument, and because it throws away the Y
, the recursion stops. So we if build an R
that at some point throws away the Y
combinator, we’ll lose our means of producing new copies of R
.
Let’s look at the example in the text, which is supposed to sum all the integers between n
and 0_
:
R = (\r n. isZero n 0_ (n succ (r (pred n))) )
sum n = Y R n
Let’s do some reductions on this, starting with sum 0_
:
sum n = Y R 0_ =>
Y (\r n. isZero n 0_ (n succ (r (pred n)))) 0_ =>
(\rn.isZero n 0_ (n succ (r (pred n)))) (Y R) 0_ =>
(isZero 0_ 0_ (0_ succ ((Y R) (pred 0_)))) =>
true 0_ (0_ succ ((Y R) (pred 0_)))) =>
0_
Now sum 1
:
Y R 1 =>
Y (\rn.isZero n 0_ (n succ (r (pred n)))) 1_ =>
(\rn.isZero n 0_ (n succ (r (pred n)))) (Y R) 1_ =>
(isZero 1_ 0_ (1_ succ ((Y R) (pred 1)))) =>
false 0_ (1_ succ ((Y R) (pred 1)))) =>
1_ succ ((Y R) (pred 1))) =>
1_ succ (Y R 0) =>
1_ succ 0 =>
1_
And sum 2_
for good measure:
Y R 2_ =>
Y (\rn.isZero n 0_ (n succ (r (pred n)))) 2_ =>
(\rn.isZero n 0_ (n succ (r (pred n)))) (Y R) 2_ =>
(isZero 2_ 0_ (2_ succ ((Y R) (pred 2_)))) =>
false 0_ (2_ succ ((Y R) (pred 2_)))) =>
2_ succ ((Y R) (pred 2_))) =>
2_ succ (Y R 1_) =>
2_ succ (1_ succ 0_) =>
3_
Let’s break this down into the general case:
loop = \ test f next start. Y (\r s. test s (f (r (next s)))) start
First we test
our state s
and return either true
or false
. In the example in the text, test
is isZero
and s
is a number n
.
If our test returns true
we terminate by returning our base
, (0_
in the above example) otherwise we recurse and return f (r (next s))
. The function f
is what we’re actually interested in evaluating over our recursion. In the above the function f
is add n
or (n succ m)
. The r
is the stand-in for the rest of the recursion that will be generated with a Y R
application. And the next
is pred
in the above example, because we want to count down from n
to 0_
by 1s.
Supposing we want to loop a function f
over the numbers from m_
to 0_
(technically the term is fold f
over the numbers m_
to 0_
, but I don’t want to get into folds just now).
All we have to do is fill apply to loop to the corresponding variables:
loop (\n. isZero n base) f pred m_ =>
Y (\r n. isZero n base
(f (r (pred n)))
)
m_
=>
(\r n. isZero n base (f (r (pred n))))
( Y (\r n. isZero base
(f (r (pred n)))
)
)
m_
=>
(\r n. isZero base
( f
( (Y (\r n. isZero base (f (r (pred n)))))
(pred m_))
)
)
=>
...
In this way we can build a wide range of finite recursive structures.