Ja, herzlich willkommen zur letzten Sitzung des Semesters. Ich fange mal mit ein paar

Materialfremdenpunkten an. Erstens Werbung. Wir bieten nächstes Semester wieder, so wie jedes

Semester Wahlpflichtveranstaltungen an. Im Bachelor ist das Säulenmodell jetzt immer noch,

naja, Sie wissen wo die Theorieveranstaltung hingehört. Also im Moment, weißt du,

dass das Säulenmodell war im Bachelor. Also im Bachelor haben Sie das Säulenmodell und wir sind

in der Säule der Theorieorientierten Vertiefungsrichtungen, wo auch sonst. So,

wir machen zum einen seit längerem mal wieder Algebra des Programmierens. Das ist unser nicht

selbst erfundener Euphemismus für Kategorien Theorie in der Informatik. Es gibt ein Buch,

das genauso heißt und das ist auch kein völliger Zufall. Also wir, also genauso, naja gut, das heißt

auf Englisch so. Also das heißt Algebra of Programming. Da gibt es also eine etablierte

Schule in Oxford, die also Programmieren durch kategorielle Gleichungstransformation machen. Das

heißt also, wir geben eine Spezifikation an und machen dann von Gleichungsumformung und haben dann

ein rekursives Programm dastehen. Ja gut, dazu wie weit das praktisch verwendbar ist, mag man stehen,

wie man will, aber wir machen hier also die Grundlagen dieses Prinzipes. Das heißt,

wir machen Datentypen und Prozesstypen in kategorieller Sichtweise. Das wird von der

tatsächlichen Kategorien Theorie her nicht endlos schwer gewichtig, also sollte auch für

interessierte Bachelorstudierende machbar sein. So das mache ich dieses Jahr selbst. Dann gibt es,

dann gibt es Hormotopie Type Theory. Das ist ein Seminar, das machen einerseits Tadeusz Likak und

andererseits Ergon Scharow, den Sie ja kennen. Das hat eine Abkürzung unter der es auch im Umgewiss

steht. Das ist die gängige Abkürzung und es ist, gut es sind zwei Dinge wahr. Also erstens das Thema

ist genauso abgefahren und irre wie der Name suggeriert und zum anderen ist es tatsächlich

genauso ein Hot Topic wie die Abkürzung andeutet. Also das ist das kommende Ding in der theoretischen

Informatik. Typentheorie bezieht sich auf die Art Typen, die Sie aus Programmiersprachen kennen.

Mit mehr theoretischer Fundierung natürlich als Sie es typischerweise aus Programmiersprachen

kennen und Hormotopie bezieht sich tatsächlich auf Hormotopie wie in Poincareische Vermutung.

Also eins der Millenniums Probleme, das vor kurzem gelöst worden ist, die Sphäre ist eindeutig

durch ihren Hormotopie Typ bestimmt. Das können Sie jetzt auf Wikipedia nachschlagen, was das heißt.

Aber genau die Hormotopie verbirgt sich tatsächlich dahinter. Also das ist was für die Leute,

die es wirklich interessiert. So und wieder mehr auf dem Boden der Tatsachen haben wir

hier. Klassiker, mittlerweile vielleicht bekannt unter den Namen Semproc,

praktische Semantik von Programmiersprachen, auch von von der Deo Schlittach und Christoph Rauch

zusammen. Da wird tatsächlich der Theorenbeweiser, den Sie hier kennengelernt haben,

nämlich Coq, verwendet, um formal aufzuschreiben die Semantik von Programmiersprachen. Das fängt an

mit Spielsprachen, die also irgendwie nur so ein bisschen im imperativen Kern können, bis hin zu

komplizierteren Features und das Ganze verbunden mit einer Verifikationslogik, die also gleichzeitig

im Theorenbeweiser mit hochgezogen wird. Also auch eine hochinteressante Sache. Auch jetzt,

irgendwie wenn man das im dritten Semester erzählt, sicher eher was für die Leute,

die sich wirklich dafür interessieren. Aber vielleicht erzählen Sie es auch weiter oder

merken Sie sich für zukünftige Semester. Gut und ein letzter. Der Daniel Hausmann bietet jetzt zum

zweiten Mal an die Modallogik. Das ist also mehr oder weniger eine direkte Fortsetzung von

dieser Veranstaltung. Also da haben Sie jetzt die Voraussetzungen beisammen, um das zu hören,

wo jetzt die Logik, wie wir sie kennen, die Aussagenlogik zunächst mal erweitert wird,

um Operatoren, die sagen, dass eine Aussage auf bestimmte Weise gilt. Deswegen Modal. Das Urlmodell

dafür ist, dass eine Aussage notwendigerweise gilt. Also 2 plus 2 ist notwendigerweise 4,

aber es ist jetzt nicht notwendigerweise der Gleuntermin montags um 16 Uhr, wenn Sachen

ein bisschen anders gelaufen wären, hätte er Dienstag um 10 sein können. Das ist also der

Unterschied zwischen Notwendigkeit und ihrem Gegenteil, dass auf Deutsch keinen anderen

einständigen Namen hat und deswegen mit dem Fremdwort Kontingenz bezeichnet wird.

Das ist nun natürlich der Teil, also die Lesart von Modalogik, die sind Informatiker weniger

interessiert. Informatiker interessiert Modalogik in zweierlei Hinsicht. Erstens Modalogik ist