A Regular and Complete Notion of Delay for Streaming String Transducers

TL;DR

The paper addresses measuring, in a regular fashion, how differently two SST executions can produce outputs for the same input. It builds a delay notion based on origin semantics and proves its regularity by constructing a finite automaton that tests whether the delay is bounded by a given $k$. Key contributions include decidability of $k$-delay equivalence and a completeness result showing that SST equivalence holds iff they are equivalent up to some computable bounded delay, giving an alternative proof of SST equivalence decidability. The results extend to deterministic two-way transducers and MSO transducers, establishing a machine-independent, regular framework for equivalence lifting and analysis.

Abstract

The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST). We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay. Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.

Figures (1)

• Figure 1: Five ways of producing the output sequence $a^4b^4$, and the corresponding origin functions.