Church Encodings

A Church encoding represents a piece of data as a lambda term whose reduction behavior mimics that data's intended use, rather than storing the data in any literal sense. The technique is named for Alonzo Church, who introduced it while developing the lambda calculus as a foundation for logic and computability in the 1930s. The guiding principle is: define a value by what happens when you eliminate it — that is, by how it responds to being applied to other functions — not by what it "contains." Concretely, this means every encoded value is a function waiting for one or more arguments that represent "what to do" with the value it encodes. A Church boolean waits for two branches and picks one. A Church numeral waits for a function and a starting point, and applies the function repeatedly. A Church pair waits for a combining function and feeds it both components. In each case, the encoded value has no internal structure a runtime could "peek into" — the only way to interact with it is to apply it, triggering beta reduction, which is exactly how the underlying computation is expressed. This matters because it shows that the primitive vocabulary of the lambda calculus — variables, abstraction (`λx. e`), and application (`e1 e2`) — is already sufficient to express conditionals, arithmetic, and compound data, with no additional machinery. The lambda calculus with Church encodings is not merely a model of computation; it is a self-contained one, in the same sense that a Turing machine's tape and head are self-contained. Everything downstream — recursion via fixed-point combinators, typed encodings of algebraic data types, and even the semantics of `if` in real compilers — descends from this same idea of representing structure through elimination behavior.

We build the encodings in three layers: booleans and conditionals, natural numbers and arithmetic, and pairs. Each layer is verified by explicit beta-reduction traces, since "correctness" here means the term reduces to what we intend when applied the way we intend.

Booleans. We want two terms, `true` and `false`, such that a conditional expression can be built from ordinary application. Define: ``` true = λt. λf. t false = λt. λf. f ``` A Church boolean is a two-argument function that discards one argument and returns the other. The conditional `if b then M else N` is then simply: ``` IF = λb. λt. λf. b t f ``` Applying `IF` to `true`, `M`, `N` reduces: ``` IF true M N = (λb.λt.λf. b t f) true M N → true M N = (λt.λf. t) M N → M ``` and symmetrically `IF false M N` reduces to `N`. Logical connectives follow immediately: ``` AND = λp. λq. p q false OR = λp. λq. p true q NOT = λp. λt. λf. p f t ``` `AND p q` reduces to `q` when `p` is `true` (since `p q false → q`) and to `false` when `p` is `false` (since `p q false → false`), matching ordinary short-circuit `and`.

Natural numbers. A Church numeral `n` is encoded as a function that takes a function `f` (the "successor action") and a base case `x`, and applies `f` exactly `n` times to `x`: ``` 0 = λf. λx. x 1 = λf. λx. f x 2 = λf. λx. f (f x) 3 = λf. λx. f (f (f x)) n = λf. λx. f^n x ``` The successor function must turn an `n`-fold application into an `(n+1)`-fold one, by wrapping one more `f` around the result: ``` SUCC = λn. λf. λx. f (n f x) ``` Trace on `1`: ``` SUCC 1 = (λn.λf.λx. f (n f x)) (λf.λx. f x) → λf.λx. f ((λf.λx. f x) f x) → λf.λx. f (f x) = 2 ```

Addition composes the iteration counts: ``` PLUS = λm. λn. λf. λx. m f (n f x) ``` This applies `f` to `x` first `n` times (via `n f x`), then applies `f` an additional `m` times to that result — total `m + n` applications.

Multiplication composes the functions themselves, using `n`'s action-of-`f` as the new "step": ``` MULT = λm. λn. λf. m (n f) ``` Here `(n f)` is the function "apply `f`, `n` times"; applying that `m` times gives `f` applied `m·n` times.

Predecessor is the hard case (discussed below) and is built using pairs, which we introduce next.

