TY - JOUR
T1 - Streaming ranked-tree-to-string transducers
AU - Takahashi, Yuta
AU - Asada, Kazuyuki
AU - Nakano, Keisuke
N1 - Funding Information:
We thank anonymous referees of this journal version and the conference version for useful comments. This work was supported by JSPS KAKENHI Grant Numbers JP17K00007 , JP18H04093 , JP18H03204 , and JP18K11156 .
Publisher Copyright:
© 2020 Elsevier B.V.
PY - 2021/5/16
Y1 - 2021/5/16
N2 - Streaming tree transducers with single-use restriction (STTsurs) were introduced by Alur and D'Antoni as an analyzable, executable, and expressive model for transforming unranked ordered trees in a single pass. The equivalence problem of STTsurs is decidable because their class is as expressive as the class of MSO-definable tree transformations. In this paper, we present streaming ranked-tree-to-string transducers (SRTSTs), based on STTsurs: SRTSTs are released from the single-use restriction while their input and output are restricted to ranked trees and strings, respectively. We show that the expressiveness of SRTSTs coincides with that of deterministic top-down tree transducers with regular look-ahead (yDTRs), whose equivalence problem is known to be decidable. Our proof is done by constructing equivalent transducers in both directions.
AB - Streaming tree transducers with single-use restriction (STTsurs) were introduced by Alur and D'Antoni as an analyzable, executable, and expressive model for transforming unranked ordered trees in a single pass. The equivalence problem of STTsurs is decidable because their class is as expressive as the class of MSO-definable tree transformations. In this paper, we present streaming ranked-tree-to-string transducers (SRTSTs), based on STTsurs: SRTSTs are released from the single-use restriction while their input and output are restricted to ranked trees and strings, respectively. We show that the expressiveness of SRTSTs coincides with that of deterministic top-down tree transducers with regular look-ahead (yDTRs), whose equivalence problem is known to be decidable. Our proof is done by constructing equivalent transducers in both directions.
KW - Equivalence
KW - Expressiveness
KW - Ranked trees
KW - Streaming transducers
UR - http://www.scopus.com/inward/record.url?scp=85098760531&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85098760531&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2020.12.033
DO - 10.1016/j.tcs.2020.12.033
M3 - Article
AN - SCOPUS:85098760531
VL - 870
SP - 165
EP - 187
JO - Theoretical Computer Science
JF - Theoretical Computer Science
SN - 0304-3975
ER -