The SKI kalkulus adalah varian dari kalkulus Lambda yang tidak menggunakan ekspresi lambda. Sebaliknya, hanya aplikasi dan kombinator S , K , dan saya yang digunakan. Dalam tantangan ini, tugas Anda adalah menerjemahkan istilah SKI ke dalam istilah Lambda dalam bentuk normal β .

Spesifikasi Input

Input adalah istilah SKI dalam representasi tekstual berikut. Anda dapat memilih untuk menerima baris tambahan opsional. Input terdiri dari karakter S, K, I, (, dan )dan memenuhi tata bahasa berikut (dalam bentuk ABNF) dengan stermmenjadi simbol awal:

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

Spesifikasi Output

Outputnya adalah istilah lambda tanpa variabel bebas dalam representasi tekstual berikut. Anda dapat memilih untuk mengeluarkan baris tambahan opsional. Keluaran harus memenuhi tata bahasa berikut dalam bentuk ABNF dengan ltermmenjadi simbol awal:

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

Kendala

Anda dapat berasumsi bahwa input memiliki bentuk normal β. Anda dapat mengasumsikan bahwa bentuk normal β menggunakan paling banyak 26 variabel yang berbeda. Anda dapat mengasumsikan bahwa input dan output mewakili 79 karakter.

Input sampel

Berikut adalah beberapa input sampel. Output adalah salah satu output yang mungkin untuk input yang diberikan.

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

Mencetak gol

Solusi terpendek dalam oktet menang. Celah umum dilarang.

Haskell , 232 byte

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]

Cobalah online!

Bagaimana itu bekerja

Ini adalah antarmuka parser yang berbeda dengan jawaban saya untuk "Menulis penerjemah untuk kalkulus lambda yang tidak diketik " , yang juga memiliki versi tidak dikenali dengan dokumentasi.

Secara singkat, Term = T (Char -> String)adalah jenis istilah kalkulus lambda, yang tahu bagaimana menerapkan diri ke istilah lain ( a :: Term -> Term -> Term) dan bagaimana menampilkan diri sebagai String( (%) :: Term -> Char -> String), diberi variabel segar awal sebagai a Char. Kita dapat mengonversi suatu fungsi dengan istilah ke suatu istilah dengan l :: (Term -> Term) -> Term, dan karena penerapan istilah yang dihasilkan cukup memanggil fungsi ( a (l f) == f), istilah secara otomatis dikurangi menjadi bentuk normal ketika ditampilkan.

Ruby, 323 byte

Saya tidak percaya omong kosong ini bekerja sama sekali:

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}

Menggunakan substitusi regex untuk melakukan reduksi β pada string mentah adalah beberapa hal Tony-the-Pony. Meskipun demikian, outputnya terlihat benar setidaknya untuk testcas mudah:

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

Ini dia penanganan K(K(K(KK)))dengan beberapa output debug, yang memakan waktu sekitar 7 detik pada laptop saya, karena rekursi ekspresi reguler lambat . Anda dapat melihat konversi α-nya beraksi!

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

Catatan: setelah while 1:, 3 baris diberi indentasi dengan karakter tab.

Ini pada dasarnya adalah kode di belakang http://ski.aditsu.net/ , diterjemahkan ke python, sangat disederhanakan dan golf.

Referensi: (ini mungkin kurang berguna sekarang karena kode dikompresi)

V = istilah variabel
A = istilah aplikasi
L = istilah lambda
c = variabel penghitung
p = ganti variabel dengan suku
r = kurangi
m = penomoran ulang variabel akhir
u = penominan ulang variabel internal (untuk istilah yang digandakan)
s = konversi string
(parameter s = diri)
C = karakter pemisah untuk konversi string
I, K, S: combinators
E = parse

Contoh:

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

(↑ ini diharapkan karena SII(SII)tidak dapat direduksi)

Terima kasih Mauris dan Sp3000 untuk membantu membunuh banyak byte :)

Lisp umum, 560 byte

"Akhirnya, aku menemukan gunanya 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))))))

Tidak disatukan

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

Pengurangan beta

Variabel terikat secara dinamis selama reduksi dengan PROGVsimbol Common Lisp baru, menggunakan MAKE-SYMBOL. Hal ini memungkinkan untuk menghindari tabrakan penamaan (misalnya bayangan variabel terikat yang tidak diinginkan). Saya bisa menggunakan GENSYM, tetapi kami ingin memiliki nama yang ramah untuk simbol. Itulah sebabnya simbol dinamai dengan huruf dari ake z(sebagaimana diizinkan oleh pertanyaan). Nmewakili kode karakter huruf yang tersedia berikutnya dalam lingkup saat ini dan dimulai dengan 97, aliasa .

Ini adalah versi R(tanpa Wmakro) yang lebih mudah dibaca :

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

Hasil antara

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

Mengurangi:

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

(Lihat jejak eksekusi)

Cukup cetak:

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

Tes

Saya menggunakan kembali suite tes yang sama dengan jawaban 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

Contoh uji 8 terlalu besar untuk tabel di atas:

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 Saya memperbarui jawaban saya untuk memiliki perilaku pengelompokan yang sama seperti pada jawaban aditsu , karena biayanya yang lebih sedikit byte untuk menulis.
• Perbedaan yang tersisa dapat dilihat untuk tes 6 dan 8. Hasilnya a.a.a.a.a.b.aadalah benar dan tidak menggunakan sebanyak huruf sebagai jawaban Python, di mana binding untuk a, b, cdan dtidak direferensikan.

Performa

Looping selama 7 tes kelulusan di atas dan mengumpulkan hasilnya segera (output 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

Melakukan pengujian yang sama ratusan kali mengarah ke ... "Penyimpanan lokal thread habis" pada SBCL, karena keterbatasan yang diketahui mengenai variabel khusus. Dengan CCL, memanggil ruang uji yang sama 10.000 kali membutuhkan 3,33 detik.