20

4

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

.

_{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 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
```

1

Related: http://codegolf.stackexchange.com/q/105991/56725

– Christian Sievers – 2017-03-06T01:08:24.4371I think your second test case is not correct. The last contains a number not in brackets. – Christian Sievers – 2017-03-06T02:06:12.040

Related: http://codegolf.stackexchange.com/q/53250/134

– FUZxxl – 2017-03-06T16:14:56.327How 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 – 2018-06-12T13:25:21.367@BarbaraKwarc Right, I meant

`SII`

, not`SKK`

. That was a mistake. – Esolanging Fruit – 2018-06-12T17:06:21.593For the last test case input

`\\`

`[0]\[1]\\``[2][0]`[1][0]`, wouldn't the equivalent lambda expression be`

λw.w(λx.λy.x)(λx.λy.λz.xz(yz))`instead of`

λw.w(λx.λy.λz.xz(yz))(λx.λy.x)`? In other words, isn't`

\``[0]EF`equivalent to`

λw.wEF`instead of to`

λw.wFE`? – r.e.s. – 2019-06-19T15:50:26.227