Félix Baschenis

Olivier Gauwin

Anca Muscholl

Gabriele Puppis

Minimizing resources of sweeping and streaming string transducers *

Keywords: 1998 ACM Subject Classification F.4.3 Formal Languages; F.1.1 Models of Computation transducers, streaming, 2-way, sweeping transducers, minimization Digital Object Identifier 10.4230/LIPIcs... 1

We consider minimization problems for natural parameters of word transducers: the number of passes performed by two-way transducers and the number of registers used by streaming transducers. We show how to compute in ExpSpace the minimum number of passes needed to implement a transduction given as sweeping transducer, and we provide effective constructions of transducers of (worst-case optimal) doubly exponential size. We then consider streaming transducers where concatenations of registers are forbidden in the register updates. Based on a correspondence between the number of passes of sweeping transducers and the number of registers of equivalent concatenation-free streaming transducers, we derive a minimization procedure for the number of registers of concatenation-free streaming transducers.

Introduction

Regular word functions extend the robust family of regular languages, preserving many of its characterizations and algorithmic properties. A word function maps words over a finite input alphabet to words over a finite output alphabet. Regular word functions have been studied in the early seventies, in the form of (deterministic) two-way finite state automata with output [START_REF] Aho | A characterization of two-way deterministic classes of languages[END_REF]. Engelfriet and Hoogeboom [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF] later showed that monadic second-order definable graph transductions, restricted to words, are an equivalent model -this justifies the notation "regular" word functions, in the spirit of classical results in automata theory and logic by Büchi, Elgot, Rabin and others. Recently, Alur and Cerný [START_REF] Alur | Expressiveness of streaming string transducers[END_REF] proposed an enhanced version of one-way transducers called streaming transducers, and showed that they equivalent to the two previous models. A streaming transducer processes the input word from left to right, and stores (partial) output words in finitely many, write-only registers. A variant of streaming transducers extended by stacks has been introduced in [START_REF] Alur | Streaming tree transducers[END_REF] and shown to capture precisely the monadic-second order definable tree transductions.

Two-way and streaming transducers raise new and challenging questions about storage requirements. The classical storage measure for automata is state complexity. State space minimization of two-way transducers is however poorly understood, even in the simpler setting of automata (cf. related work). But there are more meaningful parameters for transducer minimization. One such parameter for streaming transducers is the number of registers, and for two-way transducers it is the number of times the transducer needs to reprocess the input word. These parameters measure the required storage capacity in a more realistic way than the number of control states. For example, a two-way transducer that needs to process a very large input with several passes has much larger memory requirements in practice than the memory needed for storing the states. Ideally, the input is processed one-way, hence in one pass only, as in the streaming setting. But not every transduction can be implemented by a one-way, finite state transducer without additional memory.

The register minimization problem has been considered by Alur and Raghothaman in [START_REF] Alur | Decision problems for additive regular functions[END_REF], for a special family of deterministic streaming transducers: the output alphabet is unary, and the updates are additions/subtractions of registers by constants. For two-way transducers, Filiot et al. showed how to decide whether a transducer is equivalent to some one-way transducer [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF]. The decision procedure of [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF] is non-elementary, and we provided in [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] an elementary decision procedure and construction of equivalent one-way transducers in the special case of sweeping transducers: head reversals are only allowed at the extremities of the input. Sweeping transducers are strictly less expressive than two-way transducers, as shown by the following example: on any input of the form u 1 #u 2 # • • • #u n , where the words u i contain no occurrence of #, the corresponding output is

u n • • • u 2 u 1 .
In this paper we extend our results from [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] by showing how to compute in ExpSpace the minimal number of passes needed by a non-deterministic, functional sweeping transducer. It turns out that sweeping transducers have the same expressive power as bounded-reversal two-way transducers. In addition, we show a tight connection between sweeping transducers and streaming transducers: the former are equivalent to concatenation-free streaming transducers, i.e., transducers where concatenation of registers is not allowed in the updates. As a consequence, being concatenation-free is a real restriction for streaming transducers.

The above transformations preserve the relationship between the number of passes and the number of registers. This allows us to reduce the minimization problem for registers of concatenation-free streaming transducers to the minimization of the number of passes of sweeping transducers.

Related work.

As already mentioned, succinctness questions about two-way automata are still challenging. A longstanding open problem is whether non-deterministic two-way automata are exponentially more succinct than deterministic two-way automata. It is only known that this is the case for deterministic sweeping automata [START_REF] Sipser | Lower bounds on the size of sweeping automata[END_REF].

Regular transductions behave also nicely in terms of expressiveness: first-order definable transductions are known to be equivalent to transductions defined by aperiodic streaming transducers [START_REF] Filiot | First-order definable string transformations[END_REF] and by aperiodic two-way transducers [START_REF] Carton | Aperiodic two-way transducers and FO-transductions[END_REF].

Besides [START_REF] Alur | Decision problems for additive regular functions[END_REF], the closest work to ours is [START_REF] Daviaud | A generalised twinning property for minimisation of cost register automata[END_REF], that shows how to compute the minimal number of registers of deterministic streaming transducers with register updates of the form x := y • v, where v is a word and x, y are registers. These transducers are as expressive as one-way transducers. However, the focus of [START_REF] Daviaud | A generalised twinning property for minimisation of cost register automata[END_REF] is different from ours, since the outputs can be formed over any infinitary group. Moreover, the works [START_REF] Alur | Decision problems for additive regular functions[END_REF][START_REF] Daviaud | A generalised twinning property for minimisation of cost register automata[END_REF] consider deterministic transducers, which require in general more registers than non-deterministic functional ones. The proof techniques are based on variants of a property that has been studied for one-way transducers (the twinning property), and are quite different from ours.

Overview. After introducing two-way and streaming transducers in Sections 2 and 3, and showing some basic properties, we recall in Section 4 the key characterization of one-way definability from [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF]. Section 5 presents the main result on minimization of sweeping transducers. Finally, Section 6 concludes with a logical characterization for sweeping transducers.

Two-way transducers

A two-way transducer is a tuple T = (Q, Σ, ∆, I, E, F ), where Q is a finite set of states, Σ (resp. ∆) is a finite input (resp. output) alphabet, I (resp. F ) is a subset of Q representing the initial (resp. final) states, and E ⊆ Q×Σ×∆ ×Q×{left, right} is a finite set of transition rules describing, for each state and input symbol, the possible output string, target state, and direction of movement. To enable distinguished transitions at the extremities of the input word, we use two special symbols £ and ¡ and assume that the input of a two-way transducer is of the form u = a 1 . . . a n , with n ≥ 2, a 1 = £, a n = ¡, and a i = £, ¡ for all i = 2, . . . , n -1.

Given an input word u, we call positions the places between the symbols of u, where the head of a transducer can lie. We can identify the positions of u = a 1 . . . a n with the numbers 1, . . . , n -1, where each number x is seen as the position between a x and a x+1 . Since here we deal with two-way devices, a position can be visited several times along a run. Formally, we associate the states of the transducer with locations, namely, with pairs (x, y), where x is a position and y is a non-negative integer, called level. For convenience, we assume that, from a location at even level, the transducer can either move to the next position to the right, without changing the level, or perform a reversal, that is, increment the level by 1 and keep the same position; symmetrically, from a location at odd level, the transducer can either move leftward, without changing the level, or perform a reversal. Locations are ordered according to the following order: ≤ if = (x, y), = (x , y ) and one of the following holds: (1) y < y , or (2) y = y even and x ≤ x , or (3) y = y odd and x ≥ x .

Formally, we define a run on u = a 1 . . . a n as a sequence of locations, labeled by states and connected by edges, hereafter called transitions. The state at a location = (x, y) of a run ρ is denoted ρ( ). The transitions must connect pairs of locations ≤ that are either at adjacent positions and on the same level, or at the same position and on adjacent levels. Each transition is labeled with a pair a/v consisting of an input symbol a and a word v produced as output. There are four types of transitions: (x, 2y + 1) (x + 1, 2y + 1) (x, 2y) (x + 1, 2y)

(x + 1, 2y + 1) (x + 1, 2y + 2) (x, 2y) (x, 2y + 1) a x+1 /v a x+1 /v a x+1 /v a x+1 /v
The upper left (resp. upper right) transition can occur in a run ρ of T on u provided that ρ(x + 1, 2y + 1), a x+1 , v, ρ(x, 2y + 1), left (resp. ρ(x, 2y), a x+1 , v, ρ(x + 1, 2y), right ) is a valid transition rule of T and a x+1 is the (x+1)-th symbol of u (assuming that first symbol is £). Similarly, the lower left (resp. lower right) transition are called reversals, and can occur in a run ρ if ρ(x + 1, 2y + 1), a x+1 , v, ρ(x + 1, 2y + 2), right (resp. ρ(x, 2y), a x+1 , v, ρ(x, 2y + 1), left ) is a valid transition rule of T and a x+1 is the (x + 1)-th symbol of u.

We say that a run on u = a 1 . . . a n is successful if it starts with an initial state, either at location (1, 0) or at location (n -1, 1), and ends in a final state, at some location of the form (1, y max ) or (n -1, y max ). The output produced by a run ρ is the concatenation of the words produced by its transitions, and it is denoted by out(ρ).

Crossing sequences. An important notion associated with runs of two-way automata is that of crossing sequence. Intuitively, this is a tuple of states that label those locations of a run that visit the same position. Formally, given a successful run ρ of a two-way transducer on input u = a 1 . . . a n , the crossing sequence of ρ at a position x ∈ {1, . . . , n -1} is the tuple ρ|x = ρ(x, y 0 ), . . . , ρ(x, y h ) , where y 0 < . . . < y h are all and only the levels of the locations of ρ at position x. The classical transformation of two-way finite state automata into equivalent one-way automata [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF] uses crossing sequences.

