一句话：将经典有限值转换器的分解与判定结果推广到 copyless 流式字符串转换器，证明其有限值性可判定。
本文研究 copyless 流式字符串转换器（SST）的有限值性及其决策问题。SST 通过可存储部分输出的变量严格扩展单向转换器表达能力，但其一般等价性问题困难。作者将经典有限值转换器的分解与判定结果推广到 SST：证明任意 k-valued SST 都可有效分解为 k 个单值确定 SST 的并。由此推出有限值情形下 SST 与双向转换器等价，并给出检查有限值 SST 等价性的初等上界，改进了此前依赖 Ehrenfeucht 猜想的证明复杂度。最后证明 SST 的有限值性是可判定的，复杂度为 PSpace；当变量数固定时可在 PTime 内判定。这些结果回答了 Alur 和 Deshmukh 2011 年提出的问题。
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finite-valued transducers very attractive. For classical transducers it is also known that finite valuedness is decidable and that any k-valued finite transducer can be decomposed as a union of k single-valued finite transducers. In this paper, we extend the above results to copyless streaming string transducers (SSTs), answering questions raised by Alur and Deshmukh in 2011. SSTs strictly extend the expressiveness of oneway transducers via additional variables that store partial outputs. We prove that any k-valued SST can be effectively decomposed as a union of k (single-valued) deterministic SSTs. As a corollary, we obtain equivalence of SSTs and two-way transducers in the finite-valued case (those two models are incomparable in general). Another corollary is an elementary upper bound for checking equivalence of finite-valued SSTs. The latter problem was already known to be decidable, but the proof complexity was unknown (it relied on Ehrenfeucht's conjecture). Finally, our main result is that finite valuedness of SSTs is decidable. The complexity is PSpace, and even PTime when the number of variables is fixed.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{FiliotJLMPW24,
title = {Finite-valued Streaming String Transducers},
author = {Emmanuel Filiot and Ismaël Jecker and Christof Löding and Anca Muscholl and Gabriele Puppis and Sarah Winter},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662095}
}