Ja, herzlich willkommen!

Ja, Thema für heute, Wetterreduktion.

Mit anderen Worten das eigentliche Funktionieren der Maschine, die der Lambda-Kalkül letztlich vom Zweck her darstellt.

Ich erinnere nochmal an die Reduktionsregel.

Wann immer ich eine Lambda-Abstraktion habe, die also die anonyme Funktion bezeichnet, die x abbildet auf t,

wobei t typischerweise von x abhängt, und diese anonyme Funktion anwende auf einen Term s,

dann reduziert das zum erwarteten Term, wo ich eben schlicht und einfach den Argumentterm hier in das Vorkommen der Parameter der Variablen einsetze.

Das heißt, das reduziert zu t mit s substituiert für x. Machen wir mal ein Primitivbeispiel.

Wenn ich mir mal kurz vorstelle, in unseren Termen würden Dinge vorkommen wie x, wie 3 und plus oder sowas. Für den Moment können wir uns die vorstellen als die 3 als eine Variable, die nicht erwähnt ist,

und die ist plus sogar auch als eine Variable, die eben eine Funktion ist und die wir jetzt hier zufällig infix schreiben. Alles egal.

Wenn wir da jetzt diese Funktion anwenden auf einen Term, sagen wir y plus 4, dann reduziert das zu dem, was ich bekomme, indem ich in diesen Term hier, 3 plus x, für das x den Term hier einsetze, also y plus 4.

Richtig, danke. Der Pfeil ist natürlich ohne Null. Denn ich habe zwar keinen Kontext, aber ich wende es auf eine Substitution an.

Naja, fast. Nee, ich dürfte hier noch Null schreiben. Nee, das habe ich mir ins Boxauen jagen lassen.

Alle diese Dinge hier sind gewissermaßen Reduktionsregeln. Das heißt, die Menge der Reduktionsregeln ist in diesem Falle also insbesondere nicht endlich.

Das ist also Regel für jedes T und S. Ich könnte das S hier durch eine Variable ersetzen. Das ginge.

Ich könnte es so formulieren. Ja, und dann kann ich sogar ganz großzügig sein. Dann kann ich nämlich das Argument, auf das ich es anwende, einfach x nennen.

Dann muss ich nichts mehr tun. So, das reduziert dann einfach zu T.

Und dann kann ich in diese Regel, könnte ich dann einfach für das x einsetzen und bekomme genau diese hier. Einfach per Stabilität.

Aber es sind immer noch unendlich viele, weil ich das T über beliebige Terme laufen lasse.

Ich überlege, ob ich... Da müsste ich ziemlich hier Klimmzügen machen, um jetzt das T auch noch durch eine Variable zu ersetzen.

Das wird nichts, weil ich dann die Abhängigkeit von dem... Naja, ja doch. Dann könnte auf so eine Idee kommen.

Dann habe ich jetzt das T auch noch durch eine Variable ersetzt. Ich muss natürlich einfangen, dass das T von dem x abhängen kann.

Da ich machte, dass T jetzt also zu einer Funktionsvariable in y, für die ich jetzt beliebiges Zeugs einsetzen kann.

Aber um jetzt hier einzufangen, dass ich in der beliebigen Funktionsvariable in y den Effekt von jedem Term bekomme, brauche ich glaube ich wieder Betterreduktion.

Insofern... Ne, also ich glaube, das ist doch zu großzügig.

So, also mit anderen Worten, nein. Wir haben das hier praktisch schon voll zutriert als Regel eingeführt.

Was wir tun, ist nur noch Kontexte außenrum setzen in diesem Fall. Und insofern ist es also tatsächlich sogar gerechtfertigt, hier Index nur ranzuschreiben.

Gut.

Manchmal übrigens schreiben wir hier statt... Wofür schreiben wir das? Wir schreiben...

Für die Einschrittreduktion schreiben wir der Klarheit halber die meiste Zeit auch Index Better. Um klar zu machen, dass wir eben nach Betterregeln reduzieren.

Das ist deswegen nötig, weil es im Lambda-Kalkül durchaus auch andere Reduktionsregeln als nur dieses Better gibt.

Also außerhalb der Grundreduktion... äh, außerhalb der Grundversion gibt es also noch weitere Regeln, die da auftauchen könnten.

Und wir befassen uns aber nur mit dem Setting, wo Better die einzige Reduktionsregel ist.

So, nicht? Also...

Ja, das sollte man vielleicht mal ausdrücklich festhalten, wie dann also die Einschrittreduktion, die wir damit als den Kontext abgeschlossenen und stabilen Abschluss bekommen, aussieht.

Das ist das hier.

Ich nehme also genau den Term, den ich hier auf der linken Seite der Reduktionsregel finde, packe noch einen Kontext C außen rum und reduziere natürlich zum gleichen Kontext und dann aber mit dem Betterredukt T mit S substituiert für X hier im Freitplatz.

Das heißt, es findet keine, wie eben diskutiert, es findet hier also keine Substitution mehr statt, weil die Substitution schon da drin steckt, dass das T und S beliebige Term sind.

Ja, ich habe eben schon erwähnt, es gibt andere Reduktionsregeln, mindestens eine, obwohl wir uns damit nicht weiter befassen werden, sollte man zur Bildung zumindest mal gesehen haben.

Und zwar ist das diese hier.

Wenn ich eine Lambda-Abstruktion habe, wo schlicht und einfach im Körper nur eine Funktion, für die ich schon Bezeichner habe, also das F ist hier, ja das kann jetzt hier eine Variable sein, ist egal, auf das Argument anwende, dann ist das ja, was da entsteht, ist ja einfach der Effekt von dem F.

Und in der Tat kann man also den Lambda-Kalkül um eine Reduktionsregel erweitern, die aus so einer Lambda, also aus so einer anonymen Funktion, die in Wirklichkeit so anonymen gar nicht ist, eben schlicht und einfach dieses F wieder macht.

Und diese Regel heißt Eta, wenn Sie es mal sehen.

In Eta wird es aber viel komplizierter und es gibt auch sogar Debatten, ob Eta in dieser Richtung oder lieber in der anderen Richtung verwendet werden sollte.

Insofern, das lassen wir jetzt also mal als zu kompliziert beiseite.

So.

Dann machen wir mal Beispiele.

Wie schon angedeutet, können wir ja im Lambda-Kalkül fiese Dinge tun, zum Beispiel das Argument einfach auf sich selber anwenden.

So, wir verstehen nicht, was so ein Term soll, aber wir können, wenn er irgendwo angewendet wird, ihn better reduzieren. Wenn wir zum Beispiel so ein Ding anwenden auf, worauf wollen wir das anwenden?

Sagen wir diesen Term hier yx, also yx heißt y angewendet auf x.