Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Fantastisch. Ja, herzlich willkommen. Für Berg ist es ja geradezu noch voll.

Ja, wir beginnen mit einer Ansage. Die Intensivübung, wie sie da lesen,

ist in der Woche am 29.05. ist die übernächste, in der übernächsten Woche im H6.

So, ich habe jetzt vorgestern nochmal mit den Tutoren gesprochen, inwieweit sich der

Eindruck, dass der Stoff zu schnell in den Tutorien rankommt, nachdem er in der Vorlesung dran war.

Die Tutoren haben das nicht ganz teilen können, bzw. haben zum Teil auch mich in meiner Ansicht

bestärkt, dass das natürlich eigentlich ein wünschenswerter Effekt ist, wenn möglichst

unmittelbar geübt wird. Wir haben da keinen Schlacker mehr drin. Die Übungen sind auf Kante

genäht. Die können wir nicht nach hinten schieben. Was ich jetzt tun werde, ist folgendes. Ich werde

einen Kapitel aus dem einfach getypten Lambda-Kalkül, das jetzt eigentlich noch hätte kommen sollen,

nämlich die starke Normalisierung. Das werde ich hinten in einen anderen Block schieben,

wo wir dann das gleichzeitig mit der starken Normalisierung in System F abhandeln, also in

dem Lambda-Kalkül mit Polymorphentypen. Dadurch kommen wir jetzt also mit den folgenden Stoff

so ein bisschen nach vorne, dass wir also hoffentlich ein bisschen rechtzeitiger vor

den Übungen dran sind. Wir haben heute noch so ein bisschen Aufräumarbeiten, also mehrere

kleinere Themen aus dem einfach getypten Lambda-Kalkül und zeigen dann am Donnerstag,

nein, was ist heute Donnerstag, also zeigen dann nächste Woche, nicht am Montag, sondern am

Donnerstag, noch die Church-Rossa-Eigenschaft, die eine Eigenschaft jetzt wieder des ungetypten

Lambda-Kalküls ist, bzw. eine Eigenschaft, die von Typisierung unabhängig ist, die also in allen

Varianten gilt. Und wären dann mit dem Thema Lambda-Kalkül nach dieser leichten Planänderung,

also vorerst fertig und machen dann weiter zunächst mit induktiven Datentypen. So, heute,

wie gesagt, noch verschiedene einzelne Dinge. Wir beginnen mit einem weiteren Beispiel zum

Thema Berechnung von Prinzipaltypen. Wir haben ja bisher nur positive Beispiele gesehen und wollen

jetzt auch noch mal eins abhandeln, das negativ ist. Negativ kann ja nur heißen, dass die

Unifikation scheitert. Also die Gleichungsmenge kann ich ja immer ausrechnen, das ist einfach

eine primitiv-requersive Definition einer Menge. Was eben schiefgehen kann, ist die Unifikation dieser

Gleichungsmenge am Ende. Und jetzt sehen wir also hier, dass in unserem Standardbeispiel eines

büsentherms, Lambda x Punkt x x, dass da auch dieser Algorithmus scheitert. Muss er? Ja, wir haben ja

gezeigt, dass er korrekt ist und wir haben uns schon mal zu Fuß überlegt, dass dieser Therm keinen

Typ haben kann. Und jetzt sehen wir, dass der Algorithmus das auch leistet und wir sehen,

was da bei der Unifikation schiefgeht. Das ist vielleicht insbesondere interessant für die Leute,

die nicht in Gleun waren, die jetzt also hier das erste Mal wirklich demonstriert kriegen,

einen negativen Fall von Unifikation. Das heißt also ein Gleichungssystem, das nicht unifizierbar ist.

Also, sagen wir das mal wissenschaftlicher. So, also in der eingeführten Terminologie heißt das,

dieser Therm Lambda x Punkt x x, der ist nicht typisierbar. Dazu müssen wir eben wieder diese

Menge pt ausrechnen, dieses Gleichungssystem. Wir fangen an mit dem d-Kontext, das ist ein geschlossener

Therm, wir brauchen also keine Variable im Kontext. Da kommt der Therm und da hat er eine frische Typ-Variabe.

So, okay, wir haben ja also einen Lambda-Therm, wir sind ja nur mittlerweile in Übung, wie man das macht.

Wir führen jetzt hier im Kontext die Variable x ein. x bekommt einen frischen Typ, a ist schon

vergeben, also b. Hier kommt der Therm unter der Lambda-Abstraktion, also x x und das bekommt wieder

ein zunächst unbekanntes Typ. So, also wie gesagt, wir haben jetzt also hier eine frische Variable für den Typ von x eingeführt

und eine für den Typ des Gesamtausdrucks. Und dazu kommt ein Constraint, der uns eben sagt, der Typ,

den unser ursprünglicher Ausdruck kriegt, der muss sein ein Funktionstyp.

Wir können jetzt hier die Variable x einstellen.

Gut, jetzt sehen wir uns das hier an, hier haben wir eine Applikation.

So, bei der rekursiven Klausel für Anwendung, da bleibt also der Kontext gleich.

Und wir bekommen eine neue Typvariable für den Typ, der hier zwischensitzt zwischen der Anwendung und ihrem Argument.

Also kriegt x jetzt Typ D nach C. Nee, Quatsch, hier Semikolon, da Klammer zu.

So, dann brauchen wir eine passende Typisierung für das Argument. Gut, das ist wieder x, also muss x Typ D bekommen.