Something went wrong. Try again.
How to derive the successor function using the s and k combinators.
Something went wrong. Try again.
2.6 kB · 89 lines · Created 1w ago
Haskell
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889type Church a = (a -> a) -> a -> a
s :: (a -> b -> c) -> (a -> b) -> cs x y z = x z (y z)
k :: a -> b -> ak x y = x
succ :: Church a -> Church asucc n f x = f (n f x)
{-In order to convert actualSucc into a point-free combinator you need to abstract the lambdas from the inside out:-}
succ = \n -> \f -> \x -> f (n f x)
{-Here, we want to abstract \x -> f (n f x). This looks a lot like the definition of the s combinator.The s combinator places the second argument as an argument to the first argument, using the s combinatorwe would get something like x\ -> f x (n f x) so in order to drop the first x we can pre-compose f with k toget \x -> k f x (n f x). This is identical to s (k f) (n f).-}
succ = \n -> \f -> s (k f) (n f)
{-Similarly, we see that the innermost lambda again looks like an s combinator but with an extra s preceding it.Notice that in a simples lambda like \x -> f (g x) this is just composition. And we know that lambda evaluationis left associative, so really, the above lambda could be \f -> (s (k f)) (n f). This now shows that the solutionis to pre-compose k with s as the first argument to a new s combinator:-}
succ = \n -> s (s . k) n
{-Now notice that \n -> s (s . k) n is the same as the point-free version s (s . k) and now all we need to do isfind what the combinator for composition is. Usually, the composition combinator is called b so:-}
b :: (b -> c) -> (a -> b) -> a -> cb f g x = f (g x)
{-First, notice that k s simplifies to:-}
k s = (\x y -> x) s = \y -> s = \y -> \a b c -> a c (b c) = \y a b c -> a c (b c) = \w x y z -> x z (y z)
{-It basically just ignored the first argument and then applied the s combinator. If we then apply the s combinatorto this again we get:-}
s (k s) = (\a b c -> a c (b c)) (k s) = \b c -> (k s) c (b c) = \b c -> (\w x y z -> x z (y z)) c (b c) = \b c -> \y z -> (b c) z (y z) = \b c -> \y z -> b c z (y z) = \a b c d -> a b d (c d)
{-This may look like a mess, but the idea here was that applying s to k s brought theargument (b c) in \a b c -> a c (b c) forward and dropped the c. If we have a way of ignoring that d argumentthen this would just be \b c d -> b (c d) which is exactly the kind of lambda we need. We can do this with k.-}
s (k s) k = (\a b c d -> a b d (c d)) k = \b c d -> k b d (c d) = \b c d -> b (c d)
{-We can conclude that composition is:-}
b = s (k s) k
{-Finally, we can say that:-}
succ = \n -> s (s . k) n = \n -> s (b s k) n = \n -> s (s (k s) k s k) n = s (s (k s) k s k)