do not commit

Church Encoding: Boolean, Numerals and Arithmetic

| Comments


In my previous post about Currying, I mentioned that the λ-calculus has no primitive numbers or operation, just functions and more functions. In this post, I explore how, through simple constructs, Church was able to implement numbers, booleans, arithmetic operations and conditionals with examples in Python.

Please see my previous post on Currying, as it is critical to understanding the material here.

Church Booleans

There is no such thing as a “true” or “false” in the λ-calculus. However, we can represent those boolean values by defining the λ terms tru and fls.

# tru = λt.λf.t
tru = lambda t: lambda f: t
# fls = λt.λf.f
fls = lambda t: lambda f: f

Those terms can be used to test if a value is true or false with a term test b v w which reduces to v if b is tru and w if fls.

# test = λl.λm.λn. l m n
test = lambda l: lambda m: lambda n: (l)(m)(n)

To see how test reduces when called as test tru v w, we must first expand it and then we’ll use call-by-value reduction

  test tru v w
→ (λl.λm.λn. l m n) tru v w
→ (λm.λn. tru m n)v w
→ (λn. tru v n)w
= tru v w
→ (λt.λf.t)v w
→ (λf.v)w
= v

Making some test runs with our Python implementation:

>>> test(tru)(True)(False)
>>> test(fls)(True)(False)

Boolean Logical Operations

Since we now have the ability to represent boolean values, we can implement boolean algebra!

Implementing a logical AND and = λb.λc. b c fls, we return c if b is tru or fls if b is fls. So if b is tru and c is fls, we return c (meaning fls), otherwise if b and c are tru, we return tru.

# and = λb.λc. b c fls
And = lambda b: lambda c: (b)(c)(fls)

>>> And(tru)(tru)(True)(False)
>>> And(tru)(fls)(True)(False)
>>> And(fls)(tru)(True)(False)

To implement OR: or = λb.λc. b tru c, meaning if b is fls return c, if b is tru return tru. This, of course, would not implement XOR, since in the event that b is tru, we automatically return tru.

# or = λb.λc. b tru c
Or = lambda b: lambda c: (b)(tru)(c)
>>> Or(fls)(fls)(True)(False)
>>> Or(fls)(tru)(True)(False)
>>> Or(tru)(tru)(True)(False)
>>> Or(tru)(fls)(True)(False)

To implement NOT: not = λb. b fls tru, meaning return the opposite of b. We can apply to AND and OR operations along with boolean values.

# not = λb. b fls tru
Not = lambda b: (b)(fls)(tru)
>>> Not(tru)(True)(False)
>>> Not(fls)(True)(False)
>>> Not(And(tru)(tru))(True)(False)
>>> Not(And(tru)(fls))(True)(False)
>>> Not(Or(fls)(tru))(True)(False)
>>> Not(Or(fls)(fls))(True)(False)


Now that we have booleans, we can encode pairs of terms into one term, getting the first and second projections (fst and snd) when we apply the correct boolean value:

pair = λf.λs.λb. b f s
fst = λp. p tru
snd = λp. p fls

This means if we apply boolean value b to the function pair v w, it applies b to v and w. The application yields v if b is tru and w otherwise. Reducing the redex fst(pair v w) →* v goes as follows:

  fst(pair v w)
= fst((λf.λs.λb. b f s)v w)
→ fst((λs.λb. b v s)w)
→ fst((λb. b v w))
= (λp. p tru)(λb. b v w)
→ (λb. b v w)tru
→ tru v w
= v
# pair = λf.λs.λb. b f s
pair = lambda f: lambda s: lambda b: (b)(f)(s)
# fst = λp. p tru
fst = lambda p: (p)(tru)
# snd = λp. p fls
snd = lambda p: (p)(fls)

>>> fst(pair(tru)(fls))(True)(False)
>>> fst(pair(tru)(tru))(True)(False)
>>> fst(pair(fls)(tru))(True)(False)
>>> fst(pair(fls)(fls))(True)(False)
>>> snd(pair(fls)(fls))(True)(False)
>>> snd(pair(fls)(tru))(True)(False)
>>> snd(pair(tru)(fls))(True)(False)
>>> snd(pair(tru)(tru))(True)(False)

