Termersetzungssysteme (TErSys)7.5 ECTS
(englische Bezeichnung: Term Rewriting)

Lehrveranstaltungen:

• • Termersetzungssysteme
    (Vorlesung mit Übung, 4 SWS, Sergey Goncharov, Mi, 10:15 - 11:45, 02.133-113; Do, 12:15 - 13:45, Raum n.V.)

Inhalt:

Grundlegende Begriffe und Kernergebnisse der Theorie der Termersetzungssysteme und ihr Zusammenhang mit anderen Gebieten der Theoretischen Informatik werden behandelt:

• Terminierung, Konfluenz, Normalformen, kanonische Termersetzungssysteme.

• Techniken für Konfluenzbeweise: Newman's Lemma, Hindley-Rosen Lemma, kritische Paare, Knuth-Bendix Vervollständigungsverfahren.

• Techniken für Terminierungsbeweise: polynomische Interpretation, wohlfundierte syntaktische Ordnungen (lexikographische Pfadordnung, Multimengen-Pfadordnung).

• Starke Normalisierung für typisiertes Lambda-Kalkül, Konfluenz von typisiertem Lambda-Kalkül mit Fixpunkten (PCF).

• Beziehung zwischen Termersetzungssystemen und Logik durch Curry-Howard Korrespondenz und Gentzens Cut-Eliminations-Beweis für intuitionistische Logik.

• Termersetzungssysteme als Turing-vollständige Programmierungssprache.

Lernziele und Kompetenzen:

• Die Studierenden kennen die Kernbegrieffe von Termersetzungssystemen (Konfluenz, Terminierung, Normalform, kanonische Termersetzungssysteme, kritisches Paar) und erklären diese.

• Die Studierenden kennen die Kernergebnisse von Termersetzungssystemen (Newman's Lemma, Hindley-Rosen Lemma, starke Normalisierung für typisiertes Lambda-Kalkül) und können diese auf konkrete Beispiele anwenden.

• Die Studierenden beherrschen die Methoden und Techniken zur Sicherstellung von Terminierung und Konfluenz (polynomische Interpretation, Knuth-Bendix Vervollständigungsverfahren, Terminierungsbeweise durch wohlfundierte syntaktische Ordnungen).

• Die Studierenden wenden die Werkzeuge von Termersetzungssystemen an um formale Definitionen durch Termersetzungssysteme zu entwickeln. Sie können dabei Zwischenergebnise analysieren und bearbeiten um notwendige Eigenschaften (Konfluenz, Terminierung, starke/schwache Normalisierung) sicherzustellen.

Literatur:

• Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press.

• Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term rewriting systems, Cambridge University Press, 2003.

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. Informatik (Bachelor of Science)
   (Po-Vers. 2009s | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
2. Informatik (Bachelor of Science)
   (Po-Vers. 2009w | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
3. Informatik (Master of Science)
   (Po-Vers. 2010 | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsmodul Theoretische Informatik)

Studien-/Prüfungsleistungen:

Prüfung Termersetzungssysteme (Prüfungsnummer: 148641)

(englischer Titel: Term rewriting exam)

Prüfungsleistung, mehrteilige Prüfung, Dauer (in Minuten): 30, benotet

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
In die Prüfungsnote gehen zu 50% die Leistungen aus der Bearbeitung von Übungsaufgaben ein.

Erstablegung: SS 2014, 1. Wdh.: WS 2014/2015

1. Prüfer:

Lutz Schröder