Making Sense of Lambda Calculus 3: Truth or Dare With Booleans

Booleans are Branching

Numbers are function compositions. Akin to that, booleans are computation branching. Meaning, boolean operations are kind of building trees out of given data. For example, here's how not operator looks like in LC:

not = λp.p false true

So it takes a boolean and applies it to false and true. If the boolean is true, then it picks the false branch, and vice versa. A decision tree of sorts. Some more elegant branching operations, and & or:

and = λp.λq.p q p // If p is true, check q
or = λp.λq.p p q // If p is false, check q
// Alternative versions
and = λp.λq.p q false
or = λp.λq.p true q

Again, branching operations instead of truth tables.

And here's how XOR looks like:

xor = λp.λq.p (not q) q

Simple and smart at the same time.

Ah, Logic Again

But if we try to define operations like nand or nor, our branching doesn't help much. Here's how nand might look like:

nand = λp.λq.p (q false true) true

Not too bad, but it totally obviates the meaning of the operation. It's just boolean juggling. The truth tables I'm trying to avoid. But the good thing about Lambda Calculus is that we can use the functions from before to fix that. (Well, at least notation-wise—the compiled lambdas won't have names. Still, most LC implementations allow for some let/where syntax, so I'm safe.) This way derivative operations look much more meaningful:

nand = λp.λq.(not (and p q))
nor = λp.λq.(not (or p q))
xnor = λp.λq.(not (xor p q))

We built our primitives out of branching functions. And then used them to define derivative operations. An elegant solution mapping boolean logic directly to LC. No truth tables, which is a win. Now to actually using these operations:

Laconic If

Cutting it short, if is:

if = λb.λt.λe.b t e
// Or even
if = λb.b

Booleans already select between branches. So if doesn't need to do anything: just apply the boolean to both options. And watch the magic happen.

A person familiar with the regular if that chooses and runs only one branch: "But that's dangerous: it's evaluating both branches. There might be side-effects." There are no side-effects in LC, though. And there is no "evaluation" in it either: only reduction. It's okay.

Applying Booleans to Numbers

That's the part I've been teasing you with in the previous post. Finally, we can do comparisons and predicates on numbers. Here's the most basic—checking for zero:

iszero = λn.n (λx.false) true

Numbers are applying a function to a value. If they do apply it even once (number > 0), return false. If they don't (number = 0), return true. That simple. And it doesn't matter if the number is arbitrarily big. Applying (λx.false) has no side-effects (again, there are none in LC). So we can safely apply it as much as we wish to.

Comparisons, the simplest ones:

leq = λm.λn.iszero (sub m n)
geq = λm.λn.iszero (sub n m)

The number A is greater than another number B if subtracting B from A yield non-zero. (Notice that Church/Peano numerals are strictly non-negative. Smallest value subtraction can yield is zero.) And vice versa. Having these, other predicates are easy:

gt = λm.λn.not (leq m n)
lt = λm.λn.not (geq m n)
eq = λm.λn.and (leq m n) (leq n m)

Maps the mental model perfectly: number A is greater if it's not less than or equal than B. And equality (this is slightly tricky) is when the numbers are both less than or equal than each other. Because if both are, then both must be the same number. Otherwise one of these will be greater and the condition will be false.

Finally, Using Booleans!

The simplest example for usage of all these operators might be minimum and maximum functions:

min = λm.λn.if (lt m n) m n
max = λm.λn.if (lt m n) n m

I might've used leq here, but the behavior stays the same. It doesn't matter which of the two we pick—both are valid numbers. If they are the same number, they are fully β-equivalent and picking either is fine. So it does not matter whether there's leq or lt.

Up Next: Consing Up The World

With that, I'm ready to conclude the booleans post. What happened here was:

• Booleans as decision trees.
• Branching logic operations.
• Perfect mapping from logic to LC for derived ops.
• Number predicates.
• And, finally, conditional operations on numbers (or any data, really—the idea is the same.)

With basic data types, numbers and booleans, one can already encode a lot. But there's a point at which one wants aggregate data types. Like cons trees/lists/structures. That's the next post topic, so byte (sic) your nails until then.

Leave feedback! (via email)