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

Diese Seiten befinden sich im Aufbau!

Aktuelles

  • Ü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
17.12. Ü Übungsblatt 5

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: Thu Jan 8 15:31:32 CET 2009 		Valid CSS!