This article was originally published at 47deg.com on January 14, 2021.
We’re moving fast through this lambda calculus series! In part one, we laid out the foundations for working with JavaScript as a lambda calculus, and, through part 2, we added Booleans and numbers to our repertory. But, let’s be honest, defining addition and multiplication was kind of a magic trick. In this post, we look at the more familiar technique of recursion, leading us to talk about fixed points and, ultimately, to the swamps of non-termination.
My favorite Gauss story
If you’ve ever listened to some of my beginner talks, you’ve definitely heard this story, because I love it. They say that when Carl Friedrich Gauss was a child – let’s call him “Little Gauss” from now on – he was a bit naughty. As a punishment, his teacher asked him to sum all the numbers from 1 to 100, which he did in a blast. How? by developing a simple formula to do so. Have I mentioned Gauss is considered “The Prince of Mathematics” for his broad advancements in many areas of the discipline?
Stories aside, our goal is to help Little Gauss with his punishment. Not by developing a formula, but by programming the computer to do the sum. If we were not talking about lambda calculus, the solution would be quite simple:
const littleGaussHelper = n => n === 0 ? 0 : n + littleGaussHelper(n - 1)
We already know how to represent some of the elements; namely the conditional, the number 0, and the addition. We are missing a way to figure out whether a number is zero, and to obtain the predecessor of a number.
Are you zero?
Focusing on our first task, we want to define a function isZero(n)
such that it returns true<em>
(our encoded Boolean) whenever n
is zero, and false</em>
otherwise. Remember that Church numerals are functions themselves; as we did in part 2, we are going to figure out which arguments unknown_f
and unknown_x
should be given to obtain the desired outcome.
const isZero = n => n(unknown_f)(unknown_x)
When n
is the numeral zero
, the definition collapses into unknown_x
, because zero applies its first argument no times.
isZero(zero) = zero(unknown_f)(unknown_x) = unknown_x
On the other hand, we know that isZero(zero)
should equal true_
, so it must be the case that unknown<em>x
is true</em>
.
By the end of part 2, we understood how a Church numeral could be seen as a repeated application of a function. That is, whenever n
is not zero
, the result of isZero(n)
is going to be the application of unknown<em>f
to either true</em>
(the value we have found for unknown<em>x
) or other recursive application of unknown<em>f
. And, in both cases, we need the final result to be false</em>
. One such choice is the constantly-false function x => false</em>
. As a result, our definition of isZero
becomes:
const isZero = n => n(x => false_)(true_)
This way of thinking – considering an incomplete function and by checking the result on each argument refining its definition – is called program calculation. Graham Hutton is the absolute master of this technique. In this video – skillsmatter.com/skillscasts/8491-calculating-correct-compilers , he scales the technique up to calculating a compiler!
Predecessor woes
The function which computes n => n - 1
– usually called the predecessor function – is quite a monster:
const pred = n => (f => x => n(g => h => h(g(f)))(u => x)(u => u)
Why it works, and how to derive it, would make it lose focus on our task of recursion; furthermore, we’ll learn simpler ways to work with numbers soon. For those who are interested, the predecessor function is carefully explained in the corresponding Wikipedia article. One key point, in any case, is that the outer application of n
does not compute the number directly, but a function which then computes the number. This is why it looks like n
has three arguments, whereas formally it only has two.
Being a bit meta
It looks like we are ready to write our function. Remember that in regular JavaScript littleGaussHelper
looks as follows:
const littleGaussHelper = n => n === 0 ? 0 : n + littleGaussHelper(n - 1)
The translation can have many different forms, depending on how much of the actual definitions of if_
and the rest of components you want to bring in. Here is one possibility:
const littleGaussHelper = n => if_(isZero(n))(zero)(add(n)(littleGaussHelper(pred(n))))
“Done!,” I hear you thinking. Not really, because here we are calling littleGaussHelper
from itself. And this is not allowed by our rules.
But why is littleGaussHelper
suddenly not allowed, whereas if<em>
, zero
, or pred
pose no problem? If we were complete purists, the latter would not be accepted either, since our rules for lambda calculus only allow functions x => something
and applications f(something)
. We allow ourselves, though, to use the facilities of JavaScript as a language to record and substitute definitions: when we write if</em>
, for example, you should think of the expanded version in which if_
is replaced by its definition. For example, isZero
should be expanded to:
const isZero = n => n(x => t => f => f)(t => f => t)
This simple mechanism breaks when we have a recursive function, since we would never finish replacing names with their definitions. We need to find a way – within our strict rules – to rewrite recursion into a non-recursive form. This business of definitions within lambda calculus gets even subtler when you move into other corners of the lambda cube with powerful forms of typing (simply typed lambda calculus, System F, dependent types). The book Type Theory and Formal Proof devotes an entire chapter to discussing it!
We usually say in this situation that JavaScript is the host or macro language, and lambda calculus is the object language. We also say that JavaScript is providing meta-programming facilities for lambda calculus, where here “meta” means “programming the programs.”
Recursion-as-a-function
In an unexpected turn of events, we do not need any new element in lambda calculus to introduce recursive functions. Instead, we are going to define a fix
function which takes care of the whole recursion mechanism (Haskellers may recognize the similarly-named function.). If you have never seen this trick before, the last sentence may not make sense: how can a function “take care” of recursion?
Once again, let’s consider the function we want to implement:
const littleGaussHelper = n => if_(isZero(n))(zero)(add(n)(littleGaussHelper(pred(n))))
This is how it looks using fix
:
const littleGaussHelper = fix(lhg => n => if_(isZero(n))(zero)(add(n)(lhg(pred(n)))))
The argument to the fix
function takes an additional lhg
argument when compared with the original littleGaussHelper
. Whenever you call this function in the body of fix
, this will eventually represent the recursive call. But note that the argument to fix
now has no recursion; everything is simply an argument to the function. The fix
function is responsible for working out the recursion; that process is usually referred to as typing the knot or typing the recursive loop.
The Y combinator
Enter the Y combinator, a very odd-looking term in lambda calculus. Note that, in this case, we are taking full advantage of the untyped nature of the language, since we are applying a function x
to itself.
const Y = g => (x => g(x(x))) (x => g(x(x)))
The Y combinator is part of a family of terms called fixed points combinators. Mathematicians often call fixed points to those values x
of a function f
such that x = f(x)
. For example, 0
and 1
are fixed points of the function x => x * x
. The Y combinator applied to any function f
gives rise to a fixed point of that same function.
Y(f) = (x => f(x(x))) (x => f(x(x)))
= f ( (x => f(x(x))) (x => f(x(x))) )
= f ( Y(f) )
That’s the magic: Y combinator ends up applying f
recursively! So Y
can be used as a definition for the fix
we were looking for. Because this is sometimes difficult to believe, let’s execute littleGaussHelper(two)
:
littleGaussHelper(two)
= fix(lhg => n => if_(isZero(n))(zero)(add(n)(lhg(pred(n))))) (two)
// since fix(f) = f(fix(f))
= (n => if_(isZero(n))(zero)(add(n)(fix(lhg => ...)(pred(n))))) (two)
= if_(isZero(two))(zero)(add(two)(fix(lhg => ...)(pred(two))))
= add(two)(fix(lhg => ...)(one))
// since fix(f) = f(fix(f))
= add(two)(if_(isZero(one))(zero)(add(one)(fix(lhg => ...)(pred(one)))))
= add(two)(add(one)(fix(lhg => ...)(zero)))
// since fix(f) = f(fix(f))
= add(two)(add(one)(if_(isZero(zero))(zero)(add(zero)(fix(lhg => ...)(pred(zero))))))
= add(two)(add(one)(zero))
The never-ending term
Recursion comes with its own can of worms: you need to be very careful to ensure that every recursive function eventually terminates. Not every function in (untyped) lambda calculus terminates; one important example is called Ω
and results by specializing Y
to the identity function:
const Ω = (x => x(x)) (x => x(x))
A captivating property of Ω
is that it evaluates to itself. If you take one step and replace the argument (x => x(x))
in the function (x => x(x))
, you get the same result.
These kinds of terms are related to the halting problem. It can be (mathematically) proven that no algorithm can exist that for any term in lambda calculus, it decides whether the evaluation of such term terminates or recurs indefinitely. We say that the problem is undecidable. Historically, the fact that undecidable problems exist puts the idea of a “universal theorem decider” (Entscheidungsproblem in German, as it is usually known) to rest.
Enough for today
Booleans and conditionals; numbers, repetition, and recursion; they are all nice tools for programming. But to get a nice structure, one often uses data types, and that would be our next goal: how to represent lists or trees within our small lambda calculus? Stay tuned!