Lambda-Kalkül

Hauptstudium Mathematik und Informatik
WS 2008/09
Vorlesung: Mo 14-16 Uhr, Oettingenstr. 67, Oe .15, Mi 10-12 Uhr, Oe 0.41, Andreas Abel
Übung: Mi 10-12 Uhr, Oettingenstr. 67, Oe 0.41, im zweiwöchigen Wechsel mit Vorlesung
Schein: ja (50% Übungspunkte + mündl. Prüfung)
SWS: 3 Vorlesung + 1 Übung

Aktuelles

  • Mündliche Prüfung findet statt am Donnerstag, 26.02.2009, in meinem Büro, Raum D1.11.
    • 10.20 Uhr Matthias Benkard
    • 10.40 Uhr Julien Oster
    • 11.00 Uhr Christoph Senjak
    • 11.20 Uhr Remigios Woidanowski
    • 11.40 Uhr Michael Mayer
  • Zusammenfassung des für die mündliche Prüfung relevanten Stoffes.
  • Übung am 14. Januar 2009 ausnahmsweise im Z1.09.
  • Abgabe Blatt 3 am Montag, 1. Dezember 2008.
  • Erste Übung: Mittwoch, 22.10.2008, 10-12 Uhr, im Raum Takla-Makan (Z11 im CIP-Pool)
  • Erste Vorlesung: Montag, 13.10.2008

Zeitplan

