# Lambda calculus through JavaScript, part 3

- by Alejandro Serrano
- •
- January 14, 2021
- •
- haskell• ml• lambda calculus• functional programming• functional• javascript
- |
- 12 minutes to read.

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.