The blog of David Wickes, software developer

Lambda Calculus 4 - Logic with Church Booleans

I found Church numbers pretty tough, and I’m still not sure I fully understand them. But this post should be a little bit easier. I promised logic for this post, and logic I will give you. But not right now. First, it’s…

Data structures with functions

As modern 21st century software developers, we’re used to a strong divide between data and process. Even with object orientation we consider an object to be made of things it knows (the data) and things it does (the methods).1

I always picture my programs as big old conveyor belts, where my program-workers each beat the hell out of a piece of data as it goes past, until it comes out as a shiny new BMW piece of JSON.

Meanwhile, here in the lambda calculus… well, we’ve got numbers for sure. But how can we get data structures like a piece of shiny JSON? Or even just a list?

Take heart - through the lambda, all things are possible!2

Let’s try the simplest of all data structures - the pair. Simple, sure - but powerful. Every good Lisper knows that the can build any data interface you can conceive using enough pairs. If Lisp was written by Archimedes, he’d say “Give me a place to stand and enough cons cells and I shall move the earth”.

To get a pair as a data structure up and flying, we need three functions. One to make a pair out of two arguments, one that returns the first item in the pair, and another that returns the second item. Lispers will say “Ah! cons, car and cdr!”, but we will say $pair$, $first$ and $second$.

First $pair$:

$$ pair\quad \equiv \quad \lambda p.\lambda q.\lambda f.\ f\ p\ q $$

We take the two things we’re pairing - that much makes sense - but then we take one more argument and apply it, first to the first argument, and then the result of that to the second argument.

What’s going on?

We want something like $ first < aPair > $ to give us back the first item that we gave to the pair. So the final $f$ in pair is going to be offered both $p$ and $q$ and left to decide which one it wants.

$$ first\quad \equiv \quad \lambda pair. pair\ (\lambda a.\lambda b.\ a) $$

$first$ takes a pair, and then gives that pair a function that takes two arguments and returns… well, the first one. Given that, it’s a doddle to write $second$:

$$ second\quad \equiv \quad \lambda pair. pair\ (\lambda a.\lambda b.\ b) $$

Same again, but this time we evaluate to the second of the arguments.

Feel free to stick it into a programming language and play with it. Here it is in Scheme:

(define pair
    (lambda (p)
        (lambda (q)
            (lambda (f)
                ((f p) q)))))
(define first
    (lambda (p) (p (lambda (a) (lambda (b) a)))))
(define second
    (lambda (p) (p (lambda (a) (lambda (b) b)))))


What is truth? said jesting Pilate, and would not stay for an answer. &mdash; Francis Bacon, On Truth

Well, I hope you do stay for an answer. And there is an answer, at least for the concerns of the lambda calculus, but it’s not going to be particularly life altering. In fact, it’s probably going to remind you most of the solution to what a number is.

Numbers… AGAIN!

When we defined numbers a few posts ago, I was being fairly adamant that the best way to encode a number using functions would be to count the number of applications of a function. Remember - $zero$ was no applications, $one$ was one, etc.

But this ain’t necessarily so - we could implement numbers using the definition of pairs above:

$$ zero \quad \equiv \quad \lambda x\ x $$

$$ succ \quad \equiv \quad \lambda n.\ pair\ <FALSE>\ n $$

Here we’ve defined $zero$ as the identity function, and $succ$, the successor, as a pair of $<FALSE>$ to whatever the previous number was. Each number is now ‘counting’ using the number of times that $zero$ has been paired up with $<FALSE>$.

We can now go on to define other functions around this implementation - and we will - but the key thing I’d like to stress is that what makes a number a number isn’t really what it is, but rather how it behaves - how it behaves when being used with other functions like $add$ and $multiply$.

Let’s use that insight to imagine what $true$ and $false$ might be.

if … then … else

Every programming language I’ve ever worked in has some sort of if expression or statement - a way of choosing one bit of code or another based on whether something was true or false. You know:

if (1 + 1 == 2)
    puts "One and one is two!"
    puts "Maths is broken!"

We could think of if as being a function in the lambda calculus:

$$ if \quad \equiv \quad \lambda bool.\lambda t.\lambda f.\ tOrf $$

This is fine, but gets us nowhere. But what if there were two different functions, one of which we used for true booleans, and one of which we used for false ones. Yes, I know, that would make no sense - you’d have to know which one to use. But humour me.

$$ ifTrue \quad \equiv \quad \lambda bool.\lambda t.\lambda f.\ t $$

