Optimizing SKI compiler



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.


Posted 2015-07-16T18:27:25.037

Reputation: 9 656

7+1 because I assume this is a cool challenge; I didn't understand a word of it. – Alex A. – 2015-07-16T18:40:09.177

2Ah, I should golf my ski.aditsu.net :) – aditsu quit because SE is EVIL – 2015-07-16T18:54:55.130

You should probably state that both sterm and lterm use left-associativity when brackets are missing. – Peter Taylor – 2015-07-16T20:22:49.003

@PeterTaylor Better this way? – FUZxxl – 2015-07-16T20:33:17.583

No, I think that's actually wrong: following that changed grammar I would parse SKI as S(KI). – Peter Taylor – 2015-07-17T06:58:32.323

@PeterTaylor That's right. Let me fix it once again. – FUZxxl – 2015-07-17T07:00:04.807

Shouldn't the rule for lambdas in the output grammar be lterm = ALPHA '.' lterm? I don't think (ab).c should be valid. – Lynn – 2015-07-17T18:21:20.963

@Mauris You are right. Grammar is my weak spot. – FUZxxl – 2015-07-17T19:45:38.243

Do you also accept lterm = ALPHA or operand = '(' ALPHA ')' ? Or are they invalid? – aditsu quit because SE is EVIL – 2015-07-21T17:38:05.420

@aditsu Yes. I fixed the grammar. – FUZxxl – 2015-07-21T18:15:26.633



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.

Anders Kaseorg

Posted 2015-07-16T18:27:25.037

Reputation: 29 242


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 :)

aditsu quit because SE is EVIL

Posted 2015-07-16T18:27:25.037

Reputation: 22 326

1I'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. – Lynn – 2015-07-17T20:22:23.960

@Mauris thanks for the tip :) – aditsu quit because SE is EVIL – 2015-07-17T20:50:41.117

I fail to read a.b.c.a(c)(b(c)) as a valid lambda expression: what is (c)? – coredump – 2015-07-21T13:49:33.283

@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. – aditsu quit because SE is EVIL – 2015-07-21T17:35:45.720

@coredump It should be ok now with the updated grammar. – aditsu quit because SE is EVIL – 2015-07-21T19:10:51.617


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


Posted 2015-07-16T18:27:25.037

Reputation: 55 648

I get: ski.rb:4:in `gsub': wrong argument type nil (expected Regexp) (TypeError) with the 'I' example – aditsu quit because SE is EVIL – 2015-07-17T20:24:05.890

Should be fixed now! I had already corrected it locally, but forgot to edit my post. – Lynn – 2015-07-17T20:25:35.130

2Ok, 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. – aditsu quit because SE is EVIL – 2015-07-17T20:38:44.503


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.


Posted 2015-07-16T18:27:25.037

Reputation: 6 292

That's a neat solution! – FUZxxl – 2015-07-22T10:01:18.397

@FUZxxl Thanks! – coredump – 2015-07-22T11:54:31.627