$blog→errstr

do not commit

Church Encoding: Recursion, Z-Combinator and Factorial

| Comments

Introduction

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.

Implementation

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)
6
>>> factorialNB(5)
120
>>> factorialNB(100)
93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000