do not commit

Church Encoding: Converting to Primitives

| Comments


So far, we have been able to build in multi-argument handling, booleans, numerals, arithmetic, equality and lists all while staying in the Pure λ-Calculus. However, it is convenient to introduce primitives like numbers and booleans when working on more complicated examples in order to remove some extra cognitive steps. As an examples, which takes fewer steps to recognize: 2 or the return value of scc(scc(0))?

In this post, I describe the means of converting some of the strictly pure λ-calculus primitives to a more common numeric and boolean representations that Pierce calls λNB - which is his name for the enriched λ-calculus. I will also detail how to convert the other way from λNB→λ.


As a reminder, the Church boolean tru and fls are defined:

tru = λt. λf. t
fls = λt. λf. f

Church boolean → Boolean

To convert from λ→λNB we simply apply the λ-expression to true and false:

realbool = λb. b true false
# realbool = λb. b true false
realbool = lambda b: (b)(True)(False)

>>> realbool(tru)
>>> realbool(fls)

Boolean → Church boolean

In the other direction, λNB→λ, we use an if expression:

churchbool = λb. if b then tru else fls
# churchbool = λb. if b then tru else fls
churchbool = lambda b: (tru) if b else (fls)
>>> realbool(churchbool(False))
>>> realbool(churchbool(True))


Just like we were able to build higher level equality functions using Church booleans, we can do higher level conversions as well. As a reminder of the definition of equality:

equal = λm. λn. and (iszro (m prd n))(iszro (n prd m))

Church equality → Equality

realeq = λm. λn. (equal m n) true false
# realeq = λm. λn. (equal m n) true false
realeq = lambda m: lambda n: (equal(m)(n))(True)(False)

>>> realeq(c1)(c1)
>>> realeq(c1)(c2)

Equality → Church equality

churcheq = λm. λn. if equal m n then tru else fls
# churcheq = λm. λn. if equal m n then tru else fls
churcheq = lambda m: lambda n: (tru) if m == n else (fls)

>>> realbool(churcheq(3)(3))
>>> realbool(churcheq(3)(2))


I have already been converting Church numerals to numbers in my previous posts using the (lambda n: n+1)(0) function, here we will define it as a callable function. Church numerals are defined as:

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

Church numeral → Natural number

realnat = λm. m (λx. succ x) 0
# realnat = λm. m (λn. succ n) 0
realnat = lambda m: (m)(lambda n: n + 1)(0)

>>> realnat(c2)
>>> realnat(times(c2)(c3))

Natural number → Church numeral

This is more complicated and possible conversions require methods that I have not covered yet. I will revisit this when I post about Recursion.