Lecture notes — Conditions, Booleans and Integers

Published

2026-08-19 00:00

Keywords

ver. 1.0.1

Where we are

In Elements of Lambda Calculus you got the whole language: a grammar with three productions, and the conversions β, α and η. Nothing further is added to the language in this unit.

You also built two functions that looked like a curiosity — select_first and select_second — and a make_pair built from them.

This unit cashes that in. Those selectors become the truth values, and from there we get conditionals, boolean operators, and the natural numbers. Nothing is imported: there are no primitive booleans and no primitive integers hiding underneath.

The representations here are untyped. Typed representations of truth values, numbers and characters come later in the book, outside this module.

What you will be able to do

encode-truth-values-as-selectors — Encode true and false as the two argument-selection functions.
derive-the-conditional — Derive the conditional expression and show it reduces to the correct branch.
define-boolean-operators — Define NOT, AND and OR as λ functions and verify them by reduction.
encode-natural-numbers — Encode the natural numbers inductively using zero and a successor function.
define-number-predicates — Define iszero and pred, and take a number apart again.
use-simplified-notation — Use the chapter’s simplified bracketing and currying notation.

What we will cover

Truth values — true and false represented as select_first and select_second.
Conditional expression — cond, a version of make_pair where the condition is the selector.
Boolean operators — not, and and or, each built on the conditional.
Natural numbers — built inductively as successors of zero.
Successor and predecessor — succ wraps a number in a pair; pred strips a layer off.
Simplified notation — dropping redundant brackets and abbreviating definitions.

From pure functions to things worth computing

The claim in unit 1 was that data needs no separate mechanism. This unit makes it good.

Boolean logic is based on the truth values TRUE and FALSE with logical operations NOT, AND, OR and so on. We are going to represent TRUE by select_first and FALSE by select_second, and use a version of make_pair to build the logical operations.

Then numbers, built inductively from a chosen zero and a succ that wraps its argument.

Everything here is a λ expression you can expand and reduce. When a definition stops making sense, expanding it back to pure terms is how to find out why.

Learning outcomes

encode-truth-values-as-selectors: Encode true and false as the two argument-selection functions.
derive-the-conditional: Derive the conditional expression and show it reduces to the correct branch.

Truth values and the conditional

Why selectors are the right choice

Consider the C conditional expression:

<condition> ? <expression> : <expression>

If the condition is TRUE the first expression is selected for evaluation; if FALSE, the second. For example, to set max to the greater of x and y:

max = x>y?x:y

or to set absx to the absolute value of x:

absx = x<0?-x:x

A truth value’s whole job is to choose between two alternatives. That is exactly what a selector does. So the encoding writes itself.

The conditional function

We model the conditional using a version of make_pair:

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

Apply it to two arbitrary expressions:

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

Now apply that to select_first:

(λc.((c <expression1>) <expression2>) select_first) =>
((select_first <expression1>) <expression2>) => ... =>
<expression1>

and to select_second:

(λc.((c <expression1>) <expression2>) select_second) =>
((select_second <expression1>) <expression2>) => ... =>
<expression2>

The condition comes last

Notice that the condition is the last argument to cond, not the first. The two branches are supplied first, building a function that is then handed the condition to do the selecting.

With that working we can name the truth values:

def true = select_first
def false = select_second

In most languages if is a control structure the compiler treats specially, and booleans are a primitive type. Here both are ordinary functions, and it works because the representation was chosen to make it work. That technique is what the whole unit teaches.

Learning outcomes

encode-truth-values-as-selectors: Encode true and false as the two argument-selection functions.
derive-the-conditional: Derive the conditional expression and show it reduces to the correct branch.

Concepts

truth-values: represents TRUE and FALSE as the two selector functions
conditional-expression: builds cond from make_pair, with the condition as the selector

The boolean operators

Each operator is derived the same way: read the truth table, write it as a conditional expression, then simplify the body.

NOT

NOT is a unary operator, with truth table:

