2024-03-28T23:48:39Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00019064
2023-01-16T04:08:02Z
312:313:314
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
Nishida, Naoki
55707
Sakai, Masahiko
55708
Sakabe, Toshiki
55709
Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for a deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled TRS is left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling. Finally, we show that soundness of Ohlebusch's unraveling is the weakest in soundness of the other unravelings and a transformation, proposed by Serbanuta and Rosu, for (normal) deterministic CTRSs, i.e., soundness of them respectively implies that of Ohlebusch's unraveling.
journal article
Logical Methods in Computer Science
2012-08
application/pdf
Logical Methods in Computer Science
3
8
4
4
http://dx.doi.org/10.2168/LMCS-8(3:4)2012
http://hdl.handle.net/2237/21170
https://nagoya.repo.nii.ac.jp/record/19064/files/1206_5694.pdf
eng
https://doi.org/10.2168/LMCS-8(3:4)2012