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

Ja, herzlich willkommen.

Ja, zur Erinnerung, wir beschäftigen uns weiterhin mit System F in verschiedenen

Spielarten, das heißt heute werden es verschiedene Spielarten werden, bisher

kennen wir ja nur eine.

Ja, fassen wir noch mal zusammen, was an Eigenschaften von Lambda 2, ja, schonmal

sagen wir erwähnt worden ist, vielleicht zum Teil demonstriert worden ist und

zum Teil für die Zukunft versprochen worden ist.

Erstens Lambda 2, also der Curry Style System F, wie wir das bisher

kennengelernt haben, ist ausdrucksstark, also man kann im Gegensatz zum einfach

geteupten Lambda-Kalkül eine Menge von, ja, rekursiv programmierten Funktionen

tatsächlich im System ausdrücken, mit anderen Worten typen.

Obwohl sehr ausdrucksstark ist das System terminierend oder stark

normalisierend, das verspreche ich schon länger und das realisieren wir

Donnerstag.

Und dann gibt es diese statischen Fragen der Typ Inferenz und des Typ Checkings

und die sind, werden wir hier nicht zeigen, das ist zu kompliziert, die sind

unentscheidbar, lange offenes Problem gelöst von Wells 1994.

So, die Frage ist jetzt für die heutige Sitzung insbesondere, was tun wir denn

nun gegen das letztere Problem, ja, das ist ja doch so ein bisschen unangenehm,

also klar ist es schön also eine Sprache zu haben, wo also Terminierung von

typisierbaren Programmen garantiert ist, aber andersrum würde man auch schon

gerne mal einen Compiler bauen können, von dem garantiert ist, dass er nicht

irgendwann in den Wald läuft, ja, also man möchte da entscheidbare

Typisierung haben, gut, so dringend ist es anscheinend dann doch wieder nicht, wie

gesagt gibt es ja Compiler, die mit System F in der Curry Form, wie wir es hier

kennengelernt haben, umgehen, gut, in der Tat muss man dann bei den Compilern

damit rechnen, dass sie eventuell wahr nicht wiederkommen, ja, also dass man den

Programmtext vorwirft und die schlicht und einfach deswegen nicht terminieren,

weil sie nicht entscheiden können, ob das typ korrekt ist, was man da geschrieben

hat, gut, ist tatsächlich so, aber gut, es wäre also zumindest gut mal zu wissen,

wie weit man denn gehen kann oder ob man das irgendwie fixen kann auf eine Weise,

die eben dann doch an diesen relativ elementaren Stellen wieder

Entscheidbarkeit garantiert, so und das kann man fixen auf zwei Weisen, die Arte

ist relativ offensichtlich, wenn ich Typen nicht inferieren kann, schreibe ich sie

halt dran, so da haben wir schon einen Namen für, wir machen also aus dem System

à la Curry, wie wir es bis jetzt kennengelernt haben, ein Church System,

also eins, wo wir Typen wirklich an die Terme mit dran schreiben, dann

kollabiert der Typ, checkt zumindest mal ins Triviale, ja, weil ich einfach nur,

ja gut, wir werden sehen, inwiefern das also alles kollabiert und warum das

einfach ist, also jedenfalls die Probleme, die man hat, die verschwinden dann

schlicht und einfach, und zwar eben auf geschummelte Art und Weise, man hat eben

das Problem, was man lösen will oder was man den Computer lösen lassen will, das

hat man in Wirklichkeit schon selber gelöst, indem man also für alles, was

man da hinschreibt, insbesondere eben für gebundene Variable, schon die Typen

einfach angibt. Und, ja, während also das Church System,

zwar, naja, das ist irgendwie unangenehm, weil man natürlich Typen nicht angeben

will, die Typen sind ja dann zum Teil auch kompliziert und man muss die dann

alle dahintippen, das will man normalerweise nicht so gern, aber außer,

dass es unangenehm ist, schadet das nichts, ja, also man behält die gesamte