X	NOT X
FALSE	TRUE
TRUE	FALSE

If the operand is TRUE the answer is FALSE, and vice versa. So NOT could be written as the conditional X ? FALSE : TRUE, suggesting:

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

Simplifying the inner 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)

so we use:

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

Check it. NOT TRUE:

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

and NOT FALSE:

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

Both rows of the truth table.

AND

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

If the left operand is TRUE the value depends on the right operand; if FALSE the value is FALSE. As a conditional: X ? Y : FALSE.

def and = λx.λy.(((cond y) false) x)

Simplifying the inner body gives ((x y) false), so:

def and = λx.λy.((x y) false)

For TRUE AND FALSE:

((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

If the first operand is TRUE the value is TRUE; otherwise it is the second operand. As a conditional: X ? TRUE : Y.

def or = λx.λy.(((cond true) y) x)

Simplifying gives ((x true) y), so:

def or = λx.λy.((x true) y)

For FALSE OR TRUE:

((or false) true) ==
((λx.λy.((x true) y) false) true) =>
(λy.((false true) y) true) =>
((false true) true) => ... =>
true

Short-circuiting comes free

Look at and again. If the first operand is false, the selection returns false and the second operand is never substituted anywhere — so it is never evaluated.

Nothing in the definition asked for that. It falls out of how selection works. In an imperative language short-circuit evaluation is a special rule written into the language definition; here it is a consequence of the encoding.

Learning outcomes

define-boolean-operators: Define NOT, AND and OR as λ functions and verify them by reduction.
derive-the-conditional: Derive the conditional expression and show it reduces to the correct branch.

Concepts

boolean-operators: derives NOT, AND and OR from the conditional and verifies each against its truth table
conditional-expression: uses the conditional as the common shape behind all three operators

The natural numbers

We take numbers for granted in programming, but now we have to represent them explicitly.

Numbers as successors of zero

The approach defines the natural numbers — non-negative integers — as 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

So an arbitrary integer is that number of successors of zero. We need a function zero and a successor function succ so we can define:

def one   = (succ zero)
def two   = (succ one)
def three = (succ two)

There are several ways to represent these. We use:

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

Each time succ is applied to a number n, it builds a pair function with false first and the original number second:

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

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

and three is one layer deeper again. A number is a structure, and how deeply it nests is what makes it the number it is. No notion of quantity appears anywhere.

Testing for zero

A number is a function with an argument that may be used as a selector. For an arbitrary number $\lambda s.((s\ false)\ \langle number\rangle)$, setting the argument to select_first selects false:

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

But zero is the identity function, so applying it to select_first returns select_first — which is true by definition:

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

That difference is the test:

def iszero = λn.(n select_first)

The application is the other way round

iszero applies the number to the selector, not the selector to the number. That is because this representation models numbers as functions with selector arguments.

The predecessor

pred should strip off a layer of nesting from $\lambda s.((s\ false)\ \langle number\rangle)$ and return the number inside. select_second does exactly that:

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

So a first version:

def pred1 = λn.(n select_second)

There is a problem at zero, since we only have non-negative integers:

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

which is not a representation of a number at all. We define the predecessor of zero to be zero, checking first:

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

Simplifying the body:

((cond zero) (pred1 n)) (iszero n)) ==
((λe1.λe2.λc.((c e1) e2) zero) (pred1 n)) (iszero n)) =>
((λe2.λc.((c zero) e2) (pred1 n)) (iszero n)) =>
(λc.((c zero) (pred1 n)) (iszero n)) =>
(((iszero n) zero) (pred1 n))

and substituting for pred1:

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

Alternatively we might say the predecessor of zero is undefined; handling undefined values is not covered here. When we use pred we will have to be careful to check for a zero argument.

The pattern, again

This is the same technique as the booleans: choose a representation so the operations you need become easy, then define them and verify by reduction. Numbers being pairs is what makes pred possible at all — with a less careful encoding, going backwards is genuinely hard.