Properties of two-way transducers. We say that a two-way transducer is sweeping if every run performs the reversals only at the extremities of the input word, i.e. when reading the symbols £ or ¡; L-sweeping if it is sweeping and all successful runs start at the leftmost location (1, 0); R-sweeping if it is sweeping and all successful runs start at the rightmost location (n-1, 1); k-pass if every successful run visits every position of the input at most k times; k-reversal if every successful run performs at most k reversals; one-way if it is 1-pass, L-sweeping.

A transducer is functional if it produces at most one output on each input. It is called unambiguous if it admits at most one successful run on each input. These notions will have the same meaning for streaming transducers, defined later. Clearly, every unambiguous transducer is functional. The converse is not true in general, but we will see later that we can transform the functional transducers considered in this paper so as to enforce unambiguity.

It is easy to see that every unambiguous transducer with n states is 2n-pass. Indeed, if this were not the case, then there would exist a successful run visiting the same position twice with the same state and the same direction. By repeating the factor of the run between the two locations with the same state, one can generate other successful runs on the same input, thus contradicting unambiguity. It is convenient to assume that the number of passes performed by the successful runs of a transducer is uniformly bounded by a constant. In general, this is not possible unless the transducer is unambiguous. However, for functional transducers we can restrict ourselves to considering only normalized runs, namely, runs that never visit the same position twice with the same state and the same direction. This is without loss of generality, since for every successful run of a functional transducer, there is one that is successful, normalized, and that produces the same output.

Hereafter, we silently assume that all transducers are functional and all successful runs are normalized. As a consequence the length of the crossing sequences of the successful runs of a transducer can be bounded by 2n, where n is the number of states of the transducer.

For streaming transducers, we can observe the following. Every k-pass R-sweeping transducer can be transformed into an equivalent (k + 1)-pass L-sweeping transducer: the additional pass is used at the beginning of the run to move the head from the leftmost position to the rightmost position, without outputting anything. It is also easy to disambiguate functional sweeping transducers, that is, transform them into equivalent unambiguous sweeping transducers, without increasing the number of passes. For this it suffices to fix a total order on the successful runs, e.g. the lexicographic order, and restrict to runs that are minimal among those over the same input.

The following proposition shows an interesting correspondence between the number of passes of sweeping transducers and the number of reversals of two-way transducers. As a matter of fact, this also implies that bounded-reversal transducers have the same expressiveness as sweeping transducers.

Proposition 1. Every k-pass sweeping transducer is also (k -1)-reversal. Conversely, every (k -1)-reversal two-way transducer can be transformed in 2ExpTime into an equivalent unambiguous k-pass sweeping transducer. The transformation can be performed in ExpTime if the (k -1)-reversal transducer is unambiguous.

Proof. The first claim is trivial, so we focus on the remaining ones. We begin by considering an unambiguous (k -1)-reversal two-way transducer T , and we show how to transform it into an equivalent unambiguous k-pass sweeping transducer S. Towards the end of the proof we will discuss how to modify the constructions in order to transform an arbitrary (k -1)-reversal two-way transducer.

Hereafter, we refer to a pass of T as a maximal factor of a run of T with no reversals. Note that a pass of T might not start or end at the extremities of the input word. The goal is to simulate each pass of T with a pass of a suitable sweeping transducer S. In particular, when T performs a reversal, S needs to continue moving towards the extremity of the input (this will be either the leftmost or the rightmost position, depending on the parity of the level), without performing any output. Once the extremity is reached, S is allowed to make a reversal and move back towards the position where T made the last reversal. So the transducer S moves from one extremity of the input to the other. The main difficulty is to correctly guess the reversals when moving away from these extremities. To do so, S will keep track, not only of the states associated with the current pass of T , but also of the crossing sequences of the entire successful run of T . If, at any point of the computation, a reversal position is wrongly guessed, this can be detected by the fact that it will be impossible to guess the crossing sequences across all the positions, since otherwise one could witness the existence of different successful runs on the same input. Note that the above idea works thanks to the fact that T is unambiguous: if this were not the case, then S may be able to guess different crossing sequences during different passes, and possibly produce a different output than T .

We will show later how to deal with the case where T is not unambiguous. Below, we provide more details about the construction that we just described.

For simplicity, we only consider the case where all successful runs of T start at the leftmost position and end at the rightmost position (the more general scenario can be handled by a case distinction and similar constructions). As T performs at most k -1 reversals, the crossing sequences of its successful runs will have length at most k.

To properly reason with crossing sequences, we need to introduce some additional terminology and notation. Let u = a 1 . . . a n be an input for T , where a 1 = £ and a n = ¡, and let ρ be a successful run of T on u. Recall that the crossing sequences ρ|x are defined only at the positions x ∈ {1, . . . , n -1}. However, it is convenient to associate some crossing sequences also with the dummy positions 0 and n; we do so by letting ρ|0 = ρ|n = ε. Consider a pair of adjacent positions x, x + 1, with 0 ≤ x, x + 1 < n. Besides the crossing sequences ρ|x and ρ|x + 1, we can also identify the set of transitions of T that connect the locations at the positions x and x + 1. We call these transitions the crossing transitions of ρ between x and x + 1. Note that the crossing transitions between x and x + 1 share the same input letter a x+1 . Moreover, if h 1 and h 2 are the lengths of the crossing sequences ρ|x and ρ|x + 1, respectively, then we see that there are exactly h1+h2 2 crossing transitions between x and x + 1, and these can be ordered on the basis of the levels of their locations. We denote by ρ|x, x + 1 the tuple of crossing transitions between x and x + 1, ordered from bottom to top.

Let Q be the state space of T and E the set of its transition rules. For short, we denote by Q ≤k the set of tuples of distinct states in Q having length at most k, and we do similarly for E ≤k . We introduce a relation R ⊆ Q ≤k × E ≤k × Q ≤k that represents the possible pairs of adjacent crossing sequences with the crossing transitions between them. We omit the tedious details of the definition of R and we refer the interested reader to [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF]. What is important, here, is to know that one can define R so as to satisfy the following properties:

if ρ is a successful run of T on u = a 1 . . . a n , where a 1 = £ and a n = ¡, then R contains the triples (ρ|x, ρ|x, x + 1, ρ|x + 1), for all 0 ≤ x < x + 1 < n, if u = a 1 . . . a n , with a 1 = £ and a n = ¡, and (q 0 , e 1 , q 1 ), . . . , (q n-1 , e n , q n ) is a sequence of triples in R such that, for each 1 ≤ x < n, the transitions in e x have a x as input symbol, then there is a successful run ρ of T on u such that ρ|x = q x for all 0 ≤ x ≤ n and ρ|x, x + 1 = e x for all 1 ≤ x ≤ n. In particular, since T is unambiguous, for each input u = a 1 . . . a n , there is at most one sequence (q 0 , e 1 , q 1 ), . . . , (q n-1 , e n , q n ) ∈ R that satisfies the conditions of the second item.

We are now ready to construct the sweeping transducer S. Let us first define the notion of crossing index. We say that a location = (x, y) of a run ρ of a two-way transducer has crossing index i if ρ contains exactly i locations at position x and strictly below level y. The state space of S is the set Q ≤k × {1, . . . , k} × {follow, escape, reach}. Intuitively, if a state (q, i, follow) marks a location = (x, y) of a successful run of S, then this means that there is a corresponding successful run ρ of T such that q is the crossing sequence ρ|x, is a location of ρ, and i is its crossing index of in ρ -in particular, this means that q[i] is the state associated with the location in the run ρ of T . The states of the form (q, i, escape) and (q, i, reach) are used for moving, respectively, away and towards the last reversal of T (so, intuitively, the locations marked with these states are "outside" the run of T ).

As for the transition rules of S, below we describe those that are used to simulate a rightward pass of T (those simulating a leftward pass are just symmetric):

For each triple (q, e, q ) ∈ R and each transition (q[i], a, v, q [j], right) ∈ e, we add to S the transition (q, i, follow), a, v, (q , j, follow), right .

For each triple (q, e, q ) ∈ R and each transition (q[i], a, v, q[j], left) ∈ e (i.e. a reversal), we add to S either the transition (q, i, follow), a, v, (q , j, escape), right or the transition (q, i, follow), ¡, v, (q , j, follow), left , depending on whether a = ¡ or a = ¡.

For each triple (q, e, q ) ∈ R and each even index j ∈ {1, . . . , k}, we add to S either the transition (q, j, escape), a, ε, (q , j, escape), right or the transition (q, j, escape), ¡, ε, (q, j, reach), left , depending on whether a = ¡ or a = ¡, where a is the input symbol of the transitions of e. For each triple (q, e, q ) ∈ R and each even index j ∈ {1, . . . , k}, we add to S the transition (q , j, reach), a, ε, (q, j, reach), left , where a is the input symbol of the transitions of e.

For each triple (q, e, q ) ∈ R and each transition (q[i], a, v, q[j], left) ∈ e, we add to S the transition (q , j, reach), a, ε, (q, j, follow), left . The initial states of S are the triples (q , 1, follow), for any q that appears in a triple of R of the form (ε, £, q ). Similarly, the final states of S the triples (q, i, follow), for any even index i and any q that appears in a triple of R of the form (q, ¡, ε).

