RTA 2011 Papers

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

Authors

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Booktitle

In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
Vol. 10 of LIPIcs, pp. 267-282, May 2011.

Abstract

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.

Link

[LIPIcs]

Slides

[slides]

Program Inversion for Tail Recursive Functions

Authors

Naoki Nishida and Germán Vidal

Booktitle

In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
Vol. 10 of LIPIcs, pp. 283-298, May 2011.

Abstract

Program inversion is a fundamental problem that has been addressed in many different programming settings and applications. In the context of term rewriting, several methods already exist for computing the inverse of an injective function. These methods, however, usually return non-terminating inverted functions when the considered function is tail recursive. In this paper, we propose a direct and intuitive approach to the inversion of tail recursive functions. Our new technique is able to produce good results even without the use of an additional post-processing of determinization or completion. Moreover, when combined with a traditional approach to program inversion, it constitutes a promising approach to define a general method for program inversion. Our experimental results confirm that the new technique compares well with previous approaches.

Link

[LIPIcs] [full version (pdf)] [implementation]

Slides

[slides]