# Convert λ-expressions to SK-expressions

The λ-calculus, or lambda calculus, is a logical system based on anonymous functions. For example, this a λ-expression:

λf.(λx.xx)(λx.f(xx))


However, for the purposes of this challenge, we'll simplify the notation:

• Change λ to \ (to make it easier to type): \f.(\x.xx)(\x.f(xx))
• The . in lambda headers is unnecessary, so we can drop it: \f(\xxx)(\xf(xx))
• Use the Unlambda-style prefix notation with  for application rather than writing the two functions together (for a full explanation of how to do this, see Convert between Lambda Calculus Notations): \f\xxx\xfxx
• This is the most complicated substitution. Replace each variable with a number in brackets based on how deeply nested the variable is relative to the lambda header it belongs to (i.e. use 0-based De Bruijn indexing). For example, in \xx (the identity function), the x in the body would be replaced with [0], because it belongs to the first (0-based) header encountered when traversing the expression from the variable to the end; \x\y\xxxxy would be converted into \x\y\x[0][0][1][0]. We can now drop the variables in the headers, leaving \\\[0][0][1][0].

Combinatory logic is basically a Turing Tarpit made out of the λ-calculus (Well, actually, it came first, but that's irrelevant here.)

"Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions from which bound variables are absent."1

The most common type of combinatory logic is the SK combinator calculus, which uses the following primitives:

K = λx.λy.x
S = λx.λy.λz.xz(yz)


Sometimes a combinator I = λx.x is added, but it is redundant, as SKK (or indeed SKx for any x) is equivalent to I.

All you need is K, S, and application to be able to encode any expression in the λ-calculus. As an example, here's a translation from the function λf.(λx.xx)(λx.f(xx)) to combinatory logic:

λf.(λx.xx)(λx.f(xx)) = S(K(λx.xx))(λf.λx.f(xx))
λx.f(xx) = S(Kf)(S(SKK)(SKK))
λf.λx.f(xx) = λf.S(Kf)(S(SKK)(SKK))
λf.S(Sf)(S(SKK)(SKK)) = S(λf.S(Sf))(K(S(SKK)(SKK)))
λf.S(Sf) = S(KS)S
λf.λx.f(xx) = S(S(KS)S)(K(S(SKK)(SKK)))
λx.xx = S(SKK)(SKK)
λf.(λx.xx)(λx.f(xx)) = S(K(S(SKK)(SKK)))(S(S(KS)S)(K(S(SKK)(SKK))))


Since we are using the prefix notation, this is SKSSKKSKKSSKSSKSKK.

1 Source: Wikipedia

## The Challenge

By now, you've probably guessed what is: Write a program that takes a valid λ-expression (in the notation described above) as input and outputs (or returns) the same function, rewritten in SK-combinator calculus. Note that there are an infinite number of ways to rewrite this; you only need to output one of the infinite ways.

This is , so the shortest valid submission (measured in bytes) wins.

## Test Cases

Each test case shows one possible output. The expression on top is the equivalent λ-calculus expression.

λx.x:
\[0]                        -> SKK
λx.xx:
\[0][0]                    -> SKKSKK
λx.λy.y:
\\[0]                       -> SK
λx.λy.x:
\\[1]                       -> K
λx.λy.λz.xz(yz):
\\\[2][0][1][0]          -> S
λw.w(λx.λy.λz.xz(yz))(λx.λy.x):
\[0]\\[1]\\\[2][0][1][0] -> SSIKSKK

• – Christian Sievers Mar 6 '17 at 1:08
• I think your second test case is not correct. The last contains a number not in brackets. – Christian Sievers Mar 6 '17 at 2:06
• – FUZxxl Mar 6 '17 at 16:14
• How did you get λx.f(xx) = S(Kf)(SKK)? Shouldn't it rather be λx.f(xx) = S(Kf)(SII) = S(Kf)(S(SKK)(SKK))? When converting λx.f(xx), I get S {λx.f} {λx.xx} which reduces to S (Kf) {λx.xx} and the expression in brackets is nothing else than ω=λx.xx, which we know is represented as SII = S(SKK)(SKK), right? – BarbaraKwarc Jun 12 '18 at 13:25
• @BarbaraKwarc Right, I meant SII, not SKK. That was a mistake. – Esolanging Fruit Jun 12 '18 at 17:06

data E=S|K|E:>E|V Int
p(h:s)|h>'_',(u,a)<-p s,(v,b)<-p u=(v,a:>b)|h>'['=a<$>p s|[(n,_:t)]<-reads s=(t,V n) a(e:>f)=S:>a e:>a f a(V 0)=S:>K:>K a(V n)=K:>V(n-1) a x=K:>x o(e:>f)='':o e++o f o S="S" o K="K" f=o.snd.p  p parses the input, returning the remaining unparsed part in the first component of the resulting pair. The first character of its argument must be a backtick, a backslash or an opening bracket. The pattern guards of p check these cases in this order. In the first case, denoting an application, two more expressions are parsed and combined to an element of the E data type with the infix constructor :>. In the lambda case, the following expression is parsed and immediately given to the a function. Otherwise it is a variable, we get its number with the reads function (which returns a list) and drop the closing bracket by pattern matching with (_:t). The a function does the quite well known bracket abstraction. To abstract an application, we abstract the two subexpressions and use the S combinator to distribute the argument to both. This is always correct, but with more code we could do much better by handling special cases in order to get shorter expressions. Abstracting the current variable gives I or, when we don't have that, SKK. Usually the remaining cases can just add a K to the front, but when using this notation we have to renumber the variables as the inner lambda is abstracted. o turns the result to a string for output. f is the complete function. As in many languages, backslash is an escape character, so it has to be given twice in a string literal: *Main> f "\\[0]" "SKK" *Main> f "\\[0][0]" "SSKKSKK" *Main> f "\\\\[0]" "SSKSKKKK" *Main> f "\\\\[1]" "SKKSKK" *Main> f "\\\\\\[2][0][1][0]" "SSKSSSKSSKKKSSSKSSSKSSKKKSSSKSSKKKKSKKSKKSSKSSSKSSKKKSSKKKKSKKKKSSKSSSKSSKKKSSSKSSKKKKSSKSKKKKSSKSSSKSSKKKSSKKKKSKKKK"  • 1. On the second line, you can use (a,(b,v))<-p<$>p s. 2. The '\\' can be just _ if you move that match last. – Ørjan Johansen Mar 6 '17 at 5:06
• Actually, scratch the first part: It's shorter to swap the tuple order and use p(_:s)=a<$>p s for the (moved) '\\' line. – Ørjan Johansen Mar 6 '17 at 5:15 • Try it online! for your current version. Which by the way is only 236 bytes, you can drop the final newline. – Ørjan Johansen Mar 6 '17 at 5:23 • @Challenger5 I think it's mostly due to the fact that haskell is based on lambda calculus, so people proficient in haskell are more likely to be attracted to this kind of questions :) – Leo Mar 6 '17 at 9:43 • You can define p with a single expression with three guards, rearrange the cases and drop a superfluous pair of (): p(h:s)|h>'_',(u,a)<-p s,(v,b)<-p u=(v,a:>b)|h>'['=a<$>p s|[(n,_:t)]<-reads s=(t,V n)`. – nimi Mar 6 '17 at 16:06