O cálculo SKI é uma variante do cálculo Lambda que não usa expressões lambda. Em vez disso, apenas o aplicativo e os combinadores S , K e I são usados. Nesse desafio, sua tarefa é converter os termos de SKI em termos do Lambda na forma normal β .

Especificação de entrada

A entrada é um termo SKI na seguinte representação textual. Você pode optar por receber uma nova linha opcional à direita. A entrada é composto por caracteres S, K, I, (, e )e satisfaz a seguinte gramática (em forma ABNF) com stermsendo o símbolo inicial:

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

Especificação de saída

A saída é um termo lambda sem variáveis ​​livres na seguinte representação textual. Você pode optar por gerar uma nova linha à direita opcional. A saída deve satisfazer a seguinte gramática no formato ABNF, ltermsendo o símbolo inicial:

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

Restrições

Você pode assumir que a entrada possui uma forma normal β. Você pode supor que a forma normal β use no máximo 26 variáveis ​​diferentes. Você pode assumir que entrada e saída são representáveis ​​em 79 caracteres.

Entradas de Amostra

Aqui estão algumas entradas de amostra. A saída é uma saída possível para a entrada especificada.

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

Pontuação

A solução mais curta em octetos vence. Falhas comuns são proibidas.

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]

Experimente online!

Como funciona

Este é um front-end de analisador diferente da minha resposta para "Escreva um intérprete para o cálculo lambda não digitado " , que também possui uma versão não destruída com documentação.

Resumidamente, Term = T (Char -> String)é o tipo de termos de cálculo lambda, que sabe como se aplicar a outros termos ( a :: Term -> Term -> Term) e como se exibir como a String( (%) :: Term -> Char -> String), dada uma variável nova inicial como a Char. Podemos converter uma função em termos para um termo com l :: (Term -> Term) -> Terme, como a aplicação do termo resultante simplesmente chama a função ( a (l f) == f), os termos são automaticamente reduzidos à forma normal quando exibidos.

Ruby, 323 bytes

Não acredito que esse pedaço de porcaria funcione:

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 a substituição de regex para executar a redução de β em strings brutas é algo do Tony-the-Pony. No entanto, sua saída parece correta, pelo menos, para casos de teste fáceis:

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

Aqui está como lidar K(K(K(KK)))com alguma saída de depuração, que leva cerca de 7 segundos no meu laptop, porque a recursão da expressão regular é lenta . Você pode ver sua conversão α em ação!

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

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):%,&=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: depois while 1:, três linhas são recuadas com um caractere de tabulação.

Este é basicamente o código por trás do http://ski.aditsu.net/ , traduzido para python, bastante simplificado e com muita ação.

Referência: (isso provavelmente é menos útil agora que o código está compactado)

V = termo variável
A = termo de aplicação
L = termo lambda
c = contador de variável
p = substituir variável pelo termo
r = reduzir
m = renumeração final da variável
u = renumeração interna da variável (para termos duplicados)
s = conversão de string
(parâmetro s = self)
C = caractere (s) separador (s) para conversão de string
I, K, S: combinadores
E = analisar

Exemplos:

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

(isto ↑ é esperado porque SII(SII)é irredutível)

Obrigado Mauris e Sp3000 por ajudar a matar um monte de bytes :)

Lisp comum, 560 bytes

"Finalmente, encontrei um 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))))))

Ungolfed

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

Redução beta

As variáveis ​​são ligadas dinamicamente durante a redução com os PROGVnovos símbolos Common Lisp, usando MAKE-SYMBOL. Isso permite evitar bem as colisões de nomes (por exemplo, sombreamento indesejável de variáveis ​​associadas). Eu poderia ter usado GENSYM, mas queremos ter nomes fáceis de usar para símbolos. É por isso que os símbolos são nomeados com letras de aaté z(conforme permitido pela pergunta). Nrepresenta o código de caractere da próxima letra disponível no escopo atual e começa com 97, também conhecido como a.

Aqui está uma versão mais legível de R(sem a 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 intermediários

Analisar a partir da 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))))))

Reduzir:

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

(Veja traço de execução)

Pretty-print:

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

Testes

Eu reutilizo o mesmo conjunto de testes que a resposta do 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

O oitavo exemplo de teste é muito grande para a tabela acima:

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 Atualizei minha resposta para ter o mesmo comportamento de agrupamento da resposta do aditsu , porque custa menos bytes para escrever.
• A diferença restante pode ser visto para testes 6 e 8. O resultado a.a.a.a.a.b.aestá correcta e não usam tanto letras como a resposta do Python, onde as ligações a a, b, ce dnão são referenciados.

atuação

O loop nos 7 testes aprovados acima e a coleta dos resultados são imediatos (saída da 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

Fazer o mesmo teste centenas de vezes leva a ... "Armazenamento local de threads esgotado" na SBCL, devido a uma limitação conhecida em relação a variáveis ​​especiais. Com o CCL, chamar a mesma suíte de testes 10000 vezes leva 3,33 segundos.