FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs

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: