⇦

2022-03-09

Lambda calculus succinctly in modern JavaScript

The aim of this blog post is to give a flavour of how one might build a useful programming language (or for that matter mathematical system) from a really really small foundation. In our JavaScript notation, the building blocks are just:

f = x => M  // function definition
f(y)        // function application

That's it - no numbers, no lists, no loops, no boolean switches, no strings, no objects.

Instead, we'll give a flavour of how you might conjure up these things seemingly out of the ether.

Doing Lambda calculus with JavaScript notation

You can Google 'Lambda calculus' for a deeper description, but in a nutshell it's a very small, Turing-complete, formal system for expressing computation as symbol manipulation. We're going to rewrite some of the fundamental ideas in familiar JavaScript notation which allows us to easily evaluate them. You can try this out in your browser's console - all the assignments below are in global scope.

In Lambda calculus notation, you might write something kinda like:

(λf.f 4) (λx.x²)

Let's cut straight to the Javascript version:

(f => f(4))(x => Math.pow(x, 2))

Each anonymous function λ takes one argument. When you call a function, you simply replace the argument each time it occurs in the function's body with the value the function was called with.

It's worth noting that this process (known as β-reduction) is just a dumb mechanical one of symbol replacement - nothing else weird is happening. This is important - programs are proofs and by repeatedly applying β-reduction, we can verify them.

In the case of the example above:

(λf.f 4) (λx.x²)

We can β-reduce the f away to make:

((λx.x²) 4)

Then β-reduce the x away to make:

(4²)

Which we know is 16.

Handily, with JavaScript notation, the interpreter will do the reduction automatically! So:

(f => f(4))(x => Math.pow(x, 2))

Does the two reductions above and also evaluates to 16.

Because of this handy time saving property of JavaScript, we'll continue to use that as our Lambda calculus notation.

Integers

In the example above, we had such high level concepts as '4' and 'x²' - these are a bit cheaty, instead, we're going start from nothing except the rules of the calculus.

For integers, we're going to use a system called 'Church numerals'. These aren't nouns like 'one' and 'two', but adverbs like 'call f with a one time' or 'call f on a two times'. If that's a bit abstract, let's define 4 integers:

const _0 = f => a => a
const _1 = f => a => f(a)
const _2 = f => a => f(f(a))
const _3 = f => a => f(f(f(a)))

const toInt = a => a(n => n + 1)(0)

Now let's add in some functions that operate on integers:

const inc  = n => f => a => f(n(f)(a)) // n + 1
const plus = n => m => n(inc)(m)       // n + m
const mult = n => m => a => n(m(a))    // n * m

We can test these in our browser's console using the helper from above, try running:

toInt(plus(_1)(_2))

Neat?

Let's see how that happened by filling in the variables, then repeatedly applying β-reduction:

plus(_1)(_2)                                                   // replace plus, _1, _2
(n => m => n(inc)(m))(f => a => f(a))(f => a => f(f(a)))       // β n
(m => (f => a => f(a))(inc)(m))(f => a => f(f(a)))             // β m
(f => a => f(a))(inc)(f => a => f(f(a)))                       // replace inc
(f => a => f(a))(n => f => a => f(n(f)(a)))(f => a => f(f(a))) // β first f
(a => (n => f => a => f(n(f)(a)))(a))(f => a => f(f(a)))       // β first a
(n => f => a => f(n(f)(a)))(f => a => f(f(a)))                 // β n
f => a => f((f => a => f(f(a)))(f)(a))                         // β second f
f => a => f((a => f(f(a)))(a))                                 // β second a
f => a => f(f(f(a)))

Phewph, that was long, but we did end up with f => a => f(f(f(a))) , which is the Church numeral for '3', so we've shown definitively 1 + 2 = 3, yay!

We can see intuitively how we came up with some of the definitions. Remember earlier, we said the Church numeral 2 is the adverb 'call f on a two times', the definition for plus should make sense with that in mind:

