Convert λ-expressions to SK-expressions

Question

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`\x`xx\x`f`xx
• 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``\x`xxxy 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."¹

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 ```S`K``S``SKK``SKK``S``S`KSS`K``SKK`.

_{¹ 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 code-golf, 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]                    -> ```SKK``SKK
λ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] -> ``S``SI`KS`KK

Answer 1

Haskell, 251 237 222 214 bytes

15 bytes saved thanks to @Ørjan_Johansen (also see his TIO links in the remarks)!

8 more bytes saved thanks to @nimi!

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]"
"``S``SKK``SKK"
*Main> f "\\\\[0]"
"``S``S`KS`KK`KK"
*Main> f "\\\\[1]"
"``S`KK``SKK"
*Main> f "\\\\\\``[2][0]`[1][0]"
"``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S`KK``SKK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S``S`KS``S`KK`KK``S``S`KS`KK`KK``S``S`KS``S``S`KS``S`KK`KS``S`KK`KK``S`KK`KK"