Pairs. A Church pair packages two values `a` and `b` into a function that, when given a selector `s`, hands both values to `s`: ``` PAIR = λa. λb. λs. s a b FST = λp. p (λa. λb. a) = p true SND = λp. p (λa. λb. b) = p false ``` Note `FST` and `SND` are exactly `true` and `false` applied as selectors — a pair is "asking" its selector which component to return, and `true`/`false` are precisely the functions that make that choice. Trace: ``` FST (PAIR M N) = (PAIR M N) (λa.λb. a) = (λs. s M N) (λa.λb. a) → (λa.λb. a) M N → (λb. M) N → M ```

Predecessor via pairs. To compute `PRED n`, we cannot simply "strip one `f`" directly, because a Church numeral only knows how to apply `f` repeatedly forward — it has no way to "undo" an application. The standard trick (due to Kleene) is to iterate a pair-shifting step `n` times, starting from `(0, 0)`, where each step moves the second component into the first and increments the second: ``` SHIFT = λp. PAIR (SND p) (SUCC (SND p)) PRED = λn. FST (n SHIFT (PAIR 0 0)) ``` Starting pair `(0, 0)`, after one `SHIFT` we get `(0, 1)`, after two, `(1, 2)`, after three, `(2, 3)` — so after `n` shifts, the pair is `(n-1, n)`, and taking `FST` yields `n - 1`. For `n = 0`, `n SHIFT (PAIR 0 0)` applies `SHIFT` zero times, leaving `(0,0)`, so `PRED 0 = 0` (the conventional truncated-at-zero behavior). ```pseudocode // Full pseudocode summary of the encodings and their reductions define TRUE = λt f. t define FALSE = λt f. f define IF(b, M, N) = b M N // reduces to M if b=TRUE, N if b=FALSE define ZERO = λf x. x define SUCC(n) = λf x. f (n f x) // wraps one more application of f define PLUS(m, n) = λf x. m f (n f x) // total (m+n) applications of f define MULT(m, n) = λf. m (n f) // total (m*n) applications of f define PAIR(a, b) = λs. s a b define FST(p) = p TRUE define SND(p) = p FALSE define SHIFT(p) = PAIR(SND(p), SUCC(SND(p))) define PRED(n) = FST( n SHIFT (PAIR(ZERO, ZERO)) ) define ISZERO(n) = n (λx. FALSE) TRUE // apply "always FALSE" n times to TRUE ``` `ISZERO` works because if `n = 0`, the function `λx. FALSE` is applied zero times, leaving `TRUE` unchanged; if `n ≥ 1`, it is applied at least once, producing `FALSE` and staying `FALSE` under further applications (since `(λx. FALSE) FALSE → FALSE`).

Correctness argument. Each encoding is correct in the sense that it satisfies the defining elimination law by beta-equivalence, verified by direct calculation rather than by appeal to any external semantics:

• For booleans, `IF true M N =β M` and `IF false M N =β N` — shown above by explicit reduction, and these two equations are the specification of a boolean.
• For numerals, we show by induction on `n` that `SUCC n =β (n+1)`. Base: `SUCC 0 = λf.λx. f(0 f x) = λf.λx. f x = 1`. Inductive step: assuming `n =β λf.λx. f^n x`, `SUCC n = λf.λx. f(n f x) →β λf.λx. f(f^n x) = λf.λx. f^{n+1} x = (n+1)`. This induction is exactly what justifies calling the family `{0, 1, 2, ...}` a faithful encoding of the naturals under the successor operation.
• `PLUS m n` unfolds to `λf.λx. m f (n f x)`. Since `n f x =β f^n x` and then `m f` applied to that gives `f^{m}(f^n x) = f^{m+n} x`, we get `PLUS m n =β (m+n)`, again by nested induction on `m` and `n`.
• `MULT m n = λf. m (n f)`. Here `n f` is beta-equivalent to the function `λx. f^n x`; applying that function `m` times to `x` gives `f^{n·m} x`. So `MULT m n =β (m · n)`, verified by induction on `m` with `n` fixed.
• Pairs satisfy `FST(PAIR M N) =β M` and `SND(PAIR M N) =β N` by the direct three-step reduction shown earlier — this pair of equations is the full specification of "pairing," and nothing more is needed since the untyped calculus has no notion of "storage" to additionally verify.
• `PRED` is correct by an invariant on the shift-pair: define the invariant "after `k` applications of `SHIFT` starting from `(0,0)`, the pair equals `(max(k-1,0), k)`." This holds at `k=0` trivially and is preserved by one more `SHIFT` (which sends `(a,b) ↦ (b, b+1)`), so after `n` shifts the pair is `(n-1, n)` for `n ≥ 1` and `(0,0)` for `n=0`; taking `FST` gives the truncated predecessor.

