Kombinatorisches Rätsel!

12

Einführung: Kombinatorische Logik

Die kombinatorische Logik (CL) basiert auf sogenannten Kombinatoren , die im Grunde genommen Funktionen sind. Es gibt zwei grundlegende "eingebaute" Kombinatoren Sund K, die später erklärt werden.

Linke Assoziativität

CL ist linksassoziativ , was bedeutet, dass Klammern (die etwas enthalten), die sich ganz links von einem anderen Klammerpaar befinden, entfernt werden können, wobei das betreffende Material freigegeben wird. Zum Beispiel so etwas:

((a b) c)

Kann auf reduziert werden

(a b c)

Befindet (a b)sich der ganz links von der größeren Halterung ((a b) c), so kann er entfernt werden.

Ein viel größeres Beispiel für Linksassoziationen (eckige Klammern sind Erklärungen):

  ((a b) c ((d e) f (((g h) i) j)))
= (a b c ((d e) f (((g h) i) j)))   [((a b) c...) = (a b c...)]
= (a b c (d e f (((g h) i) j)))     [((d e) f...) = (d e f...)]
= (a b c (d e f ((g h i) j)))       [((g h) i) = (g h i)]
= (a b c (d e f (g h i j)))         [((g h i) j) = (g h i j)]

Klammern können auch reduziert werden, wenn mehr als ein Paar um dieselben Objekte gewickelt ist. Beispiele:

((((a)))) -> a
a ((((b)))) -> a b
a (((b c))) -> a (b c) [(b c) is still a group, and therefore need brackets.
                        Note that this doesn't reduce to `a b c`, because
                        `(b c)` is not on the left.]

Builtins

CL verfügt über zwei "eingebaute" Kombinatoren, Smit Kdenen Objekte (einzelne Kombinatoren oder eine Gruppe von Kombinatoren / Gruppen, die in eckige Klammern eingeschlossen sind) wie folgt gewechselt werden können:

K x y = x
S x y z = x z (y z)

Wo x, yundz kann Stand-In für alles sein.

Ein Beispiel für Sund Ksind wie folgt:

  (S K K) x [x is a stand-in for anything]
= S K K x   [left-associativity]
= K x (K x) [S combinator]
= x         [K combinator]

Ein anderes Beispiel:

  S a b c d
= a c (b c) d [combinators only work on the n objects to the right of it,
               where n is the number of "arguments" n is defined to have -
               S takes 3 arguments, so it only works on 3 terms]

Das Obige sind Beispiele für normale CL-Anweisungen, bei denen die Anweisung nicht weiter ausgewertet werden kann und ein Endergebnis in einer endlichen Zeitspanne erzielt wird. Es gibt nicht normale Anweisungen (CL-Anweisungen, die nicht enden und für immer ausgewertet werden), aber sie liegen nicht im Rahmen der Herausforderung und müssen nicht behandelt werden.

Wenn Sie mehr über CL erfahren möchten, lesen Sie diese Wikipedia-Seite .

Aufgabe:

Ihre Aufgabe ist es, zusätzliche Kombinatoren zu erstellen, die die Anzahl der Argumente und die Auswertung als Eingabe berücksichtigen.

{amount_of_args} = {evaluated}

Wo {amount_of_args}ist eine positive ganze Zahl gleich der Anzahl der Argumente und {evaluated}besteht aus:

  • Argumente bis zur Menge der 1Argumente, mit dem ersten Argument,2 wobei das das zweite usw. ist.
    • Es wird garantiert, dass Argumentnummern über der Anzahl der Argumente (also nur 4wenn ) nicht in angezeigt werden .{amount_of_args}3{evaluated}
  • Klammern ()

Beispiele für Eingaben sind:

3 = 2 3 1
4 = 1 (2 (3 4))

Bei der ersten Eingabe wird nach einem Kombinator (z. B. R) mit drei Argumenten ( R 1 2 3) gefragt , der dann ausgewertet wird zu:

R 1 2 3 -> 2 3 1

Die zweite Eingabe fragt danach (mit einem Kombinator-Namen A):

A 1 2 3 4 -> 1 (2 (3 4))

In Anbetracht der Eingabe in diesem Format, müssen Sie eine Reihe von zurückgeben S, Kund (), die , wenn sie mit einem combinator Namen ersetzt und mit Argumenten ausführen, gibt das gleiche ausgewertete Aussage wie die{evaluated} Block , wenn der Befehlsblock wird wieder für diesen combinator Namen ersetzt.

Bei der Ausgabe-Kombinator-Anweisung werden möglicherweise die Leerzeichen und die äußeren Klammern entfernt, sodass so etwas wie umgewandelt werden (S K K (S S))kannSKK(SS) .

Wenn Sie Ihr Programms der Ausgänge zu testen, hat @aditsu einen kombinatorischen Logik - Parser gemacht (einschließlich S, K, Iund auch andere , die gerne Bund C) hier .

Ergebnis:

Da es sich um einen , besteht das Ziel dieser Herausforderung darin, die geringstmögliche Anzahl von Bytes in der angegebenen Ausgabe zu erzielen diesen 50 Testfällen . Bitte geben Sie Ihre Ergebnisse für die 50 Testfälle in die Antwort ein oder erstellen Sie ein Pastebin (oder ähnliches) und veröffentlichen Sie einen Link zu diesem Pastebin.

Bei einem Gleichstand gewinnt die früheste Lösung.

Regeln:

  • Ihre Antwort muss eine RICHTIGE Ausgabe zurückgeben. Bei einer Eingabe muss die korrekte Ausgabe gemäß der Definition in der Task zurückgegeben werden.
  • Ihre Antwort muss für jeden Testfall innerhalb einer Stunde auf einem modernen Laptop ausgegeben werden.
  • Eine Hardcodierung von Lösungen ist nicht zulässig. Sie können jedoch bis zu 10 Kombinatoren fest codieren.
  • Ihr Programm muss jedes Mal dieselbe Lösung für dieselbe Eingabe zurückgeben.
  • Ihr Programm muss für jede Eingabe ein gültiges Ergebnis liefern, nicht nur für Testfälle.
