Lambda Calculus: Logic & Pairs

This page explains how booleans and pairs can be represented using only functions. To make the ideas intuitive, we first compare them with how Python handles the same concepts.

1. What the λ‑Calculus Is

The λ‑calculus is a tiny mathematical model of computation. It has only:

Variables — names like x, y
Functions — written as λx. M
Application — applying one expression to another

The main evaluation rule is:

(λx. M) N   →   M with x replaced by N

Unlike Python, the λ‑calculus has no built‑in booleans, numbers, lists, or pairs. So we must build everything using functions.

2. How Python Represents Booleans and Pairs

Booleans in Python

True
False

If‑statements in Python

if condition:
    X
else:
    Y

Pairs in Python

pair = (10, 20)
first = pair[0]
second = pair[1]

Python has built‑in data types. The λ‑calculus does not — so we must encode these ideas using functions.

3. Why Booleans Can Be Functions

To understand the encoding, think about what booleans do in Python.

True means “choose the first option”
False means “choose the second option”

Example:

if True:
    print("A")
else:
    print("B")

This prints A — the first option.

So in the λ‑calculus, we represent booleans as functions that choose between two values.

Boolean Encodings

true  ≡ λa b. a     ; choose the first
false ≡ λa b. b     ; choose the second

This means:

true  X Y   →   X
false X Y   →   Y

Now the definition of if becomes natural.

How “if” Works

An if‑statement simply applies the boolean to the two branches:

if ≡ λp x y. p x y

Here:

p is a boolean function (true or false)
x is the “then” value
y is the “else” value

Example

if true 10 20
→ true 10 20
→ 10

4. Why Pairs Can Be Functions

A pair in Python is a container holding two values:

(A, B)

But the λ‑calculus has no containers. So we ask: what does a pair actually do?

A pair gives two values to something that wants them.

So we encode a pair as a function that takes a “selector” function.

Pair Constructor

pair ≡ λx y f. f x y

This means:

The pair stores x and y
When given a function f, it calls f x y

Selectors

fst ≡ λp. p (λa b. a)
snd ≡ λp. p (λa b. b)

These work because:

λa b. a returns the first argument
λa b. b returns the second argument

Example: Storing Simple Data

Let’s store two numbers:

myPair = pair 5 8

Extract the first value:

fst myPair
→ 5

Extract the second value:

snd myPair
→ 8

Representing Logic & Pairs in the λ‑Calculus