Fakultät für Informatik

TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

TUM

Vorlesung | Sommersemester 2003
Logik (Gleichungslogik)
Prof. Tobias Nipkow

 

 

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: Mo 8:30 - 10:00, MI 00.04.011 (HS 2); Fr 10:15 - 11:45, MI HS 3
Beginn: Die Vorlesung beginnt am Montag, den 7. April.
Zentralübung: Mo 16:00 - 17:30, MI 00.04.011, beginnt am Montag, den 14. April.  Übungsblätter.
Übungsleitung: Clemens Ballarin

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.

Teil I: Termersetzung

  • Abstrakte Reduktionssysteme
    • 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.
    • Fundierte Induktion
      Satz: Fundierte Induktion gilt gdw die Reduktion terminiert. Königs Lemma.
    • Terminationsbeweise
      Einbettung in (N,>). Satz: Endlich verzweigte Reduktionen terminieren gdw sie in (N,>) einbettbar sind.
    • 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.
    • Multimengenordnung
      Multimengen und die Multimengenordnung von Dershowitz und Manna. Satz: Die Multimengenordnung termiert gdw die zugrundeliegende Ordnung terminiert.
    • Konfluenz
      Satz: Halbkonfluenz = Konfluenz. Satz: Termination & Lokale Konfluenz => Konfluenz.
  • Gleichungslogik
    • Terme und Substitutionen
      Signaturen, Terme, Positionen in Termen, Subterme an Positionen, Ersetzung von Subtermen, Substitutionen, Komposition von Substitutionen.
    • Termersetzung und Gleichungslogik
      Identitäten, Termersetzung ($\to_E$), Gleichungslogik ($=_E$). Äquivalenz von Gleichungslogik und Termersetzung.
    • Semantik der Gleichungslogik
      Algebren. Gültigkeit und semantische Konsequenz (|=). Birhoffs Theorem über die Äquivalenz von |- und |=.
  • Gleichungsprobleme
    Wortproblem, Unifikation, Matching.
    • Wortproblem
      Unentscheidbar für kombinatorische Logik und Halbgruppen; entscheidbar für konvergente TRS.
    • Syntaktische Unifikation
      Grundbegriffe: Quasiordnung auf Substitutionen, allgemeinster Unifikator, Idempotenz.
    • Unifikation durch Transformation
    • Unifikation von Termgraphen
      Von einem exponentiellen zu einem quasilinearen Algorithmus.
  • Termination von Termersetzungssystemen
    Im Schnelldurchlauf, ohne Beweise:
    • Termination ist unentscheidbar
      Reduktion des uniformen Halteproblems von Turingmaschinen auf das Terminationsproblem von TRS.
    • 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.
    • Reduktionsordnungen
      Ein TRS terminiert gdw es in einer Reduktionsordnung enthalten ist.
    • Die Interpretationsmethode
      Interpretation mit monotone Funktionen liefert eine Reduktionsordnung. Anwendung: Polynomordnungen.
  • Konfluenz von Termersetzungssystemen
    Satz: Im allgemeinen unentscheidbar.
    • Kritische Paare
      Das Kritische Paar Lemma. Korollar: Konfluenz ist entscheidbar für endliche terminierende TRSs.
    • Vervollständigung von Termersetzungssystemen
      Knuth-Bendix Algorithmus. Beispiel: Gruppen. Entscheidbarkeit des Wortproblems für endliche Mengen von Grundidentitäten mit Hilfe von Vervollständigung.
    • Orthogonale TRSs
      Satz: Orthogonale TRSs sind konfluent. Beweis mit paralleler Reduktion. Anwendung: Funktionale Programme sind konfluent.
Ein Beispiel für Gleichungsbeweise: Kleine Axiome für Boolesche Algebra
Interaktive Experimente mit dem Waldmeister System.

Teil II: Lambda-Kalkül

  • Untypisierter lambda-Kalkül
    • Syntax
      Terme; Klammerungsregeln; Currying; Statische Bindung; Freie und gebundene Variablen; Substitution; alpha-Konversion.
    • 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).
    • 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.
    • Reduktionsstrategien
      Thm (ohne Beweis): Reduktion des jeweils linkesten beta-Redexes führt zu einer beta-Normalform, falls eine existiert.
    • 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.
    • Lambda-Kalkül als Programmiersprache
      Datentypen: Wahrheitswerte, Paare
  • Typisierte lambda-Kalküle
    Motivation: Typen vermeiden logische Widersprüche (Frege, Russel, Church) und Programmierfehler. Kategorisierung von Typsystemen: statisch/dynamisch und monomorph/polymorph.
    • 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.
    • 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").
    • Let-Polymorphismus
      Erweiterung des Typsystems um allquantifizierte Typschemata. Erweiterte Typisierungsregeln mit expliziten Quantorregelen. Syntax-gesteuertes Regelsystem.
    • 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 Weitere Literatur:
  • Jürgen Avenhaus. Reduktionssyteme, Springer, 1995
  • Hendrik Pieter Barendregt. The Lambda Calculus, its Syntax and Semantics, North-Holland, 2nd edition, 1984
  • Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989
  • Chris Hankin. Lambda Calculi. A Guide for Computer Scientists, Ofxord University Press, 1994
  • J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and Lambda Calculus, Cambridge University Press, 1986

© Software & Systems Engineering Research Group
Sitemap |  Kontakt/Impressum
Letzte Änderung: 2003-11-07 13:11:07