Vorlesung Termersetzungssysteme im Sommersemester 2001

Montags 9 bis 11 , Raum 15, und Freitag 12:45 bis 14:15, Raum Z1.09, beide Oettingenstraße 67
Übungen: Mittwochs 9 bis 11, Raum Z1.09, Oettingenstraße 67

Dozent: Dr. Ralph Matthes (Raum D1.11)

Inhalt

Der Titel ist Programm:
Zentrales Anliegen ist das Studium von Systemen, mit denen sich Termumformungen beschreiben lassen. Bekannte Beispiele für konkrete Termersetzungssysteme sind die symbolischen Rechenregeln in der Schulmathematik. Der Prozeß der Umformungen wird zunächst sehr abstrakt gefaßt (abstrakte Reduktionssysteme), dann auf Terme erster Stufe über einer Signatur konkretisiert. Beantwortet werden vor allem Fragen nach der Terminierung solcher Umformungen, nach der Eindeutigkeit des erzielten Ergebnisses (Konfluenz) und nach dem Zusammenhang mit der semantischen Sicht von Gleichheit, speziell nach deren Entscheidbarkeit. Wichtige Begriffe sind die Unifikation (d. h., das syntaktische Lösen von Gleichungssystemen, das z. B. zentral ist für das Verständnis von PROLOG) und die Vervollständigung (das Gewinnen von Termersetzungsregeln, die ein terminierendes und konfluentes Termersetzungssystem ergeben, wobei man als Eingabe lediglich eine Menge von ungerichteten Gleichungen zur Verfügung hat).

Der Inhalt der Vorlesung deckt sich im wesentlichen mit dem des unten angegebenen Buches von Baader und Nipkow. Bei Interesse werden auch Implementierungen von Termersetzungssystemen sowie der behandelten Algorithmen studiert.

Literatur

Franz Baader und Tobias Nipkow: Term Rewriting and All That
Jürgen Avenhaus: Reduktionssysteme, Springer 1995

Ablauf

Die Vorlesungen entsprachen in etwa den im Folgenden angegebenen Seiten aus Baader/Nipkow:

23.4.: 1-4, 14
25.4.: 7-11
26.4.: 12, 28f
30.4.: 29-32, 16f
7.5.: 17f, 21-25
11.5.: 21-25
14.5.: 22-24, 34-38
18.5.: 38-42
21.5.: 61, 71f
25.5.: 72-76
28.5.: 76f, 79f
1.6.: 94-99
8.6.: 99-103, 44f
11.6.: 104-107
15.6.: 107-110
18.6.: 111-114
22.6.: 114-116
25.6.: 116-120
29.6.: 120f, 124-129
2.7.: 36f, 41, 134-137
6.7.: 137-141
9.7.: 158-162
13.7.: 162-165
16.7.: 166-169
20.7.: 169-172
23.7.: 172-176
25.7.: 176-180
27.7.: 180f

Übungsblätter

Blatt 1 vom 30. April (als PS)
Blatt 2 vom 11. Mai (als PS)
Blatt 3 vom 17. Mai (als PS)
Blatt 4 vom 28. Mai (als PS)
Berichtigung: In Aufgabe 1 muß "irreflexiv" durch "reflexiv" ersetzt werden. (Es handelt sich folglich um eine Quasi-Ordnung und nicht etwa um eine strikte Ordnung.)
Blatt 5 vom 7. Juni (als PS)
Blatt 6 vom 15. Juni (als PS)
Blatt 7 vom 29. Juni (als PS)
Blatt 8 vom 6. Juli (als PS)
Blatt 9 vom 13. Juli (als PS)

Ralph Matthes

Last modified: Fri Jul 27 19:28:21 CEST 2001