It is clear that the transducer S is k-pass sweeping and can be constructed in exponential time from T . Moreover, it is routine to verify that S can simulate any successful run of T . To prove that S is unambiguous, and thus equivalent to T , we consider the passes of S on some input u. Since each pass spans across all the positions of u, the series of crossing sequences guessed along the passes of S are always the same, and they represent a successful run of T on u. From this, using the fact that T is unambiguous, we easily verify that there exists at most one successful run of S on u. This proves that S is unambiguous and hence equivalent to T .

We explain now how to modify the construction of S when T is functional but not necessarily unambiguous. Consider an input word u = a 1 . . . a n . The problem with T being not unambiguous is that S might guess different series of crossing sequences along different passes on the same input u, which can lead to producing an output different from that of T . The solution to this problem is to keep track of the set of possible crossing sequences ρ|x that can be associated with a position x when ρ ranges over all successful runs of T on u. We call these crossing sequences the admissible crossing sequences of u on x, and we denote by C x the set of all admissible crossing sequences of u on x.

Recall that R is the relation describing pairs of adjacent crossing sequences together with crossing transitions between them. Using R, we can derive the following relationship between the sets C x and C x+1 associated with adjacent positions:

C x+1 = {q : q ∈ C x , (q, e, q ) ∈ R, a x+1 is the input symbol of the transitions in e} C x = {q : q ∈ C x , (q, e, q ) ∈ R, a x+1 is the input symbol of the transitions in e}.
This relationship can be used by S in order to guess the sets C x while moving across the positions of the input. In fact, there is a "warm-up" phase at the beginning of the computation, where there is no guarantee that S guesses the correct sets C x . This phase lasts until the input u is entirely processed. During the warm-up phase, S may indeed guess over-approximations of the sets C x , which are compatible with the possible continuations of the input. This is not problematic, because the only point where having an exact information about the sets C x is crucial is when S guesses the position of the last reversal performed by T , which can only happen after the warm-up phase.

With the information derived from the guessed sets C x , the transducer S can keep track of all the successful runs of T on u. It can then exploit non-determinism to guess and simulate a distinguished successful run, say the least one in some lexicographic order. The simulation carried out by S may fail in two cases: if the simulated run dies (as before, this can happen due to some wrong guesses), or if some other run that precedes the simulated one in the lexicographic order survives until the end (this means that the simulated run was not the least one). If S succeeds in simulating the distinguished run of T , then it can also guess the reversals of T along this run. We omit the formal definition of S, which is rather technical. We only remark that, as we need to consider sets of crossing sequences, here we incur into a doubly exponential blowup when transforming T into S.

Streaming transducers

Streaming transducers can implement the same transductions as two-way transducers [START_REF] Alur | Expressiveness of streaming string transducers[END_REF][START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF], but they do so using a single left-to-right pass and a fixed set of registers that can store words over the output alphabet. Formally, a streaming transducer is a tuple T = (Q, Σ, ∆, R, U, I, E, F ), where Q is a finite set of states, Σ (resp. ∆) is a finite input (resp. output) alphabet, R is a finite set of registers disjoint from ∆, U is a finite set of updates for the registers, namely, functions from R to (R ∆) , I is a subset of Q representing the initial states, E ⊆ Q × Σ × U × Q is a finite set of transition rules, describing, for each state and input symbol, the possible updates and target states, and F : Q (R ∆) is a partial output function. A well-behaved class of streaming transducers [START_REF] Alur | Expressiveness of streaming string transducers[END_REF] is obtained by restricting the allowed types of updates and partial output functions to be copyless. A streaming transducer

T = (Q, Σ, ∆, R, U, I, E, F ) is copyless if (1) for every update f ∈ U , every register z ∈ R appears at most once in f (z 1 ) • . . . • f (z k )
, where R = {z 1 , . . . , z k }, and (2) for every state q ∈ Q, every register z ∈ R appears at most once in F (q). Hereafter we assume that all streaming transducers are copyless.

To define the semantics of a streaming transducer T = (Q, Σ, ∆, R, U, I, E, F ), we introduce valuations of registers in R. These are functions of the form g : R → ∆ . Valuations can be homomorphically extended to words over R ∪ ∆ and to updates, as follows. For every valuation g : R → ∆ and every word w ∈ (R ∪ ∆) , we let g(w) be the word over ∆ obtained from w by replacing every occurrence of a register z with its valuation g(z).

Similarly, for every valuation g : R → ∆ and every update f : R → (R ∪ ∆) , we denote by g • f the valuation that maps each register z to the word g(f (z)).

A configuration of T is a pair state-valuation (q, g). This configuration is said to be initial if q ∈ I and g(z) = ε for all registers z ∈ R. When reading a symbol a, the transducer can move from a configuration (q, g) to a configuration (q , g ) if there exists a transition rule (q, a, f, q ) ∈ E such that g = g • f . We denote this by (q, g) a ---→ T (q , g ). A run of T on u = a 1 . . . a n is a sequence of configurations and transitions of the form

σ = (q 0 , g 0 ) a1 ---→ T (q 1 , g 1 ) a2 ---→ T . . . an ---→ T (q n , g n ).
The run ρ is successful if the partial output function F is defined on the last state q n . In this case, the output of T on u is g n (F (q n )).

Properties and relationships with sweeping transducers. Functional and unambiguous streaming transducers are defined as in the two-way case. A streaming transducer is k-register if it uses at most k registers. As we did for two-way transducers, we assume that all streaming transducers are functional.

It is known that (functional) streaming transducers capture precisely the transductions definable by deterministic two-way transducers or, equally, by monadic second-order logic (so-called MSO transductions) [START_REF] Alur | Expressiveness of streaming string transducers[END_REF][START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF]. Moreover, differently from two-way transducers, nondeterministic streaming transducers can be determinized. This happens at the cost of increasing the number of registers.

We show below an interesting correspondence between the number of registers in a natural subclass of streaming transducers and the number of passes performed by sweeping transducers.

Definition 2. A streaming transducer

T = (Q, Σ, ∆, R, U, I, E, F ) is concatenation-free if f (z) ∈ ∆ • (R ∪ {ε}) • ∆ , for all registers z ∈ R and all updates f ∈ U .
Intuitively, a concatenation-free streaming transducer forbids register updates with two or more registers inside a right-hand side. We note that concatenation-free streaming transducers can also be determinized effectively. Moreover, it is easy to see that allowing boundedly many updates with concatenations does not change the expressiveness of the model, as one can remove any occurrence of an update with concatenations by introducing new registers.

The following proposition shows a tight correspondence between the number of registers of the concatenation-free streaming transducers and the number of passes of the sweeping transducers. Note that the proposition considers sweeping transducers that start from the rightmost position. A slightly weaker correspondence holds for L-sweeping transducers, since any sweeping transducer can be made L-sweeping (resp. R-sweeping) by increasing the number of passes by 1. Moreover, thanks to the previous Proposition 1, this correspondence can be immediately extended to the number of reversals performed by two-way transducers. Proof. We begin by considering an unambiguous concatenation-free streaming transducer T with k registers, and we show how to transform it into an equivalent unambiguous 2k-pass R-sweeping transducer S. After this, we will show how to deal with the case where the streaming transducer is not unambiguous.

Let u = a 1 . . . a n be an arbitrary input for T and σ = (q 0 , g 0 ) a1 ---→ T (q 1 , g 1 ) a2 ---→ T . . . an ---→ T (q n , g n ) the unique successful run on u. We can write the corresponding output as

T (u) = v 0 • g n (z 1 ) • v 1 • g n (z 2 ) • . . . • g n (z h ) • v h where h ≤ k and F (q n ) = v 0 • z 1 • v 1 • z 2 • . . . • z h • v h (note
that the latter word, and in particular the order of the registers z 1 , . . . , z h , depends on the final state q n ). Further let f 1 , . . . , f n be the sequence of register updates induced by the above transitions, and recall that g x = g x-1 • f x for all x = 1, . . . , n.

The idea for obtaining an equivalent unambiguous 2k-pass sweeping transducer S is to output each factor v i • g n (z i ) during two consecutive passes that start and end at the rightmost position. For this, we fix an index i ∈ {1, . . . , h} and we consider how the factor g n (z i ) is produced along the run σ. Since T is concatenation-free and unambiguous, there exist a unique position x i ∈ {0, . . . , n}, a unique sequence of registers z i = z i,n , z i,n-1 , . . ., z i,xi ∈ R, and a unique sequence of words w i,n , w i,n , . . ., w i,xi , w i,xi ∈ ∆ such that

           g n (z i,n ) = w i,n • g n-1 (z i,n-1 ) • w i,n . . . g xi+1 (z i,xi+1 ) = w i,xi+1 • g xi (z i,xi ) • w i,xi+1 f xi (z i,xi ) = w i,xi • w i,xi .
This basically means that the factor g n (z i ) is obtained from the empty word by repeatedly prepending and appending finite words w i,x and w i,x , where x goes from x i to n. Moreover, each pair of words w i,x and w i,x is determined by the x-th transition (q x-1 , g x-1 ) ax ---→ T (q x , g x ) of T .

The sweeping transducer S that we have to construct will behave as follows. At the beginning of a right-to-left pass at level 2i -1, S outputs the word v i that precedes the factor g n (z n ) in T (u). During the same pass, it reads the input in backward direction and, while guessing the transitions (q x-1 , g x-1 ) ax ---→ T (q x , g x ), it outputs the corresponding words w i,x . Once the position x i is reached, S continues to move leftward while simulating the transitions of T , but this time without producing any output. This is needed to check that the state of T reached at the leftmost position is initial. Then S performs a reversal. Similarly, during a left-to-right pass at level 2i, the transducer S guesses the transitions (q x-1 , g x-1 ) ax ---→ T (q x , g x ) and, if x ≥ x i , it outputs the corresponding words w i,x . Once the rightmost position is reached, it checks that the last guessed state is final and performs another reversal. The last pass performed by S is the left-to-right pass at level 2h, where the last piece v h of the output can be produced.

