Reduktionssysteme

Inhalte dieser Vorlesung sind:

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 Prozeß 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.
N. Dershowitz, J.P. Jouannaud:
Rewrite Systems
in: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B (Elsevier, Amsterdam, 1990), 243-320.
Originalarbeiten.

Voraussetzungen:

Diese Vorlesung richtet sich an Studenten mittlerer und höherer Semester, die über Grundkenntnisse in Algebra und Informatik verfügen.

Leistungsnachweis:

Durch regelmäßige Teilnahme an den Übungen und Bearbeitung der wöchentlichen Aufgaben sowie das Bestehen einer mündlichen oder schriftlichen Abschlußprüfung kann ein Leistungsnachweis (Schein) erworben werden.