[Back]

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.