$$ ifFalse \quad \equiv \quad \lambda bool.\lambda t.\lambda f.\ f $$

We’re not even using the boolean any more, we’re just saying that if the boolean is true, we evaluate to first argument, and if it’s false we evaluate to the second argument.

If we’re not using the lambda that takes a boolean - the $\lambda bool$ - we can get rid of it from the end.

$$ true \quad \equiv \quad \lambda a.\lambda b.\ a $$

$$ false \quad \equiv \quad \lambda a.\lambda b.\ b $$

And there we have it. We can just say that $true$ is the function that returns the first, and $false$ is the function that returns the second.

Wait, can we? Well, why not? All we need really is a function that will signal one of two things - true or false we can call them. This ‘signal’ we choose to be the return of the first or the second of the arguments it is applied to. Who cares how truth works - this is a mechanism that does what it needs to do.

Truth Tables


So now we’ve got truth going, let’s have some fun defining some boolean operations. First, an easy one - $and$. And once again we’re going to use the behaviour of $and$ to give us a clue as to the implementation.

What’s the behaviour? This might be easier to do if we construct a truth table. What’s a truth table I hear you cry? Well, in logic we can draw up a table showing the truth or falsity of a proposition (sentence that is either true or false) based upon the truth or falsity of the propositions from which it is composed.

The truth table is just the exhaustive table of true and false values that can exist in the proposition, along with the resulting truthfulness of the overall proposition. A proposition involving ‘and’ will be made of two sub-propositions - the two being ‘anded’ together. Traditionally these are written as ‘$P$’ and ‘$Q$’ - and who are we to disagree with tradition? The symbol ‘$\land$’ is often used for ‘and’, so we’ll do the same here. Finally, true and false will be ‘$T$’ and ‘$F$’.

$$ \begin{array}{| c c | c |} P & Q & P \land Q \\ \hline T & T & T \\ T & F & F \\ F & T & F \\ F & F & F \end{array} $$

What can we learn from this? Well, two things:

So we could say something like “if $P$ then $Q$ else $false$”. And as $P$ is a boolean as described above, we can pass it a couple of arguments just like it was an ‘if… then… else’. So we can write $and$ as:

$$ and \quad \equiv \quad \lambda p.\lambda q.\ p\ q\ false $$

Or, even more concisely:

$$ and \quad \equiv \quad \lambda p.\lambda q.\ p\ q\ p $$

As if $p$ is false we can just evaluate to $p$


‘Or’ is represented by ‘$\lor$’:

$$ \begin{array}{| c c | c |} P & Q & P \lor Q \\ \hline T & T & T \\ T & F & T \\ F & T & T \\ F & F & F \end{array} $$

The pattern here should be clearer after doing $and$

Which can be written in lambdas as:

$$ or \quad \equiv \quad \lambda p.\lambda q.\ p\ p\ q $$


‘Not’ is nice and short as a truth table. We will use $\lnot$ to represent it

$$ \begin{array}{ c | c } P & \lnot P \\ \hline T & F \\ F & T \end{array} $$

We just need to flip $P$ around - if it was true (returning the first argument), we make it return false (return the second argument), and vice versa.

Like this:

$$ not \quad \equiv \quad \lambda p.\lambda a.\lambda b.\ p\ b\ a $$

if … then

$$ \begin{array}{ c c | c } P & Q & P \implies Q \\ \hline T & T & T \\ T & F & F \\ F & T & T \\ F & F & T \end{array} $$

$$ implies \quad \equiv \quad \lambda p.\lambda q. p\ q\ p $$

if and only if

$$ \begin{array}{ c c | c } P & Q & P \iff Q \\ \hline T & T & T \\ F & F & T \\ F & T & F \\ T & F & F \end{array} $$

$$ iff \quad \equiv \quad \lambda p.\lambda q. p\ q\ (not\ p) $$

$$ true \quad \equiv \quad \lambda a.\lambda b.\ a $$

$$ false \quad \equiv \quad \lambda a.\lambda b.\ b $$

$$ and \quad \equiv \quad \lambda p.\lambda q.\ p q p $$

$$ or \quad \equiv \quad \lambda p.\lambda q.\ p p q $$

$$ if \quad \equiv \quad \lambda p.\lambda a.\lambda b.\ p a b $$

  1. I will be the first to admit that this is a terrible definition of OO, mainly driven by my ignorance.
  2. All things not necessarily possible with the lambda. Terms and conditions apply.