Conditions, Booleans and Integers

Lambda Calculus

2026-08-19 09:30

Where we are

What unit 2 left you

def select_first  = λfirst.λsecond.first
def select_second = λfirst.λsecond.second
def make_pair     = λfirst.λsecond.λfunc.((func first) second)

They looked like a curiosity.

This unit cashes them in.

Nothing is imported

No primitive booleans.

No primitive integers.

Everything here is a λ expression you can expand and reduce.

These representations are untyped. Typed versions come later in the book, outside this module.

From pure functions to things worth computing

The plan

• truth values — the two selectors, unchanged
• the conditional — because choosing a branch is selecting an argument
• NOT, AND, OR — short definitions on top of the conditional
• the natural numbers — built inductively from zero and succ

Truth values and the conditional

Why selectors?

<condition> ? <expression> : <expression>

max = x>y?x:y

A truth value’s whole job is to choose between two alternatives.

That is what a selector does.

The conditional function

def cond = λe1.λe2.λc.((c e1) e2)

((cond <expression1>) <expression2>) ==
((λe1.λe2.λc.((c e1) e2) <expression1>) <expression2>) =>
(λe2.λc.((c <expression1>) e2) <expression2>) =>
λc.((c <expression1>) <expression2>)

Then hand it a selector

(λc.((c <e1>) <e2>)
   select_first) =>
((select_first <e1>) <e2>)
=> ... =>
<e1>

(λc.((c <e1>) <e2>)
   select_second) =>
((select_second <e1>) <e2>)
=> ... =>
<e2>

The condition is the last argument, not the first.

Name them

def true  = select_first
def false = select_second

In most languages if is a control structure and booleans are a primitive type.

Here both are ordinary functions.

The boolean operators

NOT

X	NOT X
FALSE	TRUE
TRUE	FALSE

As a conditional: X ? FALSE : TRUE

def not = λx.(((cond false) true) x)

Simplify the body

((cond false) true) x) ==
((λe1.λe2.λc.((c e1) e2) false) true) x) =>
((λe2.λc.((c false) e2) true) x) =>
(λc.((c false) true) x) =>
((x false) true)

def not = λx.((x false) true)

Check both rows

(not true) ==
(λx.((x false) true) true) =>
((true false) true) ==
((λfirst.λsecond.first false) true) =>
(λsecond.false true) =>
false

(not false) ==
(λx.((x false) true) false) =>
((false false) true) ==
((λfirst.λsecond.second false) true) =>
(λsecond.second true) =>
true

AND

X	Y	X AND Y
FALSE	FALSE	FALSE
FALSE	TRUE	FALSE
TRUE	FALSE	FALSE
TRUE	TRUE	TRUE

X ? Y : FALSE gives def and = λx.λy.((x y) false)

AND, reduced

((and true) false) ==
((λx.λy.((x y) false) true) false) =>
(λy.((true y) false) false) =>
((true false) false) ==
((λfirst.λsecond.first false) false) =>
(λsecond.false false) =>
false

OR

X	Y	X OR Y
FALSE	FALSE	FALSE
FALSE	TRUE	TRUE
TRUE	FALSE	TRUE
TRUE	TRUE	TRUE

X ? TRUE : Y gives def or = λx.λy.((x true) y)

Short-circuiting comes free

If and’s first operand is false, the second is never substituted anywhere.

So it is never evaluated.

Nothing in the definition asked for that.

In an imperative language, short-circuit evaluation is a special rule written into the language definition. Here it is a consequence of how selection works.

The natural numbers

Successors of zero

1 = successor of 0
2 = successor of 1  = successor of successor of 0
3 = successor of 2  = successor of successor of successor of 0

An arbitrary integer is that number of successors of zero.

The representation

def zero = identity
def succ = λn.λs.((s false) n)

Each succ builds a pair function with false first and the original number second.

Watch them nest

one ==
(succ zero) ==
(λn.λs.((s false) n) zero) =>
λs.((s false) zero)

two ==
(succ one) =>
λs.((s false) one) ==
λs.((s false) λs.((s false) zero))

A number is a structure. Its nesting depth is its value.

Testing for zero

For any \(\lambda s.((s\ false)\ \langle number\rangle)\), applying it to select_first gives false:

(λs.((s false) <number>) select_first) => ... => false

But zero is identity:

(zero select_first) ==
(λx.x select_first) =>
select_first == true

iszero

def iszero = λn.(n select_first)

Note the direction: the number is applied to the selector.

Numbers are functions with selector arguments.

The predecessor

select_second strips a layer:

(λs.((s false) <number>) select_second) => ... => <number>

def pred1 = λn.(n select_second)

But zero breaks it

(pred1 zero) ==
(λn.(n select_second) zero) =>
(zero select_second) ==
(λx.x select_second) =>
select_second == false

Not a representation of a number.

So check first

def pred = λn.(((cond zero) (pred1 n)) (iszero n))

Simplifying:

def pred = λn.(((iszero n) zero) (n select_second))

When we use pred we must be careful to check for a zero argument.

The pattern, again

Choose a representation so the operations become easy.

Then define them and verify by reduction.

Numbers being pairs is what makes pred possible at all.

Notation that keeps it readable

Dropping brackets

<function> <argument1> <argument2> ... <argumentN>

instead of

(...((<function> <argument1>) <argument2>) ... <argumentN>)

A function is applied first to the nearest argument on the right.

Two conditions stay

• if an argument is itself an application, its brackets stay
• there must be brackets round function body applications

def pred = λn.((iszero n) n (n select_second))

Note this returns n rather than zero in that branch. Both are correct — that branch is only reached when iszero n is true, and then n IS zero.

Shorter definitions

def <names> <name> = <expression>

def identity x = x
def self_apply s = s s
def apply func arg = func arg

Still removable. Always.

Summary

The library now

def cond   = λe1.λe2.λc.((c e1) e2)
def true   = select_first
def false  = select_second
def not    = λx.((x false) true)
def and    = λx.λy.((x y) false)
def or     = λx.λy.((x true) y)
def zero   = identity
def succ   = λn.λs.((s false) n)
def iszero = λn.(n select_first)
def pred   = λn.(((iszero n) zero) (n select_second))

What just happened

We started with a language containing only functions.

We now have booleans and integers.

Not simulated — built. Every definition expands to pure λ terms.

What is missing

succ and pred step by one.

No addition. No multiplication. No comparison.

Each needs to repeat an operation — and repetition needs recursion.

Where next

Recursion and Arithmetic closes the gap.

It turns out recursion is genuinely hard to get here: a definition mentioning its own name cannot work, because a name is an abbreviation that expands.

The way out is the paradoxical combinator.