El cálculo SKI es una variante del cálculo Lambda que no utiliza expresiones lambda. En cambio, solo se utilizan la aplicación y los combinadores S , K y yo . En este desafío, su tarea es traducir los términos de SKI en términos de Lambda en forma normal β .

Especificación de entrada

La entrada es un término SKI en la siguiente representación textual. Puede elegir recibir una nueva línea final opcional. La entrada se compone de los caracteres S, K, I, (, y )y satisface la siguiente gramática (en forma ABNF) con stermser el símbolo de inicio:

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

Especificación de salida

La salida es un término lambda sin variables libres en la siguiente representación textual. Puede optar por generar una nueva línea final opcional. La salida deberá satisfacer la siguiente gramática en forma ABNF con ltermel símbolo de inicio:

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

Restricciones

Puede suponer que la entrada tiene una forma normal β. Puede suponer que la forma normal β utiliza como máximo 26 variables diferentes. Puede suponer que tanto la entrada como la salida son representables en 79 caracteres.

Entradas de muestra

Aquí hay un par de entradas de muestra. La salida es una salida posible para la entrada dada.

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

Tanteo

La solución más corta en octetos gana. Las lagunas comunes están prohibidas.

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
b"K"x=l(\_->x)
b"I"x=x
p?'('=l id:p
(p:q:r)?')'=a q p:r
(p:q)?v=a p(l$b[v]):q
((%'a')=<<).foldl(?)[l id]

Pruébalo en línea!

Cómo funciona

Esta es una interfaz de analizador diferente a mi respuesta a "Escribir un intérprete para el cálculo lambda sin tipo" , que también tiene una versión no documentada con documentación.

Brevemente, Term = T (Char -> String)es el tipo de términos de cálculo lambda, que saben cómo aplicarse a otros términos (a :: Term -> Term -> Term ) y cómo mostrarse como a String( (%) :: Term -> Char -> String), dada una nueva variable inicial como a Char. Podemos convertir una función en términos en un término con l :: (Term -> Term) -> Term, y debido a que la aplicación del término resultante simplemente llama a la función ( a (l f) == f), los términos se reducen automáticamente a la forma normal cuando se muestran.

Rubí, 323 bytes.

No puedo creer que esta mierda funcione en absoluto:

h={};f=96;z=gets.chop
{?S=>'s0.t0.u0.s0u0(t0u0)',?K=>'k0.l0.k0',?I=>'i0.i0'}.each{|k,v|z.gsub!k,?(+v+?)}
loop{z=~/\((?<V>\w1*0)\.(?<A>(?<B>\w1*0|[^()]|\(\g<B>+\))+)\)(?<X>\g<B>)/
s=$`;t=$';abort z.gsub(/\w1*0/){|x|h[x]=h[x]||(f+=1).chr}if !t
z=$`+?(+$~[?A].gsub($~[?V],$~[?X].gsub(/\w1*0/){|a|s[a]?a:a.gsub(?0,'10')})+?)+t}

Usar la sustitución de expresiones regulares para realizar la reducción β en cadenas sin procesar es algo de Tony-the-Pony. No obstante, su salida parece correcta al menos para casos de prueba fáciles:

$ echo 'I' | ruby ski.rb
(a.a)
$ echo 'SKK' | ruby ski.rb
(a.(a))
$ echo 'KSK' | ruby ski.rb
((a.b.c.ac(bc)))
$ echo 'SII' | ruby ski.rb
(a.(a)((a)))

Aquí está manejando K(K(K(KK)))con algún resultado de depuración, que toma alrededor de 7 segundos en mi computadora portátil, porque la recursividad de expresión regular es lenta . ¡Puedes ver su conversión α en acción!

