Termersetzungssysteme

Prof. Tobias Nipkow

Bereich: III, Vorlesung: 3 Std.

Zeit & Ort: Mi 12:15 - 13:00 N1080, Do 8:30 - 10:00 in 2770.

Beginn: 5.11.97

Inhalt: Das Rechnen mit Gleichungen ist eine der wichtigsten mathematischen Techniken. In der Informatik bauen zum Beispiel ganze Gebiete wie höhere Programmiersprachen und -umgebungen, Programmspezifikation und -verifikation, Theorembeweisen und Symbolische Algebra direkt auf Gleichungskalkülen auf. Termersetzungssysteme sind Mengen von gerichteten Gleichungen, die als Reduktionsregeln interpretiert werden. Ziel der Vorlesung ist es, sowohl die Grundlagen der Gleichungslogik als auch die wichtigsten Algorithmen zur Manipulation von Termen, Gleichungen und Ersetzungsregeln einzuführen.

  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. Satz: Starke Konfluenz => Konfluenz.
  2. Termersetzung
    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$);
  3. Gleichungsprobleme
    Wortproblem, Unifikation, Matching.
    1. Wortproblem
      Unentscheidbar für kombinatorische Logik; 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
    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 (ohne Beweis). Falls alle Funktionen einstellig, dann schon mit 3 oder mehr Regeln unentscheidbar (ohne Beweis); 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. Vereinfachungsordnungen
      Satz: Jede Vereinfachungsordnung ist eine Reduktionsordnung (Beweisskizze unter Verwendung von Kruskals Theorem).
      1. Lexikographische Pfadordnung
        Satz: Die LPO ist eine Vereinfachungsordnung (ohne Beweis). Satz: Ist die Ordnung auf der Signatur total, dann ist die LPO auf Grundtermen total (ohne Beweis).
  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
      Beispiel: Gruppen. Transformationsregeln zur Vervollständigung. Imperative Version.
      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.
  6. Kombinationsprobleme
    1. Kombination von Termersetzungssystemen
      Satz: Konfluenz ist modular (ohne Beweis). Lemma: Lokale Konfluenz ist modular. Korollar: Konfluenz ist modular für terminierende TRSs.
    2. Kombination von Algorithmen
      Satz: Ist das Wortproblem für E0 und E1 entscheidbar und sind die Signaturen von E0 und E1 disjunkt, dann ist auch das Wortproblem für E0 vereinigt mit E1 entscheidbar (ohne Beweis!)
  7. E-Unifikation (Skizze)
  8. Ausblick
Eine Vorlesung pro Woche wird auf Englisch gehalten.

Hörerkreis: Studierende der Informatik und Mathematik

Voraussetzungen: Vordiplom. Hilfreich aber nicht notwendig: Logik.

Empfehlenswert für: alle Studierenden, die sich für die logischen Grundlagen der Informatik und Mathematik interessieren. Daher besonders als Ergänzung zu den Vorlesungen Logik und Semantik zu empfehlen.

Skript: Inzwischen ist das folgende Buch erschienen, an dem sich die Vorlesung sehr stark orientiert: 

Franz Baader and Tobias Nipkow. Term Rewriting and All That.
Cambridge University Press.

Weitere Literatur:

Sprechstunde: S2233, nach Vereinbarung.

Tobias Nipkow, 19.11.97