On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe · IEICE Technical Report; IEICE Tech. Rep. · 2004
Transformations from conditional term rewriting systems (CTRSs) over (original) signa- tures into term rewriting systems (TRSs) over the exteded signatures, are called unravelings. They are not always simulation-complete for any input CTRS. Here simulation-completeness means that every rewrite sequence of the unraveled CTRSs (the output TRSs), whose initial and final terms are over the original signatures, can be simulated by a rewrite sequence of the original CTRSs. We have proposed an unraveling which generates left-linear, right-linear and non-erasing TRSs from CTRSs satisfying some syntactic conditions, respectively. In this paper, we show two conditions that the unraveling is simulation-complete for CTRSs. One is that the unraveled CTRSs are right-linear and non-erasing, and the other is that they are left-linear. Under the latter condition, we assume that any redex introduced by extra variables is not reduced anywhere in the rewrite sequences of the unraveled CTRSs.