F. Schernhammer:

"Applications and Generalizations of Context-Sensitive Term Rewriting";

Supervisor, Reviewer: B. Gramlich, S. Lucas; Institut fuer Computersprachen, 2011; oral examination: 2011-01-31.

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 non-deterministic.

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. 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

$C_{\mathcal{E}}$-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. 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 present a method to automatically infer sets of forbidden

patterns for given rewrite systems that impose desirable restrictions

on the induced rewrite relation.

Finally, in the third part of the thesis, we describe the termination

laboratory VMTL, which has been developed to evaluate the above as

well as various other methods for the automated termination analysis

of conditional rewrite systems as well as of rewrite systems with

forbidden patterns introduced in this thesis.

Created from the Publication Database of the Vienna University of Technology.