Исчисление SKI вариант исчисления лямбда , который не использует лямбда - выражения. Вместо этого, только приложения и комбинаторов S , K и I используются. В этой задаче ваша задача состоит в том, чтобы перевести термины SKI в лямбда-термины в β нормальной форме .

Входная спецификация

Вводом является термин SKI в следующем текстовом представлении. Вы можете выбрать дополнительный трейлинг-перевод строки. Ввода состоит из символов S, K, I, (, и )и удовлетворяет следующей грамматикой (в виде ABNF) с stermявляясь начальным символом:

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

Спецификация выхода

Вывод является лямбда-термом без свободных переменных в следующем текстовом представлении. Вы можете выбрать дополнительный трейлинг-перевод строки. Выходные данные должны соответствовать следующей грамматике в форме ABNF, ltermявляющейся начальным символом:

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

Ограничения

Вы можете предположить, что вход имеет нормальную форму β. Вы можете предположить, что в нормальной форме используется не более 26 различных переменных. Вы можете предположить, что и вход, и выход представлены в 79 символах.

Образцы входов

Вот пара примеров входных данных. Выход является одним из возможных выходов для данного входа.

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

счет

Самое короткое решение в октетах выигрывает. Общие лазейки запрещены.

Haskell , 232 байта

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]

Попробуйте онлайн!

Как это работает

Это другой интерфейс синтаксического анализатора моего ответа на «Напишите интерпретатор для нетипизированного лямбда-исчисления» , который также имеет версию без документации с документацией.

Вкратце, Term = T (Char -> String)это тип терминов лямбда-исчисления, которые знают, как применять себя к другим терминам ( a :: Term -> Term -> Term) и как отображать себя как String( (%) :: Term -> Char -> String), учитывая начальную свежую переменную как Char. Мы можем преобразовать функцию по терминам в термин с помощью l :: (Term -> Term) -> Term, и поскольку применение полученного термина просто вызывает функцию ( a (l f) == f), термины автоматически отображаются в обычной форме при отображении.

Рубин, 323 байта

Я не могу поверить, что этот кусок дерьма работает вообще:

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}

Использование подстановки регулярных выражений для выполнения β-редукции необработанных строк - это кое-что для Тони-Пони. Тем не менее, его вывод выглядит правильным, по крайней мере, для простых тестовых случаев:

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

Вот что происходит K(K(K(KK)))с некоторой отладочной информацией, которая на моем ноутбуке занимает около 7 секунд, потому что рекурсия регулярного выражения медленная . Вы можете увидеть его α-преобразование в действии!

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

Питон 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)'})

Примечание: после while 1:3 строки начинаются с символа табуляции.

Это в основном код http://ski.aditsu.net/ , переведенный на python, сильно упрощенный и с большим упором на гольф.

Справка: (это, вероятно, менее полезно сейчас, когда код сжат)

V = переменный член
A = прикладной термин
L = лямбда-член
c = переменный счетчик
p = заменить переменную на член
r = уменьшить
m = окончательное перенумерация переменных
u = внутренняя перенумерация переменных (для дублированных терминов)
s = преобразование строки
(параметр s = self)
C = символ (ы) разделителя для преобразования строк
I, K, S: комбинаторы
E = анализ

Примеры:

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

(это expected ожидается, потому что SII(SII)неприводимо)

Спасибо Mauris и Sp3000 за помощь, чтобы убить кучу байтов :)

Common Lisp, 560 байт

«Наконец-то я нашел применение 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))))

Бета-восстановительная

Переменные динамически связываются во время приведения PROGVк новым символам Common Lisp, используя MAKE-SYMBOL. Это позволяет избежать коллизий именования (например, нежелательное дублирование связанных переменных). Я мог бы использовать GENSYM, но мы хотим иметь удобные имена для символов. Вот почему символы названы буквами от aдо z(как разрешено в вопросе). Nпредставляет код символа следующей доступной буквы в текущей области и начинается с 97, иначе a.

Вот более читаемая версия R(без Wмакроса):

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

Промежуточные результаты

Разбор из строки:

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

Сокращение:

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

(См. След исполнения)

Довольно-печати:

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

тесты

Я повторно использую тот же набор тестов, что и ответ 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

Восьмой тестовый пример слишком велик для приведенной выше таблицы:

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

• РЕДАКТИРОВАТЬ Я обновил свой ответ для того, чтобы иметь такое же поведение группировки, как в ответе aditsu , потому что запись стоит меньше байтов.
• Оставшаяся разница может рассматриваться для испытаний 6 и 8. Результат a.a.a.a.a.b.aявляется правильным и не использует столько же буквы , как ответ на Python, где привязки к a, b, cи dне ссылаются.

Спектакль

Цикл 7 проходящих тестов выше и сбор результатов немедленно (вывод 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

Выполнение одного и того же теста сто раз приводит к ... «Поток локального хранилища исчерпан» в SBCL из-за известного ограничения, касающегося специальных переменных. При использовании CCL вызов одного и того же набора тестов 10000 раз занимает 3,33 секунды.