# $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  # Church Encoding: Converting to Primitives | Comments # Introduction 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→λ. # Boolean 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) True >>> realbool(fls) False  ## 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)) False >>> realbool(churchbool(True)) True  # Equality 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) True >>> realeq(c1)(c2) False  ## 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)) True >>> realbool(churcheq(3)(2)) False  # Numbers 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) 2 >>> realnat(times(c2)(c3)) 6  ## 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 # Introduction 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(c1)(True)(False) False >>> iszro(c0)(True)(False) True >>> iszro(sub(c3)(c3))(True)(False) True >>> iszro(sub(c3)(c2))(True)(False) False >>> iszro(times(c0)(c1))(True)(False) True  # 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) False >>> equal(c3)(c1)(True)(False) False >>> equal(c3)(c3)(True)(False) True  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) False >>> equal(c0)(c0)(True)(False) True  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) False >>> gt(c0)(c0)(True)(False) False >>> gt(c3)(c2)(True)(False) True >>> lt(c0)(c3)(True)(False) True >>> lt(c0)(c0)(True)(False) False >>> lt(c3)(c2)(True)(False) 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. # Lists 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) False >>> isnil(nil)(True)(False) True  ## 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 # Introduction 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 Python: def f(x,y): return 2*x + 3*y  Javascript: var f = function(x,y) { return 2*x + 3*y; }  Perl: sub f { my (x,y) = @_; return 2*x + 3*y; }  ## Currying 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) >>>13  Javascript (anonymous functions): (function(x) { return (function(y) { return 2*x + 3*y; }); })(2)(3); >>>13  Perl (anonymous subroutines): sub { my$x = shift;
return sub {
return 2*x + 3*shift;
};
}->(2)->(3);
>>>13