3 ms·
Using church numerals[1], right_incr(n) = g => y => n(g)(g(y)) and using the following shorter fixed-point combinator[2], X(f) = ( a => a(a) )(
by nightlyherb 3y ago
Using church numerals[1],
right_incr(n) =
g => y => n(g)(g(y))
and using the following shorter fixed-point combinator[2],
X(f) =
( a => a(a) )( x => f(x(x)) )
I get this junk:
X(right_incr)
= ( a => a(a) )( x => g => y => x(x)(g)(g(y)) )
= ( x => g => y => x(x)(g)(g(y)) ) ( x => g => y => x(x)(g)(g(y)) )
X(right_incr)(g)(y)
= let f = ( x => g => y => x(x)(g)(g(y)) )
in f(f)(g)(y)
= let .. in f(f)(g)(g(y))
= let .. in f(f)(g)(g(g(y)))
= ...
Which, as you can see, only gets more complex when I try to transform it.
[1] https://en.m.wikipedia.org/wiki/Church_encoding https://en.m.wikipedia.org/wiki/Church_encoding
[2] https://en.m.wikipedia.org/wiki/Fixed-point_combinator#Other_fixed-point_combinators https://en.m.wikipedia.org/wiki/Fixed-point_combinator#Other...