$ echo 'K(K(K(KK)))' | ruby ski.rb
"(l0.((k10.l10.k10)((k10.l10.k10)((k10.l10.k10)(k10.l10.k10)))))"
"(l0.((l10.((k110.l110.k110)((k110.l110.k110)(k110.l110.k110))))))"
"(l0.((l10.((l110.((k1110.l1110.k1110)(k1110.l1110.k1110)))))))"
"(l0.((l10.((l110.((l1110.(k11110.l11110.k11110))))))))"
(a.((b.((c.((d.(e.f.e))))))))

Pitón 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):%,&=x
 C='()';p!,x,y:s.__$__(%.p/,&.p/);m!,x:&.m(%.m(x));u!,d:A(%.u(d),&.u(d));s!:%.s()+s.C[0]+&.s()+s.C[1:]
 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))
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)'})

Nota: después while 1: , 3 líneas se sangran con un carácter de tabulación.

Este es básicamente el código detrás de http://ski.aditsu.net/ , traducido a python, muy simplificado y muy golfizado.

Referencia: (esto probablemente sea menos útil ahora que el código está comprimido)

V = término variable
A = término de aplicación
L = término lambda
c = contador variable
p = reemplazar variable con término
r = reducir
m = renumeración de variable final
u = renumeración de variable interna (para términos duplicados)
s = conversión de cadena
(parámetro s = auto)
C = caracteres separadores para la conversión de cadenas
I, K, S: combinadores
E = análisis

Ejemplos:

python ski.py <<< "KSK"
a.b.c.a(c)(b(c))
python ski.py <<< "SII"        
a.a(a)
python ski.py <<< "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 <<< "S(K(SI))K" 
a.b.b(a)
python ski.py <<< "S(S(KS)K)I"                   
a.b.a(a(b))
python ski.py <<< "S(S(KS)K)(S(S(KS)K)I)"        
a.b.a(a(a(b)))
python ski.py <<< "K(K(K(KK)))"
a.b.c.d.e.f.e
python ski.py <<< "SII(SII)"
[...]
RuntimeError: maximum recursion depth exceeded

(se espera este ↑ porque SII(SII) es irreducible)

Gracias Mauris y Sp3000 por ayudar a matar un montón de bytes :)

Lisp común, 560 bytes

"Finalmente, encontré un uso para 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))))))

Sin golf

;; 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)
             ,lf
             ,af))))

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

Beta-reducción

Las variables se enlazan dinámicamente durante la reducción con los PROGVnuevos símbolos Common Lisp, usando MAKE-SYMBOL. Esto permite evitar muy bien las colisiones de nombres (por ejemplo, sombreado no deseado de variables enlazadas). Podría haberlo usado GENSYM, pero queremos tener nombres fáciles de usar para los símbolos. Es por eso que los símbolos se nombran con letras de aa z(según lo permitido por la pregunta). Nrepresenta el código de caracteres de la siguiente letra disponible en el alcance actual y comienza con 97, también conocido comoa .

Aquí hay una versión más legible de R(sin la Wmacro):

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

Resultados intermedios

Analizar desde la cuerda:

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

Reducir:

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

(Ver rastro de ejecución)

Bonito estampado:

CL-USER> (o *)
"a.a.a.a.a.b.a"

Pruebas

Reutilizo el mismo conjunto de pruebas que la respuesta de Python:

        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

El octavo ejemplo de prueba es demasiado grande para la tabla anterior:

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

• EDITAR He actualizado mi respuesta para tener el mismo comportamiento de agrupación que en la respuesta de aditsu , porque cuesta menos bytes escribir.
• La diferencia restante se puede ver por los tests 6 y 8. El resultado a.a.a.a.a.b.aes correcto y no utiliza tanto las letras como la respuesta Python, donde a las consolidaciones a, b, cy dno se hace referencia.

Actuación

Recorrer las 7 pruebas de aprobación anteriores y recopilar los resultados es inmediato (salida SBCL):

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

Hacer la misma prueba cientos de veces conduce a ... "Almacenamiento local de subprocesos agotado" en SBCL, debido a una limitación conocida con respecto a variables especiales. Con CCL, llamar al mismo conjunto de pruebas 10000 veces lleva 3,33 segundos.