Der SKI-Kalkül ist eine Variante des Lambda-Kalküls, die keine Lambda-Ausdrücke verwendet. Stattdessen werden nur application und die Kombinatoren S , K und I verwendet. In dieser Herausforderung besteht Ihre Aufgabe darin, SKI-Begriffe in β-Normalform in Lambda-Begriffe zu übersetzen .

Eingangsspezifikation

Die Eingabe ist ein SKI-Begriff in der folgenden Textdarstellung. Sie können sich dafür entscheiden, eine optionale nachgestellte Zeile zu erhalten. Die Eingabe wird von den Zeichen zusammengesetzt ist S, K, I, (, und , )und erfüllt die folgende Grammatik (in ABNF Form) zusammen mit stermdem Startsymbol ist durch :

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

Ausgangsspezifikation

Die Ausgabe ist ein Lambda-Term ohne freie Variablen in der folgenden Textdarstellung. Sie können eine optionale nachgestellte Newline ausgeben. Die Ausgabe muss der folgenden Grammatik in ABNF-Form ltermals Startsymbol entsprechen:

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

Einschränkungen

Sie können davon ausgehen, dass die Eingabe eine β-Normalform hat. Sie können davon ausgehen, dass die β-Normalform höchstens 26 verschiedene Variablen verwendet. Sie können davon ausgehen, dass sowohl Eingabe als auch Ausgabe in 79 Zeichen darstellbar sind.

Beispieleingaben

Hier sind einige Beispieleingaben. Die Ausgabe ist eine mögliche Ausgabe für die angegebene Eingabe.

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

Wertung

Die kürzeste Lösung in Oktetten gewinnt. Gemeinsame Schlupflöcher sind verboten.

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]

Probieren Sie es online!

Wie es funktioniert

Dies ist ein anderes Parser-Frontend als meine Antwort auf "Schreibe einen Interpreter für den untypisierten Lambda-Kalkül" , der auch eine ungolfed-Version mit Dokumentation enthält.

Kurz gesagt, Term = T (Char -> String)ist die Art der Lambda-Kalkül-Terme, die wissen, wie sie sich auf andere Terme anwenden ( a :: Term -> Term -> Term) und wie sie sich als String( (%) :: Term -> Char -> String) darstellen, eine anfängliche frische Variable als gegeben Char. Wir können eine Funktion für Terme in einen Term mit konvertieren l :: (Term -> Term) -> Term, und da die Anwendung des resultierenden Terms einfach die function ( a (l f) == f) aufruft , werden Terme bei der Anzeige automatisch auf die normale Form reduziert.

Ruby, 323 Bytes

Ich kann nicht glauben, dass dieses Stück Mist überhaupt funktioniert:

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}

Die Verwendung der Regex-Substitution zur Durchführung der β-Reduktion an rohen Saiten ist eine Sache von Tony-the-Pony. Dennoch sieht die Ausgabe zumindest für einfache Testfälle korrekt aus:

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

Hier ist die Handhabung K(K(K(KK)))mit einer Debug-Ausgabe, die auf meinem Laptop etwa 7 Sekunden dauert, da die Rekursion von regulären Ausdrücken langsam ist . Sie können die α-Umwandlung in Aktion sehen!

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

Hinweis: nach while 1: werden 3 Zeilen mit einem Tabulatorzeichen eingerückt.

Dies ist im Grunde der Code hinter http://ski.aditsu.net/ , übersetzt in Python, stark vereinfacht und stark golfen.

Referenz: (Dies ist wahrscheinlich weniger nützlich, da der Code jetzt komprimiert ist.)

V = variable Term
A = application Term
L = Lambda Begriff
c = variable Zähler
p = ersetzen Variable mit Term
r = reduzieren
m = final variable Umnummerieren
u interne Variable = Umnummerieren (für duplizierten Bedingungen)
s = string Umwandlung
(Parameter s = self)
C = Trennzeichen für die String-Konvertierung
I, K, S: Kombinatoren
E = parsen

Beispiele:

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

(Dieses ↑ wird erwartet, weil SII(SII)es nicht reduzierbar ist.)

Vielen Dank an Mauris und Sp3000, die geholfen haben, ein paar Bytes zu töten :)

Common Lisp, 560 Bytes

"Endlich habe ich eine Verwendung für gefunden 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))))

Beta-Reduktion

Variablen werden beim Reduzieren dynamisch mit PROGVneuen Common-Lisp-Symbolen verknüpft MAKE-SYMBOL. Dadurch können Namenskollisionen (zB unerwünschtes Abschatten gebundener Variablen) vermieden werden. Ich hätte es gebrauchen können GENSYM, aber wir möchten benutzerfreundliche Namen für Symbole haben. Deshalb werden Symbole mit Buchstaben von abis benannt z(wie in der Frage erlaubt). NStellt den Zeichencode des nächsten verfügbaren Buchstabens im aktuellen Bereich dar und beginnt mit 97, akaa .

Hier ist eine besser lesbare Version von R(ohne das WMakro):

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

Zwischenergebnisse

Analysieren von Zeichenfolge:

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

Reduzieren:

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

(Siehe Hinrichtungsspur)

Pretty-Print:

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

Tests

Ich verwende dieselbe Testsuite wie die Python-Antwort:

        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

Das 8. Testbeispiel ist zu groß für die obige Tabelle:

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

• BEARBEITEN Ich habe meine Antwort aktualisiert, um dasselbe Gruppierungsverhalten wie in der Antwort von aditsu zu erzielen , da das Schreiben weniger Bytes kostet.
• Die verbleibende Differenz kann für Tests zu sehen 6 und 8. Das Ergebnis a.a.a.a.a.b.akorrekt ist und nicht so viele Buchstaben wie die Python Antwort zu verwenden, wo Bindungen a, b, cund dsind nicht referenziert.

Performance

Das Durchlaufen der oben genannten 7 bestandenen Tests und das Sammeln der Ergebnisse erfolgt sofort (SBCL-Ausgabe):

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

Hundertmaliges Durchführen desselben Tests hat zur Folge, dass der lokale Thread-Speicher in SBCL aufgrund einer bekannten Einschränkung in Bezug auf spezielle Variablen erschöpft ist. Mit CCL dauert das 10000-malige Aufrufen derselben Testsuite 3,33 Sekunden.