[Back]

B. Gramlich:
"On (Un)Soundness of Unraveling Deterministic Conditional Rewrite Systems";
Talk: Annual Meeting of the IFIP Working Group 1.6 on Term Rewriting (2011), Novi Sad, Serbia; 2011-06-02.

We study (un)soundness of transformations of conditional term
rewriting systems (CTRSs) into unconditional term rewriting
systems (TRSs). From a logical as well as operational point of view
soundness and completeness of such transformations are indispensable.
The focus here is on analyzing (un)soundness of so-called unravelings,
the most basic and natural class of such transformations.
We extend our previous analysis from normal 1-CTRSs to the more
general class of deterministic CTRSs (DCTRSs) where extra variables in
right-hand sides are allowed to a certain extent.
We sketch how our previous soundness results based on weak
left-linearity and on right-linearity can indeed be extended from
normal 1-CTRSs to DCTRSs. Counterexamples show that such an extension
to DCTRSs does not work for the previous criteria which were based on
confluence and on non-erasingness, not even for right-stable
systems. Yet, we prove a weaker soundness result for confluent
right-stable CTRSs, namely soundness w.r.t. reduction to normal form.
Finally we compare our approach and results with related ones,
especially with [Nishida et al./RTA'11].