Authors: Naoki Nishida, Yuta Tsuruta and Yoshiaki Kanazawa
Paper Information
Title: | Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs |
Authors: | Naoki Nishida, Yuta Tsuruta and Yoshiaki Kanazawa |
Proceedings: | IWC Final papers |
Editors: | Jakob Grue Simonsen and Bertram Felgenhauer |
Keywords: | conditional rewriting, confluence, termination, unraveling |
Abstract: | ABSTRACT. Unravelings are transformations of a conditional term rewriting system (CTRS, for short) into an unconditional term rewriting system (a TRS, for short) that is an overapproximation of the CTRS w.r.t. reduction. Unravelings are useful to prove confluence and operational termination of some CTRSs - we unravel a CTRSs to a TRS and try to prove termination and confluence using techniques for TRSs. A simultaneous unraveling has been proposed for normal 1-CTRSs and then a sequential one has been proposed for deterministic 3-CTRSs. Both the simultaneous and sequential unravelings are applicable to normal 1-CTRSs which are deterministic 3-CTRSs. In this paper, we first show that for a normal 1-CTRS, the simultaneously unraveled TRS is orthogonal iff so is the sequentially unraveled one. Then, we show that for a normal 1-CTRS, if the simultaneously unraveled TRS is terminating, then so is the sequentially unraveled one. Finally, we show that for a normal 1-CTRS with termination of the unraveled TRS, the simultaneously unraveled TRS is locally confluent iff so is the sequentially unraveled one. |
Pages: | 5 |
Talk: | Jul 07 14:00 (Session 28F: Term Rewriting) |
Paper: |