[Back]

B. Gramlich:
"Recent Developments in Conditional via Unconditional Rewriting";
Talk: 3rd Austria-Japan Summer Workshop on Term Rewriting, Obergurgl (invited); 2010-08-01 - 2010-08-07.

Conditional rewriting is well-known to be substantially more difficult
to analyze, implement and understand than unconditional rewriting. For
this reason, transformations from conditional to unconditional systems
and their properties have been studied for a long time. Different
(classes of) transformation approaches have been designed for that
purpose. The basic and most important properties of such
transformations are effectivity and preservation properties:
Soundness and completeness w.r.t. reduction as well as soundness and
completeness w.r.t. properties like termination,
confluence and backtracking-freeness. Without further restrictions on
rewriting in the transformed system, virtually all transformations exhibit
unsoundness phenomena as discovered by [Marchiori/ALP'96] for the case
of so-called unravelings which are very elegant, simple and
intuitive. This motivated various researchers to impose
additional constraints on the transformed system, e.g.,
membership/ordersortedness constraints, context-sensitivity
constraints or reduction strategy constraints, or combinations
thereof.

In this context we will report on recent advances in transformations
of conditional rewrite systems, especially concerning the following
aspects: (Un)Sound\-ness phenomena (counterexamples and sufficient
criteria for different classes of systems), especially for unravelings
without further restrictions of the rewrite relation; a unified
systematic terminology for transformations; backtracking-free
transformations; refined preservation properties of selected
approaches.