Clismique
quelle
Wie können Sie sicherstellen, dass keine Kombinatoren gestohlen werden, die in anderen Antworten enthalten sind?
Fatalize
@Fatalize Das sollte nicht allzu wichtig sein, da sich die Leute von den Antworten anderer inspirieren lassen und darauf aufbauen können, um bessere Antworten zu erhalten.
Clismique
Apropos Inspiration: Wenn das gewünschte Ergebnis kein a enthält 1, können Sie 1von allem subtrahieren und dann die Lösung für diese Antwort einpacken K(). Beispiel: Lösung für 2 -> 1ist K, also Lösung für 3 -> 2ist KK, Lösung für 4 -> 3ist K(KK)usw.
Neil

Antworten:

8

Haskell , Punktzahl 5017

Dies kombiniert den dümmsten möglichen Algorithmus zur Abstraktionseliminierung ((λ x . X ) = I; (λ x . Y ) = K y ; (λ x . M N ) = S (λ x . M ) (λ x . N ) ) mit einem Gucklochoptimierer, der nach jeder Anwendung verwendet wird. Die wichtigste Optimierungsregel ist S (K x ) (K y ) ↦ K ( xy ), wodurch verhindert wird, dass der Algorithmus immer exponentiell explodiert .

Der Regelsatz ist als Liste von Zeichenfolgenpaaren konfiguriert, sodass Sie leicht mit neuen Regeln herumspielen können. Als besonderen Vorteil der Wiederverwendung des Eingabe-Parsers für diesen Zweck werden S, K und ich auch in den Eingabe-Kombinatoren akzeptiert.

Regeln werden nicht unbedingt angewendet; Stattdessen werden sowohl die alte als auch die neue Version beibehalten und suboptimale Versionen werden nur dann gelöscht, wenn ihre Länge die der besten Version um mehr als eine Konstante (derzeit 3 ​​Byte) überschreitet.

Die Partitur wird leicht verbessert, indem I als grundlegender Kombinator behandelt wird, bis die Ausgangsstufe es in SKK umschreibt. Auf diese Weise kann KI = K (SKK) bei der Ausgabe um 4 Byte auf SK verkürzt werden, ohne den Rest der Optimierungen zu verwechseln.

