Vorlesung Lambda-Kalkül und Typen

Vorlesung im Sommersemester 2000 im Hauptstudium (PG) 2VL + 2Ü
Veranstalter: Prof. Dr. Reinhold Letz
Dozent:       Dr. Ralph Matthes
Termine: VL Di 11-13, Raum 0.41 Oettingenstraße 67
         Ü Mo 9:00 bis 10:30, Raum 0.41 Oettingenstraße 67

Beschreibung

Getypte Lambdakalküle sind besonders einfache, getypte funktionale Programmiersprachen. Das Studium dieser Basisformalismen hat Anwendungen im Bereich des Designs und der Untersuchung von Programmiersprachen und Programmierlogiken sowie in der mathematischen Logik. Die Vorlesung soll in diesen Themenbereich einführen und den Teilnehmer/die Teilnehmerin in die Lage versetzen, sich mit aktuellen Forschungsthemen auseinanderzusetzen. Dies ist in einem solch jugendlich gebliebenen Forschungsgebiet durchaus rasch möglich.

Induktion wird eine zentrale Rolle spielen. Einerseits als Mittel, um über diese Kalküle Aussagen zu beweisen. Andererseits als die treibende Kraft hinter Erweiterungen, die Rekursion über abstrakten Datentypen bereitstellen. Diese sogenannten induktiven Typen werden an vielen Beispielen klargemacht, die z.B. in der Sprache ML auch programmiert werden können. Der reine funktionale Kern ohne Typen steht auch in der Sprache Scheme zur Verfügung, die man als (effiziente) Implementierung des gewöhnlichen ungetypten Lambda-Kalküls auffassen kann. Eine extreme Gegenposition dazu sind konstruktive mathematische Beweise der Existenz von Objekten mit bestimmten Eigenschaften. Inwiefern? Weil sie einen Algorithmus verbergen, dessen Korrektheit sich aus dem Beweis ergibt. Dieser Algorithmus läßt sich aus einem am Computer geführten Beweis auch automatisch extrahieren. Weiß man, daß der Algorithmus automatisch extrahiert wurde, so kann man auch an dessen Korrektheit glauben. Weniger gutgläubige Menschen lassen sich wenigstens einen Teil der Information noch mitgeben: die Typinformation. Aus ihr allein läßt sich in vielen Kalkülen bereits ablesen, ob ein Programm immer terminiert - eine zentrale Fragestellung in der Forschung zu Lambda-Kalkülen, die äquivalent ist zur Frage nach dem Vorhandensein eines allgemeinen Induktionsprinzip für die Terme/Programme.

Kurz gesagt: Es geht um das Verständnis der Grundprinzipien funktionaler Programmierung und die Möglichkeit, sicher korrekte funktionale Programme zu entwerfen.

Material

Ein Skriptum mit dem gesamten Inhalt der Vorlesung wird parallel erstellt und auch verteilt. Reaktionen darauf sind hochwillkommen, da das Manuskript auf einer internationalen Sommerschule als Kursmaterial dienen wird.

Literatur

The Lambda Calculus: Its Syntax and Semantics, Revised edition, Henk Barendregt, North Holland, 1984.
Lambda Calculi With Types, Henk Barendregt, im Handbook of Logic in Computer Science Oxford University Press, 1992, Eds. Samson Abramsky, Dov Gabbay, Tom Maibaum.
Proofs and Types, Jean-Yves Girard, Yves Lafont, Paul Taylor, Cambridge University Press, Cambridge Tracts in Theoretical Computer Science, 1989.
Lambda-Calculus, Types and models, J. L. Krivine, Masson , 1993 (engl. Übersetzung des französischen Originals).
Foundations for Programming Languages, John C. Mitchell, MIT Press, 1996.

Ralph Matthes

Last modified: Fri Jul 21 12:39:16 CEST 2000
http://www.tcs.informatik.uni-muenchen.de/lehre/SS00/Lambda/