Deriving Recursion from First Principles
2 Oct 2023
Or: Approaching the Y Combinator
These are some of my class notes. Learning to derive the Y Combinator from first principles is something I’ve always wanted to do. This isn’t quite the Y Combinator, but it’s very close and it still gets you recursion without relying on recursive structures to begin with.
In the beginning, we write a recursive function to compute the length of a list:
(let* ([len (λ (lst)
(if (null? lst)
0
(+ 1 (len (cdr lst)))))])
(len '(1 2 3)))
The let*
syntax allows us to create local variable bindings that can reference themselves. But let’s suppose we don’t have let*
—what do we do?
We can make a function that we give to itself. That then returns the function we want, with the outer function in scope. So, the outer function len
in this example has “type”^{1} $self → Int → Int
. That makes it clear that to get the Int → Int
function we want, we have to pass the function to itself.
(let ([len (λ (len)
(λ (lst)
(if (null? lst)
0
(+ 1 ((len len) (cdr lst))))))])
((len len) '(1 2 3)))
But it’d be nice if we could pull out that (len len)
in the body of the function. Let’s call that len1
.
(let ([len (λ (len)
(let ([len1 (λ (l) ((len len) l))])
(λ (lst)
(if (null? lst)
0
(+ 1 (len1 (cdr lst)))))
))])
((len len) '(1 2 3)))
Note that what we can’t do is this:
(let ([len (λ (len)
(let ([len1 (len len)]) ; problem here!
(λ (lst)
(if (null? lst)
0
(+ 1 (len1 (cdr lst)))))
))])
((len len) '(1 2 3)))
Because this is an eager language, so that’d loop forever.
Let’s do that same trick for the outer len len
:
(let ([len (λ (len)
(let ([len1 (λ (l) ((len len) l))])
(λ (lst)
(if (null? lst)
0
(+ 1 (len1 (cdr lst)))))
))])
(let ([len1 (len len)]) ; type of len1 is Int → Int
(len1 '(1 2 3))))
Note that the (len len)
at the end of that is OK because we’re not doing another self application.
Let’s change that inner let
to a λ
just for fun.
(let ([len (λ (len)
((λ (len1)
(λ (lst)
(if (null? lst) 0 (+ 1 (len1 (cdr lst))))))
(λ (l) ((len len) l))))])
((λ (len1)
(len1 '(1 2 3)))
(len len)))
Rename len
→ self
, len1
→ rec
, and just return the function without calling it:
(let ([self (λ (self)
((λ (rec)
(λ (lst)
(if (null? lst) 0 (+ 1 (rec (cdr lst))))))
(λ (x) ((self self) x))))])
(self self))
Ok, we are ready… let’s go ahead an extract that part (λ (lst) ...)
: that’s the only part of this that knows anything about computing the length of lists. We’ll wrap the whole thing in a function called mk_rec
which takes a function of two arguments: the first argument we will pass rec
to, and the second is the actual argument to the function.
(define (mk_rec fn_x) ; takes two args: the recursive thingy and the argument
(let ([self (λ (self)
((λ (rec)
(λ (x) (fn_x rec x)))
(λ (x) ((self self) x))))])
(self self)))
(define len (mk_rec (λ (rec lst) (if (null? lst) 0 (+ 1 (rec (cdr lst)))))))
(len '(1 2 3)) ; returns 3
(define fact (mk_rec (λ (rec x) (if (zero? x) 1 (* x (rec ( x 1)))))))
(fact 5) ; returns 120
Note that that isn’t actually the the Y combinator exactly. But hey we have recursion without using recursion!
Just for fun:
Note that we could have defined let
as:
(let ((let '`(let ((let ',let))
,let)))
`(let ((let ',let))
,let))
Source: FreeBSD fortune
files; this is probably my favorite quine ever.

Scare quotes intentional: you can’t have selfreferential types in the simplytyped lambda calculus like you see here. The STLC is called strongly normalizing, which means every welltyped term reduces to a value of that type. Thus, you can’t have something like the Y Combinator or Omega (
((λ (x) (x x)) (λ (y) (y y)))
) because these could loop forever (diverge). ↩︎