Schernhammer, F. (2010). Applications and generalizations of context-sensitive term rewriting [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-37983
term rewriting; conditional term rewriting; context-sensitivity; forbidden patterns
en
Abstract:
Termersetzung ist ein Formalismus der in vielen Gebieten der theoretischen Informatik verwendet wird, in denen symbolische Gleichungen bzw. symbolische Berechnungen eine Rolle spielen. Sie findet insbesondere in den Gebieten der gleichungsbasierten Programmierung, der formalen Verifikation von Software und im automatischen Beweisen ihre Anwendung. Die prinzipielle Idee hinter Termersetzung ist Terme zu vereinfachen, indem Teilterme durch einfachere aber semantisch gleiche Terme ersetzt werden. Da es a priori unklar ist welche Teilterme zuerst vereinfacht werden sollen, ist der Vorgang des Termersetzens hochgradig nichtdeterministisch. In der Praxis spielt die Reihenfolge in der Vereinfachungen vorgenommen werden allerdings oft eine große Rolle, beispielsweise wenn bestimmte Vereinfachungssequenzen wesentlich schneller zum gewünschten Resultat führen als andere, oder bestimmte problematische Vereinfachungssequenzen zu Nichtterminierung führen.<br />Deshalb versucht man den Nichtdeterminismus der Termersetzung durch Ersetzungsstrategien zu verringern oder zu eliminieren. Ein wichtiger konkreter Ansatz für die Definition solcher Strategien ist kontextsensitives Termersetzen. Im ersten Teil der Dissertation wird kontextsensitives Termersetzen verwendet um Reduktionen bezüglich bedingter Termersetzungssysteme zu simulieren. In bedingten Termersetzungssystemen werden für jede Ersetzungsregel Bedingungen definiert unter denen die Regel anwendbar ist. Durch die Verwendung von kontextsensitivem Termersetzen ist es tatsächlich möglich bedingtes Termersetzen akkurat durch unbedingtes kontextsensitives zu simulieren. Die Dissertation enthält eine Transformation, die bedingte Termersetzungssysteme in unbedingte kontextsensitive übersetzt, wobei nach der Übersetzung exakt die selben Resultate berechnet werden können wie davor. Diese Transformation wird in weiterer Folge dazu benutzt praktisch relevante Eigenschaften von bedingten Ersetzungssystemen, wie zum Beispiel operationale Terminierung oder CE-operationale Terminierung, zu verifizieren, indem man Terminierungseigenschaften des transformierten unbedingten Systems nachweist. Dieses Vorgehen ermöglicht es existierende Methoden für die Terminierungsanalyse von unbedingten Ersetzungssystemen wiederzuverwenden.<br />Im zweiten Teil der Dissertation wird ein neuer Ansatz zu eingeschränktem Termersetzen eingeführt, der kontextsensitives Termersetzen verallgemeinert. In diesem Ansatz werden sogenannte "Forbidden Patterns" verwendet um Teile eines Terms zu identifizieren, in denen keine Vereinfachungen durchgeführt werden dürfen. Es zeigt sich, dass viele wichtige Standardreduktionsstrategien für Termersetzung als Spezialfall von diesem neuen Ansatz hervorgehen. Trotz dieser Allgemeinheit beruht Termersetzung mit "Forbidden Patterns" auf vergleichsweise einfachen und gut handhabbaren Grundprinzipien. Dadurch ist der Ansatz einfach zu verwenden und die Analyse von Ersetzungssystemen mit "Forbidden Patterns" in der Praxis effizient möglich. Die Dissertation enthält Konfluenzkriterien, Terminierungskriterien und "Completenesskriterien" für Termersetzung mit "Forbidden Patterns". Außerdem wird gezeigt wie man für ein gegebenes Termersetzungssystem passende "Forbidden Patterns" automatisch generieren kann.<br />Im dritten Teil der Dissertation wird das Softwaretool VMTL vorgestellt, das Termersetzungssysteme automatisch auf Terminierung untersucht. Das Tool enthält Implementierungen aller Methoden zur Terminierungsanalyse, die in der Dissertation vorgestellt werden und unterstützt insbesondere bedingte Systemen und "Forbidden Patterns".<br />
de
Term rewriting is a formalism that enables us to efficiently deal with many problems related to symbolic equations. It is particularly used in fields like equational programming, formal verification of software and automated deduction. The simple idea behind term rewriting is to replace equals by equals in an object (in our case terms) until a form is reached, which represents the result of the computation. In an operational sense the formalism of term rewriting does not suggest how this replacement is carried out. Thus, in general rewrite derivations (as we call sequences of replacements) are highly nondeterministic. Especially in practical fields like equational programming and executable specifications it is important to have means to guide rewrite derivations and thus to reduce their nondeterminism in order to make them more efficient and/or produce the desired results.<br />One major approach to achieve this is context-sensitivity. The idea of context-sensitive rewriting is to exploit the term structure of the objects in order to identify positions at which replacements are allowed and others where no replacements may occur. In the first part of this thesis we investigate the benefit one gains from using traditional notions of context-sensitivity in the simulation of conditional rewrite systems by unconditional ones. Conditional rewriting is an extension of ordinary rewriting where rewrite rules are guarded by conditions. These conditional rules may only be used for computations if the conditions are satisfied. It turns out that the use of context-sensitivity significantly improves the accuracy one can achieve in this simulation. Indeed, we show that by using a concrete transformation from conditional rewrite system into unconditional context-sensitive ones, the computational power of the conditional and transformed system is entirely the same. Hence, the accuracy of a simulation of conditional rewriting by using this transformation is arguably optimal. Besides simulation, we use this transformation to derive criteria for the practically crucial properties of operational termination and CE-operational termination of conditional rewrite systems based on (local) termination properties of the transformed unconditional rewrite systems. The latter properties are easier to verify and an extensive amount of existing research deals with verifying these properties automatically. The second part of the thesis introduces a new approach to context-sensitivity in term rewriting. The basic idea is to define term patterns, which are called "forbidden patterns", that determine parts of a term that are forbidden for reduction whenever they match the term.<br />This new formalism is more general than many existing approaches to context-sensitivity. Nevertheless, the definition of rewriting with forbidden patterns is comparatively simple, thus making the approach feasible in practice despite its expressiveness. We develop a basic infrastructure of results concerning rewriting with forbidden patterns, providing in particular criteria for completeness, confluence and termination. Moreover, we provide a method to automatically infer sets of forbidden patterns for given rewrite systems that impose desirable restrictions on the induced rewrite relation.<br />Finally, in the third part of the thesis, we describe the termination laboratory VMTL,that has been developed to evaluate the methods for the automated termination analysis of conditional rewrite systems as well as rewrite systems with forbidden patterns introduced in this thesis.<br />