Booleans in the Lambda Calculus

During my undergraduate studies in Computer Science, I learned a little about the lambda calculus, Turning machines, and the Church-Turing Thesis at a fairly high level, but we never delved into the mechanics of the lambda calculus. I'm currently reading The Genius of Lisp by Cees de Groot (which I'm enjoying, BTW), and he includes a nice discussion of the lambda calculus, including a representation of parts of it in JavaScript.

What's the big deal with the lambda calculus? Church showed that anything that can be computed can be computed with just three concepts:

  1. Parameters
  2. Single-argument functions
  3. Function application

A universal model of computation from three very simple ideas!

Many-Argument Functions from Single-Argument Functions

Single-argument functions might seem very restricting, but we can create functions that take multiple arguments by currying single-argument functions. In the lambda calculus it would look something like:

λx.(λy.body)

In JavaScript it might look like:

const F = x => y => {
    // body
};

You call it like this:

F(1)(2)

Technically F doesn't take two arguments, but calling it like F(1)(2) is pretty damn close.

Boolean Values and Operations

True and False

You start by representing true (T) and false (F) not as values, but as functions that take two arguments and choose one of the arguments.

True is a function that chooses its first argument:

const T = a => b => a;

False is a function that chooses its second argument:

const F = a => b => b;

NOT

Those definitions of T and F didn't make much sense to me until I saw how they are used with NOT.

const NOT = p => p(F)(T);

Calling NOT(T) evaluates T(F)(T). Since T chooses its first argument, it returns F.

Calling NOT(F) evaluates F(F)(T). Since F chooses its second argument, it returns T.

> NOT(T)
[Function: F]
> NOT(F)
[Function: T]

And there you have it, the NOT boolean operator using only parameters, single-argument functions, and function applications.

AND

const AND = p => q => p(q)(p);

Calling AND(T)(T) evaluates T(T)(T). Since T picks the first argument, it picks T.

Calling AND(T)(F) evaluates T(F)(T). Since T picks the first argument, it picks F.

Calling AND(F)(T) evaluates F(T)(F). Since F picks the second argument, it picks F.

Calling AND(F)(F) evaluates F(F)(F). Since F picks the second argument, it picks F.

You can see how this only returns T if both arguments are T.

OR

const OR = p => q => p(p)(q);

Calling OR(T)(F) evaluates T(T)(F). Since T picks the first argument, it picks T.

Calling OR(F)(T) evaluates F(F)(T). Since F picks the second argument, it picks T.

Calling OR(T)(T) evaluates T(T)(T). Since T picks the first argument, it picks T.

Calling OR(F)(F) evaluates F(F)(F). Since F picks the second argument, it picks F.

You can see how this returns T when either argument is T.

Just the Beginning

Church also showed how numbers, arithmetic operations, and the rest can be represented by the lambda calculus. It's really an amazing discovery!

I can write about how numbers are represented in the lambda calculus as repeated function application, if anyone is interested. Just send me an email.