Clearly, S can be implemented with approximately 2k copies of the state space of T (one copy for each pass), and it performs at most 2k passes on any input. We remark that for this construction it is crucial that the streaming transducer T is unambiguous, as otherwise the described R-sweeping transducer S may guess different runs along two consecutive passes, eventually producing an output that differs from T (u).

We know consider the situation where the streaming transducer T is not unambiguous. This case can be handled by preprocessing T so as to make it unambiguous. After this, one can apply the previous construction to obtain an equivalent 2k-pass R-sweeping transducer. The transformation from a k-register streaming transducer T into an equivalent, unambiguous k-register streaming transducer T can be performed in exponential time by using standard techniques. More precisely, one performs a subset construction on the finite state automaton A underlying T . This allows one to simulate deterministically all successful runs of A on the input word. Then one exploits non-determinism to canonically guess a single run among the successful ones -as usual, this can be the least run in some lexicographic ordering. Finally, one simulates the register updates of T along the guessed successful run. The resulting transducer T has the same number of registers as T , but exponentially many more states. In particular, T can be produced in exponential time from T .

For the converse translations, we start with a unambiguous k-pass R-sweeping transducer S and we show how to produce, in exponential time, an equivalent unambiguous concatenation-free streaming transducer S with k 2 registers. Let A be the non-deterministic sweeping automaton underlying S, which recognizes the language dom(S). By applying the classical construction based on crossing sequences [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF], we transform A into an equivalent unambiguous one-way automaton B. To obtain a streaming transducer equivalent to S, we equip the automaton B with k 2 registers, say z 1 , . . . , z k 2 , and we extend the transitions with suitable register updates. The idea is that each register z i stores the output produced along the passes of S at levels 2i -1 and 2i. Consider an arbitrary input u = a 1 . . . a n for S, where a 1 = £ and a n = ¡, and recall that B admits a unique run on a 2 . . . a n-1 , say

σ = s 1 a2 ---→ B s 2 a3 ---→ B . . . an-1 ---→ B s n-1 .
Recall that the run σ determines a unique successful run ρ of S on u. In particular, each state s x determines a crossing sequence ρ|x. If ρ|x = (q 1 , . . . , q h ) and ρ|x + 1 = (q 1 , . . . , q h ) are the crossing sequences of ρ at two adjacent positions x and x + 1, for some h ≤ k, then the corresponding update f x+1 for the registers of B must satisfy:

f x+1 (z i ) = w x+1 • z i • w x+1
where w x+1 is the output produced by S with the right-to-left transition q 2i-1 ax+1 ← ---S q 2i-1 and w x+1 is the output produced by S with the left-to-right transition q 2i ax+1 ---→ S q 2i . Since f x+1 is uniquely determined by the control states s x and s x+1 and the input symbol a x+1 , the above equations can be easily turned into a definition of transition rules for a streaming transducer T having B as underlying automaton. We then specify the partial output function of T , which maps any state s of B to the juxtaposition z 1 • . . . • z h 2 of the first h 2 registers, where h is the length of the crossing sequence determined by s. The resulting transducer T is unambiguous, uses at most k 2 registers, and is equivalent to S. To conclude the proof, we briefly discuss the case where the sweeping transducer S is not unambiguous. As usual, this case can be deal with by a form of subset construction. The key observation is that all successful runs of S can be followed simultaneously because they perform the same reversals at the same positions, namely, at the extremities of the input word. In other words, one can determinize the underlying sweeping automaton in simple exponential time.

Based on the above proposition, the problem of minimizing the number of registers in a concatenation-free streaming transducer reduces to the problem of minimizing the number of passes performed by a sweeping transducer. We will thus focus on the latter problem: in Section 5, we consider the decidability and complexity of the following problem, called kpass sweeping definability problem: given a functional sweeping transducer S and a number k ∈ N, decide whether S has an equivalent k-pass sweeping transducer. One-way definability

In [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] we gave an effective characterization of sweeping transducers that are one-way definable, i.e., equivalent to some one-way transducer. This can be seen as a special case of the problem that we are considering here, and some of the technical tools developed in [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] will be used later. We briefly recall some definitions and results related to this characterization. Hereafter we assume that S is an L-sweeping transducer and ρ a successful run of S.

Intercepted factors.

An interval of positions of the run ρ has the form I = [x 1 , x 2 ], with x 1 < x 2 . We say that an interval I = [x 1 , x 2 ] contains (resp., strongly contains)

another interval I = [x 1 , x 2 ] if x 1 ≤ x 1 ≤ x 2 ≤ x 2 (resp., x 1 < x 1 ≤ x 2 < x 2 )
. We say that a factor of ρ is intercepted by an interval I = [x 1 , x 2 ] if it is maximal among the factors of ρ that visit only positions in I and that never make a reversal (recall that reversals in sweeping transducers can only occur at the extremities of the input word).

Pumping loops.

A loop of a run ρ is an interval L = [x 1 , x 2 ] of positions such that the crossing sequences ρ|x 1 and ρ|x 2 are equal. If L is a loop of ρ, we can obtain new runs by replicating any number of times the factors of ρ intercepted by L and, simultaneously, the factor of the input word u between positions x 1 and x 2 . This operation is called pumping and is formally defined as follows. Let L = [x 1 , x 2 ] be a loop of a run ρ on u. The run obtained by pumping n times the loop L is the sequence

pump n L (ρ) = α 1 β n 1 γ 1 1st pass α 2 β n 2 γ 2 2nd pass • • • α k β n k γ h k-th pass
where k is the number of passes performed by ρ, β i is the factor intercepted by L at the i-th level, α i is the factor intercepted either by [1, x 1 ] or by [x 2 +1, |u|] at the i-th level, depending on whether this level is even or odd, and, symmetrically, γ i is the factor intercepted either by [x 2 + 1, |u|] or by [1, x 1 ] at the i-th level, depending on whether this level is even or odd. We also define

pump n L (u) = u[1, x 1 ] • u[x 1 + 1, x 2 ] n • u[x 2 + 1
, |u|] and we observe that pump n L (ρ) is a valid run on pump n L (u). We remark that the above definition of pumped run are correct only for sweeping transducers: for arbitrary two-way transducers we would need to take into account the possible reversals within a loop L and combine the intercepted factors in a more complex way.

It is convenient to introduce some notation for pumping runs on multiple loops. If the loops are pairwise non-overlapping this can be done by simply pumping each loop separately, since the order in which we pump the loops does not really matter. The situation is a bit more complicated when some loops overlap. In particular, when pumping a loop L of ρ, several copies of the original locations of ρ are introduced, and with this several copies of other loops may appear (think, for example, of a loop L that is contained in L). We say that a location ˜ in pump n L (ρ) corresponds to in ρ if ˜ is one of the copies of that is introduced when pumping ρ on L. We extend this correspondence to sets of locations and loops. With a slight abuse of notation, we denote by pump n2 L2 (pump n1 L1 (ρ)) the run obtained by first pumping n 1 times the loop L 1 in ρ, and then pumping n 2 times every loop that corresponds to L 2 in pump n1 L1 (ρ) (note that the copies of L 2 in pump n1 L1 (ρ) are pairwise non-overlapping). It is routine to check that the two runs pump n2 L2 (pump n1 L1 (ρ)) and pump n1 L1 (pump n2 L2 (ρ)) are isomorphic. This allows us to use the shorthand pump n L (ρ) to denote runs obtained from ρ by pumping the loops L = L 1 , . . . , L m with the numbers n = n 1 , . . . , n m , respectively.

Inversions. The notion of inversion is crucial for characterizing one-way definability [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF]. Let L be a loop of ρ. A location 1 is called an entry point of L if it is the first location of a factor intercepted by L. Similarly, a location 2 is called an exit point of L if it is the last location of a factor intercepted by L. Note that every entry/exit point of L = [x 1 , x 2 ] occurs either at position x 1 or at position x 2 . Definition 4. An inversion of a run ρ is a pair of locations 1 and 2 for which there exist two loops L 1 = [x 1 , x 1 ] and L 2 = [x 2 , x 2 ] such that (also refer to the figure on the right):

1 is an entry point of L 1 and 2 is an exit point of L 2 , 1 < 2 and x 2 ≤ x 1 , for both i = 1 and i = 2, the factor intercepted by L i and visiting i has non-empty output, and no other loop strongly contained in L i has the same property as L i w.r.t. this factor.

L2 L1

1 2

We say that the loops L 1 and L 2 are the witnessing loops of the inversion ( 1 , 2 ).

Periodic words.

A word w is said to have period p if w ∈ u * v for some word u of length p and some prefix v of u. For example, w = abc abc ab has period p = 3. We are interested in factors of the outputs of S that are periodic, with uniformly bounded periods. To do this, we fix the constant e S = c S • |Q| 2|Q| , where c S is the maximum number of symbols output by a single transition of S and Q is the state space of S. A crucial result from [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] shows that, if S is equivalent to a one-way transducer, then all outputs out(ρ[ 1 , 2 ]) produced between the locations of an inversion of ρ are periodic, and the periods are uniformly bounded by the constant e S . This result is obtained by considering the output produced by pumped runs of the form pump n2 L2 (pump n1 L1 )(ρ)) and between copies of the locations 1 and 2 . By observing how these outputs are covered by the words produced by an equivalent one-way transducer T , and by exploiting Fine-Wilf's Theorem, one derives the periodicity of the outputs.