const plus = n => m => n(inc)(m)

Just says 'call inc on m n times'

Booleans

Now we have a representation of integers based just on the calculus, let's define True and False:

const True  = a => b => a
const False = a => b => b

These are, like our integers, very abstract. It's important to consider that the choice is somewhat arbitrary - we're just going to do β-reduction on expressions involving these, and if an expression reduces to a => b => a then we consider it True.

const toBool = a => a(true)(false)

Now let's add some functions that operate on boolean values:

const not = a => a(False)(True)
const and = a => b => a(b)(a)
const or  = a => b => a(a)(b)

Again, try them in your browser's console like:

toBool(or(False)(True))

someBool ? a : b

false ? console.log(1) : console.log(2)

const _ = True  // stands in for 'any value'

someBool(_ => a)(_ => b)(_)

We're also going to define some functions that take an integer and return a boolean:

const isEven = n => n(not)(True)
const isZero = n => n(True(False))(True)

Composite data

Let's create a function to bundle two pieces of data into one, similar to what we might do with an Array in JavaScript.

const pair = a => b => f => f(a)(b)

That's great, but how do we get anything out of it?

const first  = p => p(True)
const second = p => p(False)

Try this in your browser's console:

const myPair = pair(_2)(_0)
toInt(second(myPair))

We're in effect using the pair function's closure to store information.

What can we do that's useful with this? We already have inc that returns the next integer, let's write a dec that returns the previous integer.

const incSecond = p => pair(second(p))(inc(second(p)))
const dec       = n => first(n(incSecond)(pair(_0)(_0)))

Huh? Let's consider just n(incSecond)(pair(_0)(_0))

This says 'call incSecond on pair(_0)(_0) n times'

So if n were 3, then incSecond(incSecond(incSecond(pair(_0)(_0))))

Let's run through that (you might want to write your own helper function to console.log pair s):

incSecond(pair(_0)(_0))                        // pair(_0)(_1)
incSecond(incSecond(pair(_0)(_1)))             // pair(_1)(_2)
incSecond(incSecond(incSecond(pair(_1)(_2))))  // pair(_2)(_3)

Then we take the first of pair(_2)(_3) which is _2 - groovy!

Now we've got all the pieces to add a few other useful functions:

const minus = n => m => m(dec)(n)
const gte   = n => m => isZero(n(dec)(m))
const lt    = n => m => not(gte(n)(m))
const eq    = n => m => and(gte(n)(m))(gte(m)(n))

Loops

We've got a load of handy bits and bobs, now we can start making something that looks like a useful bit of code. In this case, we're going to recreate this JavaScript looping construct using just Lambda calculus:

const loop = (n, m, f, a) => {
    let k = a
    for (let i = n; i < m; i++){
        k = f(i, k)
    }
    return k
}

I'll leave it to the reader to work out the meaning of it:

const incAndCall = f => p => pair(
    inc(first(p))
)(
    f(first(p))(second(p))
)

const loop = n => m => f => a => second(
    (minus(m)(n))(incAndCall(f))(pair(n)(a))
)

Combinators

Now for a sum function, in conventional JavaScript:

const sum = (n) => {
    if (n == 0) return 0
    else return sum(n - 1) + n
}

And in (nearly) pure Lambda calculus:

const sum = n => isZero(n)(_ => _0)(_ => plus(n)(sum(dec(n))))(_)

This works, but is only 'nearly' pure Lambda calculus because sum is referred to within the sum function itself. It only works because that's how our JavaScript interpreter works, and is not built in syntax of the Lambda calculus.

To make it work without refering to itself, we define the 'Y-combinator':

const Y = f => (x => f(_ => x(x)))(x => f(_ => x(x)))

If you work through the β-reduction, this is equivalent to:

Y = f => f(_ => Y(f))

Now we're able to redefine sum without self-reference as:

const sum = Y(g => n => isZero(n)
    (_ => _0)
    (_ => plus(n)(g(_)(dec(n))))
(_))