Le calcul SKI est une variante du calcul Lambda qui n'utilise pas d'expressions lambda. Au lieu de cela, seule l'application et les combinateurs S , K et I sont utilisés. Dans ce défi, votre tâche consiste à traduire les termes SKI en termes Lambda sous forme normale β .

Spécification d'entrée

L'entrée est un terme SKI dans la représentation textuelle suivante. Vous pouvez choisir de recevoir un retour à la ligne facultatif. L'entrée est composé des caractères S, K, I, (, et )et satisfait la grammaire suivante (sous forme ABNF) avec stermétant le symbole de début:

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

Spécifications de sortie

La sortie est un terme lambda sans variable libre dans la représentation textuelle suivante. Vous pouvez choisir de sortir une nouvelle ligne de fin facultative. La sortie doit satisfaire la grammaire suivante sous forme ABNF en ltermétant le symbole de début:

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

Contraintes

Vous pouvez supposer que l'entrée a une forme normale β. Vous pouvez supposer que la forme normale β utilise au plus 26 variables différentes. Vous pouvez supposer que l'entrée et la sortie sont représentables en 79 caractères.

Exemples d'entrées

Voici quelques exemples d'entrées. La sortie est une sortie possible pour l'entrée donnée.

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

Notation

La solution la plus courte en octets l'emporte. Les failles communes sont interdites.

Haskell , 232 octets

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]

Essayez-le en ligne!

Comment ça marche

Ceci est une interface d'analyse différente de ma réponse à «Écrire un interprète pour le calcul lambda non typé» , qui a également une version non golfée avec de la documentation.

En bref, Term = T (Char -> String)est le type de termes de calcul lambda, qui savent comment s’appliquer à d’autres termes ( a :: Term -> Term -> Term) et comment s’afficher en tant que String( (%) :: Term -> Char -> String), étant donné une nouvelle variable initiale comme a Char. Nous pouvons convertir une fonction sur des termes en un terme avec l :: (Term -> Term) -> Term, et parce que l'application du terme résultant appelle simplement la fonction ( a (l f) == f), les termes sont automatiquement réduits à leur forme normale lorsqu'ils sont affichés.

Rubis, 323 octets

Je ne peux pas croire que ce morceau de merde fonctionne du tout:

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}

Utiliser la substitution de regex pour effectuer une réduction β sur des chaînes brutes est un truc de Tony-the-Pony. Néanmoins, sa sortie semble correcte au moins pour des tests faciles:

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

Voici la gestion K(K(K(KK)))avec une sortie de débogage, ce qui prend environ 7 secondes sur mon ordinateur portable, car la récursivité des expressions régulières est lente . Vous pouvez voir sa conversion α en action!

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

Remarque: après while 1:, 3 lignes sont en retrait avec un caractère de tabulation.

Il s'agit essentiellement du code derrière http://ski.aditsu.net/ , traduit en python, grandement simplifié et très utilisé.

Référence: (c'est probablement moins utile maintenant que le code est compressé)

V = terme variable
A = terme d'application
L = terme lambda
c = compteur de variables
p = remplacer la variable par le terme
r = réduire
m = renumérotation variable finale
u = renumérotation variable interne (pour les termes dupliqués)
s = conversion de chaîne
(paramètre s = self)
C = caractère (s) de séparation pour la conversion de chaînes
I, K, S: combinateurs
E = analyse

Exemples:

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

(ce ↑ est attendu car SII(SII)irréductible)

Merci Mauris et Sp3000 d'avoir aidé à tuer un tas d'octets :)

Lisp commun, 560 octets

"Enfin, j'ai trouvé une utilisation pour 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))))))

Non golfé

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

Réduction bêta

Les variables sont liées dynamiquement pendant la réduction avec PROGVde nouveaux symboles Common Lisp, en utilisant MAKE-SYMBOL. Cela permet d'éviter les collisions de noms (par exemple, l'observation indésirable des variables liées). J'aurais pu utiliser GENSYM, mais nous voulons avoir des noms conviviaux pour les symboles. C'est pourquoi les symboles sont nommés avec les lettres de aà z(comme le permet la question). Nreprésente le code de caractère de la prochaine lettre disponible dans la portée actuelle et commence par 97, alias a.

Voici une version plus lisible de R(sans la 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))))))

Résultats intermédiaires

Analyse de la chaîne:

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

Réduire:

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

(Voir trace d'exécution)

Jolie impression:

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

Les tests

Je réutilise la même suite de tests que la réponse 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

Le 8ème exemple de test est trop grand pour le tableau ci-dessus:

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 J'ai mis à jour ma réponse afin d'avoir le même comportement de regroupement que dans la réponse d'Aditsu , car cela coûte moins d'octets à écrire.
• La différence restante peut être vu pour les tests 6 et 8. Le résultat a.a.a.a.a.b.aest correct et ne pas utiliser autant de lettres que la réponse Python, où les liaisons à a, b, cet dne sont pas référencés.

Performance

Faire une boucle sur les 7 tests réussis ci-dessus et collecter les résultats est immédiat (sortie 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

Faire le même test une centaine de fois conduit à ... "Thread local storage exhausted" sur SBCL, en raison d'une limitation connue concernant les variables spéciales. Avec CCL, appeler la même suite de tests 10000 fois prend 3,33 secondes.