Encoding Data in Lambda Calculus: An Introduction
Frank(Peng) Fu
September 26, 2017
Abstract
Lambda calculus is a formalism introduced by Alonzo Church in the 1930s for his research on thefoundations of mathematics. It is now widely used as a theoretical foundation for the functional programming languages (e.g. Haskell, OCaml, Lisp). I will first give a short introduction to lambda calculus, thenI will discuss how to encode natural numbers using the encoding schemes invented by Alonzo Church,Dana Scott and Michel Parigot. Although we will mostly focus on numbers, these encoding schemes also
works for more general data structures such as lists and trees. If time permits, I will talk about the typetheoretical aspects of these encodings.

1

Introduction to Lambda Calculus

Lambda calculus was invented by Alonzo Church, a lot of early results are due to him and his students.
Currently, the definitive reference for lambda calculus is the book by Henk Barendregt [1].
Definition 1 (Lambda Calculus) The set of lambda term Λ is defined inductively as following.
• x ∈ Λ for any variable x.
• If e ∈ Λ, then λx.e ∈ Λ.
• If e1 , e2 ∈ Λ, then e1 e2 ∈ Λ.
Some computer scientists express lambda terms as: e, n ::= x | e1 e2 | λx.e. Lambda terms are almost
symbolic, except we only consider lambda terms modulo alpha-equivalence, i.e. we view λx.e as the same
term as λy.[y/x]e, where y does not occurs in e.
Definition 2 Beta-reduction: (λx.e1 ) e2
variable x in e1 by e2 .

[e2 /x]e1 , where [e2 /x]e1 means the result of replacing all theNote that we allow beta-reduction occurs anywhere inside a lambda term. Let us see some examples.
Example 1 (λx.x x) (λx.x)(λx.x) (λx.x)
λx.x(λx.x x) (λx.x x)(λx.x x) (λx.x x)...
(λx.(λy.y) x) (λx.x x)(λx.x) (λx.x x)(λx.x x)The beta-reduction can be intuitively understood as performing computation step by step, and sometimes
computation diverges. If a lambda term can not be further reduced by beta-reduction, then it is in normalform.
∗∗
Theorem 1 (Church-Rosser/Confluence) If e
e1 and ee2 , then there exist a e0 such that∗ 0∗ 0∗e1e and e2e . Heremeans performing reduction in one or more steps.

12Lambda Encoded Numbers

One reason that lambda calculus is interesting is that we can use lambda term to represent algorithm andlet the beta-reduction to calculate the result.
Definition 3 (Fixpoint combinator) A fixpoint combinator in lambda calculus is a term n such thatn e ∗ e (n e) for any lambda term e.
Example 2 (Turing’s Fixpoint) Let A be λx.λy.y (x x y). Then A A is a fixpoint combinator. Let e byany lambda term. A A e = (λx.λy.y (x x y)) A ee (A A e).
We usually write fix to means a fixpoint combinator, and compuationally it behaves as fix e ∗ e (fix e).
Fixpoint combinator allows us to represent recursive definition such as a = G a, (where G is a lambdaterm) by a lambda term a = fix G

2.1

Scott Encoded Numbers

Scott encoded numbers, or more generally, Scott encoding, is attributed to Dana Scott1 .
Definition 4 (Scott numerals)
Zero Z := λz.λs.z
Successor S := λn.λz.λs.s n
Pattern matching caseN := λn.λu.λf.n u f
The normal form of natural numbers in Scott encoding looks like: one := λz.λs.s Z, two := λz.λs.s one, three :=λz.λs.s two, .... With the pattern matching, we can define predecessor function for natural number: pred :=λn.caseN n Z (λn0 .n0 ).
Definition 5 (Addition) A typical recursive definition of addition:
add n m = case n ofZ -> m(S n’) -> S (add n’ m)
To obtain the Scott encoded addition, observe the followings.
add= \ n . \ m.
caseN nm(\ n’ . S (add n’ m))

G = \ r . \ n . \ m .
caseN nm(\ n’ . S (r n’ m))
add = G add
add’ = fix G
1 Who himself did not remember this encoding according to folklore.

2

2.2

Church Encoded Numbers

Definition 6pair := λa.λb.λp.p a b
p1 := λp.p (λx.λy.x)
p2 := λp.p (λx.λy.y)
If we have type, then pair : A → B → A × B, p1 : A × B → A, p2 : A × B → B.
Definition 7 (Church numerals)
Zero Z := λz.λs.z
Successor S := λn.λz.λs.s (n z s)
Iteration iterN := λn.λu.λf.n u f
The normal form of each Church numeral looks like: one := λz.λs.s z, two := λz.λs.s (s z), three :=λz.λs.s (s (s z)), ....
Note that iterN 3 u f ∗ f (f (f u)). One nice(?) thing about Church encoding is that it allows programming
without using fixpoint combinators.
Definition 8 (Addition) The addition function we seen has this property:
add n m ∗ (S...(S m))| {z }
nThus we can use iterator to represent addition. add := λn.λm.iterN n m S.
Note that the number of beta-reduction steps that this addition takes is proportioned to the input n.
Rosser has a much clever constant time definition of addition, which is add := λn.λm.λz.λs.n (m z s) s.
Rosser addition take four beta-reduction steps for any number n, m (assuming n, m are in normal forms).
Definition 9 (Predecessor) Since in Church encoding, we do not have the pattern matching like Scottencoding, how are we going to represent predecessor? Idea: use pair and iteration: (0, 0) 7→ (0, 1) 7→ (1, 2)...,
i.e. to get the predecessor of m, we can iterate m times the function (n, n0 ) 7→ (n0 , n0 + 1) over (0, 0), andproject the left element on the result. This is due to Kleene.
So pred := λm.p1 (iterN m (pair Z Z)(λr.pair (p2 r) (S (p2 r))))
Note that the number of beta-reduction steps that this predecessor function takes is proportioned to thesize of input number m, unlike Scott encoded predecessor, which take three steps.

2.3

Parigot Encoded Numbers

Parigot encoding was proposed to enable constant time predecessor function while allowing programmingwith the iterators.
Definition 10 (Parigot numerals)
Zero Z := λz.λs.z
Successor S := λn.λz.λs.s n (n z s)
Primitive recursion recN := λn.λu.λf.n u f
The normal form of each Church numeral looks like: one := λz.λs.s Z z, two := λz.λs.s one (s Z z), three :=λz.λs.s two (s one (s Z z)), .... Note that recN 3 u f ∗ f 2 (f 1 (f 0 u)).
Definition 11
Addition add = λn.λm.recN n m (λa.λr.S r)
Multiplication mult = λn.λm.recN n zero (λa.λr.add m r)
Predecessor pred = λn.n Z (λa.λr.a)
Factorial fac = λn.n one (λa.λr.mult (S a) r)
3

References[1] HP Barendregt. The lambda calculus: Its syntax and semantics, volume 103 of studies in logic and thefoundations of computer science, 1981.

4