5. Church Numerals and Arithmetic

Contents

Working System

This chapter stays in untyped lambda encodings of naturals (Church numerals), executed as Python functions.

5. Church Numerals and Arithmetic#

Goal. Represent natural numbers as higher-order functions and build arithmetic operators.

You will learn

  • Church numerals as iterators and how to convert to/from Python integers

  • How successor, addition, and multiplication are definable as lambda terms

  • How pairs let you implement predecessor by state-passing iteration

  • How to build basic predicates such as is_zero and leq

  • How to validate algebraic laws by small finite checks

Roadmap#

  1. Define Church numerals and conversions (church, to_int, from_int).

  2. Implement succ, add, and mul and test them on small inputs.

  3. Implement Church pairs and use them to define pred.

  4. Build basic predicates (is_zero, leq) from arithmetic.

  5. Validate laws (associativity, distributivity) by computation.

Definition (Church Numerals)

A natural number n is encoded as a function that applies another function n times.

n ≡ λf. λx. f^n(x)

def church(n):
    return lambda f: (lambda x: _iterate(f, x, n))

def _iterate(f, x, n):
    for _ in range(n):
        x = f(x)
    return x

def to_int(n):
    return n(lambda k: k + 1)(0)

zero = church(0)
one = church(1)
two = church(2)
three = church(3)

Definition (Successor)

succ n ≡ λf. λx. f (n f x).

succ = lambda n: (lambda f: (lambda x: f(n(f)(x))))

def from_int(n):
    current = zero
    for _ in range(n):
        current = succ(current)
    return current

Definition (Addition and Multiplication)

  • add m n ≡ λf. λx. m f (n f x)

  • mul m n ≡ λf. m (n f)

The multiplication form is eta-short. It is eta-equivalent to the fully expanded λf. λx. m (n f) x.

add = lambda m: (lambda n: (lambda f: (lambda x: m(f)(n(f)(x)))))
mul = lambda m: (lambda n: (lambda f: m(n(f))))
pow = lambda b: (lambda e: e(b))

print(to_int(add(two)(three)))
print(to_int(mul(two)(three)))
print(to_int(pow(two)(three)))

5
6
8

Definition (Pairs and Predecessor)

Predecessor is trickier. We use pairs to carry a “previous” value while iterating.

pair = lambda a: (lambda b: (lambda f: f(a)(b)))
fst = lambda p: p(lambda a: (lambda b: a))
snd = lambda p: p(lambda a: (lambda b: b))

def pred(n):
    def step(p):
        return pair(snd(p))(succ(snd(p)))
    start = pair(zero)(zero)
    return fst(n(step)(start))

sub = lambda m: (lambda n: n(pred)(m))

print(to_int(pred(three)))
print(to_int(sub(three)(two)))

2
1

Exercise

  1. Define is_zero using Church booleans.

  2. Implement leq m n (m <= n) using subtraction and is_zero.

  3. Show that add is associative by testing on a small range of numbers.

  4. Show that mul distributes over add by testing on a small range of numbers. See solution: Exercise 5 (Church Numerals)

Summary#

  • A Church numeral is an iterator: it applies a function n times.

  • succ, add, and mul can be defined purely by function composition and iteration.

  • Predecessor is defined by carrying state through an iteration (pairs).

  • Predicates like is_zero and comparisons like leq can be built from these encodings.

  • Operationally: build confidence by testing small ranges, then use induction chapters for fully general proofs.

  • Next: recursion via fixpoints and how to make Church-style recursion work in eager Python (Chapter 6).

Contents