Church Subtraction

Question

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.

Answer 1

Haskell, 35 bytes

(r%s)f x=s(x:)(iterate f x)!!r(+1)0

Try it online!

Say that r and s are the church encodings of m and n. We want r%s to apply f m-n times to some initial value x. We first generate the infinite list

iterate f x = [x, f x, f (f x), f (f (f x)), ...]

then use s(x:) to prepend n copies of x, that is, shift each value n indices right:

s(x:)(iterate f x) = [x, x, x, ...,  x, f x, f (f x), f (f (f x)), ...]

We then compute m directly as r(+1)0, and take the m'th element of that list as !!r(+1)0. An indexing-free solution could instead do head$r tail$..., that is drop the first element m times and then take the first element, but the indexing syntax is much shorter.

Note that the classic solution doesn't work in Haskell without extensions because its strong typing can't represent the predecessor operation.

Answer 2

Python 2, 82 80 bytes

eval('!u:!v:v(!n:!f:!x:n(!g:!h:h(g(f)))(!u:x)(!u:u))(u)'.replace('!','lambda '))

Try it online!

2 bytes thx to Nick Kennedy noting an un-needed pair of parens.

Anonymous function that implements minus.

Mostly this is just compressing the definition found at the Wikipedia page; not like I truly understand the code yet. But interesting!

Answer 3

Python 2, 77 bytes

lambda r,s:s(lambda r:lambda f:lambda x:r(lambda(_,x):(x,f(x)))((x,x))[0])(r)

Try it online!

We do Church decrement by tracking the previous value for each iteration and outputting that at the end. 39% of the code length is "lambda"'s...

Answer 4

C++ (clang), 112 bytes

#define L(x,y)[&](auto x){return y;}
auto m=L(u,L(v,v(L(n,L(f,L(x,n(L(g,L(h,h(g(f)))))(L(u,x))(L(u,u))))))(u)));

Try it online!

This is by far the most incomprehensible C++ code I've ever written. That said, I think that ungolfing this code will only make it worse.

Answer 5

Underload, 37 bytes

(~(((!())~):*^(~!:(:)~*(*)*)~^^!)~^^)

Try it online!

The inner (((!())~):*^(~!:(:)~*(*)*)~^^!) is the pred function, implemented via pairs:

(               ( start pred function )!
  (
    (!())~      ( push zero below argument )!
  ):*^          ( do that twice )!

  (             ( start pair-increasing function )!
    ~!          ( remove second argument)!
    :           ( duplicate first argument )!
    (:)~*(*)*   ( increment first return value )!
  )
  ~^^           ( run pair-increasing function n times )
  !             ( remove first in returned pair )!
)

Answer 6

JavaScript (Node.js), 87 85 81 76 74 bytes

f=>g=>h=>x=>f(([x,[g,a]])=>[g(x),a])([x,g(a=>[x=>x,a])(f(a=>[h,a])())])[0]

Try it online! Not going to win any awards, but I thought I'd try a different approach.

a=>[h,a] is a stage that applies h, while a=>[x=>x,a] is a stage that doesn't apply h. We apply the first function f times and the second function g times. We then apply the inverse function ([f,[g,a]])=>[g(x),a] f times. This skips over the g second stages and performs f-g first stages as desired. It then remains to extract the final value.

The tuples can of course be converted to lambda functions which results in the following expression:

f=>g=>h=>x=>f(e=>e(x=>d=>d(g=>a=>e=>e(g(x))(a))))(e=>e(x)(g(a=>e=>e(x=>x)(a))(f(a=>e=>e(h)(a))())))(x=>a=>x)

Answer 7

R, 86 bytes

eval(parse(t=gsub("!(.)","function(\\1)","!u!vv(!n!f!xn(!g!hh(g(f)))(!ux)(!uu))(u)")))

Try it online!

R port of @ChasBrown’s Python answer so be sure to upvote that one too.

Answer 8

J, 56 bytes

c=:3 :0
t=.^:y
5!:1<'t'
)
m=.2 :'c 0>.(>:u 5!:0->:v 5!:0)0'

Try it online!

Note: -3 bytes off TIO count for m=.

Higher order functions in J are achieved using adverbs and conjunctions. Here a church numeral is the gerund form of the adverb formed by combining the "power of" conjunction (which repeatedly applies a verb) and an integer. The following verb c (for "create") uses J's Atomic Representation to transform an integer into such a gerund:

c=:3 :0
t=.^:y
5!:1<'t'
)

Our "minus" operator (which is a conjunction) subtracts the right gerund church numeral from the left. It does not, however, assume any particular implementation of church numerals, including the one from our c verb. Instead, it relies on the general definition and turns each gerund church numeral back into an adverb by inverting it with 5!:0, and then applying that adverb to the increment verb >:, and then applying that to 0.

It then subtracts and takes the maximum with 0, and applies c to get the final result: a new gerund church numeral.

Answer 9

Wolfram Language (Mathematica), 55 48 47 39 bytes (33 characters)

#2[(fx#[g#@g@f&][x&][#&])&]@#&

Try it online!

The  symbol is 0xF4A1, a special Mathematica code point that denotes a rightward arrow for \[Function]. See here for more explanations. This is what the code looks like in the Mathematica front end:

We can do it in 40 bytes / 32 characters, which may be shorter depending on the measurement scheme: #2[n⟼f⟼x⟼n[g⟼#@g@f&][x&][#&]]@#&

The un-golfed version is a literal translation of the classical definition of pred:

pred = n \[Function] f \[Function] x \[Function] n[g \[Function] h \[Function] h[g[f]]][u \[Function] x][u \[Function] u];
subtract[m_, n_] := n[pred][m]

which looks like this in the Mathematica front end:

This subtraction function works with the Church numerals defined with

c@0=#& &;c@n_=#@*c[n-1][#]&

(un-golfed: c[0] = Identity &; c[n_] = Function[a, a@*c[n-1][a]])

so that we have

Table[c[n][f][x], {n, 0, 6}]
(*    {x, f[x], f[f[x]], f[f[f[x]]], f[f[f[f[x]]]], f[f[f[f[f[x]]]]], f[f[f[f[f[f[x]]]]]]}    *)

and

subtract[c[7],c[5]][f][x]
(*    f[f[x]]    *)