Bridge to Encodings

Can a pattern choose? Can it count? The encoding principle.

8 topics • ~1505 words

For four topics, the compositor has been setting type mechanically. Pick up a stick, find the tagged blanks, press in the type pieces, repeat. The results are always more sticks — sometimes simpler, sometimes identical, sometimes looping endlessly. But always just sticks and type pieces. No numbers on the type. No labels saying "true" or "false." Just... patterns, rearranging themselves.

And yet something is hiding in the patterns.

We have learned the entire mechanics of lambda calculus: terms, variables, binding, substitution, beta reduction, currying, normal forms, reduction strategies, divergence, eta reduction. That is everything. There are no more rules to learn. But so far, every result has been another lambda term — we have never seen anything that looks like data. No booleans, no numbers, no choices. Can patterns made of nothing but substitution actually do something?

Patterns So Far

Lambda calculus has exactly three term forms (variables, abstractions, applications) and one computation rule (beta reduction). With these tools, we can:

Substitute — replace variables with terms
Reduce — apply abstractions to arguments
Diverge — create terms that never reach normal form
Curry — handle multiple arguments one at a time

But we have not seen anything resembling data. Every result is another lambda term. There are no built-in booleans, numbers, or data structures.

Behavior from Structure

A composing stick with two tagged blanks, x and y, whose body is just x. No matter what type pieces you press in, the stick always keeps the first and discards the second. That is not an accident. That is a pattern doing something predictable.

Consider the term λx.λy.x. We have seen it in the currying topic. Applied to two arguments:

(λx.λy.x) a b →β (λy.a) b →β a

It always returns the first argument. This is not a special case — it happens for any choice of a and b. The structure of the term determines its behavior: the body is x, which is bound to the first argument, so the second argument is always discarded.

Consistent Behavior

The compositor has set type with this stick hundreds of times. Different type pieces every time — ornate capitals, plain letters, foreign characters. The stick does not care. It always keeps the first piece and discards the second. That is not the stick being simple. That is the stick being reliable.

A term exhibits consistent behavior when its output follows the same pattern for all possible inputs. λx.λy.x always returns its first argument — whether the arguments are simple variables, complex expressions, or even other abstractions.

This consistency is not fragile or coincidental. It is guaranteed by the structure of the term itself. The body is x, which is always bound to the first argument. No input can change this.

When a pattern behaves the same way regardless of input, we might say it has a character — a stable identity defined by what it does, not by what it is made of.

Can a Pattern Choose?

Two sticks sit side by side on the bench. Same shape — two tagged blanks each. But one has its body wired to the first blank, and the other to the second. Give them both the same pair of type pieces, and they produce different results. Not because they received different instructions. Because they are different instructions.

Consider these two terms side by side:

λx.λy.x — always returns the first of two arguments
λx.λy.y — always returns the second of two arguments

Applied to the same arguments a and b:

(λx.λy.x) a b →β a (λx.λy.y) a b →β b

The two terms make opposite selections. This is not a coincidence — it is structurally determined and holds for all inputs. One term selects the first option; the other selects the second. Together, they embody a binary choice without any built-in notion of choosing.

Selectors Are Functions

Set the type and see what the stick keeps. Two blanks, two pieces. The stick does the rest.

A selector is a term that takes two arguments and returns one of them. We have seen two selectors:

λx.λy.x — selects the first argument
λx.λy.y — selects the second argument

To see selection in action, reduce:

(λx.λy.x) a b →β (λy.a) b →β a

Two steps. The first argument is returned.

Behavior Is Identity

Two composing sticks, built at different times from different type metal. One is old and worn; the other is freshly cast. But set any pair of type pieces, and both sticks produce the same printed output. The compositor does not care about the metal. The compositor cares about what appears on the page.

Two terms are behaviorally equivalent if they produce the same output for every possible input. We already know one version of this: alpha equivalence says λx.λy.x and λa.λb.a are the same term because renaming bound variables does not change behavior.

But the principle runs deeper. If two terms with genuinely different internal structure always produce the same results when applied to the same arguments, then from the outside — from the perspective of anything that uses them — they are indistinguishable.

This leads to a powerful idea: a term's identity is not its syntax, not its variable names, not its internal structure. Its identity is its behavior — what it does when you use it.

The Encoding Principle

The compositor stares at the two sticks. One keeps the first piece. The other keeps the second. Nobody built "choosing" into the workshop. Nobody added a special mechanism for selection. The sticks are made of the same material as every other stick — blanks, tags, type metal. And yet they choose. The behavior was not added. It was already there, waiting to be noticed.

The encoding principle: a lambda term's identity is constituted by its behavior. A term is what it does.

This is not a definition we impose from outside. It follows from what we have already seen:

λx.λy.x reliably selects the first of two arguments
λx.λy.y reliably selects the second
Their behavior is consistent, universal, and structurally guaranteed
Two terms with identical behavior are the same in every way that matters

The encoding principle says: if a lambda term behaves like a boolean, a number, or a data structure, then it is one. No external labels or type annotations needed. Behavior alone is sufficient to constitute identity.

We do not need to add data to lambda calculus. We need to recognize the data that is already there.

What Comes Next?

The compositor looks around the workshop with new eyes. These sticks are not inert. They select, they discard, they repeat. The workshop has been full of logic and arithmetic this whole time — hidden in the grain of the type metal, waiting for someone to notice. What else is in here?

We now know that:

Lambda terms can exhibit consistent, reliable behavior
Two terms can make opposite selections (first vs second argument)
Behavior constitutes identity — a term IS what it does
No external data, types, or labels are needed

Selection is just the beginning. If a pattern can choose between two options, might other patterns be able to count? To pair values together? To repeat an operation? The mechanics we learned in Topics 00-04 are not just symbolic manipulation — they are the raw material from which all of computation can be built.

Next, we will discover that specific lambda terms already behave as booleans, numbers, and data structures — not by convention, but by the encoding principle.

Ready to test your understanding?

Bitwit uses spaced repetition to help you truly master concepts like this—not just read about them. Each card generates with different values, so you can't just memorize answers.

Practice Bridge to Encodings →