Church Numerals

So far, we have been able to implement the basis of Boolean Algebra with only functions! Church uses a slightly more intricate representation of numbers by use of composite functions. Basically, to represent a natural number n, you simply encapsulate an argument n times with a successor function scc. You can think of scc = n + 1. To represent 0, Church used the same definition as fls (our False representation) - this should be familiar to most programmers as 0 == False in many languages. So a break down of 0..Nth Church numeral is as such:

c0 = λs. λz. z
c1 = λs. λz. s z
c2 = λs. λz. s (s z)
c3 = λs. λz. s (s (s z))
... and so on

The scc combinator is defined as: scc = λn. λs. λz. s (n s z)

It works by combining a numeral n and returns another Church numeral. It does this by yielding a function that takes s and z as arguments and applies s repeatedly to z, specifically n times.

Note: For the example output below, the two arguments to each Church numeral are a lambda function that is equivalent to scc and the numeral 0, since those are the parameters required for a Church numeral. It merely maps each function to the natural number value it represents. c0->0, c1->1.

# scc = λn. λs. λz. s (n s z)
scc = lambda n: lambda s: lambda z: (s)((n)(s)(z))
c0 = lambda s: lambda z: z
c1 = scc(c0)
c2 = scc(c1)
c3 = scc(c2)

>>> (c1)(lambda n: n+1)(0)
>>> (c2)(lambda n: n+1)(0)
>>> (c3)(lambda n: n+1)(0)

Addition is essentially the scc combinator applied m times to a Church numeral n, where n + m = v. Equivalently, scc is merely plus applied once.

plus = λm. λn. λs. λz. m s (n s z)
# plus = λm. λn. λs. λz. m s (n s z)
plus = lambda m: lambda n: lambda s: lambda z: (m)(s)((n)(s)(z))

>>> plus(c1)(c2)(lambda n: n+1)(0)
>>> plus(c3)(c2)(lambda n: n+1)(0)

Multiplication is the repeated application of plus, since 2+2+2 = 2*3.

times = λm. λn. m (plus n) c0
times = lambda m: lambda n: (m)(plus(n))(c0)

>>> times(c2)(c3)(lambda n: n+1)(0)
>>> times(c3)(c3)(lambda n: n+1)(0)

Exponentiation uses repeated multiplication to get the intended value since 2**3 = 2*2*2.

exp = λm. λn. n (times m) c1

This translates to, (m * 1)**n.

exp = lambda m: lambda n: (n)(times(m))(c1)

>>> exp(c3)(c3)(lambda n: n+1)(0)
>>> exp(c3)(c0)(lambda n: n+1)(0)
>>> exp(c0)(c1)(lambda n: n+1)(0)
>>> exp(c2)(c1)(lambda n: n+1)(0)
>>> exp(c3)(c2)(lambda n: n+1)(0)

Subtraction requires quite a bit more work to function, involving the predecessor combinator prd. First we must define two pairs zz (a starting value) and ss that takes two arguments ci, cj then yields cj, cj+1. Applying ss, mtimes to pair c0,c0 yields 0,0 when m is 0, otherwise cm-1, cm when m is positive. The pred is always found in the first component of the pair.

zz = pair c0 c0
ss = λp. pair (snd p) (plus c1 (snd p))
prd = λm. fst (m ss zz)
# zz = pair c0 c0
zz = pair(c0)(c0)
# ss = λp. pair (snd p) (plus c1 (snd p))
ss = lambda p: pair(snd(p))(plus(c1)(snd(p)))
# prd = λm. fst (m ss zz)
prd = lambda m: fst((m)(ss)(zz))

Now that we have the prd combinator, we can define subtraction. Like addition, where we find a successor by iteratively adding 1 to 0, we can subtract by iteratively subtracting 1, n-times from m, where m - n = v.

sub = λm. λn. n prd m
# sub = λm. λn. n prd m
sub = lambda m: lambda n: (n)(prd)(m)

>>> sub(c3)(c1)(lambda n: n+1)(0)
>>> sub(c3)(c2)(lambda n: n+1)(0)
>>> sub(c0)(c0)(lambda n: n+1)(0)