University of Ulm ,
Faculty of Computer Science ,
Theoretical Computer Science Department
 |
Vorlesung (WS 2005/06):
Termersetzungssysteme |
 |
Vorlesungszeiten und Ankündigung
- Vorlesung: Montags, 10-12 Uhr im Raum 122
- Übung: Freitags, 12-14 Uhr im Raum 2203
Vorlesungsankündigung auf der elektronischen Pinnwand
Inhalt
Termersetzungssysteme dienen unter anderem zum Rechnen und Schließen in logischen Strukturen, die durch definierende Gleichungen beschrieben werden können. Abstrakte Datentypen werden z.B. häufig durch Gleichungen spezifiziert. Diese Spezifikationen können dann (unter bestimmten Voraussetzungen) ausführbar gemacht werden, indem man sie in ein Termersetzungssystem mit speziellen Eigenschaften übersetzt.
Die operationale Semantik von Termersetzungssystemen ähnelt der von funktionalen Programmiersprachen: Falls die linke Seite einer Termersetzungsregel auf einen Teilterm eines gegebenen Termes passt, so darf sie durch die entsprechende rechte Seite ersetzt werden. Dies wird solange wiederholt, bis keine Regel mehr passt. Das Ergebnis einer Berechnung ist also ein irreduzibler Term, eine sogenannte Normalform.
Typische Fragen in diesem Zusammenhang sind:
Wie kann man Normalformen (effizient) berechnen?
Existiert eine solche Normalform immer?
Sind Normalformen eindeutig? etc.
Literatur
- Jürgen Avenhaus: Reduktionssysteme, Springer-Verlag 1995.
- Franz Baader und Tobias Nipkow: Term Rewriting and All That, Cambridge University Press 1998.
- Enno Ohlebusch: Advanced Topics in Term Rewriting, Springer-Verlag, 2002.
- Terese: Term Rewriting Systems, Cambridge University Press, 2003.
Online verfügbare Materialien zur Vorlesung
Script (enthält die ersten 4 Kapitel)
Übungen zur Vorlesung
Informationen zu den Übungen sind
hier zu finden.