SKI rachunek jest wariant rachunku lambda, która nie używać wyrażeń lambda. Zamiast tego używana jest tylko aplikacja i kombinatory S , K i I. W tym wyzwaniu Twoim zadaniem jest przetłumaczenie terminów SKI na terminy Lambda w postaci β normalnej .

Specyfikacja wejściowa

Dane wejściowe to termin SKI w następującej reprezentacji tekstowej. Możesz zdecydować się na opcjonalny końcowy znak nowej linii. Sygnał wejściowy składa się z postaci S, K, I, (i )i spełnia następujące gramatyczne (w postaci ABNF) przy stermczym symbol start:

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

Specyfikacja wyjściowa

Dane wyjściowe to termin lambda bez wolnych zmiennych w następującej reprezentacji tekstowej. Możesz zdecydować się na wydrukowanie opcjonalnego końcowego znaku nowej linii. Wyjście powinno spełniać następującą gramatykę w formie ABNF, ltermbędąc symbolem początkowym:

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

Ograniczenia

Możesz założyć, że dane wejściowe mają postać β normalną. Możesz założyć, że postać normalna β wykorzystuje maksymalnie 26 różnych zmiennych. Możesz założyć, że zarówno dane wejściowe, jak i wyjściowe są reprezentowalne w 79 znakach.

Przykładowe dane wejściowe

Oto kilka przykładowych danych wejściowych. Wyjście jest jednym możliwym wyjściem dla danego wejścia.

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

Punktacja

Najkrótsze rozwiązanie w oktetach wygrywa. Częste luki są zabronione.

Haskell , 232 bajty

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]

Wypróbuj online!

Jak to działa

To jest inny frontser parsera do mojej odpowiedzi na „Napisz interpreter dla niepisanego rachunku lambda” , która również ma wersję bez golfisty z dokumentacją.

W skrócie, Term = T (Char -> String)to rodzaj wyrażeń rachunku lambda, które wiedzą, jak stosować się do innych wyrażeń ( a :: Term -> Term -> Term) i jak wyświetlać się jako String( (%) :: Term -> Char -> String), biorąc pod uwagę początkową świeżą zmienną jakoChar . Możemy przekonwertować funkcję na warunkach na termin za pomocą l :: (Term -> Term) -> Term, a ponieważ zastosowanie wynikowego terminu po prostu wywołuje funkcję ( a (l f) == f), warunki są automatycznie redukowane do normalnej postaci, gdy są wyświetlane.

Rubinowy, 323 bajty

Nie mogę uwierzyć, że ten gówno w ogóle działa:

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}

Używanie podstawienia wyrażenia regularnego do przeprowadzania redukcji β na surowych ciągach to niektóre rzeczy Tony-the-Pony. Niemniej jednak jego wynik wygląda poprawnie przynajmniej w przypadku łatwych przypadków testowych:

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

Oto sposób obsługi K(K(K(KK)))niektórych danych wyjściowych debugowania, co zajmuje około 7 sekund na moim laptopie, ponieważ rekurencja wyrażeń regularnych jest powolna . Możesz zobaczyć jego konwersję α w akcji!

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

Uwaga: po while 1:3 linie są wcięte znakiem tabulacji.

Jest to w zasadzie kod za http://ski.aditsu.net/ , przetłumaczony na python, znacznie uproszczony i mocno golfowy.

Odniesienie: (prawdopodobnie jest to mniej przydatne teraz, gdy kod jest skompresowany)

V = termin zmienny
A = termin stosowania
L = współczynnik lambda
c = licznik zmiennej
p = zamień zmienną na termin
r = zmniejsz
m = ostateczna numeracja zmiennej
u = zmienna numeracja zmiennej wewnętrznej (dla zduplikowanych terminów)
s = konwersja łańcucha
(parametr s = jaźń)
C = znak (-y) separatora dla konwersji łańcucha
I, K, S: kombinatory
E = parsowanie

Przykłady:

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

(ten ↑ jest oczekiwany, ponieważ SII(SII) jest nieredukowalny)

Dzięki Mauris i Sp3000 za pomoc w zabiciu kilku bajtów :)

Common Lisp, 560 bajtów

„Wreszcie znalazłem zastosowanie 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))))))

Nie golfił

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

Zmniejszenie beta

Zmienne są dynamicznie powiązane podczas redukcji z PROGVnowymi symbolami Common Lisp, za pomocą MAKE-SYMBOL. Pozwala to ładnie uniknąć kolizji nazewnictwa (np. Niepożądane cieniowanie powiązanych zmiennych). Mógłbym użyć GENSYM, ale chcemy mieć przyjazne nazwy dla symboli. Dlatego symbole są nazywane literami od ado z(zgodnie z pytaniem). Nreprezentuje kod znakowy następnej dostępnej litery w bieżącym zakresie i zaczyna się od 97, aliasa .

Oto bardziej czytelna wersja R(bez Wmakra):

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

Wyniki pośrednie

Analizuj z ciągu:

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

Redukować:

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

(Zobacz ślad wykonania)

Ładny druk:

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

Testy

Używam ponownie tego samego zestawu testów, co odpowiedź w języku 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

Ósmy przykład testu jest zbyt duży dla powyższej tabeli:

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

• EDYCJA Zaktualizowałem moją odpowiedź, aby zachować takie samo zachowanie grupowania jak w odpowiedzi aditsu , ponieważ napisanie kosztuje mniej bajtów.
• Pozostałą różnicę widać na testach 6 i 8. Wynik a.a.a.a.a.b.ajest prawidłowy i nie używa jako dużo listów jako odpowiedź Python, gdzie wiązanie do a, b, ci dnie odwołuje.

Wydajność

Zapętlanie 7 powyższych testów pozytywnych i zbieranie wyników jest natychmiastowe (wynik 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

Wykonanie tego samego testu sto razy prowadzi do… „Wyczerpanie lokalnego magazynu wątków” na SBCL, ze względu na znane ograniczenie dotyczące zmiennych specjalnych. W przypadku CCL wywołanie tego samego zestawu testów 10000 razy zajmuje 3,33 sekundy.