Programm für das zweiundzwanzigste Treffen am 26. Januar 2017

quchen hielt einen Vortrag über STG und erklärte so, wie Haskell eigentlich ausgeführt wird. Wenn man Haskell programmiert, arbeitet man ja in einem platonischen Ideenhimmel, in dem auch unendliche und zirkuläre Datenstrukturen möglich und sinnvoll sind. Wie zum Tautomorphismus schafft es der Haskell-Compiler, aus einem abstrakten Haskell-Programm Maschinencode zu erzeugen, die der Computer tatsächlich ausführen kann?

Marc stellte die gefeierte Curry–Howard-Korrespondenz vor. Dernach sind Beweisen in der Mathematik und Programmieren in der Informatik zwei Seiten einer Medaille. Aus jedem Beweis kann man ein Programm extrahieren und jedes Programm beweist eine Behauptung.

Die Curry–Howard-Korrespondenz ist damit eine der drei Brücken des computational trinitarianism, einer Philosophie, die vielen Leuten sehr wichtig ist: Gleich sind nämlich nicht nur Beweisen und Programmieren, sondern auch noch Morphismen von Kategorien. Programme, Beweise und Morphismen in Kategorien sind alles verschiedene Seiten der selben (dreiseitigen) Medaille.

Im Rahmen des Vortrags gab es oder gab es nicht ein kurzes einstudiertes Schauspiel geben.

Außerdem haben wir nun verstanden, inwieweit die Benutzung von klassischer Logik Zeitreisen ähnelt. (Der Fachbegriff dazu ist “Continuations”.)