Reduktionssysteme I

(3 Std. Vorlesung, 1 Std. Übung)

Aktuelles zur


Vorlesung:Montag14-16 Uhrin WAalt -1319
Dienstag10-11 Uhrin WAalt -1319
Übung:Dienstag11-12 Uhrin WAalt -1319
Beginn: Montag, den 24.10.2016, 14.15 Uhr

In dieser Vorlesung soll eine Einführung in die Theorie und die Anwendung von Reduktionssystemen gegeben werden. Dabei ist die grundlegende Idee die Folgende: Sei S eine Menge syntaktischer Objekte, z.B. Terme erster Ordnung über einer gegebenen Signatur, Formeln der Prädikatenlogik erster Stufe, Polynom-Ausdrücke oder Programme in einer gegebenen Programmiersprache, und sei ~ eine Äquivalenzrelation auf S, die Semantik der Objekte in S. Das Wortproblem für (S,~) ist dann das Problem zu entscheiden, ob zwei syntaktische Objekte dieselbe Bedeutung haben, d.h., ob sie äquivalent sind modulo ~. Der Rewrite-Ansatz zur Lösung dieses Problems geht wie folgt vor: Es wird zunächst eine wohl-fundierte Ordnung > auf S festgelegt. Ist s1 > s2, so ist das Objekt s2 einfacher als das Objekt s1. Der Prozess der Reduktion oder der Simplifikation besteht nun darin, ein gegebenes Objekt s effektiv durch ein äquivalentes Objekt s1 zu ersetzen, das einfacher ist als s. Sind s und t zwei Objekte, so erhält man durch wiederholte Reduktion zwei Folgen s > s1 > s2 > ... > sm und t > t1 > t2 > ... > tn von jeweils äquivalenten Objekten. Unter gewissen Voraussetzungen enden diese Folgen mit identischen Objekten, d.h. sm = tn, genau dann, wenn s und t äquivalent sind. Die Untersuchung dieser Voraussetzungen wird einen wesentlichen Teil der Vorlesung einnehmen.

Weitere Themen, die behandelt werden sollen, sind:

Literatur

J. Avenhaus:
Reduktionssysteme
Springer, Berlin, 1995.
F. Baader, T. Nipkow:
Term Rewriting and All That
Cambridge University Press, 1998.
L. Bachmair:
Canonical Equational Proofs
Birkhäuser, Basel, 1991.
R. Book, F. Otto:
String-Rewriting Systems
Springer, New York, 1993.
R. Bündgen:
Termersetzungssysteme
Vieweg, 1998.
E. Ohlebusch:
Advanced Topics in Term Rewriting
Springer, 2002.

Angesprochener Hörerkreis:

Vorkenntnisse:

Grundvorlesungen der Theoretischen Informatik

Leistungsnachweis:

Mündliche Prüfung am Ende des Semesters. Aktive Teilnahme an den Übungen sowie erfolgreiche Bearbeitung der wöchentlichen Übungsaufgaben sind Voraussetzungen für die Zulassung zur Prüfung.