On Reversible Transducers

TL;DR

This paper introduces reversible two-way transducers, enabling polynomial complexity in composition, and shows how any two-way transducer can be made reversible with a single exponential blow-up, improving previous bounds.

Contribution

It defines reversible transducers, proves their expressive power, and provides efficient algorithms for composition and uniformization of two-way transducers.

Findings

Composition of two-way transducers can be done with a single exponential blow-up.

Any two-way transducer can be made reversible with a single exponential increase in size.

Uniformization of non-deterministic two-way transducers can be achieved with a single exponential blow-up.

Abstract

Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition. However, the best known algorithms for composing two-way transducers cause a double exponential blow-up in the size of the inputs. In this paper, we introduce a class of transducers for which the composition has polynomial complexity. It is the class of reversible transducers, for which the computation steps can be reversed deterministically. While in the one-way setting this class is not very expressive, we prove that any two-way transducer can be made reversible through a single exponential blow-up. As a consequence, we prove that the composition of two-way transducers can be done with a single exponential blow-up in the number of states. A uniformization of a relation is a function with the same domain and which is included in the original relation. Our main result actually states that we can uniformize any non-deterministic two-way transducer by a reversible transducer with a single exponential blow-up, improving the known result by de Souza which has a quadruple exponential complexity. As a side result, our construction also gives a quadratic transformation from copyless streaming string transducers to two-way transducers, improving the exponential previous bound.