Complexity when actually executed (e.g., under a reduction strategy such as call-by-value or normal order, as would happen in an interpreter):

The headline honesty point: `PRED` costs Θ(n) while `SUCC` costs O(1) at the term-construction level — a striking asymmetry absent from ordinary machine arithmetic, where both increment and decrement are O(1). This is intrinsic to the representation, not an artifact of a bad implementation: a Church numeral's only capability is "apply `f` this many times," so extracting "one less" requires simulating all `n` steps to reconstruct the previous count via the pair trick. Later systems (e.g., Scott encodings) fix this by encoding numerals so that predecessor is O(1), trading away some other convenience — a genuine tradeoff, not a free improvement.

Space. The lambda term for numeral `n` in fully-reduced (normal) form has size Θ(n) (it literally contains `n` occurrences of `f`). This mirrors unary rather than binary representation of numbers — an important honesty point: Church numerals are exponentially less space-efficient than binary encodings, which is why no real language uses them for actual arithmetic; their purpose is expressiveness and foundational proof, not performance.

Let's compute `PLUS 2 3` fully and confirm it beta-reduces to `5`, tracing every step.

Setup: ``` 2 = λf.λx. f (f x) 3 = λf.λx. f (f (f x)) PLUS = λm.λn.λf.λx. m f (n f x) ```

Step-by-step trace:

Five nested applications of `f` to `x` — exactly `2 + 3`. The trace required `3` reductions to unroll numeral `3` and `2` reductions to unroll numeral `2`, for `Θ(m+n) = 5` total unrolling steps, matching the complexity claim above.

Second trace — `PRED 2`, to show the asymmetric cost: ``` PRED 2 = FST( 2 SHIFT (PAIR 0 0) ) ``` `2 SHIFT p₀` applies `SHIFT` twice to `p₀ = (0,0)`:

Final pair `(1, 2)`; `FST(1,2) = 1`. So `PRED 2 = 1`, correct — but it cost two full `SHIFT` applications (each itself several beta steps for the pair selection), where a machine integer decrement costs one hardware instruction. This concretely demonstrates the Θ(n) claim: reaching `PRED n` always walks all `n` layers of the numeral, regardless of how small the answer is.

Church encodings are foundational rather than performance-oriented, but their influence pervades real systems. Functional languages such as Haskell and Scheme trace their semantic core directly to the lambda calculus that Church encodings inhabit; understanding how booleans and pairs reduce to pure function application demystifies how these languages implement `if` and tuples "under the hood" at the level of core-language desugaring. Proof assistants and dependently typed languages (Coq, Agda, Lean) use Church-style (and closely related Scott-style) encodings of inductive data as one strategy for representing data purely in terms of its elimination principle, connecting directly to how the Lambda Calculus models constructive proofs via the Curry–Howard correspondence. Compiler intermediate representations that desugar high-level constructs into lambda-calculus-like cores (continuation-passing style transformations, closure conversion) rely on the same principle that structured control flow and data can be flattened into pure application chains. The technique also underlies classic interview and pedagogical exercises in demonstrating Turing-completeness of minimal systems — showing that a language with "just functions" is not a toy but a complete computational substrate. Finally, the iteration pattern used for Church numerals (apply a function `n` times) is the direct ancestor of the `fold`/`reduce` combinators ubiquitous in functional programming, and it foreshadows how general-purpose Recursion and Higher-Order Functions are constructed from fixed-point combinators once self-reference is added to the picture.

Ask the tutor: How would you extend Church encodings to represent signed integers or lists, and what does that cost in reduction complexity?