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

Also Stärke-Normalisierung für den einfach getypten Lambda-Kalkül.

Ja, das hatte ich ja schon mal angekündigt. Wir haben zwar gesehen, dass der untypisierte Lambda-Kalkül

nicht stark normalisierend ist. Das ist sogar Therme, da gibt es die gar keine Normalform haben,

also der ist noch nicht mal schwach normalisierend.

Dass aber die getypten Systeme vielfach jedenfalls durchaus stark normalisierend sind.

Das ist jetzt, wenn man sich mal ein paar Übungen angeguckt hat, welche Funktionen man im getypten Lambda-Kalkül so schreiben kann.

Das ist nicht gesteigert überraschend. Der einfach getypte Lambda-Kalkül ist insbesondere eindeutig nicht Turing-mächtig.

Man kann also nichts hinschreiben, was irgendwie in der recursiven Definition oder so was ähnelt.

In der Tat sind also die Funktionen, die man schreiben kann, alle eher so ein bisschen von der langweiligen Sorte, muss man mal sagen.

Und insofern ist also die Tatsache, dass der stark normalisierend ist, nicht überraschend.

Der Beweis, den wir heute also anstreben, ist auch dementsprechend noch nicht mal besonders schwer.

Das Erstaunliche ist, dass eben genau derselbe Beweis mit eben entsprechenden Erweiterungen auch für wesentlich kompliziertere Systeme,

also wesentlich kompliziertere Typsysteme und ausdrucksstärkere Typsysteme funktioniert, in denen man durchaus ernsthaft programmieren kann.

Zum Beispiel funktioniert er für den Lambda-Kalküls weiter Ordnung, wie man ihn nennt, oder System F,

in dem man nicht alle Turing programmierbaren Funktionen natürlich programmieren kann, wenn er stark normalisierend ist.

Das wäre ein eindeutiger Widerspruch.

Aber man kann in ihm alle Funktionen typisieren, die beweisbar total sind mit Mitteln der normalen Mathematik,

also mit Mitteln der Arithmetik zweiter Stufe, also Arithmetik zweiter Stufe gleich Analysis.

Das heißt, man muss sich schon ziemlich auf den Kopf stellen, um eine Funktion zu finden, die rekursiv ist und total

sich aber im System F nicht typisieren lässt.

Gut. Ja, machen wir einfach mal...

So, was wir dazu tun, ist, wir führen etwas ein, was wir bisher nicht hatten.

Wir haben bisher rein syntaktisch agiert und wir fügen ein sowas Ähnliches wie eine Semantik, also eine Interpretation von Typen und Termen.

Das ist alles sehr unsemantisch, weil wir einfach nur wieder durch syntaktisches Material interpretieren.

Insofern schreibe ich jetzt mal Pseudo-Semantik. Das ist kein wissenschaftlicher Ausdruck, deswegen setze ich es hier in Anführungsstriche.

Wenn Sie selber mal Texte schreiben, wenn Sie was in Anführungsstriche schreiben, dann überlegen Sie sich, ob Sie es sagen wollen.

Entweder man will es wirklich sagen, dann lässt man die Anführungsstriche weg oder man schreibt etwas anderes, aber hier in der Tafel spare ich lieber Platz.

Und zwar definieren wir eine Pseudo-Semantik für Typen. Die schreiben wir, wie man Semantiken halt so schreibt, und zwar mit diesen komischen Doppelklammern hier,

für die es in LaTeX kein anständiges Symbol gibt und die man sich deswegen irgendwie zurecht schummeln muss, indem man zweieckige Klammern übereinander schreibt.

Und zwar definiere ich die Semantik eines Typs als jeweils eine Teilmenge der Menge aller Terme, und zwar konkreter,

als eine Teilmenge einer Menge, die nenne ich Sn, mit der offensichtlichen Bedeutung.

So, das ist die Menge aller Terme T im Lambda-Kalkül. Das Symbol habe ich bisher noch nicht benutzt, das füre ich jetzt mal ein.

Also, groß Lambda ist einfach die Menge aller Lambda-Termen. Und Sn besteht aus denjenigen Lambda-Termen T, die stark normalisierend sind.

Um das jetzt einzuführen, brauche ich einen Operator auf solchen Teilmengen.

Und zwar definiere ich für beliebige Mengen A und B von Lambda-Termen, zum Beispiel die Interpretationen irgendwelcher Typen,

eine Menge, die schreibe ich ab Pfeil B, und die schreibe ich nicht zufällig so, die hält mir also später her als Interpretation für Funktiontypen.

So, und das ist dann die Menge aller Lambda-Terme T. So, das gilt für alle Lambda-Terme S in A,

ist der Lambda-Term, den ich bekomme, indem ich T auf S anwende, ein Element von B.

Ja, das ist so an der Oberfläche eine relativ offensichtliche Funktion, eine Definition.

Also ich interpretiere, wenn ich zwei Mengen von Lambda-Termen habe, definiere ich also den Funktionentyp gewissermaßen von A nach B,

als die Menge derjenigen Terme, die, wenn ich sie auf Dinge in A anwende, was in B liefert, so weit so offensichtlich.

Aber man muss sich klarmachen, dass das hier rein syntaktisch ist.

Also das heißt nicht etwa zum Beispiel, dass ich T auf S anwende und dann irgendwie Beta reduziere und dann in B lande oder sowas,

die rein syntaktische Definition, dass wirklich der Term, der vorne aus T und hinten aus S besteht, in B sein muss.

Das ist also sehr, sehr unsymantisch. Gut, trotzdem klappt es.

Ich schreibe mal einen Doppelpunkt davor, um klarzulachen, dass es eine Definition ist.

Ja, so damit definiere ich jetzt diese Semantikfunktion, die mir also zu jedem Typ eine Teilmenge von S n definiert.

Das mache ich durch Rekursion über die Grammatik der Typen. Das ist recht kurz.

Es gibt ja nur zwei Alternativen in dieser Grammatik. Ein Typ kann eine Typvariable sein oder ein Funktionentyp.