Conditional via Unconditional Rewriting - Some Recent Developments


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.  

In this context we will report on recent advances in transformations of
conditional rewrite systems, especially concerning the following aspects:
(Un)Soundness phenomena (counterexamples and new sufficient criteria for
different classes of systems), especially for unravelings without
restrictions of the rewrite relation; a unified systematic terminology for
transformations; backtracking-free transformations; proving properties of
conditional systems via context-sensitive unravelings.