{-# LANGUAGE ViewPatterns #-}

import qualified Data.IntMap as I
import qualified Data.List.NonEmpty as N
import System.IO

data Term
  = V Int
  | S
  | K
  | I
  | A (N.NonEmpty (Int, Term, Term))
  deriving (Show, Eq, Ord)

parse :: String -> (Term, String)
parse = parseApp . parse1

parseApp :: (Term, String) -> (Term, String)
parseApp (t, ' ':s) = parseApp (t, s)
parseApp (t, "") = (t, "")
parseApp (t, ')':s) = (t, ')' : s)
parseApp (t1, parse1 -> (t2, s)) =
  parseApp (A (pure (appLen (t1, t2), t1, t2)), s)

parse1 :: String -> (Term, String)
parse1 (' ':s) = parse1 s
parse1 ('(':(parse -> (t, ')':s))) = (t, s)
parse1 ('S':s) = (S, s)
parse1 ('K':s) = (K, s)
parse1 ('I':s) = (I, s)
parse1 (lex -> [(i, s)]) = (V (read i), s)

ruleStrings :: [(String, String)]
ruleStrings =
  [ ("1 3(2 3)", "S1 2 3")
  , ("S(K(S(K1)))(S(K(S(K2)))3)", "S(K(S(K(S(K1)2))))3")
  , ("S(K(S(K1)))(S(K2))", "S(K(S(K1)2))")
  , ("S(K1)(K2)", "K(1 2)")
  , ("S(K1)I", "1")
  , ("S(S(K1)2)(K3)", "S(K(S1(K3)))2")
  , ("S(SI1)I", "S(SSK)1")
  ]

rules :: [(Term, Term)]
rules = [(a, b) | (parse -> (a, ""), parse -> (b, "")) <- ruleStrings]

len :: Term -> Int
len (V _) = 1
len S = 1
len K = 1
len I = 3
len (A ((l, _, _) N.:| _)) = l

appLen :: (Term, Term) -> Int
appLen (t1, S) = len t1 + 1
appLen (t1, K) = len t1 + 1
appLen (K, I) = 2
appLen (t1, t2) = len t1 + len t2 + 2

notA :: Term -> Bool
notA (A _) = False
notA _ = True

alt :: N.NonEmpty Term -> Term
alt ts =
  head $
  N.filter notA ts ++
  [A (N.nub (a N.:| filter (\(l, _, _) -> l <= minLen + 3) aa))]
  where
    a@(minLen, _, _) N.:| aa =
      N.sort $ do
        A b <- ts
        b

match :: Term -> Term -> I.IntMap Term -> [I.IntMap Term]
match (V i) t m =
  case I.lookup i m of
    Just ((/= t) -> True) -> []
    _ -> [I.insert i t m]
match S S m = [m]
match K K m = [m]
match I I m = [m]
match (A a) (A a') m = do
  (_, t1, t2) <- N.toList a
  (_, t1', t2') <- N.toList a'
  m1 <- match t1 t1' m
  match t2 t2' m1
match _ _ _ = []

sub :: I.IntMap Term -> Term -> Term
sub _ S = S
sub _ K = K
sub _ I = I
sub m (V i) = m I.! i
sub m (A a) =
  alt $ do
    (_, t1, t2) <- a
    pure (sub m t1 & sub m t2)

optimize :: Term -> Term
optimize t = alt $ t N.:| [sub m b | (a, b) <- rules, m <- match a t I.empty]

infixl 5 &

(&) :: Term -> Term -> Term
t1 & t2 = optimize (A (pure (appLen (t1, t2), t1, t2)))

elim :: Int -> Term -> Term
elim n (V ((== n) -> True)) = I
elim n (A a) =
  alt $ do
    (_, t1, t2) <- a
    pure (S & elim n t1 & elim n t2)
elim _ t = K & t

paren :: String -> Bool -> String
paren s True = "(" ++ s ++ ")"
paren s False = s

output :: Term -> Bool -> String
output S = const "S"
output K = const "K"
output I = paren "SKK"
output (V i) = \_ -> show i ++ " "
output (A ((_, K, I) N.:| _)) = paren "SK"
output (A ((_, t1, t2) N.:| _)) = paren (output t1 False ++ output t2 True)

convert :: Int -> Term -> Term
convert 0 t = t
convert n t = convert (n - 1) (elim n t)

process :: String -> String
process (lex -> [(n, lex -> [((`elem` ["=", "->"]) -> True, parse -> (t, ""))])]) =
  output (convert (read n) t) False

main :: IO ()
main = do
  line <- getLine
  putStrLn (process line)
  hFlush stdout
  main

Probieren Sie es online!

Ausgabe

  1. S (KS) K
  2. S (K (SS (KK))) (S (KK) S)
  3. S (K (SS)) (S (KK) K)
  4. S (K (SS (KK))) (S (KK) (S (KS) (S (K (S (SKK))) K))
  5. S (K (S (K (SS (SK)))) (S (K (SS (SK))) (S (SKK) (SKK))
  6. KK
  7. S (K (S (S (KS) (S (K (S (SKK))) K))) (S (KK) K)
  8. S (K (SS (K (KK) (S (SKK) (SKK))))) (S (SSK (KS)) (S (S (KS) (S (KK) (S (KS) K))) (K (S (K (S (SSK))) K)))
  9. S (K (S (KK))) (S (K (S (S (SKK) (SKK)))) K)
  10. SK
  11. S (KS) (S (KK) (S (K (SS)) (S (KK) K))
  12. S (K (SS (K (KK) K))) (S (KK) (S (KS) (S (SSK (KS)) (S (K (SS)) (S (KK) K) ))))
  13. S (K (S (K (K (SS (KK))) (S (KK) S)))) (S (K (SS (KK))) (S (KK) (S (KS) (S (K (S (SKK))) K)))
  14. S (K (S (K (S (K (SS (KK)))) (S (KK) S)))) (S (K (S (SKK))) K)
  15. S (K (S (K (S (KS) K))) (S (KS) K)
  16. S (K (S (KS) K))
  17. S (K (S (K (K (SS (K (S (S) KS) (S (KK) (SSK))) (K (S (SKK) (SKK))))) (S (KK) (S (KS) K))))) (S (K (SS (K (SSK))) (S (KK) (S (KS) (S (KK) (SSK))) )
  18. SSS (KK)
  19. KK
  20. S (KK) (S (KK) (S (S (KS) K) (S (K (S (SKK))) (S (K (S (SKK))) K)))
  21. S (S (KS) (S (KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K)))) (K (S (K (S ( S (KS) (S (K (S (SKK)) K))) (S (KK) K)))
  22. S (KK)
  23. S (KS) (S (KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K))))
  24. S (K (S (K (S (KS) K))) (S (K (S (S (KS)) (S (KK) (S (K (SS)) (S (KK) K))) ))) (S (KK) (S (K (SS)) (S (KK) K))))
  25. S (KS) (S (KK) (S (KS) K)
  26. S (S (KS) (S (KK) (S (KS) (S (KK) (S (K (S (SS (KK))))) (S (KS) (S (KK) (S (SSK (KS)) (S (KS) (S (SKK) (SKK))))))))) (K (S (S (KS) (S (K (S (K (S (KS ) (S (K (S (KS) (S (K (S (SKK)))))))) (S (K (S (SKK))))) (S (K ( S (K (S (KK) K))) (S (K (S (SKK))) K)))
  27. S (K (S (K (S (K) (K (S (S (KS) (S (S (SKK))) K))) (S (KK) K)) ))) (S (KK) (S (KS) K)))) (S (K (SS (K (S (K (SS)) (S (KK) K)))) (S ( KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K)))))
  28. K (S (KK))
  29. S (K (S (K (S (K (K (S (KS) K)))) (S (K (S (KS)) (S (KK) (S (K (SS))) ( S (KK) K))))) K)))) (S (K (S (S (KS) (S (KK) (S (K (SS)) (S (KK) K))) ))) (S (KK) (S (K (SS)) (S (KK) K))))
  30. S (KK) (S (K (SSS (KK))))
  31. K (SSS (KK))
  32. S (K (SS (K (S (KS) (S (KK) (S (KS) K))) (K (S (K (S (SKK))) K)))) (S (KK) (S (KS) (SS (S (S (KS) (S (KK) (S (KS) (S (S (KS) (S (KK) (S (KS) K))) )))))) (KK))))
  33. S (K (S (K (S (S (K (SS (KK)))) (S (KK) S))))) (S (K (SS (K (S (KK) K) ))) (S (KK) (SSS (KS))))
  34. S (K (S (K (S (KK) K))))
  35. S (K (S (K (K (S (K (SS (K (K (S (SKK))) K)))) (S (KK) (S (KS) (S (KK) (S (K (SS (K (S (K (S (SKK))) K))) (S (KK) (S (K (SS)) (S (KK) K)))))) ))))) (S (K (S (S (KS) (S (K (S (SKK))) K))) (S (KK) K))
  36. S (K (SS (K (K (SS (K (K (S (SKK))) K))) (S (KK) (S (KS)) (SS (S (S (KS) (S (KK) (S (KS) (S (K (S (SKK))) K))) (KK))))))) (S (KK) (S (KS) (S ( KK) (S (K (S (K (S (KK))) (S (K (S (K (SS (KK))))))) (S (K (SS (KK))) (S (KK) (S (KS) (S (K (S (KS) (S (KK) (S (KS) K))))))))))
  37. S (KK) (S (K (S (K (S (KK) (S (KK) K)))) (SS (SK))
  38. K (S (K (SSS (KK))))
  39. S (K (S (K (K (K (K (K (K (K (K (K (K (SS (K (K (K)))))))))) ))) K))) (S (KK) K)))) (S (KK) (S (KS) K)))) (S (K (SS (K (S (K (SS )) (S (KK) K)))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S ( KK) K)))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S (K) K)) ))) (S (KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K)))))
  40. S (K (S (KK))) (S (KS) (S (KK) (S (K (S (KK) (S (KK) K))))))
  41. S (K (SS (K (S (KS) (S (KK) (S (KS) K))) (K (S (K (S (SKK))) K)))) (S (KK) (S (KS) (S (KK) (S (K (S (K (K (SS (K (K (SS))) (S (KK) K))))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (KK) (S (K (SS)) K))) (S (KK) (S ( K (SS)) (S (KK) (S (K (S (K (S (KK) (S (KS) K)))) (S (KS) K))))))))
  42. S (K (S (K (S (K (S (K (K (S (K (K (K (S (K (S (S (KS))))))))))))))))))) (S (K (S (SKK))) K))) (S (KK) K)))) (S (KK) (S (KS) K)))) (S (K (SS (K (S (K (SS)) (S (KK) K))) (S (KK) (S (KS) K)))))) (S (K (SS (K (S ( K (SS)) (S (KK) K)))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S (KK) K)))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S (KK) K)))) (S (KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K)))))
  43. K (K (K (K (K (S (KK) (S (KK) (S (K (SS (SK))) (SSK)))))))
  44. S (KK) (S (K (S (KK) (S (KK) (S (KK) (S (KK) K)))))
  45. S (K (S (K (S (K (S (K (S (S (K (S (K (S (K (S (K (S (K))))))))))))))))) K (S (S (KS) (S (K (S (SKK))) K))) (S (KK) K))) (S (KK) (S (KS) K)))) )) (S (K (SS (K (S (K (SS)) (S (KK) K)))) (S (KK) (S (KS) K)))))) (S ( K (SS (K (S (K (SS)) (S (KK) K))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S (KK) K))) (S (KK) (S (KS) K)))))) (S (K (SS (K (S (K (K ( SS)) (S (KK) K)))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S (KK) K)))) (S (KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K))))))
  46. S (K (S (K (K (K (K (K (K (K (K (K))))) (S (K) (S ( KS) (S (K (S (SKK)) K))))) (S (KK) (S (KS) (S (KK) (S (SSK (KS)) (S (K (SS )) (S (KK) K)))))))) (S (KK) (S (KS) (S (KK) (S (K (SS (K (S (KK) (S (KS ) (S (KK) (S (K (SS (K (S (KK) (S (KS) K)))) (S (KK) (S (K (SS)) (S (KK) (S (K (SS (K (KK) K))) (S (KK) S)))))))))) (S (KK) (S (K (SS)) K) )))))) (S (K (SS (K (S (KK) (S (K (S (S (KS) (S (KK) (S (K (SS))) (S (KK) K))))) (S (KK) (S (K (SS)) (S (KK) K)))))) (S (K) S))))) (S (K (SS (K (S (K (S (KS) (S (KK) (S (K (SS)) (S (KK) K))))) (S (KK) (S (K ( SS)) (S (KK) K)))))) (S (KK) (S (KS) (S (KK) (S (K (S (K (S (KS) (S (KK) ( S (KS) K))))) (S (KS) (S (KK) (S (K (SS)) (S (KK) K)))))))))
  47. S (K (SS (K (SS (S (S) KS) (S (KK) S)) (KK)))) (S (KK) (S (KS) (S (K (S (K (S (KS) (S (KK) (S (KS) (S (KK) (S (K (S (K (K (SS) K (S (K (S (S (KS) (S ( KK) (S (K (SS)) (S (KK) K)))) (S (KK) (S (K (SS)) (S (KK) K)))) (S (KK) (S (KS) K)))))))))) (S (K (S (S (KS) (S (KK) (S (K (SS)) (S ( KK) (S (K (S (K (S (KS) K))) (S (K (SS (K (S (K (SS)) (S (KK) K)))) (S ( KK) (S (KS) (S (KK) (S (K (SS)) (S (KK) K)))))))))) (S (KK) (S (K (S (K (S (KK) (S (KS) (S (KK) (S (K (SS (K (S (KK) (S (KS) K))))) (S (KK) (S (K (SS)) K))))))) (S (KS) (S (KK) (S (K (SS (K (KK) K))) (S (KK) (S ( KS) (S (SSK (KS)) (S (K (SS (KK))) (S (KK) (S (KS) (S (K (S (SKK))) K))))) ))))))))
  48. K (S (K (S (KK) (S (K (S (KK) (S (K (S (KK) (S (KK) K)))))))))
  49. S (KK) (S (K (S (K (S (KK)) (S (S (K (S (KK)) (S (S (K (S (KK)) (S (K (S ( K (S (KK) (S (K (S (KK))) (S (K (S (SKK)) K)))) (S (K (S (SKK))) K)) ))) (S (K (S (SKK)) K))))) (S (K (S (SKK)) K))))) (S (K (S (SKK)) K))
  50. S (K (S (K (S (K))) (S (K (K (K))) (S (K (SS (K (K (S (S (KS))) (S (K ( S (SKK))) K))) (S (KK))))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) (S (KK) K))) (S (KK) (S (KS) K))))) (S (K (SS (K (S (K (SS)) ) (S (KK) K)))) (S (KK) (S (KS) (S (KK) (S (K (K (S (KK) (S (KK) (S (KK) (S (KK) K)))))) (S (K (SS)) (S (KK) K)))))
Anders Kaseorg
quelle
Wäre es möglich, die Ausdrücke automatisch zu optimieren (z. B. S (K x) (K y) = K (x y))?
CalculatorFeline
@CalculatorFeline Ich verstehe Ihre Frage nicht. S (K x ) (K y ) wird automatisch auf K ( xy ) optimiert .
Anders Kaseorg
Warten Sie, werden diese Ausdrücke als teilweise angewendete Funktionen oder etwas anderes dargestellt? Wenn teilweise angewandte Funktionen, dann könnten Sie vielleicht so etwas wie meinen letzten Kommentar machen.
CalculatorFeline
@CalculatorFeline Die Darstellung sieht beispielsweise so aus: 3 = 1 (2 3) ↦ 2 = S (K1) (S (K2) I) ↦ 2 = S (K1) 2 ↦ 1 = S (S (KS) (S (KK) (K1))) I ≤ 1 = S (S (KS) (K (K1))) I ≤ 1 = S (K (S (K1))) I ≤ 1 = S (K (S (K1 ))) I ≤ 1 = S (K1) ≤ S (KS) (S (KK) I) ≤ S (KS) K. Wie Sie sehen, haben wir bereits viele Male die Regel S (K x ) (K y ) ↦ K ( xy ) verwendet, zusammen mit den anderen, in denen ich aufgeführt bin ruleStrings. Wenn wir das nicht getan hätten, wäre die Ausgabe exponentiell länger: Für dieses winzige Beispiel hätten wir S (S (KS) (S (KS) (S (KK) (KS))) (S (S (KS) (S (KK) (KK)) (S (KK) (SKK)))) (S (S (KS) (S (S (KS) (S (KK) (KS))) ( S (S (KS) (S (KK) (KK)) (SK))) (S (KK) (SK))) anstelle von S (KS) K.
Anders Kaseorg
5

Summe der Lösungslängen: 12945 8508 5872

Haskell-Code, der Eingabezeilen von stdin nimmt und sich nicht darum kümmert, ob das Trennzeichen =oder ->:

data E=S|K|V Int|A E E deriving Eq

instance Show E where
  showsPrec _ S = showChar 'S'
  showsPrec _ K = showChar 'K'
  showsPrec _ (V i) = shows i
  showsPrec p (A e f) = showParen (p>0) $ showsPrec 0 e . showsPrec 1 f

type SRead a = String -> (a,String) -- a simpler variation of ReadS

parse :: String -> E
parse s = let (e,"")=parseList (s++")") in e
parseList :: SRead E
parseList s = let (l,s')=parseL s in (foldl1 A l,s')
parseL :: SRead [E]
parseL (c:s) | c==' ' = parseL s
             | c==')' = ([],s)
parseL s = let (p,s')=parseExp s; (l,s'')=parseL s' in (p:l,s'')
parseExp :: SRead E
parseExp ('(':s) = parseList s
parseExp s = let [(n,s')]=reads s in (V n,s')

k e = A K e
s e f = A (A S e) f
i = s K K
s3 e f g = A (s e f) g
sk = A S K
ssk e f = A (s3 S K e) f

n `invars` (A e f) = n `invars` e || n `invars` f
n `invars` (V m)   = n==m
_ `invars` _       = False

comb (A e f) = comb e && comb f
comb (V _)   = False
comb _       = True

abstract _ (A (A S K) _) = sk
abstract n e | not (n `invars` e) = k e
abstract n (A e (V _)) | not (n `invars` e) = e
abstract n (A (A (V i) e) (V j)) | n==i && n==j =
                                   abstract n (ssk (V i) e)
abstract n (A e (A f g)) | comb e && comb f =
                                   abstract n (s3 (abstract n e) f g)
abstract n (A (A e f) g) | comb e && comb g =
                                   abstract n (s3 e (abstract n g) f)
abstract n (A (A e f) (A g h)) | comb e && comb g && f==h =
                                   abstract n (s3 e g f)
abstract n (A e f) = s (abstract n e) (abstract n f)
abstract n _ = i

abstractAll 0 e = e
abstractAll n e = abstractAll (n-1) $ abstract n e

parseLine :: String -> (Int,E)
parseLine s = let [(n,s')] = reads s
                  s''=dropWhile(`elem` " =->") s'
              in (n, parse s'')

solveLine :: String -> E
solveLine s = let (n,e) = parseLine s in abstractAll n e

main = interact $ unlines . map (show . solveLine) . lines

Es implementiert die verbesserte Klammerabstraktion aus Abschnitt 3.2 von John Tromp: Binäre Lambda-Rechnung und kombinatorische Logik, auf die aus dem Wikipedia-Artikel über kombinatorische Logik verwiesen wird. Die nützlichsten Sonderfälle verwenden den SKombinator nur, um die Anzahl der Subtermini zu erhöhen, um ein tiefes Verschachteln von Variablen zu vermeiden. Der Fall, der die Gleichheit einiger Subtermen prüft, wird für keinen der Testfälle benötigt. Während es keinen speziellen Fall für die Behandlung des WKombinators gibt (siehe Peters Antwort), arbeiten die Regeln zusammen, um den kürzeren SS(SK)Ausdruck zu finden . (Ich habe zuerst einen Fehler gemacht, indem ich versucht habe, die inneren Aufrufe zu optimieren abstract, dann diesW Optimierung nicht erfolgt und das Gesamtergebnis war 16 Byte länger.)

Und hier sind die Ergebnisse aus den Testfällen:

S(KS)K
S(K(S(K(SS(KK)))K))S
S(K(S(K(SS))K))K
S(K(S(K(S(K(S(K(SS(KK)))K))S))(S(SKK))))K
S(K(S(K(SS(SK)))))(S(K(SS(SK)))(S(SKK)(SKK)))
KK
S(K(S(K(S(S(K(S(KS)(S(SKK))))K)))K))K
S(K(S(K(SS(K(S(KK)(S(SKK)(SKK))))))(S(KS))))(S(K(S(K(S(K(SS(K(S(K(S(SSK)))K))))K))S))K)
S(K(S(K(S(KK)))(S(S(SKK)(SKK)))))K
SK
S(K(S(K(S(K(S(S(KS)(S(KS)))))K))K))K
S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(KK)K))))K))S))(S(KS))))(SS)))K))K
S(K(S(K(S(K(S(K(SS(KK)))K))S))))(S(K(S(K(S(K(S(K(SS(KK)))K))S))(S(SKK))))K)
S(K(S(K(S(K(S(K(S(K(SS(KK)))K))S))))(S(SKK))))K
S(K(S(K(S(K(S(K(S(K(SS(K(S(KS)K))))K))S))K))S))K
S(K(S(KS)K))
S(S(K(S(KS)(S(K(S(KS)(S(KS)))))))(S(K(S(K(S(K(S(K(S(K(SS(K(S(S(K(S(KS)(S(KS))))(S(K(S(K(S(K(SS(K(S(S(KS)(S(K(SS(K(S(SKK)(SKK)))))K))K))))K))S))K))(S(KK)K)))))K))S))K))S))K))(S(K(S(KK)K))K)
S(KK)(S(KK))
KK
S(K(S(KK)K))(S(S(KS)K)(S(K(S(K(S(SKK)))(S(SKK))))K))
S(K(S(K(S(K(S(S(K(S(K(S(K(S(KS)(S(KS))))(S(S(K(S(KS)(S(SKK))))K))))K))K)))K))K))K
S(KK)
S(K(S(K(S(K(S(K(S(S(KS)(S(K(S(KS)(S(KS))))))))K))K))K))K
S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))(S(S(KS)(S(KS))))))K))K))K
S(K(S(K(S(KS)K))S))K
S(K(S(K(S(K(S(K(SS(KK)))(S(KS))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(K(S(KS)(S(SKK))))K))))))))(S(SKK))))K)(S(K(S(K(S(K(S(KK)K))))(S(SKK))))K)))))K))S))K))S))K))S))(S(SKK)(SKK)))
S(K(S(K(S(K(S(K(S(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(KS)))))))(S(S(K(S(K(S(K(S(KS)(S(KS))))(S(S(K(S(KS)(S(SKK))))K))))K))K))))K))K))K)))K))K))K))K
K(S(KK))
S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))(S(S(KS)(S(KS))))))K))K))K)
S(KK)(S(K(S(KK)(S(KK)))))
K(S(KK)(S(KK)))
S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)))(S(K(S(K(S(K(SS(K(S(K(S(SKK)))K))))K))S))K)))))K))S))K))S))(S(K(S(K(S(K(S(KS)K))S))K)))
S(K(S(K(S(K(S(K(S(K(SS(KK)))K))S))))))(S(K(S(K(S(K(SS(K(S(KK)K))))K))S))(S(KS)))
S(K(S(K(S(KK)K))))
S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(S(K(S(K(S(KS)(S(K(S(K(S(KS)(S(SKK))))K)))))(S(SKK))))K)))K))K))K))))))(S(S(K(S(KS)(S(SKK))))K))))K))K
S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(KK)))K))S))))))))))(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)))(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(K(S(KK)))(S(SKK))))K))))K))S))K))S))(S(SKK))))K)))))K))S))K))S))(S(K(S(K(S(K(S(KS)K))S))K))))
S(K(S(KK)(S(K(S(K(S(KK)K))K)))))(SS(SK))
K(S(K(S(KK)(S(KK)))))
S(K(S(K(S(K(S(K(S(K(S(K(S(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))(S(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(KS)))))))(S(S(K(S(K(S(K(S(KS)(S(KS))))(S(S(K(S(KS)(S(SKK))))K))))K))K))))K))K))K))))K))K))K))K))))K))K))K))K))K)))K))K))K))K))K))K
S(K(S(K(S(K(S(KK)(S(K(S(K(S(KK)K))K)))))))S))K
S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))(S(S(K(S(K(S(KS)K))S))K))))K))))(S(K(S(K(S(K(SS(K(S(K(S(SKK)))K))))K))S))K)))))K))S))K))S))K))S))K))S))K))S))K
S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))(S(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(KS)))))))(S(S(K(S(K(S(K(S(KS)(S(KS))))(S(S(K(S(KS)(S(SKK))))K))))K))K))))K))K))K))))K))K))K))K))))K))K))K))K))K))))K))K))K))K))K))K)))K))K))K))K))K))K))K
K(K(K(K(K(S(K(S(KK)K))(S(K(SS(SK)))(SSK)))))))
S(KK)(S(K(S(K(S(K(S(K(S(KK)K))K))K))K)))
S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))(S(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(KS)))))))(S(S(K(S(K(S(K(S(KS)(S(KS))))(S(S(K(S(KS)(S(SKK))))K))))K))K))))K))K))K))))K))K))K))K))))K))K))K))K))K))))K))K))K))K))K))K))))K))K))K))K))K))K))K)))K))K))K))K))K))K))K))K
S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))))))))(S(K(S(K(S(K(S(K(SS(K(S(K(S(K(S(KK)K))K))K))))K))S))(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))(S(K(S(K(S(K(S(K(SS(K(S(KK)K))))K))S))(S(KS)))))))(S(S(K(S(KS)(S(KS))))(S(K(S(K(S(K(S(K(SS(KK)))K))S))(S(SKK))))K)))))K))K))K))))K))K))K))K))K))))K))K))K))K))K))K))K)))K))K))K))K))K))K))K))K))K
S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KK)K))K))K))K))K))K))K))))K))S))(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))))))))(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(K(S(K(S(KK)K))K))K))K))))K))S))(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS)))))))))))))(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))))))))(S(K(S(K(S(K(S(K(SS(K(S(K(S(KK)K))K))))K))S))(S(K(S(KS)(S(KS)))))))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(SS(K(S(K(S(K(S(K(S(K(S(KK)K))))))))(S(K(S(K(SS(KK)))K))S)))))K))S))K))S))K))S))K))S))(S(KS))))(S(K(S(K(S(K(S(K(SS(KK)))K))S))(S(SKK))))K))
K(S(K(S(KK)(S(K(S(KK)(S(K(S(K(S(KK)K))K)))))))))
S(K(S(K(S(KK)(S(K(S(K(S(K(S(KK)(S(K(S(K(S(K(S(KK)(S(K(S(K(S(K(S(KK)(S(K(S(K(S(K(S(KK)(S(KK))))(S(SKK))))K)))))(S(SKK))))K)))))(S(SKK))))K)))))(S(SKK))))K)))))(S(SKK))))K
S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KK)(S(K(S(K(S(K(S(K(S(KK)K))K))K))K)))))))))))(S(S(K(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(K(S(KS)(S(KS))))))))))(S(S(K(S(K(S(K(S(K(S(KS)(S(K(S(KS)(S(KS)))))))(S(S(K(S(K(S(K(S(KS)(S(KS))))(S(S(K(S(KS)(S(SKK))))K))))K))K))))K))K))K))))K))K))K))K))))K))K))K))K))K
Christian Sievers
quelle
3

