The SKI calculus is a variant of the Lambda calculus that doesn't use lambda expressions. Instead, only application and the combinators S, K, and I are used. In this challenge, your task is to translate SKI terms into Lambda terms in β normal form.

Input Specification

The input is an SKI term in the following textual representation. You may choose to receive an optional trailing newline. The input is composed of the characters S, K, I, (, and ) and satisfies the following grammar (in ABNF form) with sterm being the start symbol:

sterm = sterm combinator     ; application
sterm = combinator           ;
sterm = '(' sterm ')'        ; grouping
combinator = 'S' | 'K' | 'I' ; primitives

Output Specification

The output is a lambda term with no free variables in the following textual representation. You may choose to output an optional trailing newline. The output shall satisfy the following grammar in ABNF form with lterm being the start symbol:

lterm   = lterm operand     ; application
lterm   = ALPHA '.' lterm   ; lambda
lterm   = operand
operand = '(' lterm ')'     ; grouping
operand = ALPHA             ; variable (a letter)


You may assume that the input has a β normal form. You may assume that the β normal form uses at most 26 different variables. You may assume that both input and output are representable in 79 characters.

Sample inputs

Here are a couple of sample inputs. The output is one possible output for the given input.

input                        output
I                            a.a
SKK                          a.a
KSK                          a.b.c.ac(bc)
SII                          a.aa


The shortest solution in octets wins. Common loopholes are prohibited.

  • 12
    \$\begingroup\$ +1 because I assume this is a cool challenge; I didn't understand a word of it. \$\endgroup\$
    – Alex A.
    Commented Jul 16, 2015 at 18:40
  • 3
    \$\begingroup\$ Ah, I should golf my ski.aditsu.net :) \$\endgroup\$ Commented Jul 16, 2015 at 18:54
  • \$\begingroup\$ You should probably state that both sterm and lterm use left-associativity when brackets are missing. \$\endgroup\$ Commented Jul 16, 2015 at 20:22
  • \$\begingroup\$ @PeterTaylor Better this way? \$\endgroup\$
    – FUZxxl
    Commented Jul 16, 2015 at 20:33
  • \$\begingroup\$ No, I think that's actually wrong: following that changed grammar I would parse SKI as S(KI). \$\endgroup\$ Commented Jul 17, 2015 at 6:58

4 Answers 4


Ruby, 323 bytes

I can't believe this piece of crap works at all:

s=$`;t=$';abort z.gsub(/\w1*0/){|x|h[x]=h[x]||(f+=1).chr}if !t

Using regex substitution to perform β-reduction on raw strings is some Tony-the-Pony stuff. Nonetheless, its output looks correct at least for easy testcases:

$ echo 'I' | ruby ski.rb
$ echo 'SKK' | ruby ski.rb
$ echo 'KSK' | ruby ski.rb
$ echo 'SII' | ruby ski.rb

Here's it handling K(K(K(KK))) with some debug output, which takes about 7 seconds on my laptop, because regular expression recursion is slow. You can see its α-conversion in action!

$ echo 'K(K(K(KK)))' | ruby ski.rb
  • \$\begingroup\$ I get: ski.rb:4:in `gsub': wrong argument type nil (expected Regexp) (TypeError) with the 'I' example \$\endgroup\$ Commented Jul 17, 2015 at 20:24
  • \$\begingroup\$ Should be fixed now! I had already corrected it locally, but forgot to edit my post. \$\endgroup\$
    – lynn
    Commented Jul 17, 2015 at 20:25
  • 2
    \$\begingroup\$ Ok, it's s........l.......................o...........w, but it seems to work.... eventually :) I think the result for S(K(SI))K is not correct though. \$\endgroup\$ Commented Jul 17, 2015 at 20:38

Python 2, 674

exec u"""import sys
$ V#):%=V.c;V.c+=1
 def m(s,x):%=min(%,x);-(%==x)+x
$ A#,*x):%,&=x
 def r(s):x=%.r();y=&.r();-x.b.p(x.a,y).r()if'L'in`x`else s.__$__/
$ L(A):C='.';u!,d:L(d.setdefault(%,V()),&.u(d))
def E():
 while 1:
    if q in')\\n':-t
print t.s()""".translate({33:u'=lambda s',35:u':\n def __init__(s',36:u'class',37:u's.a',38:u's.b',45:u'return ',47:u'(x,y)'})

Note: after while 1:, 3 lines are indented with a tab character.

This is basically the code behind http://ski.aditsu.net/ , translated to python, greatly simplified and heavily golfed.