Proposition 5 (Prop. 7 in [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF]). If S is a one-way definable L-sweeping transducer and

( 1 , 2 ) is an inversion of a successful run ρ of S, then out(ρ[ 1 , 2 ]) has period at most e S .
The above result justifies the following definition: let L S ⊆ dom(S) be the language of those words u that induce a successful run ρ of S such that, for all inversions ( 1 , 2 ) of ρ, out(ρ[ 1 , 2 ]) is periodic with period at most e S . We denote by S| L S the transducer S restricted to inputs from L S . One-way definability is characterized as follows:

Theorem 6 (Th. 1 in [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF]). An L-sweeping transducer S is one-way definable if and only if L S = dom(S). Moreover, given an L-sweeping transducer S, one can construct in doubly exponential time a one-way transducer T that is equivalent to S| L S .

In the next section we show how to generalize the above results in order to characterize k-pass definability.

k-pass sweeping definability

We begin by defining the objects that need to be considered for characterizing k-pass definability, i.e., whether a sweeping transducer is equivalent to some k-pass sweeping transducer.

Let S be an L-sweeping transducer. The idea is to consider factors of runs of S that can be simulated alternatively from left to right and from right to left. We begin by introducing a notion of inversion that looks symmetric to that of Definition 4 (specifically, it is obtained by reversing the order of the witnessing loops):

Definition 7.
A co-inversion of a run ρ is a pair of locations 1 and 2 for which there exist two loops L 1 = [x 1 , x 1 ] and L 2 = [x 2 , x 2 ] such that: for both i = 1 and i = 2, the factor intercepted by L i and visiting i has non-empty output, and no other loop strongly contained in L i has the same property as L i w.r.t. this factor. We say that the above loops L 1 and L 2 are the witnessing loops of the co-inversion ( 1 , 2 ).

We then combine inversions and co-inversions, as follows:

Definition 8. A k-inversion of ρ is a sequence = ( 1 , 2 ), . . . , ( 2k-1 , 2k ) such that: 1 < 2 < . . . < 2k-1 < 2k are distinct locations in ρ, for all even i ∈ {0, . . . , k-1}, ( 2i+1 , 2i+2 ) is an inversion of ρ, for all odd i ∈ {0, . . . , k -1}, ( 2i+1 , 2i+2 ) is a co- inversion of ρ.
An example of a 3-inversion is depicted to the right. We say that is safe if out(ρ[ 2i+1 , ρ 2i+2 ]) has period at most e S , for some i ∈ {0, . . . , k -1}. We denote by L (k) S the language of words u ∈ such that all kinversions of all successful runs of S on u are safe.

Example 9. Consider the 3-pass transducer that on input u#v, with u, v ∈ {a, b} * , outputs (ab) |uvv| (ba) |uuv| . This transduction can also be realized in 2 passes. This means that every 2-inversion is safe. For example, the 2-inversion depicted to the right is safe, as the output ρ[ 3 , 4 ] is periodic. An analogous result for deciding k-pass R-sweeping definability can be derived by symmetry, by mirroring the input and reversing the computation. We also observe that, for k = 1, the above theorem improves the previous 2ExpSpace upper bound from [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] for deciding one-way definability of a sweeping transducer S. Concerning the doubly exponential size of an equivalent k-pass L-sweeping transducer, we observe that this is optimal, as in [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF] we have shown that there are sweeping transducers S such that any equivalent one-way transducer has size at least doubly exponential in S.

Before turning to the proof of Theorem 10, we list some simple consequences of this theorem and of Propositions 1 and 3.

Corollary 11.

One can compute in ExpSpace the minimum number of passes needed to implement a transduction given as a sweeping transducer. One can compute in 3ExpSpace the minimum number of reversals needed to implement a transduction given as a bounded-reversal two-way transducer. The complexity is 2ExpSpace if the given two-way transducer is unambiguous.

One can compute in 2ExpSpace the minimum number of registers needed to implement a transduction given as a concatenation-free streaming transducer. The complexity is

ExpSpace if the given streaming transducer is unambiguous.

The proof of Theorem 10 is split into two parts. The first part, called "soundness", deals with the construction of the k-pass L-sweeping transducer T of the second claim. Since L (k) S = dom(S) implies that T is equivalent to S, this construction also proves the right-to-left direction of the first claim. Moreover, as a side result, we prove that whether L (k) S = dom(S) holds is decidable in ExpSpace. The second part, called "completeness", deals with the left-to-right direction of the first claim.

Soundness. We show how to construct from S a k-pass L-sweeping transducer T equivalent to S| L (k)

S

. The idea is to consider a successful run ρ of S on a word u ∈ L (k) S , and divide it into k factors. We then simulate each factor of the run in a single pass, alternatively from left to right and from right to left, using [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF]. First we need the notion of k-factorizations: Definition 12. A k-factorization of a successful run ρ of S is any sequence of locations = 0 , 1 , . . . , k of ρ such that: 0 ≤ 1 ≤ . . . ≤ k , 0 is the first location of ρ, and k is the last location of ρ, for all even indexes i, with 0 ≤ i < k, and all inversions ( , ) of ρ, with i ≤ ≤ ≤ i+1 , the word out(ρ[ , ]) has period at most e S , for all odd indexes i, with 1 ≤ i < k, and all co-inversions ( , ) of ρ, with i ≤ ≤ ≤ i+1 , the word out(ρ[ , ]) has period at most e S .

Example 13. We consider the transducer of Example 9 and we depict a 2-factorization of a run of it (gray nodes). All the inversions between 0 and 1 , and all the co-inversions between 1 and 2 , must be periodic. Note that the run does contain non-periodic inversions (e.g. those crossing 1 ), and hence it does not admit a 1-factorization.

0 1 2 u # v
The following lemma shows that we can reason equally in terms of safe k-inversions (Definition 8) and in terms of k-factorizations. Lemma 14. For every word u ∈ dom(S), we have that u ∈ L (k)

S if and only if all successful runs of S on u admit k-factorizations.

Proof. We prove the left-to-right direction. Let u ∈ L (k) S and let ρ be a successful run of S on u. We define the locations 0 , 1 , . . . , k forming a k-factorization of ρ by an iterative process. The location 0 is clearly the first of the run. Let us now assume that we have defined the locations up to i , with i < k. We distinguish two cases depending on the parity of i. If i is odd, then we look at the inversions ( , ) of ρ such that ≥ i and out(ρ[ , ]) has period strictly larger than e S . For short, we call such inversions bad inversions after i . If there are no bad inversions after i , then we simply define i+1 to be the last location of the run. Otherwise, we take the first bad inversion after i , following the lexicographic order on pairs of locations, and we denote it by ( ˜ i , ˜ i ). Accordingly, we define the next location i+1 to be the one that immediately precedes ˜ i in the run ρ. The case where i is even is dealt with in a similar way, by considering co-inversions instead of inversions.

We verify that the constructed sequence 0 , 1 , . . . , k is indeed a k-factorization. By definition, for all even (resp. odd) indexes 0 ≤ i < k and all inversions (resp. co-inversions) ( , ), with i ≤ ≤ ≤ i+1 , the period of out(ρ[ , ]) is at most e S . Moreover, 0 was F. Baschenis, O. Gauwin, A. Muscholl, G. Puppis XX:15 chosen to be the first location of ρ, and we clearly have 0 ≤ 1 ≤ . . . ≤ k . It remains to prove that k is the last location of ρ. Suppose that this is not the case. Of course, this can happen only if for each location i , with i = 1, . . . , k, there exist bad inversions (or coinversions, depending on the parity of i) after i-1 . For each i = 1, . . . , k, let ( ˜ i , ˜ i ) be the first bad (co-)inversion after i-1 . The sequence ( ˜ 1 , ˜ 1 ), . . . , ( ˜ k , ˜ k ) is clearly a k-inversion. Moreover, it is unsafe, because the period of every word out(ρ[ ˜ i , ˜ i ]) exceeds e S . However, this is against the hypothesis that ρ was a successful run on u ∈ L (k) S . We thus conclude that = 0 , 1 , . . . , k is a k-factorization of ρ.

We now prove the converse direction. Fix a word u such that all successful runs on it admit k-factorizations. Consider a successful run ρ on u and a k-inversion = ( 1 , 2 ), . . . , ( 2k-1 , 2k ) of ρ. The goal is to prove that is safe. As ρ is a successful run on u, it admits a k-factorization, say = 0 , . . . , k . As the locations of the k-inversion are ordered, i.e.

1 ≤ 2 ≤ . . . ≤ 2k-1 ≤ 2k , there is an index i ∈ {0, . . . , k -1} such that i ≤ 2i+1 ≤ 2i+2 ≤ i+1
. By definition of k-factorization, this means that the period of out(ρ[ 2i+1 , 2i+2 ]) is at most e S , and hence the k-inversion is safe. As we chose ρ and in a general way, we conclude that u ∈ L (k) S .

