Das Lambda-Kalkül und die Turing-Maschine sind zwei formale Systeme, die beide die theoretischen Grundlagen der Berechenbarkeit darstellen. Sie wurden unabhängig voneinander entwickelt, um zu zeigen, wie man Funktionen berechnen und Algorithmen formulieren kann. Obwohl sie unterschiedlich in ihrer Herangehensweise und Struktur sind, haben sie viele Gemeinsamkeiten, da sie beide universelle Berechnungsmodelle darstellen. Jedes Problem, das mit einer Turing-Maschine gelöst werden kann, kann auch im Lambda-Kalkül ausgedrückt und gelöst werden und umgekehrt.
Im Folgenden steht \ für das Lambda-Zeichen \(\lambda\), welches aber nur im Browser gerendert wird.
Ein Lambda-Term besteht aus Variablen (x, y, z, A, B, C, 1, 2, 3, ...), Lambda-Abstraktionen \x.t, Anwendungen t s und Klammerungen (t). t und s sind hier ebenfalls Lambda-Terme. Dabei ist zu beachten, dass Zahlen nicht ihrem Wert entsprechen, sondern genau wie Buchstaben einfach nur Variablen darstellen. Außerdem bindet jede Lambda-Abstraktion nur eine Variable.
Ein Lambda-Term lässt sich ggf. reduzieren, also vereinfachen, bis zu seiner Normalform. Es gibt drei Reduktionsformen: Alpha, Beta und Gamma. Ein Term ist in seiner Normalform, wenn er nicht weiter beta-reduziert werden kann. Zudem ist eine Normalform immer eindeutig, sprich, wenn es eine Normalform gibt, dann gibt es nur genau eine. Im Folgenden benutzen wir die deterministische Reduktionsstrategie Leftmost outermost.
Hier ein paar Beispiele:
Wahrheitswerte:
true = \x.\y.x (eine Funktion mit zwei Parametern, der zweite wird verworfen)
false = \x.\y.y (eine Funktion mit zwei Parametern, der erste wird verworfen)
Logische Operatoren:
and = \p.\q.p q p
or = \p.\q.p p q
not = \p.\a.\b.p b a
Wem das Ganze verwirrend vorkommt, der liest sich am besten im Internet in die Thematik ein, es lohnt sich!
So, nun zu der Geschichte:
Ich hatte schon länger an einem Lambda Term Generator gearbeitet und ihn auch fast fehlerfrei zum Laufen bekommen, als ich eines Tages nach einer längeren Coding Session, vergaß meine Änderungen zu speichern und somit all die Arbeit verloren war. Zuvor hatte ich die Koordinaten eines Schatzes in einen Lambda-Term verwandelt, der mir, zusammen mit einem Auszug einer Logdatei der Prozedur, von dem ganzen Schlamassel übrig geblieben ist. Als ich mir die Datei genauer anschaute, traf mich der Schlag: scheinbar hatte ich ein paar Fehler eingebaut und die Koordinaten somit falsch kodiert. Jetzt ist es an dir, mir zu helfen und zusammen mit der Logdatei und dem Lambda-Term die ursprünglichen Koordinaten herauszufinden.
Hier die Logdatei, welche bei der Generierung des Terms erzeugt wurde:
> Input: N 4 8 ... E 0 0 9 ...
> Schritt 1: erfolgreich
> Schritt 2: erfolgreich
> Schritt 3: erfolgreich
> Schritt 4: Warnung: Vor der Beta-Reduktion wurde keine Alpha-Konvertierung durchgeführt
> Schritt 5: Warnung: Vor der Beta-Reduktion wurde keine Alpha-Konvertierung durchgeführt
> Schritt 6: erfolgreich
> Schritt 7: erfolgreich
> Schritt 8: Warnung: Vertauschung von erster und letzter Klammer
> Schritt 9: Warnung: Der Wert aller geraden Zahlen wurde halbiert
> Resultierender Term: (\u.\s.\o.\g.\p.N 2 4 1 s E o o 9 u D) A (\m.\l.l (g g p) (g m p) 0 5 (G B))
Edit 14.09.24: Da hat sich von Beginn an ein kleiner Zahlendreher eingeschlichen (Minute der Ostkoordinate -1).
Edit 22.11.24: D3.5 -> D4