Lambda-Kalkül

Prof. Tobias Nipkow

Bereich: III (Theorie), Vorlesung: 2 Std.

Zeit & Ort: Dienstag 10:15 - 11:45, 2770

Beginn: 5.5.98

Inhalt: Der Lambda-Kalkül ist eine minimale Sprache bestehend aus Variablen, Konstanten, Funktions-Abstraktion und Funktions-Applikation. Er ist der Kern aller funktionalen Programmiersprachen, eignet sich aber genauso zur Modellierung sequentieller Programmiersprachen, da man in ihm verschiedenste Typsysteme und Semantiken ausdrücken kann. Aus Sicht der Logik kann der Lambda-Kalkül auch als Sprache zur Formulierung konstruktiver Beweise gesehen werden. Die Vorlesung vermittelt die Grundlagen des Lambda-Kalküls und beschäftigt sich im einzelnen mit den folgenden Themen:

  1. Untypisierter lambda-Kalkül
    1. Syntax
      Terme; Klammerungsregeln; Currying; Statische Bindung; Freie und gebundene Variablen; Substitution; alpha-Konversion.
    2. Beta-Reduktion
      Definitionen: Reduktion in Teilterm und induktiv. Lemma: Beta-Reduktion ist Kompatibel mit Substitution. Lemma: Diamanteigenschaft impliziert Konfluenz. Versuche zum Konfluenzbeweis: Beta hat die Diamanteigenschaft nicht; braucht parallele Reduktion. Parallels beta hat die D.E. auch nicht: braucht geschachtelte Reduktion. Definition der parallelen bottom-up Reduktion >. Lemma: Hat > die D.E. so ist beta konfluent. Thm: > hat die Diamanteigenschaft. Alternativer Beweis mit Thm: s > t => t > s*. wobei s* die vollständige Reduktion aller Redexe in s ist.
    3. Eta-Reduktion
      Lemma: Eta ist lokal konfluent. Fact: Eta terminiert. Thm (ohne Beweis): Terminiert -> und ist lokal konfluent, dann ist -> konfluent. Korollar: Eta ist konfluent. Lemma: Beta* und eta* kommutieren. Lemma: Falls ->1 und ->2 konfluent sind und ->1* und ->2* kommutieren, dann ist ->1 + ->2 konfluent. Korollar: Beta+eta ist konfluent.
    4. Reduktionsstrategien
      Thm (ohne Beweis): Reduktion des jeweils linkesten beta-Redexes führt zu einer beta-Normalform, falls eine existiert.
    5. Markierte Terme
      Motivation: let-Terme. Formalisierung als unterstrichene lambda-Terme. Thm (ohne Beweis): Reduktion unterstrichener beta-Redexe terminiert und ist konfluent. Beziehung zu > im Konfluenzbeweis von beta.
    6. Lambda-Kalkül als Gleichungstheorie
      Äquivalenz von Konfluenz und Church-Rosser Eigenschaft. Entscheidbarkeit der Konvertibilität von Termen mit Normalform. Unentscheidbarkeit der Konvertibilität bei beta und beta+eta (ohne Beweis), Entscheidbarkeit bei eta (wg. Termination von eta). Äquivalenz von eta und Extensionalität.
    7. Lambda-Kalkül als Programmiersprache
      Datentypen: Wahrheitswerte, Paare, Church-Numerale. Rekursive Funktionen als Fixpunkte. Fixpunktkombinatoren von Church (Y) und Turing. Def: lambda-definierbare Funktionen. Thm (ohne Beweis): Eine Funktion ist durch eine Turing-Maschine berechenbar gdw sie lambda-definierbar ist.
  2. Kombinatorische Logik
    Syntax. Reduktionsregeln. Thm (ohne Beweis): Konfluenz. Thm (ohne Beweis): Fortgesetzte Kontraktion des jeweils linkesten Redexes findet Normalform.
    1. Übersetzung zwischen lambda-Kalkül und Kombinatorischer Logik
      Der Abstraktionsalgorithmus. Lemma: Abstrahierter Term verhält sich wie lambda-Abstraktion. Übersetzung von lambda nach CL und zurück. Lemma: Resultat beta-reduzierbar auf ursprünglichen lambda-Term. Korollar: S+K sind funktional vollständig.
    2. Implementierungsaspekte
      Problem bei der naiven Implementierung von beta-Reduktion durch Sharing: der Ausgangsgraph wird verändert und muss daher u.U. kopiert werden. Lösungen: a) Übersetzung in Kombinatoren, wo kopier-freie Reduktion möglich ist. b) Clevere Graphenstruktur ("optimal reduction").
      Problem mit alpha-Konversion lässt sich durch de Bruijn-Terme (namensfreie Darstellung) lösen.
  3. Typisierte Lambda-Kalküle
    Motivation: Typen vermeiden logische Widersprüche (Frege, Russel, Church) und Programmierfehler. Kategorisierung von Typsystemen: statisch/dynamisch und monomorph/polymorph.
    1. Der einfach typisierte Lambda-Kalkül
      Syntax der Typen. Implizit und explizit typisierte Terme. Typüberprüfungsregeln. Eigenschaften: 1. Teilterme typkorrekter Terme sind typkorrekt (ohne Beweis). 2. Beta-Reduktion erhält Typen ("Subject reduction") (ohne Beweis). 3. Beta-Reduktion auf typkorrekten Termen terminiert (mit Beweis, der sich an dem Manuskript von Matthes und Joachimski ( Short proofs of Normalisation for the lambda-calculus...) orientiert. Siehe auch Hankin und Hindley/Seldin). 4. Beta-Reduktion ist confluent (trivial). Beta-äquivalenz ist daher entscheidbar, Komplexität aber nicht-elementar; in der Praxis aber gutartig. Korollar: Im einfach typisierte Lambda-Kalkül sind nur totale Funktionen repräsentierbar. Thm (ohne Beweis): Jede berechenbare Funktion ist als geschlossener typkorrekter lambda-Term darstellbar, der als einzige Konstante den Fixpunktoperator enthät.
    2. Typinferenz für einfach typisierte Terme
      Die Regeln. Typkorrekte Terme haben keinen eindeutigen Typ mehr, aber immer einen allgemeinsten Typ. Dieser kann durch eine Prolog-artige Interpretation der Regeln berechnet werden ("rückwärts rechnen").
    3. Let-Polymorphismus
      Erweiterung des Typsystems um allquantifizierte Typschemata. Erweiterte Typisierungsregeln mit expliziten Quantorregelen. Syntax-gesteuertes Regelsystem nur angedeutet.
    4. Der Curry-Howard Isomorphismus
      Die Grundidee: Typen = Formeln, Lambda-Terme = Beweise.

Hoererkreis: Studenten/-innen der Informatik und Mathematik

Voraussetzungen: Vordiplom. Hilfreich aber nicht notwendig: Logik oder Termersetzungssysteme.

Empfehlenswert für: alle Studierenden, die sich für die Grundlagen von Programmiersprachen und Logik interessieren. Daher besonders als Ergänzung zu den Vorlesungen Semantik, Logik und Termersetzung zu empfehlen.

Skript

Literatur: (in der Fachbereichsbibliothek verfügbar)

Sprechstunde: S2233, nach Vereinbarung.

Tobias Nipkow, 30.4.98