What is still missing is arithmetic. succ and pred step one at a time, and addition needs repetition.

Learning outcomes

encode-natural-numbers: Encode the natural numbers inductively using zero and a successor function.
define-number-predicates: Define iszero and pred, and take a number apart again.

Concepts

natural-numbers: defines numbers inductively as nested pairs built by succ from zero
truth-values: reuses the selectors to test and dismantle a number

Notation that keeps it readable

By now you will have noticed that manipulating λ expressions involves lots of brackets. As well as being tedious and fiddly, it is a major source of mistakes through unmatched or mismatched brackets.

Dropping brackets

For the application of a function to $N$ arguments we allow:

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

instead of:

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

So in an application, a function is applied first to the nearest argument on the right. Two conditions stay:

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

For example, pred can be rewritten:

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

Why n and not zero in that branch

The rewritten form returns n rather than zero where the earlier version returned zero. Both are correct: that branch is only reached when iszero n is true, and then n is zero.

Abbreviating definitions

Definitions themselves get shorter. Instead of

def <names> = λ<name>.<expression>

we may write

def <names> <name> = <expression>

so the library from unit 2 becomes:

def identity x = x
def self_apply s = s s
def apply func = λarg.(func arg)

and apply may be shortened further, moving both parameters to the left:

def apply func arg = func arg

Keep the discipline from unit 2: the sugar is always removable. When a derivation in the next unit stops making sense, expanding back to pure terms is how to find out why.

Learning outcomes

use-simplified-notation: Use the chapter’s simplified bracketing and currying notation.

Concepts

syntactic-sugar: introduces bracket-dropping and shorter definition forms that expand back to pure λ terms

What you can now build

Looking back over the unit, here is the library you now have on top of unit 2’s:

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))

We started this module with a language containing only functions, and we now have booleans and integers. Not simulated — built, from three grammar productions and three conversion rules, with every definition expandable to pure λ terms.

One thing is conspicuously missing. We have succ and pred, which step by one, but no addition, no multiplication, no comparison. Each needs to repeat an operation a number of times, and repetition needs recursion.

Learning outcomes

encode-truth-values-as-selectors: Encode true and false as the two argument-selection functions.
derive-the-conditional: Derive the conditional expression and show it reduces to the correct branch.
define-boolean-operators: Define NOT, AND and OR as λ functions and verify them by reduction.
encode-natural-numbers: Encode the natural numbers inductively using zero and a successor function.
define-number-predicates: Define iszero and pred, and take a number apart again.
use-simplified-notation: Use the chapter’s simplified bracketing and currying notation.

Concepts

natural-numbers: collects the number representation and its operations
boolean-operators: collects the logical operations built on the conditional

Conclusion

Truth values are modelled directly as selector functions.

A truth value’s job is to pick between two alternatives, and that is what a selector does. Choosing that representation is what makes the conditional expression nearly derive itself.
The conditional is an ordinary function, not a control structure.

cond is a version of make_pair whose last argument is the condition. Everything else in the unit — not, and, or, pred — is built on it.
Natural numbers are modelled inductively as structured pairs.

zero is identity; succ n wraps n in a pair with false first. A number is a structure whose nesting depth is its value, with no notion of quantity anywhere.
The representation is chosen so the operations become easy.

iszero works because zero alone returns its selector unchanged. pred works because a number’s second component is the number it wrapped. Neither would be simple under a careless encoding.
Syntactic sugar bridges pure λ terms and readable definitions.

Dropping redundant brackets and shortening definitions changes nothing about meaning. Every abbreviation can be expanded back, which is the check to run whenever a derivation confuses you.

Where next

The next unit, Recursion and Arithmetic, closes the gap. It discovers that recursion is genuinely hard to obtain here — a definition that mentions its own name cannot work, because a name is an abbreviation that expands. The way out is the paradoxical combinator, and once it exists the arithmetic follows quickly.

← Conditions, Booleans and Integers Recursion and Arithmetic →

