Jürgen Avenhaus: Reduktionssysteme, Kartoniert / Broschiert

Inhaltsangabe

0 Einleitung.- 0.1 Motivation.- 0.2 Termersetzungssysteme und abstrakte Datentypen.- 1 Abstrakte Reduktionssysteme.- 1.1 Definitionen und erste Ergebnisse.- 1.2 Konfluenz und die Church-Rosser-Eigenschaft.- 1.3 Konstruktion von Noetherschen Partialordnungen.- 1.4 Konstruktion von konvergenten Reduktionssystemen.- 2 Wortersetzungssysteme.- 2.1 Motivation.- 2.2 Termination und Konfluenz.- 2.2.1 Termination.- 2.2.2 Konfluenz.- 2.3 Die Vervollständigung nach Knuth-Bendix.- 2.3.1 Ein einfacher Algorithmus.- 2.3.2 Ein verbesserter Algorithmus.- 2.3.3 Das Verhalten des Vervollständigungsverfahrens.- 2.4 Entscheidbarkeitsfragen.- 2.4.1 Entscheidbare Probleme.- 2.4.2 Unentscheidbare Probleme.- 3 Termersetzungssysteme.- 3.1 Motivation.- 3.2 Spezifikation von Datentypen.- 3.2.1 Syntax und Semantik von Spezifikationen.- 3.2.2 Konstruktion von Modellen und der Satz von Birkhoff.- 3.3 Termersetzungssysteme.- 3.3.1 Regelsysteme und ihre Reduktionsrelation.- 3.3.2 Entscheidbarkeitsfragen.- 3.4 Matching und Unifikation.- 3.4.1 Matching.- 3.4.2 Unifikation.- 3.5 Konfluenz und Termination.- 3.5.1 Konfluenz.- 3.5.2 Einfache Terminationskriterien.- 3.6 Die Vervollständigung nach Knuth-Bendix.- 3.6.1 Ein einfacher Algorithmus.- 3.6.2 Das Inferenzsystem P.- 3.6.3 Ein effizienter Algorithmus.- 3.6.4 Normierung und Existenz von Regelsystemen zu (E, ).- 3.7 Reduktionsordnungen.- 3.7.1 Simplifikationsordnungen.- 3.7.2 Semantische Reduktionsordnungen.- 3.7.3 Syntaktische Reduktionsordnungen.- 3.8 Modularität.- 4 Termersetzung modulo einer Kongruenz.- 4.1 Die Church-Rosser-Eigenschaft modulo A.- 4.1.1 Motivation und einige Reduktionsrelationen.- 4.1.2 Termination und Konfluenzeigenschaften modulo A.- 4.2 A-Vervollständigung für links-lineare Regeln.- 4.2.1 Lokale Konfluenzkriterien für ? r.- 4.2.2 Das Inferenzsystem L.- 4.3 A-Vervollständigung für beliebige Regeln.- 4.3.1 Lokale Konffuenzkritereien für ? r. a.- 4.3.2 Das Inferenzsystem A.- 4.4 A-verträgliche Reduktionsordnungen.- 4.4.1 Semantische Reduktionsordnungen.- 4.4.2 Die assoziative Pfadordnung.- 5 Ausblick.- Wegweiser zur Originalliteratur.

Klappentext

Reduktions- und Vervollständigungstechniken dienen zum Rechnen und Schließen in gleichungsdefinierten algebraischen Strukturen wie Abstrakten Datentypen. In dieser ersten systematischen Einführung in das Gebiet der Reduktionssysteme werden die Grundlagen entwickelt und auf unterschiedliche Ersetzungssysteme angewandt. Themenschwerpunkte sind: 1. denotationale, operationale und rewrite-basierte Semantik, 2. effiziente und nachweisbar korrekte Vervollständigungsalgorithmen, 3. Inferenzsysteme, die auf Beweistransformation und Beweisordnung basieren, und 4. prinzipielle Entscheidbarkeit grundlegender Eigenschaften. Das Buch eignet sich für eine Vorlesung im Informatik-Hauptstudium. Durch Beispiele und Übungsaufgaben wird die anschauliche, übersichtliche Darstellung abgerundet.