Reference: (this is probably less useful now that the code is compressed)

V = variable term
A = application term
L = lambda term
c = variable counter
p = replace variable with term
r = reduce
m = final variable renumbering
u = internal variable renumbering (for duplicated terms)
s = string conversion
(parameter s = self)
C = separator character(s) for string conversion
I,K,S: combinators
E = parse


python ski.py <<< "KSK"
python ski.py <<< "SII"        
python ski.py <<< "SS(SS)(SS)"
python ski.py <<< "S(K(SI))K" 
python ski.py <<< "S(S(KS)K)I"                   
python ski.py <<< "S(S(KS)K)(S(S(KS)K)I)"        
python ski.py <<< "K(K(K(KK)))"
python ski.py <<< "SII(SII)"
RuntimeError: maximum recursion depth exceeded

(this ↑ is expected because SII(SII) is irreducible)

Thanks Mauris and Sp3000 for helping to kill a bunch of bytes :)

  • 1
    \$\begingroup\$ I'm pretty sure you can turn def m(a,b,c):return foo into m=lambda a,b,c:foo even inside classes, which might save you lots of bytes. \$\endgroup\$
    – lynn
    Commented Jul 17, 2015 at 20:22
  • \$\begingroup\$ @Mauris thanks for the tip :) \$\endgroup\$ Commented Jul 17, 2015 at 20:50
  • \$\begingroup\$ I fail to read a.b.c.a(c)(b(c)) as a valid lambda expression: what is (c)? \$\endgroup\$
    – coredump
    Commented Jul 21, 2015 at 13:49
  • \$\begingroup\$ @coredump it's an operand with unnecessary grouping... and you're right, it doesn't exactly match the OP's grammar rules. I wonder how important it is; I'll ask. \$\endgroup\$ Commented Jul 21, 2015 at 17:35
  • \$\begingroup\$ @coredump It should be ok now with the updated grammar. \$\endgroup\$ Commented Jul 21, 2015 at 19:10

Haskell, 232 bytes

data T s=T{a::T s->T s,(%)::s}
i d=T(i. \x v->d v++'(':x%v++")")d
l f=f`T`\v->v:'.':f(i(\_->[v]))%succ v
b"S"x=l$l.(a.a x<*>).a
p?'('=l id:p
(p:q:r)?')'=a q p:r
(p:q)?v=a p(l$b[v]):q
((%'a')=<<).foldl(?)[l id]

Try it online!

How it works

This is a different parser frontend to my answer to “Write an interpreter for the untyped lambda calculus”, which also has an ungolfed version with documentation.

Briefly, Term = T (Char -> String) is the type of lambda calculus terms, which know how to apply themselves to other terms (a :: Term -> Term -> Term) and how to display themselves as a String ((%) :: Term -> Char -> String), given an initial fresh variable as a Char. We can convert a function on terms to a term with l :: (Term -> Term) -> Term, and because application of the resulting term simply calls the function (a (l f) == f), terms are automatically reduced to normal form when displayed.


Common Lisp, 560 bytes

"Finally, I found a use for PROGV."

