Lambda-Kalkül

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

Aktuelles

  • Zusammenfassungen des für die mündliche Prüfung relevanten Stoffes.
  • Skript zum Polymorphismus.
  • Letzte Vorlesung am Donnerstag, 08.02.2007, 14-16 Uhr, Raum D1.02 (hinter der Küche).

Zeitplan

Datum Stoff Material
16.10. VL Überblick über Themen des Lambda-Kalküls
Im Schnelldurchlauf: Lambda-Terme, Lambda-Definierbarkeit, Reduktion, Normalform, Divergenz, Konfluenz, Auswertungsstrategien, Gleichheit und Extensionalität, Böhm's Theorem, Modelle, Getypter Kalkül, Anwendungen von Typsystemen.

Theorem (Böhm): Gegeben zwei verschiedene, geschlossene βη-Normalformen t und t' und zwei beliebige Terme r und r'. Dann gibt es Terme s1 ... sn, so dass ((t s1) ... sn) = r und ((t' s1) ... sn) = r'.

Konsequenz: Ungleiche Normalformen können also durch ein geeignetes Experiment s1...sn unterschieden werden. Es kann keine Gleichung zwischen verschiedenen, geschlossenen βη-Normalformen t, t' zur Theorie hinzugefügt werden, ohne sie inkonsistent zu machen.

20.10. VL α-Äquivalenz, Substitution, β-Äquivalenz
Formale Definition der λ-Terme als Bäume, deren Höhe und Größe. Freie und gebundene Variablen, Variablenumbenennung, α-Äquivalenz, Barendregt'sche Variablenkonvention. Substitution und β-Äquivalenz.
23.10. VL Strukturelle Induktion, kongruente Hülle, β-Reduktion
Strukturelle Induktion am Beispiel eines Lemmas über Substitution. Definition der kongruenten und transitiven Hülle durch Regeln. Beweis der Korrektheit der transitiven Hülle durch Regelinduktion. Schrittweises Bilden der kongruent-symmetrisch-transitiv-reflexiven Hülle. Definition der β-Reduktion. Redex und Redukt.
27.10. Ü Church-Ziffern, Regel-Induktion Übungsblatt 1
Es wurden Präsenzaufgaben selbständig erarbeitet, präsentiert, und diskutiert: Definition von Tupeln (Paaren) und Projektionen im Lambda-Kalkül, Addition auf Church-Ziffern, Fibonacci-Funktion im Lambda-Kalkül. Ausserdem eine Aufgabe zur Regelinduktion.
30.10. VL Lokale Konfluenz
Begriffe: Diamanteigenschaft impliziert Konfluenz impliziert lokale Konfluenz. β-Reduktion ist lokal konfluent, hat jedoch Diamanteigenschaft nicht. Standardbeispiel für lokal konfluent, aber nicht konfluent. Weiteres Beispiel: δ t t → ε (Klop's Doktorarbeit, 1980). Parallele Reduktion.
03.11. VL Konfluenz Abgabe Üb. 1
Eigenschaften der parallelen 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 β.

Normalform. Induktive Def. der $\beta$-Normalformen. Standard- und Turing'scher Fixpunktkombinator.

06.11. VL Lambda-Definierbarkeit
Induktive Charakterisierung der Klasse der totalen berechenbaren (μ-rekursiven) Funktionen. Repräsentation von Komposition, primitiver und μ-Rekursion im λ-Kalkül. Jede μ-rekursive Funktion ist λ-definierbar.
10.11. Ü Rekursion, Konfluenz Übungsblatt 2
13.11. VL Standardisierung
(Schwache) Kopf-Reduktion und -Normalform, Standardreduktion, Beweis der Standardisierung, Korrektheit und Vollständigkeit der (schwachen) Kopf-Reduktion.
17.11. VL Schwache Normalisierung, Äußere Reduktion, η-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. η-Reduktion ist eine Optimierung, die überflüssige λ-Abstraktionen entfernt. Sie ist konfluent und stark normalisierend.
20.11. VL Konfluenz von βη, Beginn η-Aufschiebung
η 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.
24.11. Ü (Schwache) Kopf-Normalform, Standardisierung, η-Normalisierung Übungsblatt 3
27.11. VL Beweis der η-Aufschiebung
01.12. VL Starke Normalisierung, Newman's Lemma
Wohlfundierte bzw. stark Normalisierende Relationen, maximale Reduktionslängen. Newman's Lemma: Starke Normalisierung + lokale Konfluenz = Konfluenz.
04.12. VL SN, Böhm's Theorem
Abschluss von sn unter Subtermbildung. Induktive Charakterisierung SN von stark βη-normalisierenden Termen. Beweis von snβη ≤ snβ ≤ SN ≤ snβη. Kontexte (Terme mit Löchern). Böhms Theorem und Vorüberlegungen zum Beweis.
08.12. Ü η-Aufschiebung, starke Normalisierung Übungsblatt 4
11.12. VL Beweis von Böhm's Theorem. Einfache Typen
15.12. VL Eigenschaften des einfach getypten Lambda-Kalküls
Der Typisierungskalkül hat folgende Eigenschaften: weakening, strengthening, substitution, subject reduction.
18.12. VL Normalisierung durch Auswertung (F. Barral)
22.12. Ü Einfach getypter Lambda-Kalkuel Übungsblatt 5
Weihnachtsferien
08.01. VL Beweisterme für intuitionistische Aussagenlogik (IPL)
Einführung in die intuitionistische/konstruktive Logik, Disjunktionseigenschaft, Brouwer-Heyting-Kolmogorov-Interpretation von Aussagen als Menge ihrer Beweise. Beweisterme für IPL (intuitionistic propositional logic) als λ-Terme. Kalkül des natürlichen Schließens.
12.01. VL Normale Beweise, bidirectional type checking
Durch die Einführung von 2 Modi im Beweiskalkül, Synthese von Ziel-Aussagen und Analyse von hypothetischen Aussagen (=Annahmen), erhält man einen Kalkül für normale Beweise, d.h. Beweise ohne Umwege (Redexe). Aus diesem bidirektionalen Kalkül gewinnt man durch Analogieschluss einen bidirektionalen Algorithmus zur Typprüfung (bidirectional type checking).
15.01. VL Modelle des einfach getypten λ
Kurzer Überblick über Modelle des einfach getypten Lambda-Kalküs; Mengentheoretisches Modell mit vollem Funktionsraum, Bereichsmodell, Termmodelle (modulo β oder β&eta), geschlossene Termmodelle, Turing-/Registermaschinen, partiell-rekursive Funktionen. Axiomatisierung von Modellen.
19.01. Ü Konstruktive Logik, Modelle Übungsblatt 6
22.01. VL Mengentheoretisches Modell, Einführung Bereichstheorie
26.01. VL Vollständige partielle Ordnungen (CPOs)
29.01. VL Polymorphismus
System F (Curry-Stil). Imprädikative Kodierungen von Datentypen.
02.02. Ü System F Übungsblatt 7
05.02. VL Typinferenz und let-Polymorphismus
Wir zeigen Korrektheit und Vollständigkeit von Typinferenz für den einfach getypten Lambda-Kalkül und beschreiben eine Algorithmus für ML-Typinferenz (let-Polymorphismus).
08.02. VL Unentscheidbarkeit von Typprünfung in System F
Joe Wells reduzierte 1994 das type-checking-Problem für System F auf das Semi-Unifikationsproblem. Dieses ist unentscheidbar (Kfoury, Tiurin, Urzyczyn 1993).

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 19 11:53:28 CET 2007 		Valid CSS!