Next we show that being a k-factorization is a regular property. To formalize this, we need to explain how to encode runs and sequences of locations as annotations of the underlying input. Formally, given a word u ∈ dom(S), a successful run ρ of S on u, and a tuple of locations = 1 , . . . , m in ρ, we denote by u, ρ, the word obtained by annotating each position 1 ≤ x < |u| of u with the crossing sequence ρ|x and with the m-tuple y = (y 1 (x), . . . , y m (x)), where each y i (x) is either the level of i or ⊥, depending on whether i is at position x or not. Based on this encoding, we can define the language F (k) S of all words of the form u, ρ, , where ρ is a successful run of S on u and = 0 , . . . , k is a k-factorization of ρ. Lemma 15 below proves that this language is regular. In fact, in order to better handle the complexity of our characterization, the lemma shows that both F Proof. To prove that F (k) S is recognized by an automaton of doubly exponential size, we rely again on results from [START_REF] Baschenis | One-way definability of sweeping transducers[END_REF]. Recall that L S is the language of words that induce successful runs such that, for all inversions ( , ), the period of out(ρ[ , ]) is at most e S . Theorem 6 shows that L S is the domain of a one-way transducer T that can be constructed from S in doubly exponential time, so L S is recognized by an automaton of doubly exponential size w.r.t. S. We can apply this theorem to the transducer S factors , and obtain in this way an automaton that recognizes the language L S factors . By definition, if ρ is a successful run on u and 1 , 2 are two locations in it, then u, ρ, 1 , 2 belongs to L S factors if and only if, for all inversions ( , ), with 1 ≤ ≤ ≤ 2 , the period of out(ρ[ , ]) is at most e S . A similar automaton can be constructed for the language R S factors that contains the words u, ρ, 1 , 2 such that the outputs produced by all co-inversions between 1 and 2 have period at most e S . Therefore, to recognize F (k) S , it is sufficient to construct an automaton that reads a word u, ρ, 0 , . . . , k and checks that (i) ρ is a successful run of S on u, (ii) 0 ≤ . . . ≤ k are locations that delimit factors of ρ, and (iii) for every i ∈ {0, . . . , k -1}, u, ρ, i , i+1 belongs to either L S factors or R S factors , depending on the parity of i. A close inspection to the above constructions shows that all the automata can be produced in doubly exponential time w.r.t. S.

XX:16 Minimizing resources of sweeping and streaming string transducers

We now show that the complement F (k) S can also be recognized by an automaton of doubly exponential size. Indeed, checking that a word u, ρ, does not belong to F (k) S boils down to verifying that one the following conditions holds: 1. ρ is not a successful run on u. This can be checked by looking at the crossing sequences annotated on the positions of u, using an exponential number of states. 2. The locations in do not define a factorization of ρ. This can be easily checked with polynomially many states.

3.

There exist an index i ∈ {0, . . . , k -1} and an inversion ( , ) (or a co-inversion, depending on the parity of i), with i ≤ ≤ ≤ i+1 , such that, for all periods 0 ≤ p ≤ e S , out(ρ[ , ])[z] = out(ρ[ , ])[z + p] for some position z -note that this is equivalent to saying that is not a k-factorization. The latter condition can be checked by guessing i, ( , ), and a function that maps numbers p ∈ {0, . . . , e S } to positions z p in out(ρ [ , ]). This can be done with doubly exponentially many states.

Using the above encodings, we can also relativize the outputs produced by the transducer S to factors of successful runs. More precisely, we denote by S factors the transducer that reads words of the form u, ρ, 1 , 2 and outputs words of the form out(ρ[ 1 , 2 ]), provided that ρ is a successful run of S on u and 1 , 2 are two locations in it. Note that S factors does not check that the input is well-formed, in particular, that ρ is a successful run of S on u. Because of this, the number of states of S factors is polynomial in the number of states of S, and a succinct representation of S factors can be produced in polynomial time. Now, it is easy to construct a k-pass L-sweeping transducer T equivalent to S| L (k)

S

, as claimed in Theorem 10. The idea is that, on reading the input u, the transducer T guesses a successful run ρ on u and a k-factorization = 0 , . . . , k of ρ -this can be done using the encoding u, ρ, and Lemma 15. While guessing these objects, T performs k passes and outputs

T 0 ( u, ρ, 0 , 1 ) • T 1 ( u, ρ, 1 , 2 ) • . . . • T k-1 ( u, ρ, k-1 , k )
where each T i is the 1-pass sweeping transducer obtained by applying Theorem 6 to S factor (as usual, some mirroring is required for dealing with the odd indexes i). The only technical detail, here, is that different objects ρ, may be guessed along the different passes of T . If this happens, the output produced by T might not be equal to that of S. We can overcome this problem by exploiting disambiguation, namely, by guessing canonical encodings u, ρ, in the language F (k) S . For example, we can fix a lexicographic ordering on these encodings and commit to always guessing the least encoding among those that agree on the input word u. This requires reasoning with both the language F (k) S and its complement F (k) S . By Lemma 15, the two languages are recognized by automata of doubly exponential size in S, and hence T can be constructed in doubly exponential time from S. As a matter of fact, the transducer T that we just constructed is also unambiguous.

We conclude this part by showing how to decide in exponential space if L (k) S = dom(S). In fact, as we already know that L we prove the claim by observing that n must belong to C i,j : indeed, if this is not the case, then the last factor w n (k -1) of T (u n ) would end strictly before the end of the factor v n (i), thus contradicting the hypothesis that S(u n ) = T (u n ). If j < k -1 and n ∈ C i,j , then the claim holds trivially. Finally, suppose that j < k -1 and n ∈ C i,j . Since n ∈ D i,j , we know that the factor v n (i) begins after the beginning of w n (j). However, because v n (i) is not a factor of w n (j), we also know that v n (i) ends after the ending of w n (j). This implies that v n (i + 1) begins after the beginning of w n (j + 1), whence n ∈ D i+1,j+1 .

Using the above claim we can derive the first important equation:

N 2k = D 0,0 ⊆ C 0,0 ∪ D 1,1 ⊆ . . . ⊆ i C i,i ∪ D k,k = i C i,i . (3)
This basically means that it is sufficient to consider only the coverability between pairs of factors v n (i) and w n (i), having the same index i. Now, recall that P i (n) denotes the property " v n (i) is a factor of w n (i) ". The latter property can be equally stated as n ∈ C i,i , and thus can be seen as a special case of a more general property, parametrized by subsets of N 2k . Formally, for every set N ⊆ N 2k , we define the property

R N (n) = " n ∈ N ".
Clearly, the statement of Lemma 17 is equivalent to saying that there exist an index i ∈ {0, . . . , k-1} and a set N ⊆ N 2k such that R N ∩Ci,i (n) holds unboundedly on the coordinates 2i+1 and 2i+2. Based on this, we can prove Lemma 17 by way of contradiction, namely, by assuming that for all i = 0, . . . , k -1 and all N ⊆ N 2k , R N ∩Ci,i does not hold unboundedly on the coordinates 2i + 1 and 2i + 2. More precisely, we will use the latter assumption and exploit an induction on i = 0, . . . , k to construct some sets N i ⊆ N 2k satisfying the following conditions: 1. N i is a Cartesian product of the form {m i } × N 2k-2i , for some tuple

m i ∈ N 2i , 2. if i > 0, then N i ⊆ N i-1 , 3. N i ⊆ j≥i C j,j .
We will reach a contradiction when i = k, since the first condition implies that N k is a singleton, while the last condition requires N k to be empty (indeed, j≥k C j,j is the empty union).

For the base case i = 0, we simply let N 0 = N 2k and observe that conditions 1.-3. hold trivially (in particular, the third condition follows from Equation (3)).

As for the inductive step, we assume that i < k and that N i satisfies conditions 1.-3, and we show how to construct N i+1 satisfying analogous properties. The idea is to fix the components 2i + 1 and 2i + 2 in N i in such a way that the resulting set is contained in N i \ C i,i . Recall that we assumed, towards a contradiction, that R Ni∩Ci,i (n) does not hold unboundedly on the coordinates 2i + 1 and 2i + 2. By Definition 16, this means that there exists a number n 0 ∈ N that satisfies one of the two cases below: a) for all n

∈ N i ∩ C i,i , n[2i + 1] < n 0 or n[2i + 2] -n[2i + 1] < n 0 , b) for all n ∈ N i ∩ C i,i , n[2i + 2] < n 0 or n[2i + 1] -n[2i + 2] < n 0 .
We define N i+1 on the basis of n 0 and of which case holds:

N i+1 =    {n ∈ N i : n[2i + 1] = n 0 , n[2i + 2] = 2n 0 } if case a) holds {n ∈ N i : n[2i + 2] = n 0 , n[2i + 1] = 2n 0 } if case b) holds.
We now verify that N i+1 satisfies the conditions 1.-3. for the index i + 1. The first condition holds by construction and thanks to the inductive hypothesis: indeed, N i projected on and 2i + 2 of n. From this, by applying Proposition 18, we derive that the k-inversion is safe. This proves the left-to-right direction of the first claim of Theorem 10.

Sweeping transducers and MSO

We provide a logical characterization of sweeping transducers. For this we will consider restricted forms of transductions definable in monadic-second order logic (MSO) [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF]. MSO transductions are described by specifying the output (seen as a relational structure) from a fixed number of copies of the input. Formally, an MSO transduction with m copies consists of an MSO sentence Φ dom , some unary MSO formulas Φ i a (x), one for each i ∈ {1, . . . , m} and a ∈ ∆, and some binary MSO formulas Φ i,j ≤ (x, y), one for each i, j ∈ {1, . . . , m}. Intuitively, the sentence Φ dom tells whether the transduction is defined on some input u. The unary formula Φ i a (x) tells whether the element x of the i-th copy of the input belongs to the output and is labeled with the letter a. The formula Φ i,j ≤ (x, y) tells whether, in the produced output, the element x of the i-th copy of the input precedes the element y of the j-th copy of the input. Note that the sentence Φ dom can easily guarantee that, whenever the output is defined, it is well-formed, namely, it is a word. For the sake of simplicity, we assume that Φ i a (x) entails Φ dom , namely, for all words u and all positions x, u |= Φ i a (x) implies u |= Φ dom . Similarly, we assume that Φ i,j ≤ (x, y) entails Φ i (x) and Φ j (y).

