Theoretische Informatik II: Sommersemester 2022

Termine

Blockunterricht täglich von (Raum und Zeit Angaben noch vorläufig)
Montag 11.7.2018 bis Freitag 15.7.2018 und
Montag 18.7.2018 bis Freitag 22.7.2018
Vorlesung: 8:15 bis 9:45, Raum R 1.006, am Donnerstag 14.7 und Freitag 15.7 in R 0.058
Praktikum: 10:00-11:30 und 12:30-14:00, Raum R 2.009

Anmeldung

Die Anzahl der Plätze für diese Veranstaltung ist beschränkt. Eine Anmeldung erfolgt über das ZPA.

Erfahrungsgemäß erscheinen nicht alle angemeldeten Studierenden zur Veranstaltung. Freie Plätze werden daher noch am Beginn der ersten Vorlesung (siehe oben) vergeben.

Prüfung

Die mündlichen Prüfungen finden am Montag 25.7.2022 und mit individueller Terminvereinbarung ab Freitag 22.7.2022 statt.

Vorlesung

Die Vorlesung beschäftigt sich mit der Theorie und den Anwendungen des Lambda Kalküls, insbesondere mit der funktionalen Programmierung und der Programmiersprache Scheme.

Direkt inspiriert vom Lambda Kalkül ist die Programmiersprache LISP, zusammen mit FORTRAN und COBOL eine der ältesten höheren Programmiersprachen. Es entwickelten sich im Laufe der Zeit verschiedene Dialekte dieser Sprache, die versuchten den jeweiligen neuen Entwicklungen bei den Programmiersprachen zu folgen. Dadurch wurden diese Sprachen zum einen leistungsfähiger, aber auch komplizierter.

Die Programmiersprache Scheme, war dann der Versuch alte Zöpfe abzuschneiden, sich auf das Wesentliche zu konzentrieren und auf dem aktuellen Stand der Forschungen eine klare, einfache und effiziente Implementierung der grundlegenden Ideen von LISP zu realisieren. Deswegen beschäftigen wir uns mit Scheme.

Nach einer Einführung in die Programmierung mit Scheme, und einem systematischen Vergleich von Scheme mit anderen Programmiersprachen lernen wir die theoretischen Grundlagen von Scheme kennen, den Lambda Kalkül. Wir studieren Fragen der Semantik und Korrektheit und den Zusammenhang zwischen mathematischer Logik und Programmierung (Curry-Howard Korrespondenz).

Praktikum

Im Praktikum setzen wir die Erkenntnisse aus der Theorie praktisch um indem wir einen Interpreter für die Sprache Scheme implementieren.

Um den Lerneffekt zu verstärken verwenden wir zur Implementierung die Sprache Scheme selbst. (Man verwendet ja auch einen C Compiler um einen C Compiler zu übersetzen ;-). Wir sehen Scheme also in zwei Funktionen: als Implementierungssprache für ein relativ komplexes Programm und als eine Spezifikation, die in einen ausführbaren Interpreter übersetzt werden will.

Neuere Spezifikationen von Scheme findet man im Revised6 Report on the Algorithmic Language Scheme und Revised7 (short) Report on the Algorithmic Language Scheme. Die erste der beiden Spezifikationen (R6RS) ist nicht kompatibel mit den älteren Spezifikationen und war kein grosser Erfolg. Danach teilte man die Entwicklung in zwei Zweige R7RS-small und R7RS-large. Alle diese Varianten findet man auf www.schemers.org. Eine Diskussion des Was und Warum zum Beispiel auf ycombinator.com (was ein Y-Combinator ist lernen wir noch im Kurs).

Für unseren Kurs greifen wir auf die etwas ältere aber auch kürzer Fassung (nur 50 Seiten) des Revised 5 Report on the Algorithmic Language Scheme zurück. (Sie erhalten einen Ausdruck dieser Spezifiaktion in der ersten Praktiukumsstunde.)

Die neueste Weiterentwicklung von Scheme ist die Programmiersprache Racket. Zu Racket gibt es z.B. im Heft der Communciations of the ACM, Januar 2012, Vol. 55, No. 1, einen ausführlichen Artikel: Creating Languages in Racket. (Dieser Artikel ist innerhalb des Netzes der HM abrufbar). Die Entwicklung geht also weiter.

Wir werden im Praktikum auch die Racket Implementierung von Scheme verwenden, die unter www.racket-lang.org/download zu finden ist.

Materialien

Die Spezifikation: Revised 5 Report on the Algorithmic Language Scheme.
Diese Spezifikation ist Grundlage unserer Implementierung im Praktikum. Sie erhalten eine gedruckte Version in der Vorlesung.

Eine Fülle von Material zu Scheme findet man im Internet unter www.schemers.org.

Zu Scheme gibt es auch eine praktische Reference Card.

Die Racket Implementierung von Scheme findet man hier: www.racket-lang.org/download.

Es existiert ein Skript von Prof. Dr. Schwichtenberg, LMU, dem ich allerdings nicht streng folgen werde.

Sehr zum Lesen empfohlen wird auch Scheme: A Interpreter for Extended Lambda Calculus ein Teil der Original 'Lambda Papers' by Guy Steele and Gerald Sussman in denen die Entwicklungsgeschichte von LISP und Scheme sichtbar wird.

Zum Lambda Kalül gibt es ein sehr schönes aber auch anspruchsvolles Skript von Klaus Aelig und Thomas Fischbacher und ein etwas kompakteres Skript von Tobias Nipkow in dem auch die Beweise ausgeführt sind.

Aufgaben und Lösungen für das Pratikum: