Theorie funktionaler Ersetzungssysteme: eine Übersicht

Ausgehend von einer Zusammenfassung wichtiger Eigenschaften von Stan- dardersetzungssystemen untersuchen wir Ersetzungssysteme auf ihre funktionale Semantik, daß heißt auf Existenz und Eindeutigkeit von Normalformen. Diese Eigenschaften werden auf Terinnation und auf die Konfluenz von kritischen Situationen zurückgeführt. Wir führen Standardersetzungssysteme mit Substi- tution ein und zeigen weiche Eigenschaften solche Systeme haben müssen, damit aus der Konfluenz kritischer Paare die lokale Konfluenz des Systems folgt. Wir stellen eine Vervollständigung von Standardsysternen mit Substitution vor, die aus nicht konfluenten Systemen konfluente macht. Wir präsentieren kategorielle Ersetzungssysteme als eine Erweiterung von Standardsystemen mit Substituti- on, indem wir binäre Relationen bzw. partielle Ordnungen zu Morphismen in Kategorien verfeinern. Wir zeigen auf, welche Eigenschaften kategorielle Erset- zunalssysteme haben müssen, damit aus der Konfluenz kritischer Paare die lokale Ko nfluenz des gesamten Systems folgt.