Definition 19. Let T be an MSO transduction with m copies. We say that T is order-preserving if each formula Φ i,j ≤ (x, y) entails x ≤ y; order-inversing if each formula Φ i,j ≤ (x, y) entails x ≥ y; k-phase if there is a partition I 0 , I 1 , . . . , I k-1 of the set of indexes {1, . . . , m} such that I 0 < I 1 < . . . < I k-1 , namely, i < j for all 0 ≤ h < h < k, i ∈ I h , and j ∈ I h , and each formula Φ i,j ≤ (x, y) entails x ≤ y if h is even, or x ≥ y otherwise.

We know from [START_REF] Filiot | Logic-automata connections for transformations[END_REF] that order-preserving MSO transductions capture precisely the one-way definable transductions. Symmetrically, order-inversing MSO transductions capture the transductions definable by 1-pass R-sweeping transducers. So it is not surprising that kphase MSO transductions correspond to k-pass L-sweeping transducers:

Theorem 20. k-phase MSO transductions have the same expressive power as functional, k-pass L-sweeping transducers.

Proof. We first show how to translate a k-pass L-sweeping, functional transducer S into an equivalent k-phase MSO transduction. The technique is a variant of the classical translation from two-way transducers to MSO transductions (see for instance [START_REF] Filiot | Logic-automata connections for transformations[END_REF]).

First, thanks to Proposition 1, we can assume, without loss of generality, that the sweeping transducer S is unambiguous. Recall that S performs at most k passes, and let c S be the maximal number of characters output by a single transition of S. To logically define the output of the MSO transduction, we will take k • c S copies of the input. Each copy of the input is thus indexed by a pair (h, i), where 0 ≤ h < k and 1 ≤ i ≤ c S . Intuitively, the copy indexed by (h, i) represents the i-th letter of the output produced during the pass at level h. Using the classical correspondence between automata and MSO, we can build an MSO sentence Φ dom that tells whether a word u belongs to the domain of the transduction. Similarly, for each index 0 ≤ h < k and each transition rule τ of S, we can build an MSO formula Φ h,τ (x) such that, for all u ∈ dom(S), u |= Φ h,τ (x) iff the transition rule τ is applied at the location = (x, h) of the unique successful run of S induced by u. We complete the definition of the MSO transduction equivalent to S as follows:

XX:22 Minimizing resources of sweeping and streaming string transducers

For the formulas defining the output elements and their labels, we let Φ (h,i) a (x) be the disjunction of the formulas Φ h,τ (x), for all 0 ≤ h < k and τ = (p, a, v, q) such that |v| > i and v(i) = a. Note that, because only one transition rule can be used at each location of the successful run, for each 1 ≤ x ≤ |u| and each 0 ≤ h < k, there can exist at most letter a such that u |= Φ (h,i) a (x). For the formulas ordering the output elements, we define Φ (h,i),(h ,i ) ≤ (x, y) by a case distinction:

Φ (h,i),(h ,i ) ≤ (x, y) =                  true if h < h
x ≤ y if h = h is even and i ≤ i

x < y if h = h is even and i > i

x ≥ y if h = h is odd and i ≤ i

x > y if h = h is odd and i > i .

It is easy to see that the formulas Φ (h,i),(h ,i ) ≤ (x, y) define a total order on the output structure. It remains to show that the above MSO transduction is k-phase. For this, we order lexicographically the index set (h, i) : 0 ≤ h < k, 1 ≤ i ≤ c S , and partition it into k subsets I 0 < I 1 < . . . , I k-1 , where I h = (h, i) : 1 ≤ i ≤ c S for all h = 0, 1, . . . , k -1. We then observe that the defined partition satisfies Definition 19: indeed, for all pairs (h, i), (h, j) ∈ I h , Φ (h,i)(h,j) ≤ (x, y) entails either x ≤ y or x ≥ y, depending on whether h is even or odd.

We now prove the converse translation, from a k-phase MSO transduction to an equivalent k-pass L-sweeping transducer. Let Φ dom , Φ i a (x), and Φ i,j ≤ (x, y) be the formulas defining an arbitrary k-phase MSO transduction, where i, j range over some finite set I. Further let I 0 < I 1 < . . . , I k-1 be a partition of I satisfying the third item of Definition 19. Note that, for a fixed 0 ≤ h < k, the family of formulas Φ i a (x) and Φ i,j ≤ (x, y) where i, j range over I h define an MSO transduction that is either order-preserving or order-inversing, depending on whether h is even or odd. For the sake of brevity, we denote by T the original k-pass MSO transduction, and by T 0 , T 1 , . . . , T k-1 the corresponding order-preserving/order-inversing MSO transductions.

If each T h maps an input word u to an output v h , then we know that T maps u to the juxtaposition v 0 • v 1 • . . . • v k-1 . Moreover, we know from [START_REF] Filiot | Logic-automata connections for transformations[END_REF] that we can translate the orderpreserving transductions T 0 , T 2 , . . . to equivalent one-way transducers S 0 , S 2 , . . .. Similarly, we can translate the order-inversing transductions T 1 , T 3 , . . . to equivalent 1-pass R-sweeping transducers S 1 , S 3 , . . .. Thus, we can obtain the desired k-pass L-sweeping transducer S by simply concatenating the transducers S 0 , S 1 , S 2 , S 3 , . . ..

Conclusions

We showed that sweeping transducers, bounded-reversal transducers, and concatenation-free streaming transducers define the same subclass of regular word transductions. Our main result is an effective characterization of transductions definable by sweeping transducers with a fixed number of passes. As a consequence we obtained a procedure that minimizes the number of registers in a concatenation-free sweeping transducer. We believe that similar results can be proven for two-way (non-sweeping) transducers, using a refined version of the constructions presented here. In this respect, an interesting open problem is to characterize the two-way transducers that are equivalent to sweeping transducers, but with an arbitrary (unspecified) number of passes.

Proposition 3 .

 3 Every concatenation-free streaming transducer with k registers can be transformed in ExpTime into an equivalent unambiguous 2k-pass R-sweeping transducer. The transformation is in Ptime if the streaming transducer is unambiguous. Conversely, every k-pass R-sweeping transducer can be transformed in 2ExpTime into an equivalent unambiguous concatenation-free streaming transducer with k 2 registers. The transformation is in ExpTime if the sweeping transducer is unambiguous.

  Note that the definition of 1-inversion is the same as Definition 4, and hence L (1) S = L S . In particular, by Theorem 6, we know that S is one-way definable iff L (1) S = dom(S). The generalization of this result is provided in Theorem 10 below: k-pass definability is equivalent to k-inversions being all safe, in the same way as one-way definability is equivalent to all inversions having periodic output. Theorem 10. A sweeping transducer S is k-pass L-sweeping definable iff L (k) S = dom(S), and this can be decided in ExpSpace. Moreover, given a sweeping transducer S, one can construct in 2ExpTime an unambiguous k-pass L-sweeping transducer T equivalent to S| L (k) S .

S

  are recognized by automata of doubly exponential size. Lemma 15. The language F (k) S and its complement F (k) S are recognized by non-deterministic finite state automata of size double exponential w.r.t. S.

⊆

  dom(S), it suffices to decide only the containment L (k) S ⊇ dom(S). We know from Lemma 14 that the language L (k) S coincides with the projection of F (k) S on the underlying words u. Thus, we have L (k) S ⊇ dom(S) if and only if F (k) S ∩ D = ∅ where D = { u, ρ, : u ∈ dom(S)}. A close inspection of the construction of the automaton for F (k) S shows that the emptiness of F (k) S ∩ D can be decided in ExpSpace.

is an entry point of L 1 and

is an exit point of L 2 , 1 < 2 and x 1 ≤ x 2 ,

This work was partially supported by the ExStream project (ANR-13-JS02-0010) and the TUM-IAS. † On leave at the Institute for Advanced Studies of the Technical University of Munich.

© Félix Baschenis, Olivier Gauwin, Anca Muscholl, Gabriele Puppis; licensed under Creative

Completeness. Here we prove the left-to-right direction of the first claim of Theorem 10. We suppose that S is an L-sweeping transducer and T is an equivalent k-pass Lsweeping transducer. We fix, once and for all, a successful run ρ of S on u and a k-inversion = ( 1 , 2 ), . . . , ( 2k-1 , 2k ) of ρ.

The goal is to prove that is safe, namely, that the factor of the output produced between the locations of some (co-)inversion ( 2i+1 , 2i+2 ) of is periodic, with uniformly bounded period. The main idea is to try to find a factor out(ρ[ 2i+1 , 2i+2 ]) that is entirely covered by the output produced along a single pass of the equivalent transducer T , and apply a suitable generalization of Proposition 5. Informally, this works by pumping the output out(ρ[ 2i+1 , 2i+2 ]) through repeating the witnessing loops of ( 2i+1 , 2i+2 ). In a similar way, we pump the output produced along a single pass of T . Then, by analyzing how the former outputs are covered by the latter outputs, we deduce the periodicity of out(ρ[ 2i+1 , 2i+2 ]).

The main difficulty in formalizing the above idea lies in the fact that the k passes of the supposed transducer T cannot be identified directly on the run ρ of S. Therefore we need to reason in a proper way about families of factors associated with (co-)inversions inside pumped runs. Below, we introduce some terminology and notation to ease this task.