--- title: Lecture notes — Conditions, Booleans and Integers keywords: - ver. 1.0.1 date: '2026-08-19' --- [← Conditions, Booleans and Integers](index.qmd){.hg-back} ## Where we are In **Elements of Lambda Calculus** you got the whole language: a grammar with three productions, and the conversions β, α and η. Nothing further is added to the language in this unit. You also built two functions that looked like a curiosity — `select_first` and `select_second` — and a `make_pair` built from them. This unit cashes that in. Those selectors become the truth values, and from there we get conditionals, boolean operators, and the natural numbers. Nothing is imported: there are no primitive booleans and no primitive integers hiding underneath. ::: {.column-margin} The representations here are **untyped**. Typed representations of truth values, numbers and characters come later in the book, outside this module. ::: ## What you will be able to do 1. `encode-truth-values-as-selectors` — Encode true and false as the two argument-selection functions. 2. `derive-the-conditional` — Derive the conditional expression and show it reduces to the correct branch. 3. `define-boolean-operators` — Define NOT, AND and OR as λ functions and verify them by reduction. 4. `encode-natural-numbers` — Encode the natural numbers inductively using zero and a successor function. 5. `define-number-predicates` — Define iszero and pred, and take a number apart again. 6. `use-simplified-notation` — Use the chapter's simplified bracketing and currying notation. ## What we will cover - **Truth values** — `true` and `false` represented as `select_first` and `select_second`. - **Conditional expression** — `cond`, a version of `make_pair` where the condition is the selector. - **Boolean operators** — `not`, `and` and `or`, each built on the conditional. - **Natural numbers** — built inductively as successors of `zero`. - **Successor and predecessor** — `succ` wraps a number in a pair; `pred` strips a layer off. - **Simplified notation** — dropping redundant brackets and abbreviating definitions. ## From pure functions to things worth computing The claim in unit 1 was that data needs no separate mechanism. This unit makes it good. Boolean logic is based on the truth values `TRUE` and `FALSE` with logical operations `NOT`, `AND`, `OR` and so on. We are going to represent `TRUE` by `select_first` and `FALSE` by `select_second`, and use a version of `make_pair` to build the logical operations. Then numbers, built inductively from a chosen `zero` and a `succ` that wraps its argument. Everything here is a λ expression you can expand and reduce. When a definition stops making sense, expanding it back to pure terms is how to find out why. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "encode-truth-values-as-selectors" >}}: Encode true and false as the two argument-selection functions. - {{< badge outcome "derive-the-conditional" >}}: Derive the conditional expression and show it reduces to the correct branch. ::: ## Truth values and the conditional ### Why selectors are the right choice Consider the C conditional expression: ```text <condition> ? <expression> : <expression> ``` If the condition is `TRUE` the first expression is selected for evaluation; if `FALSE`, the second. For example, to set `max` to the greater of `x` and `y`: ```text max = x>y?x:y ``` or to set `absx` to the absolute value of `x`: ```text absx = x<0?-x:x ``` [A truth value's whole job is to choose between two alternatives.]{.hg-key} That is exactly what a selector does. So the encoding writes itself. ### The conditional function We model the conditional using a version of `make_pair`: ```text def cond = λe1.λe2.λc.((c e1) e2) ``` Apply it to two arbitrary expressions: ```text ((cond <expression1>) <expression2>) == ((λe1.λe2.λc.((c e1) e2) <expression1>) <expression2>) => (λe2.λc.((c <expression1>) e2) <expression2>) => λc.((c <expression1>) <expression2>) ``` Now apply that to `select_first`: ```text (λc.((c <expression1>) <expression2>) select_first) => ((select_first <expression1>) <expression2>) => ... => <expression1> ``` and to `select_second`: ```text (λc.((c <expression1>) <expression2>) select_second) => ((select_second <expression1>) <expression2>) => ... => <expression2> ``` ::: {.callout-important title="The condition comes last"} Notice that the condition is the **last** argument to `cond`, not the first. The two branches are supplied first, building a function that is then handed the condition to do the selecting. ::: With that working we can name the truth values: ```text def true = select_first def false = select_second ``` In most languages `if` is a control structure the compiler treats specially, and booleans are a primitive type. Here both are ordinary functions, and it works because the *representation was chosen to make it work*. That technique is what the whole unit teaches. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "encode-truth-values-as-selectors" >}}: Encode true and false as the two argument-selection functions. - {{< badge outcome "derive-the-conditional" >}}: Derive the conditional expression and show it reduces to the correct branch. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "truth-values" >}}: represents TRUE and FALSE as the two selector functions - {{< badge concept "conditional-expression" >}}: builds cond from make_pair, with the condition as the selector ::: ## The boolean operators Each operator is derived the same way: read the truth table, write it as a conditional expression, then simplify the body. ### NOT `NOT` is a unary operator, with truth table: | X | NOT X | |---|---| | FALSE | TRUE | | TRUE | FALSE | If the operand is `TRUE` the answer is `FALSE`, and vice versa. So `NOT` could be written as the conditional `X ? FALSE : TRUE`, suggesting: ```text def not = λx.(((cond false) true) x) ``` Simplifying the inner body: ```text ((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) ``` so we use: ```text def not = λx.((x false) true) ``` Check it. `NOT TRUE`: ```text (not true) == (λx.((x false) true) true) => ((true false) true) == ((λfirst.λsecond.first false) true) => (λsecond.false true) => false ``` and `NOT FALSE`: ```text (not false) == (λx.((x false) true) false) => ((false false) true) == ((λfirst.λsecond.second false) true) => (λsecond.second true) => true ``` Both rows of the truth table. ### AND | X | Y | X AND Y | |---|---|---| | FALSE | FALSE | FALSE | | FALSE | TRUE | FALSE | | TRUE | FALSE | FALSE | | TRUE | TRUE | TRUE | If the left operand is `TRUE` the value depends on the right operand; if `FALSE` the value is `FALSE`. As a conditional: `X ? Y : FALSE`. ```text def and = λx.λy.(((cond y) false) x) ``` Simplifying the inner body gives `((x y) false)`, so: ```text def and = λx.λy.((x y) false) ``` For `TRUE AND FALSE`: ```text ((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 | If the first operand is `TRUE` the value is `TRUE`; otherwise it is the second operand. As a conditional: `X ? TRUE : Y`. ```text def or = λx.λy.(((cond true) y) x) ``` Simplifying gives `((x true) y)`, so: ```text def or = λx.λy.((x true) y) ``` For `FALSE OR TRUE`: ```text ((or false) true) == ((λx.λy.((x true) y) false) true) => (λy.((false true) y) true) => ((false true) true) => ... => true ``` ::: {.callout-tip title="Short-circuiting comes free"} Look at `and` again. If the first operand is `false`, the selection returns `false` and the second operand is never substituted anywhere — so it is never evaluated. Nothing in the definition asked for that. It falls out of how selection works. In an imperative language short-circuit evaluation is a special rule written into the language definition; here it is a consequence of the encoding. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "define-boolean-operators" >}}: Define NOT, AND and OR as λ functions and verify them by reduction. - {{< badge outcome "derive-the-conditional" >}}: Derive the conditional expression and show it reduces to the correct branch. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "boolean-operators" >}}: derives NOT, AND and OR from the conditional and verifies each against its truth table - {{< badge concept "conditional-expression" >}}: uses the conditional as the common shape behind all three operators ::: ## The natural numbers We take numbers for granted in programming, but now we have to represent them explicitly. ### Numbers as successors of zero The approach defines the natural numbers — non-negative integers — as successors of zero: ```text 1 = successor of 0 2 = successor of 1 = successor of successor of 0 3 = successor of 2 = successor of successor of successor of 0 ``` So an arbitrary integer is *that number of successors of zero*. We need a function `zero` and a successor function `succ` so we can define: ```text def one = (succ zero) def two = (succ one) def three = (succ two) ``` There are several ways to represent these. We use: ```text def zero = identity def succ = λn.λs.((s false) n) ``` Each time `succ` is applied to a number `n`, it builds a **pair function** with `false` first and the original number second: ```text one == (succ zero) == (λn.λs.((s false) n) zero) => λs.((s false) zero) ``` ```text two == (succ one) == (λn.λs.((s false) n) one) => λs.((s false) one) == λs.((s false) λs.((s false) zero)) ``` and `three` is one layer deeper again. A number *is* a structure, and how deeply it nests is what makes it the number it is. No notion of quantity appears anywhere. ### Testing for zero A number is a function with an argument that may be used as a selector. For an arbitrary number $\lambda s.((s\ false)\ \langle number\rangle)$, setting the argument to `select_first` selects `false`: ```text (λs.((s false) <number>) select_first) => ((select_first false) <number>) == ((λfirst.λsecond.first false) <number>) => (λsecond.false <number>) => false ``` But `zero` is the identity function, so applying it to `select_first` returns `select_first` — which is `true` by definition: ```text (zero select_first) == (λx.x select_first) => select_first == true ``` That difference is the test: ```text def iszero = λn.(n select_first) ``` ::: {.callout-note title="The application is the other way round"} `iszero` applies the **number to the selector**, not the selector to the number. That is because this representation models numbers as functions with selector arguments. ::: ### The predecessor `pred` should strip off a layer of nesting from $\lambda s.((s\ false)\ \langle number\rangle)$ and return the number inside. `select_second` does exactly that: ```text (λs.((s false) <number>) select_second) => ((select_second false) <number>) == ((λfirst.λsecond.second false) <number>) => (λsecond.second <number>) => <number> ``` So a first version: ```text def pred1 = λn.(n select_second) ``` There is a problem at zero, since we only have non-negative integers: ```text (pred1 zero) == (λn.(n select_second) zero) => (zero select_second) == (λx.x select_second) => select_second == false ``` which is not a representation of a number at all. We define the predecessor of zero to be zero, checking first: ```text def pred = λn.(((cond zero) (pred1 n)) (iszero n)) ``` Simplifying the body: ```text ((cond zero) (pred1 n)) (iszero n)) == ((λe1.λe2.λc.((c e1) e2) zero) (pred1 n)) (iszero n)) => ((λe2.λc.((c zero) e2) (pred1 n)) (iszero n)) => (λc.((c zero) (pred1 n)) (iszero n)) => (((iszero n) zero) (pred1 n)) ``` and substituting for `pred1`: ```text def pred = λn.(((iszero n) zero) (n select_second)) ``` Alternatively we might say the predecessor of zero is undefined; handling undefined values is not covered here. **When we use `pred` we will have to be careful to check for a zero argument.** ::: {.callout-note title="The pattern, again"} This is the same technique as the booleans: choose a representation so the operations you need become easy, then define them and verify by reduction. Numbers being pairs is what makes `pred` possible at all — with a less careful encoding, going backwards is genuinely hard. ::: What is still missing is arithmetic. `succ` and `pred` step one at a time, and addition needs repetition. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "encode-natural-numbers" >}}: Encode the natural numbers inductively using zero and a successor function. - {{< badge outcome "define-number-predicates" >}}: Define iszero and pred, and take a number apart again. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "natural-numbers" >}}: defines numbers inductively as nested pairs built by succ from zero - {{< badge concept "truth-values" >}}: reuses the selectors to test and dismantle a number ::: ## Notation that keeps it readable By now you will have noticed that manipulating λ expressions involves lots of brackets. As well as being tedious and fiddly, it is a major source of mistakes through unmatched or mismatched brackets. ### Dropping brackets For the application of a function to $N$ arguments we allow: ```text <function> <argument1> <argument2> ... <argumentN> ``` instead of: ```text (...((<function> <argument1>) <argument2>) ... <argumentN>) ``` So in an application, a function is applied first to the nearest argument on the right. Two conditions stay: - if an argument is itself a function application, its **brackets must stay** - there must be **brackets round function body applications** For example, `pred` can be rewritten: ```text def pred = λn.((iszero n) n (n select_second)) ``` ::: {.callout-tip title="Why `n` and not `zero` in that branch"} The rewritten form returns `n` rather than `zero` where the earlier version returned `zero`. Both are correct: that branch is only reached when `iszero n` is true, and then `n` **is** `zero`. ::: ### Abbreviating definitions Definitions themselves get shorter. Instead of ```text def <names> = λ<name>.<expression> ``` we may write ```text def <names> <name> = <expression> ``` so the library from unit 2 becomes: ```text def identity x = x def self_apply s = s s def apply func = λarg.(func arg) ``` and `apply` may be shortened further, moving both parameters to the left: ```text def apply func arg = func arg ``` Keep the discipline from unit 2: the sugar is always removable. When a derivation in the next unit stops making sense, expanding back to pure terms is how to find out why. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "use-simplified-notation" >}}: Use the chapter's simplified bracketing and currying notation. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "syntactic-sugar" >}}: introduces bracket-dropping and shorter definition forms that expand back to pure λ terms ::: ## What you can now build Looking back over the unit, here is the library you now have on top of unit 2's: ```text 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)) ``` We started this module with a language containing only functions, and we now have booleans and integers. Not simulated — **built**, from three grammar productions and three conversion rules, with every definition expandable to pure λ terms. One thing is conspicuously missing. We have `succ` and `pred`, which step by one, but no addition, no multiplication, no comparison. Each needs to repeat an operation a number of times, and repetition needs recursion. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "encode-truth-values-as-selectors" >}}: Encode true and false as the two argument-selection functions. - {{< badge outcome "derive-the-conditional" >}}: Derive the conditional expression and show it reduces to the correct branch. - {{< badge outcome "define-boolean-operators" >}}: Define NOT, AND and OR as λ functions and verify them by reduction. - {{< badge outcome "encode-natural-numbers" >}}: Encode the natural numbers inductively using zero and a successor function. - {{< badge outcome "define-number-predicates" >}}: Define iszero and pred, and take a number apart again. - {{< badge outcome "use-simplified-notation" >}}: Use the chapter's simplified bracketing and currying notation. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "natural-numbers" >}}: collects the number representation and its operations - {{< badge concept "boolean-operators" >}}: collects the logical operations built on the conditional ::: ## Conclusion - Truth values are modelled directly as selector functions. > A truth value's job is to pick between two alternatives, and that is what a selector does. Choosing that representation is what makes the conditional expression nearly derive itself. - The conditional is an ordinary function, not a control structure. > `cond` is a version of `make_pair` whose last argument is the condition. Everything else in the unit — `not`, `and`, `or`, `pred` — is built on it. - Natural numbers are modelled inductively as structured pairs. > `zero` is `identity`; `succ n` wraps `n` in a pair with `false` first. A number is a structure whose nesting depth *is* its value, with no notion of quantity anywhere. - The representation is chosen so the operations become easy. > `iszero` works because `zero` alone returns its selector unchanged. `pred` works because a number's second component is the number it wrapped. Neither would be simple under a careless encoding. - Syntactic sugar bridges pure λ terms and readable definitions. > Dropping redundant brackets and shortening definitions changes nothing about meaning. Every abbreviation can be expanded back, which is the check to run whenever a derivation confuses you. ### Where next The next unit, **Recursion and Arithmetic**, closes the gap. It discovers that recursion is genuinely hard to obtain here — a definition that mentions its own name cannot work, because a name is an abbreviation that expands. The way out is the paradoxical combinator, and once it exists the arithmetic follows quickly. ::: {.hg-nav} [← Conditions, Booleans and Integers](index.qmd){.hg-prev} [Recursion and Arithmetic →](../4_recursion_and_arithmetic/index.qmd){.hg-next} :::