A Regular and Complete Notion of Delay for Streaming String Transducers

TL;DR

This paper introduces a new regular notion of delay for streaming string transducers (SST) that enables decidable equivalence checking up to fixed delay, improving understanding of SST similarity and equivalence.

Contribution

It defines a machine-independent delay notion for SSTs, proves its regularity, and shows that SST equivalence up to fixed delay is decidable, providing new insights into SST theory.

Findings

Delay is regular and checkable by finite automaton.

Equivalence up to fixed delay is decidable for SSTs.

The delay notion applies to other transducer models, like two-way transducers.

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.