Recall that = ( 1 , 2 ), . . . , ( 2k-1 , 2k ) is a k-inversion of the run ρ. For all i = 0, . . . , k -1, let L 2i+1 and L 2i+2 be the witnessing loops of ( 2i+1 , 2i+2 ). For a given tuple of numbers n = (n 1 , . . . , n 2k ) ∈ N 2k , we define

where L = L 1 , . . . , L 2k and n = n 1 , . . . , n 2k (recall that this is the run obtained by pumping the loops L 1 , . . . , L 2k respectively n 1 , . . . , n 2k times, as described in Section 4). Similarly, we denote by u n the word parsed by the pumped run ρ n . We would like to map the inversions and co-inversions of on the pumped runs ρ n . Consider an inversion ( 2i+1 , 2i+2 ), for some i ∈ {1, . . . , 2k} (the case of a co-inversion is similar). Recall that when pumping loops in ρ, several copies of the original locations may be introduced. In particular, among the copies of the inversion ( 2i+1 , 2i+2 ) that appear in the pumped run ρ n , we will consider the maximal one, which is identified by taking the first copy ˜ 2i+1 of 2i+1 and the last copy ˜ 2i+2 of 2i+2 . For the sake of brevity, we say that ( ˜ 2i+1 , ˜ 2i+2 ) is the inversion of ρ n that corresponds to ( 2i+1 , 2i+2 ).

We can now define the key objects for our reasoning, that is, the factors of the output of a pumped run ρ n that correspond in the original run ρ to the factors produced between the locations of the (co-)inversions of . Formally, for every 2k-tuple n of natural numbers and every index i = 0, . . . , k -1, we define

where ( ˜ 2i+1 , ˜ 2i+2 ) is the (co-)inversion of ρ n that corresponds to ( 2i+1 , 2i+2 ). Note that the above factors depend on the k-inversion and on the tuple n, which represents the number of times we pump each witnessing loop of . For simplicity, since is understood from the context, we will often drop the subscript from the notation, thus writing v n (i). Below we highlight the relevant factors inside the output produced by S on u n :

where ˜ 0 is the first location of ρ n , ˜ 2k+1 is the last location of ρ n .

In a similar way, we can factorize the output produced by the k-pass L-sweeping transducer T when reading the input u n . However, the focus here is on the factors of the output XX:18 Minimizing resources of sweeping and streaming string transducers produced along each pass. Formally, given n ∈ N 2k , we let σ n be some successful run of T on u n . For every j = 0, . . . , k -1, we let j be the first location of σ n at level j. We further let k be the last location of σ n , which is at level k -1. We then define

and factorize the output of T on u n as follows:

(

The next step is to exploit the hypothesis that S and T are equivalent. This means that Equations ( 1) and ( 2) represent the same word. From this we derive that, for any given n ∈ N 2k , at least one of the words v n (i) highlighted in Equation ( 1) is a factor of the word w n (i) highlighted in Equation [START_REF] Alur | Expressiveness of streaming string transducers[END_REF]. However, what is the index i for which this coverability relation holds depends on the parameter n. In order to enable a reasoning similar to that of Proposition 5, we need to find a single index i such that, for "sufficiently many" parameters n, v n (i) is a factor of w n (i). The definition below, formalizes what we mean precisely by "sufficiently many" n -intuitively, we require that specific coordinates of n are unbounded, as well the differences between these coordinates.

Definition 16. Let P(n) denote an arbitrary property of tuples n ∈ N 2k . Further let h, h be two distinct coordinates in {1, . . . , 2k}. We say that P(n) holds unboundedly on the coordinates h, h of n if, for all numbers n 0 ∈ N, there exist n 1 , n 2 ∈ N 2k such that: P(n 1 ) and P(n 2 ) hold,

We recall that each factor v n (i) is associated with the (co-)inversion ( 2i+1 , 2i+2 ), and that the corresponding components n[2i + 1] and n[2i + 2] of the parameter n denote the number of times the witnessing loops L 2i+1 and L 2i+2 are pumped in ρ n . The specific properties we are interested in are the following ones, for i = 0, . . . , k -1:

It is not difficult to see that for every tuple n ∈ N 2k , P i (n) holds for some i ∈ {0, . . . , k -1}. From this, using a suitable counting argument, we can prove the crucial lemma below. Lemma 17. There exists an index i ∈ {0, . . . , k -1} such that the property P i (n) = " v n (i) is a factor of w n (i)" holds unboundedly on the coordinates 2i + 1 and 2i + 2 of n.

Proof. The proof is rather technical, and we need to reason on coverability between pairs of factors v n (i) and w n (j), for possibly distinct indexes i, j ∈ {0, . . . , k -1}. For the sake of brevity, we denote by C i,j the set of tuples n ∈ N 2k such that v n (i) is a factor of w n (j). Similarly, we denote by D i,j the set of tuples n ∈ N 2k such that the suffix out ρ n [ ˜ 2i+1 , ˜ 2k+1 ] of S(u n ) -i.e. the one that starts with v n (i) -is a factor of the suffix out σ n [ j , k ] of T (u n ) -i.e. the one that starts with w n (j). Note that D 0,0 = N 2k since S(u n ) = T (u n ). For convenience, we also let C i,j = D i,j = ∅ whenever i = k or j = k.

Claim. For all i, j ∈ {0, . . . , k -1}, we have D i,j ⊆ C i,j ∪ D i+1,j+1 .

Proof. Consider a tuple n in D i,j . By definition, we know that the suffix of S(u n ) that starts with v n (i) is a factor of the suffix of T (u n ) that starts with w n (j). We distinguish some cases depending on whether j = k -1 or j < k -1, and whether n ∈ C i,j or not. If j = k -1, the components h ≤ 2i is a singleton, and N i projected on the components h ≥ 2i + 1 is N 2k-2i . The second condition N i+1 ⊆ N i holds trivially by construction. As for the third condition, we first claim that N i+1 ∩ C i,i is empty. Indeed, if N i+1 was defined from case a), then all the tuples n in it satisfy n[2i

If any of these tuples belonged also to C i,i , we would get a contradiction with case a). The argument for case b) is just symmetric. Now that we know that N i+1 ∩ C i,i = ∅, we can easily derive

Summing up, we assumed, by way of contradiction, that for all i = 0, . . . , k -1 and all N ⊆ N 2k , R N ∩Ci,i (n) does not hold unboundedly on the coordinates 2i + 1 and 2i + 2. Using this assumption, we defined inductively some sets N 0 , N 1 , . . . , N k satisfying conditions 1.-3. We also observed that, for i = k, the conditions 1. and 3. contradict each other. From this we must conclude that, for some index i and some N ⊆ N 2k , the property R N ∩Ci,i (n) (and hence P i (n) as well) holds unboundedly on the coordinates 2i + 1 and 2i + 2.

The last piece of the puzzle consists of generalizing the statement of Proposition 5. The idea is that we can replace the hypothesis that S is one-way definable by the weaker assumption of Lemma 17. That is, if P i (n) holds unboundedly on the coordinates 2i + 1 and 2i + 2 of n, we can still use the same arguments based on pumping and Fine-Wilf's Theorem as in Proposition 5, in order to deduce that the output out(ρ[ 2i+1 , 2i+2 ]) between the locations of the (co-)inversion is periodic: Proposition 18. If the property P i (n) = " v n (i) is a factor of w n (i) " holds unboundedly on the coordinates 2i+1 and 2i+2 of n, then the output out(ρ[ 2i+1 , 2i+2 ]) produced between the locations of the (co-)inversion ( 2i+1 , 2i+2 ) is periodic, with period e S . In particular, the k-inversion = ( 1 , 2 ), . . . , ( 2k-1 , 2k ) is safe.

Proof. We begin by distinguishing two cases, depending on whether i is even or odd. If i is even, then ( 2i+1 , 2i+2 ) is an inversion and the factor w n (i) is produced along a left-to-right pass of T , therefore like in a one-way transduction. Otherwise, if i is odd, then ( 2i+1 , 2i+2 ) is a co-inversion and the factor w n (i) is produced along a right-to-left pass of T . As the two cases are symmetric, we can focus only on one of the two, say the case where i is even. The proof that out(ρ[ 2i+1 , 2i+2 ]) is periodic is exactly the same as that of Proposition 5. We briefly recall the crucial arguments below.

In that proof we considered an inversion ( 1 , 2 ) and the outputs produced by runs of the form pump n2 L2 (pump n1 L1 (ρ)) between the locations 1 and 2 . The latter outputs were then compared with the outputs produced by an equivalent one-way transducer T . In particular, we observed that the former outputs are factors of the latter outputs. More precisely, by letting the parameters n 1 and n 2 grow independently, it was possible to exploit Fine-Wilf's Theorem and derive the periodicity of the former outputs.

The same argument can be applied here with the inversion ( 2i+1 , 2i+2 ) and the factors v n (i) and w n (i), produced respectively by S and T . Indeed, to apply Fine-Wilf's Theorem, it is sufficient that the coverability relationship holds for pairs of arbitrarily large numbers n[2i + 1] and n[2i + 2], and that these numbers can vary independently of each other. This is precisely what it means for the property P i (n) to hold unboundedly on the coordinates 2i + 1 and 2i + 2 of n.

To conclude, we assumed that the L-sweeping transducer S is equivalent to a k-pass Lsweeping transducer T . We considered a successful run ρ of S and an arbitrary k-inversion of it. By Lemma 17, we know that there is an index i ∈ {0, . . . , k -1} for which the property P i (n) = " v n (i) is a factor of w n (i) " holds unboundedly on the coordinates 2i + 1