do not commit

Church Encoding: Recursion, Z-Combinator and Factorial

| Comments


Now that I have the basis for an enriched λ-calculus , I can add a very important aspect to programming: recursion.

Recursion-making Combinators Primer

There are several ways to arrive at recursion, some include: * Directly with the call-by-name Y-combinator Y = λf. (λx. f (x x))(λx. f (x x)) * Derive the Y-combinator by functionals and the U-combinator * Use the call-by-value Z-combinator: Z = λf. (λx. f (λy. x x y))(λx. f (λy. x x y))

In the case of a call-by-value language such as Python, it is useless to use the fixed-point Y-combinator since it diverges. For this post, I will be using the Z-combinator. Pierce does not go into the details of this intricate structure, instead opting for understanding through example.

Here is my Python implementation of the Z-combinator:

Z = λf. (λx. f (λy. x x y))(λx. f (λy. x x y))
# Z = λf. (λx. f (λy. x x y))(λx. f (λy. x x y))
Z = lambda f: (lambda x: f(lambda y: (x)(x)(y)))(lambda x: f(lambda y: (x)(x)(y)))

What The Fixed-Point Combinator Does

Let’s take Pierce’s example of factorial from earlier in his book:

factorial = λn. if n=0 then 1 else n * factorial(n-1)

The use of a fixed-point combinator is to essentially unroll the recursive definition of factorial to where it occurs, where I would rewrite the above definition unrolled:

if n=0 then 1
else n* (if n-1=0 then 1)
    else (n-1) * (if (n-2)=0 then 1)
        else (n-2) *...))

You could imagine this in Church’s Pure λ-calculus:

