10.4230/LIPICS.RTA.2011.267
Nishida, Naoki
Naoki
Nishida
Sakai, Masahiko
Masahiko
Sakai
Sakabe, Toshiki
Toshiki
Sakabe
Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
conditional term rewriting
program transformation
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
2011
2011-04-26
2011-04-26
2011-04-26
en
urn:nbn:de:0030-drops-31244
10.4230/LIPIcs.RTA.2011
978-3-939897-30-9
1868-8969
10.4230/LIPIcs.RTA.2011
LIPIcs, Volume 10, RTA 2011
22nd International Conference on Rewriting Techniques and Applications (RTA'11)
2013
10
23
267
282
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
10
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
16 pages
503810 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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 for every CTRS w.r.t. reduction, 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 deterministic CTRSs is sound w.r.t. reduction if the
corresponding unraveled TRSs are left-linear or both right-linear and
non-erasing. We also show that soundness of the variant implies that
of Ohlebusch's unraveling.
LIPIcs, Vol. 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), pages 267-282