8486 mit S, K, I, W

Erläuterung

Der Standard - Algorithmus (wie beispielsweise in Kapitel 18 von To a Mockingbird Mock ) vier Fälle verwendet, entsprechend den Kombinatoren S, K, I = SKKund eine einfache Links Association. Ich denke, das ist es, was Christians Antwort umsetzt. Dies ist ausreichend, aber nicht unbedingt optimal. Da wir bis zu 10 Kombinatoren fest codieren dürfen, bleiben 7 Optionen.

Andere bekannte kombinatorische Kombinatoren sind

B x y z = x (y z)
C x y z = x z y
W x y = x y y

die zusammen mit K, eine vollständige Basis machen . In SK sind dies

B = S (K S) K
C = S (S (K (S (K S) K)) S) (K K)
W = S S (S K)

und die SKIRegeln leiten dieselben Ausdrücke für Bund ab C, aber für Wsie S S (K (S K K)). Ich habe mich daher für Weinen Sonderfall entschieden.

Programm (CJam)

e# A tests whether argument is an array
{W=!!}:A;

e# F "flattens" an expression by removing unnecessary parentheses, although if the expression is a primitive
e# it actually wraps it in an array
{
  e# A primitive is already flat, so we only need to process arrays
  _A{
    ee{
      ~
      e# Stack: ... index elt
      e# First recurse to see how far that simplifies the element
      F
      e# If it's an array...
      _A{
        e# ... we can drop a level of nesting if either it's the first one (since combinator application
        e# is left-associative) or if it's a one-element array
        _,1=@!|{
          e# The tricky bit is that it might be a string, so we can't just use ~
          {}/
        }*
      }{
        \;
      }?
    }%
  }{a}?
}:F;


