科研之友
微信
新浪微博
Facebook
分享链接
摘要
Unravelings are transformations from conditional term rewriting systems (CTRSs) into unconditional term rewriting systems (TRSs) over extended signatures. They are complete, but in general, not sound w.r.t. reduction. Here, soundness w.r.t. reduction for a CTRS means that for every term over the original signature of the CTRS, if the corresponding unraveled TRS reduces the term to a term over the original signature, then so does the original CTRS. In this paper, we show that an optimized variant of Ohlebusch%26apos;s unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear, or both right-linear and non-erasing. Then, we show that soundness of the variant implies soundness of Ohlebusch%26apos;s unraveling, and show that soundness of Marchiori%26apos;s unravelings for join and normal CTRSs also implies soundness of Ohlebusch%26apos;s unraveling. Finally, we show that soundness of a transformation proposed by Serbanuta and Rosu for deterministic CTRSs implies soundness of Ohlebusch%26apos;s unraveling.
- 出版日期2012
