Inhalt

Übung

Literatur

Bereich:	III, Wahlpflichtvorlesung: 4 Std. (+2Ü) Die diesjährige Logik-Vorlesung kann wegen der starken Überlappung nicht zusammen mit Termersetzung oder Lambda-Kalkül in die DHP eingebracht werden.
Zeit und Ort:	Montag, 10.15-11.45 Uhr (2770) Mittwoch, 10.15-11.45 Uhr (2770)
Beginn:	Mittwoch, 3. 5. 2000
Zentralübung:	Montag, 12:15 - 13:45 (1180)
Übungsleitung:	Gertrud Bauer und Gerwin Klein

Prüfung:
Die Semestralprüfung findet in Form einer schriftlichen Klausur anstelle der Übung von 12:15 Uhr bis 13:45 Uhr am Montag, den 31.7.2000 im Hörsaal 1180 statt. Als Hilfsmittel sind eigene Aufzeichnungen, die Unterlagen zur Übung, das Skript zur Vorlesung Lambda-Kalkül, und das Buch Term Rewriting and All That zugelassen.

Teilnahmeberechtigt sind alle Studierenden, die mindestens 40% der Punkte aus den Haus- und Programmieraufgaben erreicht haben.

Inhalt:
Diese Vorlesung konzentriert sich ausschliesslich auf Gleichungslogik statt der sonst üblichen erststufigen Logik.
Sie kombiniert die Themen Termersetzung und Lambda-Kalkül mit einer logischen Sicht. Frühere Vorlesungen zu den beiden Themen (Termersetzung und Lambda-Kalkül) vermitteln einen guten Eindruck vom geplanten Inhalt.

Teil I: Termersetzung

1. Abstrakte Reduktionssysteme
   1. Abstrakte Reduktionssysteme
      Grundlegende Definitionen: reflexive, transitive, symmetrische Hüllen; Termination, Konfluenz, Church-Rosser. Satz: Church-Rosser gdw Konfluenz. Satz: Äquivalenz ist für konvergente Reduktionen durch Vergleich von Normalformen entscheidbar.
   2. Fundierte Induktion
      Satz: Fundierte Induktion gilt gdw die Reduktion terminiert. Königs Lemma.
   3. Terminationsbeweise
      Einbettung in (N,>). Satz: Endlich verzweigte Reduktionen terminieren gdw sie in (N,>) einbettbar sind.
   4. Lexikographische Ordnungen
      Lexikographisches Produkt von Ordnungen. Satz: Lex. Produkt terminiert gdw die Komponenten terminieren. Lexikographische Ordnung auf Strings. Satz: Die lex. Ordnung terminiert gdw die zugrundeliegende Ordnung terminiert.
   5. Multimengenordnung
      Multimengen und die Multimengenordnung von Dershowitz und Manna. Satz: Die Multimengenordnung termiert gdw die zugrundeliegende Ordnung terminiert.
   6. Konfluenz
      Satz: Halbkonfluenz = Konfluenz. Satz: Termination & Lokale Konfluenz => Konfluenz.
2. Gleichungslogik
   1. Terme und Substitutionen
      Signaturen, Terme, Positionen in Termen, Subterme an Positionen, Ersetzung von Subtermen, Substitutionen, Komposition von Substitutionen.
   2. Termersetzung und Gleichungslogik
      Identitäten, Termersetzung ($\to_E$), Gleichungslogik ($=_E$). Äquivalenz von Gleichungslogik und Termersetzung.
   3. Semantik der Gleichungslogik
      Algebren. Gültigkeit und semantische Konsequenz (|=). Birhoffs Theorem über die Äquivalenz von |- und |=.
3. Gleichungsprobleme
   Wortproblem, Unifikation, Matching.
   1. Wortproblem
      Unentscheidbar für kombinatorische Logik und Halbgruppen; entscheidbar für konvergente TRS.
   2. Syntaktische Unifikation
      Grundbegriffe: Quasiordnung auf Substitutionen, allgemeinster Unifikator, Idempotenz.
   3. Unifikation durch Transformation
   4. Unifikation von Termgraphen
      Von einem exponentiellen zu einem quasilinearen Algorithmus.
4. Termination von Termersetzungssystemen
   Im Schnelldurchlauf, ohne Beweise:
   1. Termination ist unentscheidbar
      Reduktion des uniformen Halteproblems von Turingmaschinen auf das Terminationsproblem von TRS.
   2. Einige (un)entscheidbare Teilklassen
      Entscheidbar falls rechts keine Variablen. Unentscheidbar schon für eine Regel. Falls alle Funktionen einstellig, dann schon mit 3 oder mehr Regeln unentscheidbar; offen für 1 oder 2 Regeln.
   3. Reduktionsordnungen
      Ein TRS terminiert gdw es in einer Reduktionsordnung enthalten ist.
   4. Die Interpretationsmethode
      Interpretation mit monotone Funktionen liefert eine Reduktionsordnung. Anwendung: Polynomordnungen.
5. Konfluenz von Termersetzungssystemen
   Satz: Im allgemeinen unentscheidbar.
   1. Kritische Paare
      Das Kritische Paar Lemma. Korollar: Konfluenz ist entscheidbar für endliche terminierende TRSs.
   2. Vervollständigung von Termersetzungssystemen
      Knuth-Bendix Algorithmus. Beispiel: Gruppen. Entscheidbarkeit des Wortproblems für endliche Mengen von Grundidentitäten mit Hilfe von Vervollständigung.
   3. Orthogonale TRSs
      Satz: Orthogonale TRSs sind konfluent. Beweis mit paralleler Reduktion. Anwendung: Funktionale Programme sind konfluent.

Teil II: Lambda-Kalkül

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. 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 (ohne Beweis).
   3. Eta-Reduktion
      Lemma: Eta ist lokal konfluent. Fact: Eta terminiert. Korollar: Eta ist konfluent. Lemma: Beta* und eta* kommutieren (ohne Beweis). Lemma von Hindley und Rosen. 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. Lambda-Kalkül als Gleichungstheorie
      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.
   6. Lambda-Kalkül als Programmiersprache
      Datentypen: Wahrheitswerte, Paare
2. 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 (ohne Beweis). 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.
   4. Der Curry-Howard Isomorphismus
      Die Grundidee: Typen = Formeln, Lambda-Terme = Beweise. Beta-Reduktion = Beweis-Reduktion. Beweis der Entscheidbarkeit der konstruktiven Aussagenlogik (nur mit ->) durch Suche nach Beweisen in Normalform.

Hörerkreis: Studenten/-innen der Informatik und Mathematik

Voraussetzungen: Vordiplom

Empfehlenswert für: jegliche Fragestellungen und Anwendungen von Logik-basierten Formalismen (ein Pleonasmus!), von der Softwarespezifikation bis zur Künstlichen Intelligenz.

Übungsschein: Einen Schein erhält, wer mindestens 40% der Punkte aus den Hausaufgaben und Programmieraufgaben erreicht und erfolgreich an der Semestralprüfung teilnimmt.

Literatur:
Die Vorlesung orientiert sich stark an

1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press.
2. Skript zur Vorlesung Lambda-Kalkül.

1. Jürgen Avenhaus. Reduktionssyteme, Springer, 1995
2. Hendrik Pieter Barendregt. The Lambda Calculus, its Syntax and Semantics, North-Holland, 2nd edition, 1984
3. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989
4. Chris Hankin. Lambda Calculi. A Guide for Computer Scientists, Ofxord University Press, 1994
5. J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and Lambda Calculus, Cambridge University Press, 1986