Zur Seitenansicht
 

Titelaufnahme

Titel
Confluence of term rewriting : theory and automation / by Bertram Felgenhauer
VerfasserFelgenhauer, Bertram
Begutachter / BegutachterinnenMiddeldorp, Aart ; Toyoama, Yoshihito
Betreuer / BetreuerinnenMiddeldorp, Aart
Erschienen2015
UmfangXI, 155 S. : Ill., graph. Darst.
HochschulschriftInnsbruck, Univ., Diss., 2015
Datum der AbgabeFebruar 2015
SpracheEnglisch
DokumenttypDissertation
Schlagwörter (DE)Konfluenz / Automatisierung / Ersetzungssysteme / Termersetzung / schrumpfende Diagramme / Modularität von Konfluenz
Schlagwörter (EN)confluence / automation / rewriting / term rewriting / decreasing diagrams / modularity of confluence / confluence - automation - rewriting - term rewriting - decreasing diagrams - modularity of confluence
Schlagwörter (GND)Termersetzungssystem / Konfluenz <Informatik>
URNurn:nbn:at:at-ubi:1-1954 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Confluence of term rewriting [1.74 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Thema dieser Dissertation ist die Theorie der Konfluenz von

Termersetzungssystemen und deren Automatisierung.

Termersetzungssysteme sind ein Berechnungsmodell bei dem Terme

sukzessiv abgeändert werden, indem man Instanzen der linken Seite

von Gleichungen durch entsprechende Instanzen der rechten Seite

ersetzt. Konfluenz ist eine wichtige Eigenschaft von Ersetzungssystemen welche eng mit der Eindeutigkeit von Normalformen verbunden ist,und daher mit der Eindeutigkeit von Funktionsdefinitionen. Für den Fall dass Termination eines Systems nicht gegeben ist, drückt Konfluenz eine Art deterministisches Verhalten aus: wenn zwei Berechnungen vom gleichen Ausgangszustand begonnen werden, so ist es auch möglich, diese wieder zu einem gemeinsamen Zustand zusammenzuführen.

Wie die meisten interessanten Eigenschaften in der Informatik ist

auch Konfluenz eine unentscheidbare Eigenschaft. Festzustellen ob

ein Ersetzungssystem konfluent ist, ist deshalb oft eine Herausforderung.

Dennoch gibt es automatische Beweiser für Konfluenz, die versuchen, diese Aufgabe selbständig zu bewältigen. Das Ziel dieser Arbeit ist es, den Stand der Technik auf dem Gebiet des automatischen Beweisens von Konfluenz voranzubringen. Zu diesem Zweck erweitern wir die Theorie der Konfluenz in mehreren Bereichen um Konfluenzkriterien abzuleiten, die sowohl mächtig als auch programmierbar sind.

Zusammenfassung (Englisch)

The topic of this thesis is confluence of first-order term rewriting systems, both its theory and its automation.

Term rewrite systems are a model of computation in which terms are successively modified by replacing instances of left-hand sides of equations by the corresponding instance of the right-hand side.

Confluence is an important property of rewrite systems which is intimately connected to uniqueness of normal forms, and therefore well-definedness of functions. In the absence of termination, confluence expresses a kind of deterministic behavior: for any two computations starting at the same

initial state, it is always possible to continue both of them until they reach a common state again.

Like most interesting properties in computer science, confluence is an undecidable property of term rewrite systems.

Therefore, determining whether a system is confluent is often challenging. Nevertheless, there are automated confluence provers that attempt to solve this task automatically. The goal of this thesis is to advance the state of the art of the field of automated confluence proving. To this end, we extend the theory of confluence in several areas to obtain confluence criteria that are both powerful and implementable.

Statistik
Das PDF-Dokument wurde 55 mal heruntergeladen.