qN%{

e# Parse line of input
"->=()"" [[[]"er']+~
e# Eliminate the appropriate variables in reverse order. E eliminates the variable currently stored in V.
\,:)W%{
  e# Flatten current expression
  F

  e# Identify cases; X holds the eXpression and is guaranteed to be non-primitive
  :X
  [
    XVa=                  e# [V]
    Xe_V&!                e# case V-free expression
    X)_A0{V=}?\e_V&!*     e# case array with exactly one V, which is the last element
    X_e_Ve=~)>[VV]=X,2>*  e# case array with exactly two Vs, which are the last two elements
  ]
  1#
  e# Corresponding combinators
  [
    {;"SKK"}              e# I
    {['K\]}               e# K
    {);}                  e# X (less that final V)
    {););['S 'S "SK"]\a+} e# W special-cased as SS(SK) because the general-case algorithm derives SS(K(SKK))
    {['S\)E\E\]}          e# S (catch-all case)
  ]=~
}:EfV

e# Format for output
F
{
  _A{
    '(\{P}%')
  }*
}:P%

oNo}/

Online-Testsuite

Generierte Ausgaben:

S(KS)K
S(S(KS)(S(KK)S))(KK)
S(K(SS))(S(KK)K)
S(S(KS)(S(KK)(S(KS)(S(K(S(SKK)))K))))(KK)
S(K(S(K(SS(SK)))))(S(K(SS(SK)))(S(SKK)(SKK)))
KK
S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K)
S(S(KS)(S(K(S(KS)))(S(S(KS)(S(KK)(S(KS)K)))(K(S(S(KS)(S(K(S(SKK)))K))(K(SKK)))))))(K(S(KK)(S(SKK)(SKK))))
S(K(S(KK)))(S(K(S(S(SKK)(SKK))))K)
K(SKK)
S(K(S(S(KS)(S(KS)))))(S(KK)(S(KK)K))
S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))(S(K(SS))(S(KK)K))))))(K(S(KK)K))
S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(S(KS)(S(KK)(S(KS)(S(K(S(SKK)))K))))(KK))))))(K(KK))
S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(K(S(SKK)))K)))))(K(KK))
S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)K)))))(K(S(KS)K))
S(K(S(KS)))(S(KK))
S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)K)))))(K(S(S(KS)(S(K(S(KS)))(S(S(KS)(S(KK)(S(KS)K)))(K(S(S(KS)(S(S(KS)K)(K(S(SKK)(SKK)))))K)))))(S(KK)K)))))))(S(KK)(S(KK)K))
S(KK)(S(KK))
KK
S(KK)(S(KK)(S(S(KS)K)(S(K(S(SKK)))(S(K(S(SKK)))K))))
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K))))))(S(KK)(S(KK)K))
S(KK)
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(KS))))))))(S(KK)(S(KK)(S(KK)K)))
S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(KS)))))(S(KK)(S(KK)K))))))))(K(S(KK)(S(KK)K)))
S(KS)(S(KK)(S(KS)K))
S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(SKK)(SKK)))))))))(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(SKK)))))))(S(K(S(K(S(KK)))))(S(K(S(SKK)))K))))))(S(K(S(KK)))(S(K(S(KK)))(S(K(S(SKK)))K))))))))))(K(K(KK)))
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K))))))(S(KK)(S(KK)K))))))))(S(KK)(S(KK)(S(KK)K)))
K(S(KK))
S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(KS)))))(S(KK)(S(KK)K))))))))(K(S(KK)(S(KK)K))))))))))(K(K(S(KK)(S(KK)K))))
S(KK)(S(K(S(KK)))(S(K(S(KK)))))
K(S(KK)(S(KK)))
S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(KK))))))))))(K(S(K(S(KK)))(S(S(KS)(S(KK)(S(KS)K)))(K(S(K(S(SKK)))K)))))
S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(KK)))))(S(K(S(K(S(KS)))))(S(S(KS)(S(KK)(S(KS)(S(KS)))))(K(S(KK)K))))))))(K(K(KK)))
S(K(S(K(S(KK)))))(S(K(S(KK))))
S(K(S(K(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(SKK)))))(S(K(S(KK)))(S(K(S(SKK)))K)))))))))))(S(K(S(K(S(KK)))))(S(K(S(K(S(KK)))))(S(K(S(K(S(KK)))))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K)))))
S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(KK))))))))))(K(S(K(S(KK)))(S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(K(S(SKK)))K))))))(K(S(K(S(KK)))(S(K(S(SKK)))K))))))))))))))(K(K(K(K(KK)))))
S(KK)(S(K(S(KK)))(S(K(S(KK)))(S(K(S(KK)))(SS(SK)))))
K(S(K(S(KK)))(S(K(S(KK)))))
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K))))))(S(KK)(S(KK)K))))))))(S(KK)(S(KK)(S(KK)K))))))))))(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K)))))
S(K(S(KK)))(S(K(S(K(S(KK)))))(S(K(S(K(S(KK)))))(S(K(S(K(S(KK)))))(S(KS)K))))
S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)K)))))))))))(K(S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(S(KS)(S(KK)(S(KS)K)))))))(S(K(S(KK)))(S(S(KS)(S(KK)(S(KS)K)))(K(S(K(S(SKK)))K)))))))))))(K(K(S(KK)(S(KK)K))))))
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K))))))(S(KK)(S(KK)K))))))))(S(KK)(S(KK)(S(KK)K))))))))))(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K))))))
K(K(K(K(K(S(KK)(S(KK)(S(S(KS)(SSK))(K(SKK)))))))))
S(KK)(S(K(S(KK)))(S(K(S(KK)))(S(K(S(KK)))(S(K(S(KK)))(S(KK))))))
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K))))))(S(KK)(S(KK)K))))))))(S(KK)(S(KK)(S(KK)K))))))))))(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K)))))))
S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))))(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(KK)))))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(K(S(KS)))(S(S(KS)(S(KK)(S(KS)(S(K(S(SKK)))K))))(KK))))))(S(KK)(S(KK)K))))))))(K(K(S(KK)K))))))))))(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))(K(K(K(S(KK)(S(KK)K))))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))))))(K(K(K(K(S(KK)(S(KK)(S(KK)K))))))))))))))))))(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K))))))))
S(S(KS)(S(K(S(KS)))(S(K(S(KK)))(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))))))(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))))(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(K(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))))(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(K(S(K(S(K(S(KS)))))))))(S(K(S(K(S(K(S(K(S(K(S(KS)))))))))))(S(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(KK)(S(KS)(S(K(S(KS)))(S(S(KS)(S(KK)(S(KS)(S(K(S(SKK)))K))))(KK))))))))))))(K(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(KK)))))))(S(S(KS)(S(KK)S))(KK))))))))))))))(K(K(K(K(S(KK)(S(KK)K))))))))))))))))(K(K(K(K(K(S(KK)(S(KK)K))))))))))))))))))(K(K(K(K(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))))))))))))(K(K(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)(S(KK)K)))))))))
K(S(K(S(KK)))(S(K(S(K(S(KK)))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(KK))))))))))
S(KK)(S(K(S(KK)))(S(K(S(K(S(KK)))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(K(S(KK)))))))))))(S(K(S(K(S(K(S(K(S(K(S(SKK)))))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(SKK)))))))))(S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(SKK)))))))(S(K(S(K(S(KK)))))(S(K(S(K(S(SKK)))))(S(K(S(KK)))(S(K(S(SKK)))K))))))))))))))
S(K(S(K(S(K(S(KK)))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(K(S(K(S(K(S(KK)))))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(K(S(K(S(KS)))))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(K(S(KS)))))(S(K(S(S(KS)(S(K(S(KS)))(S(K(S(S(KS)(S(K(S(SKK)))K))))(S(KK)K))))))(S(KK)(S(KK)K))))))))(S(KK)(S(KK)(S(KK)K))))))))))(S(KK)(S(KK)(S(KK)(S(KK)K))))))))))
Peter Taylor
quelle