In Part 1, we built a boolean algebra using Church Encoding. In this post, we are going to reuse some of the previous work to build a similar algebra, this time for numerals.
In the algebra we built in the previous post, Church booleans were encoded using higher-order functions. The way Church numerals are represented is similar: given a number n and a function f, the Church numeral of n is the number of times f encapsulates n. For example, for n = 3, the function f encapsulates n three times:
The general case n would look like this:
where f^n = f ∘ f ∘ f ∘ … ∘ f, being f composed n times. f is also known as the successor function.
n = 0 is a special case where we just return the parameter:
Church numerals in Clojure
Using the macro we created in Part 1, we can now implement Church numerals in Clojure using a notation close to Lambda Calculus:
(λ f (λ x x)))
(λ f (λ x (f x))))
(λ f (λ x (f (f x)))))
(λ f (λ x (f (f (f x))))))
The following numbers are implemented in the same way, composing fn times. But this is not the only way to build Church numerals. As we have seen, f is actually the successor function, which can be defined like:
; λn.λf.λx.f (n f x)
(λ n (λ f (λ x (f ((n f) x))))))
The successor of n is a function that:
returns another function that takes x
applies f to the result of applying n f to x. This is a way of generalising the n compositions of f that we have seen in the general case n of the Church numerals.
We can define the numbers of the example above in terms of succ:
(succ (succ zero))
(succ (succ (succ zero)))
Printing Church numerals
Church numerals, and the functions built around them, can be, sometimes, difficult to visualise. Another thing we can explore in this post is how we can convert Church numerals into string representations. The idea is to consume the expression (which is a combination of functions applied to a parameter) and add the representation of each application:
(λ f ((f (λ n (format"f(%s)" n))) "n")))
For clarity (to avoid calling succ many times), we can add two functions to convert Church numerals to integers, and the other way around. To get a Church numeral from an integer, we can create a recursive function that encapsulates the previous numeral in the successor function, until it reaches 0. This is the same idea as the original definition of Church numerals:
(if (= n 0)
(succ (fromInt (- n 1))))))
For example, we could try to convert 5 into a Church numeral:
This expression will return a Church numeral that can be represented as:
The predecessor function is quite complicated compared with the functions described so far:
λn.λf.λx.n (λg.λh.h (gf)) (λu.x) (λu.u)
If Church numerals apply a function n times using the successor function, we could do the reverse reasoning and say that predecessor applies the function n - 1 times. This is achieved by wrapping f and x to skip the first application of f. This way, we get the remaining n - 1 applications. Here is a more detailed explanation.
We have seen how to extend the work we did with booleans, to create a simple numeral calculator. This is a step further to understand Church encoding better, and explore more complex operations. There are even more complex things that might be worth exploring; arithmetic operations such as division or modulo, and new primitive terms such as pairs or lists, that would introduce new challenges in this game of functions with a single parameter.