12
1
Church Subtraction
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?
Challenge
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.
Input
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 add25
, mult7
, or any other unary function.)
Output
A Church numeral. It should be noted that if m < n
then m - n
is always the same as the identity function.
Examples:
minus(two)(one) = one
minus(one)(two) = zero
...
also acceptable:
minus(two, one) = one
minus(one, two) = zero
Credit:
This github gist for giving me a python implementation of Church Numerals.
1(The comment in the gist is wrong;
exp(m, n)
calculatesm^n
of course.) – Neil – 2019-08-23T20:46:09.4631I'm not sure what you mean that "the input can be positional or curried". Is it OK to define the main function as
lambda m,n,f:apply f m-n times
(or evenlambda m,n,f,x:apply f m-n times to x
) instead oflambda m,n:lambda f:...
? Or does this just apply to the two inputsm
andn
? – xnor – 2019-08-25T04:14:34.497Also, may we take the arguments
m
andn
in the other order? This would help with currying. – xnor – 2019-08-25T04:28:49.657@xnor as long as you can prove it subtracts two church numerals then you can take the inputs anyway you want. – Ryan Schaefer – 2019-08-25T13:58:16.260