(macrolet((w(S Z G #1=&optional(J Z))`(if(symbolp,S),Z(destructuring-bind(a b #1#c),S(if(eq a'L),G,J)))))(labels((r(S #1#(N 97))(w S(symbol-value s)(let((v(make-symbol(coerce`(,(code-char N))'string))))(progv`(,b,v)`(,v,v)`(L,v,(r c(1+ n)))))(let((F(r a N))(U(r b N)))(w F`(,F,U)(progv`(,b)`(,U)(r c N))))))(p()(do((c()(read-char()()#\)))q u)((eql c #\))u)(setf q(case c(#\S'(L x(L y(L z((x z)(y z))))))(#\K'(L x(L u x)))(#\I'(L a a))(#\((p)))u(if u`(,u,q)q))))(o(S)(w S(symbol-name S)(#2=format()"~A.~A"b(o c))(#2#()"~A(~A)"(o a)(o b)))))(lambda()(o(r(p))))))


;; Bind S, K and I symbols to their lambda-calculus equivalent.
;; L means lambda, and thus:
;; -  (L x S) is variable binding, i.e. "x.S"
;; -  (F x)   is function application

(define-symbol-macro S '(L x (L y (L z ((x z) (y z))))))
(define-symbol-macro K '(L x (L u x)))
(define-symbol-macro I '(L x x))

;; helper macro: used twice in R and once in O

(defmacro w (S sf lf &optional(af sf))
  `(if (symbolp ,S) ,sf
       (destructuring-bind(a b &optional c) ,S
         (if (eq a 'L)

;; R : beta-reduction

(defun r (S &optional (N 97))
  (w S
      (symbol-value s)
      (let ((v(make-symbol(make-string 1 :initial-element(code-char N)))))
              `(L ,v ,(r c (1+ n)))))
      (let ((F (r a N))
            (U (r b N)))
        (w F`(,F,U)(progv`(,b)`(,U)(r c N))))))

;; P : parse from stream to lambda tree

(defun p (&optional (stream *standard-output*))
  (loop for c = (read-char stream nil #\))
        until (eql c #\))
        for q = (case c (#\S S) (#\K K) (#\I I) (#\( (p stream)))
        for u = q then `(,u ,q)
        finally (return u)))

;; O : output lambda forms as strings

(defun o (S)
  (w S
      (princ-to-string S)
      (format nil "~A.~A" b (o c))
      (format nil (w b "(~A~A)" "(~A(~A))") (o a) (o b))))


Variables are dynamically bound during reduction with PROGV to new Common Lisp symbols, using MAKE-SYMBOL. This allows to nicely avoid naming collisions (e.g. undesired shadowing of bound variables). I could have used GENSYM, but we want to have user-friendly names for symbols. That is why symbols are named with letters from a to z (as allowed by the question). N represents the character code of the next available letter in current scope and starts with 97, a.k.a. a.

Here is a more readable version of R (without the W macro):

(defun beta-reduce (S &optional (N 97))
  (if (symbolp s)
      (symbol-value s)
      (if (eq (car s) 'L)
          ;; lambda
          (let ((v (make-symbol (make-string 1 :initial-element (code-char N)))))
            (progv (list (second s) v)(list v v)
              `(L ,v ,(beta-reduce (third s) (1+ n)))))
          (let ((fn (beta-reduce (first s) N))
                (arg (beta-reduce (second s) N)))
            (if (and(consp fn)(eq'L(car fn)))
                (progv (list (second fn)) (list arg)
                  (beta-reduce (third fn) N))
                `(,fn ,arg))))))

Intermediate results

Parse from string:

CL-USER> (p (make-string-input-stream "K(K(K(KK)))"))
((L X (L U X)) ((L X (L U X)) ((L X (L U X)) ((L X (L U X)) (L X (L U X))))))


CL-USER> (r *)
(L #:|a| (L #:|a| (L #:|a| (L #:|a| (L #:|a| (L #:|b| #:|a|))))))

(See trace of execution)


CL-USER> (o *)


I reuse the same test suite as the Python answer:

        Input                    Output              Python output (for comparison)

   1.   KSK                      a.b.c.a(c)(b(c))    a.b.c.a(c)(b(c))              
   2.   SII                      a.a(a)              a.a(a)                        
   3.   S(K(SI))K                a.b.b(a)            a.b.b(a)                      
   4.   S(S(KS)K)I               a.b.a(a(b))         a.b.a(a(b))                   
   5.   S(S(KS)K)(S(S(KS)K)I)    a.b.a(a(a(b)))      a.b.a(a(a(b)))                
   6.   K(K(K(KK)))              a.a.a.a.a.b.a       a.b.c.d.e.f.e 
   7.   SII(SII)                 ERROR               ERROR

The 8th test example is too large for the table above:

8.      SS(SS)(SS)
CL      a.b.a(b)(c.b(c)(a(b)(c)))(a(b.a(b)(c.b(c)(a(b)(c))))(b))      
Python  a.b.a(b)(c.b(c)(a(b)(c)))(a(d.a(d)(e.d(e)(a(d)(e))))(b))
  • EDIT I updated my answer in order to have the same grouping behavior as in aditsu's answer, because it costs less bytes to write.
  • The remaining difference can be seen for tests 6 and 8. The result a.a.a.a.a.b.a is correct and does not use as much letters as the Python answer, where bindings to a, b, c and d are not referenced.


Looping over the 7 passing tests above and collecting the results is immediate (SBCL output):

Evaluation took:
  0.000 seconds of real time
  0.000000 seconds of total run time (0.000000 user, 0.000000 system)
  100.00% CPU
  310,837 processor cycles
  129,792 bytes consed

Doing the same test a hundred of times lead to ... "Thread local storage exhausted" on SBCL, due to a known limitation regarding special variables. With CCL, calling the same test suite 10000 times takes 3.33 seconds.

  • \$\begingroup\$ That's a neat solution! \$\endgroup\$
    – FUZxxl
    Commented Jul 22, 2015 at 10:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.