Herzlich willkommen!

Ja, wir sind an sich beim Thema einfach getüpter Lambda-Kalkül.

Sie erinnern sich noch an meinen Hänger letzte Woche beim Thema Standardisierungssatz,

beziehungsweise dem Beweis des Hauptlambas.

Die technischen Einzelheiten haben alle gestimmt.

Die Grobstruktur des Beweises war nicht richtig angegeben.

Korrekt lautet sie wie folgt.

Induktion über U wie ursprünglich angegeben, das hatte ich irgendwann in meiner Verwirrung auch über V korrigiert,

weil ich Eigenschaften von V und nicht von U brauchte.

Und diese Eigenschaften verschafft man sich aber stattdessen, indem man dann eine Fallunterscheidung über V1 aufmacht.

Ansonsten ändert sich am Beweis nichts, er geht dann genauso durch, wie wir ihn geführt haben.

Korrigierte Versionen finden Sie schon im Onlineskript.

So, kurze Überschrift.

Das hier ist das Symbol für den einfach getüpten Lambda-Kalkül.

Oder den Unterstrich, also der Unterstrich ist der Unterstrich unter der Überschrift, also das Symbol ist das hier mit dem Pfeil zu Ehren des einzigen Typkonstruktors.

Wir hatten die Typregeln letztes Mal kennengelernt und wir hatten auch schon ein ganz einfaches Beispiel gesehen, wie man also einen Term typisiert.

Das war dieser hier, der also wenig überraschenderweise im leeren Kontext, der hat ja keine freien Variablen, den Typ A nach A bekommt.

Das können Sie übrigens auch in jeder funktionalen Programmiersprache spielen, wenn Sie also einen Haskell-Interpreter laden oder sowas,

dann können Sie dem Term in die Hand drücken und sagen, er soll gefälligst den Typ dazu ausspucken und dann spuckt er das da aus.

Wird vielleicht anderer Schreibweise, ich glaube statt A schreibt er Stern oder sowas.

So, machen wir mal ein ernsthaftes Beispiel.

Das hier war ja wirklich nicht so richtig ernsthaft, das ein, nein, ernsthaft nehme ich zurück.

Also das nächste, das kommt jetzt auch nicht ernsthaft, dann könnte ich es nicht hier an der Tafel machen.

Aber immerhin enthält es mal überhaupt alle syntaktischen Konstrukte, nämlich auch Applikationen, die ja hier nicht vorkamen.

So, ja, jetzt fangen wir also wieder an mit der Publikumsfrage.

Was ist der Typ von dem Ding? Glauben Sie.

Ja.

Moment, nochmal.

Ja, ne.

Also, ja, es ist eine Funktion mit zwei Argumenten, insofern der Typ wird so aussehen ungefähr.

So, die Frage ist jetzt, kann man da wirklich beliebige Argumente reinstecken?

Wahrscheinlich nicht, denn man möchte eines der Argumente auf das andere anwenden.

Ja, genau, so müsste, wenn alles mit rechten Dingen zugeht, nachher der Typ von dem Ding aussehen.

Wobei, also der Typ werden wir sehen, ist jetzt eine noch etwas unpräzise Sprechweise,

aber es ist in einem relativ präzisen Sinne der Typ oder der beste Typ dieses Ausdrucks.

Ja, so müsste das klappen und dann versuchen wir mal, ob unsere Typregeln das wirklich hergeben.

So, ich brauche ein bisschen mehr Platz.

Wahrscheinlich ist das übertrieben und ich brauche ihn gar nicht. Mal gucken.

So, wir bauen mal so einen Herleitungsbaum von unten nach oben.

Also, der Kontext, den können wir wieder leer lassen. Es gibt wieder keine freien Variablen.

So, da muss also irgendwas rauskommen. Wir gehen jetzt mal ganz lustig vor.

Das hier ist ja eine Abkürzung für zwei Lambdas hintereinander. Lambda x, Lambda y.

Was wir oben drauf sehen, ist also ein einzelnes Lambda. Das heißt, irgendwie muss da das rauskommen.

Na ja gut, wir wissen, der Typ ist etwas länger, also machen wir das irgendwie vielleicht hier vielleicht.

Ist das richtig? Reicht noch nicht ganz.

Wir wissen nicht, was links steht, wir wissen nicht, was rechts steht, aber ein Funktionpfeil sollte da hoffentlich stehen.

Den müssen wir per der einzigen Regel, die auf Terme dieser Form passt, der Einführungsregel für ein Funktionpfeil, eben einführen.

So, wie funktioniert die Regel? Nun, die Regel sagt, wir nehmen uns die abstrahierte Variable hier, das x, packen sie in den Kontext.

Gut, das kriegt dann einen zunächst noch nicht bekannten Typ.

So, und da müssen wir dann den Rest typisieren. Lambda y, x, y.