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

Ja, ich erinnere ans letzte Mal, wir waren stehen geblieben,

dass wir uns überlegt hatten, dass rekursive Definitionen im wesentlichen Fixpunktgleichungen

sind. Wir hatten angegeben die rekursive Definition der Fakultätsfunktion.

Die Fakultätsfunktion wird also definiert als gleich zu folgender Funktion, nämlich diejenige

Funktion, die N, also eine natürliche Zahl, abbildet auf 1, wenn N gleich 0 ist, und ansonsten auf N mal

Fakultät des Vorgängers. Und diesen Ausdruck auf der rechten Seite, den kann man eben seinerseits

ansehen als eine Funktion, die hier Fact als Argument nimmt und eine neue Funktion ausspuckt.

Das kann ich jetzt noch mal umschreiben, etwas informell. Ich kann schreiben,

Fact sei eben definiert als der Fixpunkt von F. Da kommt jetzt plötzlich keine Rekursion mehr vor,

die verstecke ich hier in diesem Fixpunkt. Ja, ich habe jetzt also hier einen Fixpunkt-Operator,

der nimmt sich diese komplizierte Funktion hier auf der rechten Seite, das Funktionalgroße,

F und spuckt aus, einen Fixpunkt von F. Das heißt, ich unterstelle, dass im Allgemeinen gilt,

wenn ich den Fixpunkt von F ausrechne mittels meiner noch zu bestimmenden Funktion Fix und

das Funktional auf diese Funktion anwende, dann kommt da genau dieser Fixpunkt raus. Das ist eben

genau die Definition eines Fixpunkts, er wird von der Funktion in diesem Fall den Berufs F nicht

verändert. So, also das nochmals zur Erinnerung an die Motivation. Ja, rekurisive Definitionen sind

praktisch Fixpunktgleichungen. Das Ganze hatten wir uns angeguckt auf dem Weg dahin zu sehen,

dass der Lambda-Kalkül, der ungetübte Lambda-Kalkül, wohlgemerkt tatsächlich ein universelles

Berechnungsmodell ist, mit anderen Worten Turing mächtig. Das heißt, er braucht irgendeine Form von,

was weiß ich, Schleife oder Ähnlichem oder eben Rekursion. Man kann ja Schleifen durch Rekursion

ersetzen. Und das leistet im Wesentlichen folgender Satz. Also im ungetübten Lambda-Kalkül gilt folgendes,

zwei Teile. Erstens, so ich rede jetzt einmal über diese Funktion F4 allgemeiner, beschreibe ich die

also durch einen Term T, der irgendwo eine freie Variable hat, für die ich hier dieses Fakt eingesetzt

habe. So, und ich sage, jeder Term T hat einen Fixpunkt, das unterstreiche ich deswegen, weil

ich es gleich noch genauer definiere, als wir es bisher definiert haben. Der Fixpunkt ist ein Term S,

so und jetzt will ich im Wesentlichen, dass TS gleich S ist. Ja, das ist das Wesen eines Fixpunktes.

Ja, dass S ein Fixpunkt von S ist, heißt, dass TS im Wesentlichen dasselbe ist wie S. Gut,

in einer schwachen Version des Theorems könnte ich jetzt einfach die Konvertierbarkeit verlangen,

es gilt aber noch mehr. Und zwar, jetzt muss ich es richtig rummalen, zwar gilt Reduktion in einer

Richtung. Man fällt da leicht drauf rein, man denkt ja irgendwie, das hier ist ja ein einfacher

Term als der da. Meint man so, weil hier TS steht und da ist. Aber das ist natürlich nicht das,

was die Ausführungsmaschine einer funktionalen Sprache tun würde. Die Ausführungsmaschine einer

funktionalen Sprache, die, ja was wäre das? Das T, das wäre hier das F, das wäre also hier

die rechte Seite. T von S entspricht hier der rechten Seite und S der linken. Also eine

funktionale Sprache würde nicht hingehen und die rechte Seite hier mir zur linken zusammenfalten.

Ganz im Gegenteil, sie würde, wenn ich das Fact irgendwo verwende, das Fact auffalten zu seiner

Definition auf der rechten Seite und dann mal weitersehen. Das heißt, die Reduktion geht in

eine andere Richtung. Das S reduziert gemäß Better auf TS sogar in einem Schritt.

So und zweitens gilt, die Berechnung dieses Fixpunkts, die kann ich sogar durch einen

Term übernehmen lassen. Das heißt, es gibt im ungetöpten Lambda-Kalkül sogar einen Fixpunkt

Kombinator Y. Das ist also wieder ein Term. Das ist wieder unterstrichen, das heißt,

ich definiere es jetzt. Naja, das heißt, das Y rechnet mir den Fixpunkt, der nach 1 existiert,

aus. Das heißt, wenn ich einen T habe, deswegen dessen Fixpunkt ich haben will,

dann wende ich einfach Y drauf an und bekomme einen Fixpunkt. Und dass das ein Fixpunkt ist,

heißt ja, dass Yt Better reduziert auf T von Yt. So, das hier für alle T.

So, ja, gut. Schön und gut. Also wenn wir das jetzt bewiesen haben, und es ist tatsächlich

nicht mal schwer zu beweisen, man muss eben nur diese Terme erfinden. Sehen wir also,

F.A. wie für alle. Gut. So, wenn wir das also bewiesen haben, ja, dann haben wir im

Wesentlichen den Sack zugemacht. Also man muss da noch ein bisschen rechnen. Okay, also es gibt ja