Datum Stoff Material
13.10. VL Überblick über Themen des Lambda-Kalküls
Im Schnelldurchlauf: Lambda-Terme, Reduktion, Normalform, Divergenz, Konfluenz, Auswertungsstrategien, Gleichheit und Extensionalität, Böhm's Theorem, Modelle, Getypter Kalkül, Anwendungen von Typsystemen.
15.10. VL Terme als Bäume, Substitution
Formale Definition der λ-Terme als Bäume, deren Höhe und Größe. Freie und gebundene Variablen. Substitution.
20.10. VL α-Äquivalenz, lokal-namenlose Repr"asentation
Variablenumbenennung, α-Äquivalenz, Barendregt'sche Variablenkonvention. Lokal-namenlose Repr"asentation
22.10. Ü Implementation, Regel-Induktion Übungsblatt 1
Implementierung von benamster und namenloser abstrakter Syntax in SML.
27.10. VL Relationen und Hüllen, β-Reduktion
Definition der kompatiblen und transitiven Hülle durch Regeln. Beweis der Korrektheit der transitiven Hülle durch Regelinduktion. Schrittweises Bilden der kompatibel-symmetrisch-transitiv-reflexiven Hülle. Definition der β-Reduktion. Redex und Redukt.
29.10. VL Programmieren im λ-Kalkül
Repräsentation von Wahrheitswerten (Bits), Paaren, natürlichen Zahlen. Vorgängerfunktion und primitive Rekursion durch Übersetzung der entsprechenden LOOP-Programme. Fixpunktkombinatoren.
03.11. VL Lambda-Definierbarkeit und lokale Konfluenz
Induktive Charakterisierung der Klasse der totalen berechenbaren (μ-rekursiven) Funktionen. Repräsentation von Komposition, primitiver und μ-Rekursion im λ-Kalkül. Jede μ-rekursive Funktion ist λ-definierbar.
Begriffe: Diamanteigenschaft impliziert Konfluenz impliziert lokale Konfluenz. β-Reduktion ist lokal konfluent, hat jedoch Diamanteigenschaft nicht. Standardbeispiel für lokal konfluent, aber nicht konfluent.
05.11. Ü Programmieren im λ-Kalkül, lokale Konfluenz Übungsblatt 2
10.11. VL Konfluenz Abgabe Üb. 1
Bbeispiel für lokal konfluent, aber nicht konfluent: δ t t → ε (Klop's Doktorarbeit, 1980).
Parallele Reduktion: Einbettung der Ein-Schritt-Reduktion, Einbettung in Mehr-Schritt-Reduktion, Abschluss unter Substitution. Vollständige Entwicklung. Jede parallele Reduktion lässt sich zur vollst. Entwicklung "verlägern"; daraus folgt die Diamanteigenschaft der par. Red. und die Konfluenz von β.

12.11. VL Standardisierung
Normalform. Induktive Def. der β-Normalformen. (Schwache) Kopf-Reduktion und -Normalform, Standardreduktion.
17.11. VL Standardiserung, Schwache Normalisierung, Äußere Reduktion
Beweis der Standardisierung, Korrektheit und Vollständigkeit der (schwachen) Kopf-Reduktion. Durch Einschränkung der rechten Seite der Standardreduktionsrelation auf β-Normalformen erhält man eine induktive Charakterisierung von schwach β-normalisierenden Termen. Die äußere Reduktion (leftmost-outermost reduction) ist eine deterministische Reduktionsstrategie, die schwach normalisierende Terme in ihre Normalform überführt.
19.11. Ü Konfluenz, (Schwache) Kopf-Normalform, Standardisierung Übungsblatt 3
24.11. VL Konfluenz von βη
η kommuntiert mit β, nach dem Lemma von Hindley und Rosen ist βη-Reduktion damit konfluent. Ein Term hat genau dann eine βη-Normalform, wenn er eine β-Normalform hat. Die schwierige Richtung &arrow; wird durch η-Aufschiebung bewiesen: In einer βη-Reduktionsfolge kann man die η-Schritte nach hinten verschieben. Dies bestätigt formal die Klassifikation der η-Reduktion als bloße Optimierung.
26.11. VL Beweis der η-Aufschiebung
01.12. VL Beweis der η-Aufschiebung. Starke Normalisierung.
Wohlfundierte bzw. stark Normalisierende Relationen, maximale Reduktionslängen.
03.12. Ü η-Aufschiebung, starke Normalisierung Übungsblatt 4
08.12. VL Starke Normalisierung.
Newman's Lemma: Starke Normalisierung + lokale Konfluenz = Konfluenz.
10.12. VL Starke Normalisierung.
bschluss von sn unter Subtermbildung. Induktive Charakterisierung SN von stark βη-normalisierenden Termen. Beweis von snβη ≤ snβ ≤ SN ≤ snβη.
15.12. VL Böhm's Theorem
Böhms Theorem und Beweis.
17.12. Ü Übungsblatt 5
22.12. VL Böhm's Theorem
Beweis fertig.
12.01. VL Typinferenz
Typinferenz für einfach getypte Terme à la Church und à la Curry.
14.01. Ü Übungsblatt 6
19.01. VL Typerhaltung unter Reduktion. Schwache Normalisierung.
Inversion der Typherleitung. Satz von der Typerhaltung unter Reduktion (subject reduction theorem). Ein kombinatorischer Beweis der schwachen Normalisierung des einfach getypten λ-Kalküs. Hereditäre Substitutionen.
21.01. VL Starke Normalisierung des einfach getypten Kalküls LFM'04 Artikel
Syntaktischer Beweis der starken Normalisierung.
26.01. VL Modelle des einfach getypten Kalküls
Modelbegriff. Mengentheoretisches Modell. Einführung ins bereichstheoretische Modell.
28.01. Ü Beweisterme, Normalisierung mittels Modell Übungsblatt 7

Inhalt

Der Lambda-Kalkül ist eine minimale funktionale Programmiersprache. Er verfügt nur über Variablen, Funktionsbildung durch Variablenabstraktion, und Funktionsanwendung. Dennoch ist er Turing-mächtig; alle berechenbaren Funktionen sind in ihm darstellbar. Die Theorie des Lambda-Kalküls als mathematischer Struktur ist reichhaltig und bietet überraschende Resultate. In der Informatik bildet der Lambda-Kalkül die Grundlage der funktionalen Programmiersprachen und bietet den optimalen Rahmen zum Studium von Variablenbehandlung, Auswertungsstrategien, Typsystemen, Polymorphismus, Termination.

In der Vorlesung behandeln wir unter anderem die Syntax des Lambda-Kalküls, Programmieren im Lambda-Kalkül, Auswertungsstrategien, Boehm's Theorem und Modelle des Lambda-Kalküls. Dann erweitern wir den Lambda-Kalkül um Typen, Polymorphismus, und diskutieren seine Verwendung als Notationssystem für mathematische Beweise.

Literatur

  • The Lambda Calculus: Its Syntax and Semantics, Second revised edition, Henk Barendregt, North Holland, 1984
  • Types and Programming Languages, Benjamin C. Pierce, MIT Press, 2002 Lambda Calculi with Types, Henk Barendregt, im Handbook of Logic in Computer Science, Band 2, Oxford University Press, 1993

WWW-Ressourcen

Valid HTML 4.01!
Andreas Abel
Last modified: Mon Feb 23 13:57:11 CET 2009 		Valid CSS!