Lambda calculus has always been a fascination of mine and the emergent behaviors of passing functions into each other is delightfully complex. Church numerals are representations of natural numbers contructed from the repeated application of a function (normally the unary addition of a constant). For example, the number zero returns x and "ignores" the input function, one is
f(x), two is
f(f(x)) and so on:
ident = lambda x: x zero = lambda f: ident succ = lambda n: lambda f: lambda x: f(n(f)(x)) one = succ(zero) add1 = lambda x: x + 1 to_int = lambda f: f(add1)(0) print(to_int(one)) >>> 1
From this we can easily see that addition is accomplished by applying the first function to x then applying the second function to x:
add = lambda m: lambda n: lambda f: lambda x: n(f)(m(f)(x)) print(to_int(add(one)(two))) >>> 3
Addition is relatively easy to understand. However, to a newcomer it might be inconceivable to think of what subtraction looks like in a Church encoded number system. What could it possibly mean to un-apply a function?
Implement the subtraction function in a Church encoded numeral system. Where subtraction performs the monus operation and unapplies a function
n times if the result will be greater than zero or zero otherwise. This is code-golf so shortest code wins.
Two Church numerals that have been encoded in your choice of language. The input can be positional or curried. To prove these are true Church numerals they will have to take in any function and apply them repeatedly (
add1 is given in the examples but it could be
mult7, or any other unary function.)
A Church numeral. It should be noted that if
m < n then
m - n is always the same as the identity function.
minus(two)(one) = one minus(one)(two) = zero ...
minus(two, one) = one minus(one, two) = zero
This github gist for giving me a python implementation of Church Numerals.