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 &beta; 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)


Constraints

You may assume that the input has a &beta; normal form. You may assume that the &beta; 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


Scoring

The shortest solution in octets wins. Common loopholes are prohibited.
Python 2, 674



exec u"""import sys
$ V#):%=V.c;V.c+=1
 c=97;p!,v,t:[s,t.u({})][v==s];r!:s;u!,d:d.get(s,s);s!:chr(%)
 def m(s,x):%=min(%,x);-(%==x)+x
$ A#,*x):%,&amp;=x
 C='()';p!,x,y:s.__$__(%.p/,&amp;.p/);m!,x:&amp;.m(%.m(x));u!,d:A(%.u(d),&amp;.u(d));s!:%.s()+s.C[0]+&amp;.s()+s.C[1:]
 def r(s):x=%.r();y=&amp;.r();-x.b.p(x.a,y).r()if'L'in`x`else s.__$__/
$ L(A):C='.';u!,d:L(d.setdefault(%,V()),&amp;.u(d))
x=V();y=V();z=V()
I=L(x,x)
K=L(y,L/)
S=L(x,L(z,L(y,A(A/,A(z,y)))))
def E():
 t=I
 while 1:
    q=sys.stdin.read(1)
    if q in')\\n':-t
    t=A(t,eval(max(q,'E()')).u({}))
t=E().r()
t.m(97)
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

Examples:

python ski.py &lt;&lt;&lt; "KSK"
a.b.c.a(c)(b(c))
python ski.py &lt;&lt;&lt; "SII"        
a.a(a)
python ski.py &lt;&lt;&lt; "SS(SS)(SS)"
a.b.a(b)(c.b(c)(a(b)(c)))(a(d.a(d)(e.d(e)(a(d)(e))))(b))
python ski.py &lt;&lt;&lt; "S(K(SI))K" 
a.b.b(a)
python ski.py &lt;&lt;&lt; "S(S(KS)K)I"                   
a.b.a(a(b))
python ski.py &lt;&lt;&lt; "S(S(KS)K)(S(S(KS)K)I)"        
a.b.a(a(a(b)))
python ski.py &lt;&lt;&lt; "K(K(K(KK)))"
a.b.c.d.e.f.e
python ski.py &lt;&lt;&lt; "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 :)