if realeq n c0 then c1
else time n (if realeq (prd n) c0 then c1
    else times (prd n)
                (if realeq (prd (prd n)) c0 then c1
                 else times (prd (prd n)) ...)

The same unrolling effect is achieved when using the Z-combinator by first defining the recursive function g = λf.〈body containing f〉 then h = Z g.


Now that I have the abstract idea of how to generate a recursive function using the fixed-point combinator (Z), I can implement the λ-calculus definition in Python for our enriched (λNB) and pure versions.

g = λfct. λn. if realeq n c0 then c1 else (times n (fct (prd n))) ;
factorial = Z g
# g = λfct. λn. if realeq n c0 then c1 else (times n (fct (prd n))) ;
g = lambda fct: lambda n: (c0) if realeq(n)(c0) else (times(n)(fct((prd)(n))))
gNB = lambda fct: lambda n: 1 if n == 0 else (n * (fct(n-1)))
# factorial = Z g
factorial = Z(g)
factorialNB = Z(gNB)

>>> factorialNB(3)
>>> factorialNB(5)
>>> factorialNB(100)

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.

Church Encoding: (In)Equality and Lists

| Comments


In my previous post about Church Encoding, I built up some booleans and their respective operators, numerals and several arithmetic operators. This post will focus on building two important constructs for any programming language: equality testing and lists. I will also continue my implementation with Python.

Testing For Zero

Determining if a Church numeral is zero is done by finding a pair of arguments that will return whether the numeral is zero or not (a True/False expression). We can use the zz and ss terms from the subtraction operation, by applying our numeral to the pair ss and zz. The trick is, if ss is applied at all to zz we know that the numeral is not zero and return fls, otherwise we return tru. This makes perfect sense, since the numeral will be applied the number of times equal to its value.

In other words, if the Church numeral is 0, then ss will be applied 0 times to zz and will return tru. Once ss is applied to zz (if the numeral is not 0), it will return fls - not 0.

iszro = λm. m (λx. fls) tru
# iszro = λm. m (λx. fls) tru
iszro = lambda m: (m)(lambda x: fls)(tru)

>>> iszro(c0)(True)(False)
>>> iszro(sub(c3)(c3))(True)(False)
>>> iszro(sub(c3)(c2))(True)(False)
>>> iszro(times(c0)(c1))(True)(False)

Numeric Equality

There are probably many ways to define numeric equality, however, the trick I will use is that m - n = 0 when m = n. So, testing for equality is as simple as applying sub then applying iszro to the result.

equal = λm. λn. iszro (sub m n)
# equal = λm. λn. iszro (sub m n)
equal = lambda m: lambda n: iszro(sub(m)(n))

>>> equal(c3)(c2)(True)(False)
>>> equal(c3)(c1)(True)(False)
>>> equal(c3)(c3)(True)(False)

There is are two big problems with this definition, however. First, each sub operation is O(n), second the resulting Church numeral must be defined otherwise iszro will evaluate to tru.

Pierce has a different definition of equal which has fewer evaluations than mine.

equal = λm. λn. and (iszro (m prd n))(iszro (n prd m))
# equal = λm. λn. and (iszro (m prd n))(iszro (n prd m))
equal = lambda m: lambda n: And(iszro((m)(prd)(n)))(iszro((n)(prd)(m)))

>>> equal(c2)(c3)(True)(False)
>>> equal(c0)(c0)(True)(False)

His definition is both more efficient and works in cases that mine does not. Since my definition does left-to-right subtraction, negative Church numerals (which I haven’t defined) evaluate to tru, since sub(2)(3) = -1.

Numeric Greater or Less Than

Since we can define equal it shouldn’t be too hard to define greater and less than, and it turns out that it isn’t.

For strictly greater-than, we exploit the fact that prd will return 0 when m >= n. So, if m > 0 then it could be said that the following holds true: m >= n && !(n >= m) which makes m strictly greater-than n.

For strictly less-than, a simple trick of switching the order of arguments accomplishes the same thing: n >= m && !(m >= n) which means that m must be strictly less than n.

gt = λm. λn. and (iszro (m prd n))(not iszro(n prd m))
lt = λm. λn. and (iszro (n prd m))(not iszro(m prd n))
# gt = λm. λn. and (iszro (m prd n))(not iszro(n prd m))
gt = lambda m: lambda n: And(iszro((m)(prd)(n)))(Not(iszro((n)(prd)(m))))
# lt = λm. λn. and (iszro (n prd m))(not iszro(m prd n))
lt = lambda m: lambda n: And(iszro((n)(prd)(m)))(Not(iszro((m)(prd)(n))))

>>> gt(c0)(c3)(True)(False)
>>> gt(c0)(c0)(True)(False)
>>> gt(c3)(c2)(True)(False)
>>> lt(c0)(c3)(True)(False)
>>> lt(c0)(c0)(True)(False)
>>> lt(c3)(c2)(True)(False)

Greater-than-or-equal and less-than-or-equal can simply be calculated by concatenating gt|equal and lt|equal, which is trivial and I’ll leave that up to the reader.


A list can be represented by a reduce or fold function in the λ-calculus. So the list [x y z] becomes a two-argument (c n) function that returns c x (c y (c z n)). There are several steps required to build lists detailed below.

Representing nil

nil can be represented by the same expression as 0 and fls, using the arguments c n we can define:

nil = λc. λn. n
# nil = λc. λn. n
nil = lambda c: lambda n: n

cons Function

cons is a function that will take an argument h and a list t and returns a folded representation of t with h prepended.

cons = λh. λt. λc. λn . c h (t c n)
# cons = λh. λt. λc. λn . c h (t c n)
cons = lambda h: lambda t: lambda c: lambda n: ((c)(h))((t)(c)(n))

isnil Function

The isnil function will mimic the iszero function, since the definition of nil is the same as 0. However, we are running it on a list, so there is a little more to is.

isnil = λl. l (λh. λt. fls) tru
# isnil = λl. l (λh. λt. fls) tru
isnil = lambda l: (l)(lambda h: lambda t: fls)(tru)

>>> isnil(c1)(True)(False)
>>> isnil(nil)(True)(False)

head Function

head is similar to isnil, except that we element at the beginning of the list instead of a Church boolean, otherwise fls.

head = λl. l (λh. λt.  h) fls
# head = λl. l (λh. λt.  h) fls
head = lambda l: (l)(lambda h: lambda t: h)(fls)

tail Function

tail is much more difficult and employs a similar trick as the pred function did. I was unable to figure out tail without help from the book, so here is Pierce’s solution:

tail = λl.
         fst (l (λx. λp. pair (snd p)(cons x (snd p)))
                (pair nil nil))
# tail = λl.
#          fst (l (λx. λp. pair (snd p)(cons x (snd p)))
#                 (pair nil nil))
tail = lambda l: fst((l)(lambda x: lambda p: pair((snd(p))(cons(x)(snd(p))))(pair(nil)(nil))))

Multi-Argument Handling Through Currying

| Comments


Since the λ-calculus does not have numbers or operators, only functions, it seems limited and useless, but with simple constructs one can create numbers, then build to operators, then data structure like lists. In fact, the λ-calculus is Turing Complete! The λ-calculus also lacks the built-in ability to handle multiple arguments, instead it employs Currying.

In this post I implement a simple multi-argument function transformed into a curried form in Python, Javascript and Perl.

Primer on Multi-Argument Functions

We must understand that the λ-calculus has no built-in ability to handle multiple arguments for a function - or abstraction. Instead, we rely on a transformation of multiple arguments to higher-order functions called currying - named after Haskell Curry. The principle is straight-forward: “Suppose that s is a term involving two free variables x and y and that we want to write a function f that, for each pair (v,w) of arguments, yields the result of substituting v for x and w for y in s.” (Pierce).

So, as an example of what you would do in a rich programming language for a multiple argument function f = λ(x,y).s, where v = 2x and w = 3y:

Rich Language Examples


def f(x,y):
    return 2*x + 3*y


var f = function(x,y) {
    return 2*x + 3*y;


sub f {
    my (x,y) = @_;
    return 2*x + 3*y;


In the λ-calculus, we employ currying where the expression f = λ(x,y).s is transformed into f = λx.λy.s. This simply means that f is a function that returns a function when given a value v for x, that returned function then returns the result when given a value w for y. In reducible expression form: f v w reduces to ((λy.[x → v]s)w) once the value for x is passed, then is reduced to [y → w][x → v]s.

In the following examples, I continue with v = 2x and w = 3y.

Curried Examples

Python (built-in lambda):

(lambda x: (lambda y: 2*x + 3*y)(3))(2)

Javascript (anonymous functions):

(function(x) {
    return (function(y) {
        return 2*x + 3*y;

Perl (anonymous subroutines):

sub {
    my $x = shift;
    return sub {
        return 2*x + 3*shift;