Pairs

What Is a Pair

A pair in lambda calculus is a function that holds two values and waits for a selector to choose between them.

Given values a and b, a pair packages them into a single term. When you hand the pair a selector:

• TRUE selects the first value
• FALSE selects the second value

The pair does not know which value you want until you provide the selector. It simply holds both and waits.

PAIR Definition

The PAIR constructor takes two values and produces a function that waits for a selector:

PAIR = λa.λb.λs. s a b

Read it in stages:

1. λa. -- take the first value
2. λb. -- take the second value
3. λs. s a b -- return a function that waits for a selector s, then applies s to both stored values

The result of PAIR a b is λs. s a b -- a closed-over function that remembers a and b and will hand them to whatever selector it receives.

PAIR Holds Values

When we apply PAIR to two values, we get a function that holds them:

PAIR a b = (λa.λb.λs. s a b) a b →β λs. s a b

The result λs. s a b is the pair itself. It is a function of one argument -- the selector s. When called with a selector, it applies s to both stored values.

Crucially, the pair does not return a or b on its own. It waits for s and then evaluates s a b, letting the selector decide which value to keep.

FST Definition

To extract the first element from a pair, we need to hand it the "pick first" selector. That selector is TRUE (λx.λy.x).

FST = λp. p TRUE

FST takes a pair p and applies it to TRUE. Since a pair is λs. s a b, this becomes:

(λs. s a b) TRUE →β TRUE a b →β a

TRUE selects the first of two arguments, so the pair yields a. FST does not inspect the pair or know what is inside it -- it simply hands the pair the right selector and lets the mechanism work.

SND Definition

To extract the second element from a pair, hand it the "pick second" selector. That selector is FALSE (λx.λy.y).

SND = λp. p FALSE

SND takes a pair p and applies it to FALSE. Since a pair is λs. s a b, this becomes:

(λs. s a b) FALSE →β FALSE a b →β b

FALSE selects the second of two arguments, so the pair yields b. The symmetry with FST is exact: same mechanism, different selector.

FST of a PAIR

Putting FST and PAIR together:

FST (PAIR a b)

Step 1 -- construct the pair: PAIR a b →β λs. s a b

Step 2 -- apply FST: FST (λs. s a b) = (λp. p TRUE)(λs. s a b) →β (λs. s a b) TRUE

Step 3 -- the pair receives the selector: (λs. s a b) TRUE →β TRUE a b

Step 4 -- TRUE selects the first: TRUE a b = (λx.λy.x) a b →β a

Result: a

SND of a PAIR

Putting SND and PAIR together:

SND (PAIR a b)

Step 1 -- construct the pair: PAIR a b →β λs. s a b

Step 2 -- apply SND: SND (λs. s a b) = (λp. p FALSE)(λs. s a b) →β (λs. s a b) FALSE

Step 3 -- the pair receives the selector: (λs. s a b) FALSE →β FALSE a b

Step 4 -- FALSE selects the second: FALSE a b = (λx.λy.y) a b →β b

Result: b

Booleans Reused

FST and SND are strikingly simple:

• FST = λp. p TRUE
• SND = λp. p FALSE

They reuse Church booleans -- the same TRUE and FALSE from Topic 05. This is not a coincidence. TRUE (λx.λy.x) selects the first of two arguments. FALSE (λx.λy.y) selects the second. A pair λs. s a b presents two values to a selector.

The connection: a pair is a function that offers two choices, and a boolean is a function that makes a choice. They were designed for each other -- or rather, neither was designed at all. The pattern just fits.

A Pair Is a Closure

When we write PAIR a b, the result is λs. s a b. The values a and b appear free inside the body, but they are "captured" from the surrounding application. The function λs. s a b carries a and b with it wherever it goes.

This is a closure -- a function bundled with the values it references from its enclosing scope. In most programming languages, closures are a feature that must be implemented. In lambda calculus, every function is already a closure. Substitution is the mechanism: when PAIR receives a and b, substitution places them directly into the body, and they stay there.

A pair does not have a special storage mechanism. It is just a function that, through substitution, happens to carry data.

Nested Pairs

Since a pair is just a lambda term, it can hold anything -- including other pairs. There is no restriction on what values go into a pair.

Consider: PAIR (PAIR a b) c

The first element is itself a pair: PAIR a b = λs. s a b. The second element is c. The outer pair packages them both:

λs. s (λs. s a b) c

Applying FST extracts the first element -- which is the inner pair, not a:

FST (PAIR (PAIR a b) c) → PAIR a b

To get a, you would need a second FST: FST (FST (PAIR (PAIR a b) c)). Each FST peels off one layer.