Convert λ-expressions to SK-expressions



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


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 , 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.

\[0]                        -> ``SKK
\`[0][0]                    -> ```SKK``SKK
\\[0]                       -> `SK
\\[1]                       -> K
\\\``[2][0]`[1][0]          -> S
\``[0]\\[1]\\\``[2][0]`[1][0] -> ``S``SI`KS`KK

Esolanging Fruit

Posted 2017-03-05T23:51:13.323

Reputation: 13 542



– Christian Sievers – 2017-03-06T01:08:24.437

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


– FUZxxl – 2017-03-06T16:14:56.327

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 – 2018-06-12T13:25:21.367

@BarbaraKwarc Right, I meant SII, not SKK. That was a mistake. – Esolanging Fruit – 2018-06-12T17:06:21.593

For 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]EFequivalent toλw.wEFinstead of toλw.wFE`? – r.e.s. – 2019-06-19T15:50:26.227



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"

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

Christian Sievers

Posted 2017-03-05T23:51:13.323

Reputation: 6 366


  • 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 – 2017-03-06T05:06:51.977

    1Actually, 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 – 2017-03-06T05:15:09.770

    1Try it online! for your current version. Which by the way is only 236 bytes, you can drop the final newline. – Ørjan Johansen – 2017-03-06T05:23:09.047

    1Try it online! with my suggestions. – Ørjan Johansen – 2017-03-06T05:29:26.210

    How come all my λ-calculus problems are solved in Haskell? Does it have some λ-expression manipulation capabilities? – Esolanging Fruit – 2017-03-06T06:05:09.433

    2@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 – 2017-03-06T09:43:26.857

    @Challenger5 I agree with Leo, plus your sample size is not that big. Stateless parsing doesn't help golfing, a concise notation for algebraic data types does (but that's not used in the other challenge). – Christian Sievers – 2017-03-06T10:54:43.033

    2You 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 – 2017-03-06T16:06:36.983