Ja, herzlich willkommen.

Ja, wir sind weiterhin dabei, uns den Lambda-Kalkül anzusehen, insbesondere mit Blick darauf,

dass der Lambda-Kalkül eben als Berechnungsmodell dient. Wir haben uns ein bisschen angesehen,

wie das mit ganz elementaren Datentypen funktioniert, wie Booleans oder Produkttypen,

also Structs. Und wir wollen uns heute im Prinzip das Schlüsselfeature ansehen. Was ist das

Schlüsselfeature, um eine vollständige Programmiersprache zu erhalten? Nun,

Rekursion muss man halt haben in irgendeiner Form. So, und in der Tat,

in der Tat, die haben wir uns zwar völlig uneingeschränkt, also nichts mit primitiv

Rekursiv oder sowas oder sonstigen syntaktischen Einschränkungen. Wir können also beliebigen Müll

an rekursiven Definitionen hinschreiben. Und zwar wie folgt. Ja, erstmal müssen wir uns klar machen,

was Rekursion überhaupt von so leicht abstrakterer Warte aus gesehen ist.

Dazu sehen wir uns mal eine rekursive Definition an, mal sowas richtig schweres,

die Fakultätsfunktion. So, also ich schreibe das mal hin in einer Sprache, die ich ja so in

Haskell oder Lisp auch verwenden könnte. Also die Zeile hier könnte ich modulo evidenter

syntaktischer Umsetzung in Haskell schreiben. Also ich will diese Fakultätsfunktion,

English factorial, deswegen Fact, rekursiv definieren. Gut, und ich sage die Fakultätsfunktion

ist die Funktion, die eine natürliche Zahl n abbildet auf. Naja, dann gibt es eine Fallunterscheidung,

je nachdem ob n jetzt null ist oder nicht, sprich ob wir im terminierenden Fall oder im

Rekursionsfall sind. Also n gleich null ist der terminierende Fall. Nullfakultät ist per

Konvention eins. Und hier im Erzzweig bekommen wir dann den rekursiven Fall. Naja, wir multiplizieren

eben mit n die Fakultät von eins weniger. So, ok, nicht so weit, so unaufregend. Die Frage ist,

was passiert hier eigentlich? Wir schreiben irgendwie so eine Gleichung hin und behaupten,

das sei jetzt also eine Definition dieser Fakultätfunktion. Was passiert hier? Nun,

wir sagen Fakultät hat eine bestimmte Eigenschaft. Also Fact kommt auf der linken Seite vor und Fact

kommt auf der rechten Seite vor. Gut, auf der linken Seite steht es halt einfach so alleine.

Und auf der rechten Seite steht irgendwas sehr Kompliziertes, wo Fact in der Mitte steht.

Und wenn wir das jetzt mal in Bausch und Bogen abstrahieren, können wir sagen, gut das was da

sehr Kompliziertes steht, das kriegt jetzt mal einen Namen. Sagen wir Groß F und das wenden wir

an auf Fact. So, jetzt können wir noch genau sagen was Fact ist. F ist dann so in etwa das hier,

ja also eine Funktion, die sich eine Funktion auf den natürlichen Zahlen nimmt und uns eine

neue Funktion auf den natürlichen Zahlen zurückgibt und die so definiert ist. F von so einer Funktion

klein f ist eben der selbe Kram mit Fact durch F ersetzt. Ich mache es einmal in genanlose

Ausführlichkeit. Lambda n, if n gleich 0, then 1, else n mal F von n minus 1. So, ja nicht,

das ist einfach nur jetzt, also wenn ich F so definiere, kann ich jetzt diese rekursive

Gleichung hier so umschreiben. Für ihr zukünftiges Leben Dinge von so einem Typ her,

die also Funktionen sind, die wiederum Funktionen verarbeiten, die heißen oft Funktionale,

also dieses Groß F ist ein Funktional, also ein Funktional ist eine Funktion, deren Argumente

wieder Funktionen sind. Ja, und was wir hier sehen, diese Gleichung hier, Fact ist gleich

F von Fact, das ist ein wiederkehrendes Phänomen in einerseits der Informatik, andererseits

auch der Mathematik, sogar schätze ich in der Physik, gut, ich kenne mich nicht so aus.

Das hier ist eine Fixpunktgleichung. Hier wird ja, in Ingmat wird ganz viel Analysis

gemacht, ist das so? Hier stehen die Computergrafiker drauf glaube ich, Informatiker müssen wissen,

was ein H-Maus ist, können Sie es mir irgendwann erklären. Also, Banachscher Fixpunktsatz,

da dran, was war der Banachscher Fixpunktsatz, wir orientieren uns mal, der ist für die Informatik

übrigens wichtig, also ich bin froh, dass Sie den kennen. Wir haben hier einen kompakten

Banachraum, hübsch, und wir haben eine Kontraktion auf dem Ding, also eine abstandsverkleinernde

Abbildung, also abstandsverkleinernd heißt es gibt eine Konstante etwas kleiner als

eins, sodass immer der Abstand des Bildes kleiner gleich der Konstanten mal dem Abstand

der Urbilder ist. So, und Banachs Fixpunkt sagt, wenn ich einen vollständigen metrischen

Raum, Banachraum war Quatsch, Banachraum ist etwas anderes, also wenn ich einen vollständigen