Algorithmen für Termgleichungen

Hartwig, Rolf

Teilnehmerkreis:

Studenten der Informatik und Mathematik im Hauptstudium

Übersicht:

Mit der Definition eines abstrakten Datentyps durch Termgleichungen wird eine Kongruenzrelation induziert. Wegen der Unentscheidbarkeit des sogenannten Wortproblems ist aber für beliebige Terme t und t' für den Computer im allgemeinen nicht entscheidbar, ob diese Gleichung im Sinne der induzierten Kongruenzrelation in einem gegebenen abstrakten Datentyp nun gilt oder nicht. Termersetzungssysteme sind eine Methode, derartige Fragen anzugehen und damit den Computer das "algebraische Rechnen" mit Gleichungen zu lehren.

Hauptanwendungsgebiete des Term Rewriting bzw. der Termersetzungssysteme sind die operationale Semantik von abstrakten Datentypen, und damit die Implementation entsprechender Spezifikationssprachen, sowie die funktionalen Programmiersprachen mit deren "Pattern Matching".

Im Mittelpunkt der Vorlesung stehen einerseits die Begriffe und Sätze, die die "Critical Pair / Completion Procedure" fundieren, die als Knuth-Bendix-Algorithmus bekannt geworden ist, andererseits Kriterien für die algorithmische Entscheidbarkeit der Termination von Termersetzungssystemen.

Stichworte zur Vorlesung sind:

• Abstrakte Datentypen, gleichungsdefinierbare Klassen von Algebren, algebraisch-logische Gleichungstheorie;
• Termalgebren, Operationen und Relationen über Termen;
• Reduktions- und Termersetzungssysteme;
• Konfluenz und lokale Konfluenz, noethersche Reduktionen, Vervollständigung von Termersetzungssystemen, Knuth-Bendix-Algorithmus;
• Termination von Termersetzungssystemen, Kriterien für Termination und Nichttermination;
• Termordnungen, homöomorphe Einbettungsrelation, Simplifikationsordnungen, rekursive Pfade-Ordnung

Literatur:

• Bachmann, P.: Mathematische Grundlagen der Informatik. Akademie-Verlag, Berlin, 1992 *
• Buchberger, B. (ed.) : Rewriting Techniques and Applications. Journal of Symbolic Computation, Vol.3 , (1 & 2)1987
• Ehrich, H.-D., M. Gogolla, U. W. Lipeck: Algebraische Spezifikation abstrakter Datentypen. B.G.Teubner, Stuttgart, 1989 *
• Huet, G., D.C. Oppen: Equations and rewrite rules: a survey. Formal Languages: Perspectives and Open Problems (R.Book, ed.), Academic Press, 1980
• Jouannaud, J.-P., P. Lescanne: La réécriture. Report CRIN 85-R-099, Nancy, 1985
• Klaeren, H.A.: Algebraische Spezifikation. Springer-Verlag, 1983 *
• Klop, J.W., Term rewriting systems: a tutorial. Report Centrum voor Wiskunde en Informatica, Amsterdam, 1987

  * Diese Bücher befinden sich in der Bibliothek Informatik/URZ (Hauptgebäude, Raum 03-30).

Erwartete Vorkenntnisse:

Mengentheoretisch-algebraische Grundkenntnisse

Scheinvergabe:

Bei regelmäßigem Vorlesungsbesuch

Sonstiges:

Zu den in der Vorlesung behandelten Themen wird den Teilnehmern ein gut ausgearbeitetes Skript zur Verfügung gestellt werden.