Lambda calculus through JavaScript, part 3

Lambda calculus through JavaScript, part 3

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_ (our encoded Boolean) whenever n is zero, and false_ 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_x is true_.

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_f to either true_ (the value we have found for unknown_x) or other recursive application of unknown_f. And, in both cases, we need the final result to be false_. One such choice is the constantly-false function x => false_. 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, 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_, 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_, 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!

At 47 Degrees, we are true lovers of functional programming in all its forms. You can check our upcoming and past courses and talks at 47 Degrees Academy, and our broad contributions to open source in the functional community.

Ensure the success of your project

47 Degrees can work with you to help manage the risks of technology evolution, develop a team of top-tier engaged developers, improve productivity, lower maintenance cost, increase hardware utilization, and improve product quality; all while using the best technologies.