Félix Baschenis
email: fbaschen@labri.fr

Olivier Gauwin
email: ogauwin@labri.fr

Anca Muscholl

Gabriele Puppis
email: gpuppis@labri.fr

One-way definability of sweeping transducers *

Keywords: 1998 ACM Subject Classification Theory of computation -F.4.3 Formal Languages Regular word transductions, sweeping transducers, one-way definability 1

Two-way finite-state transducers on words are strictly more expressive than one-way transducers. It has been shown recently how to decide if a two-way functional transducer has an equivalent one-way transducer, and the complexity of the algorithm is non-elementary. We propose an alternative and simpler characterization for sweeping functional transducers, namely, for transducers that can only reverse their head direction at the extremities of the input. Our algorithm works in 2ExpSpace and, in the positive case, produces an equivalent one-way transducer of doubly exponential size. We also show that the bound on the size of the transducer is tight, and that the one-way definability problem is undecidable for (sweeping) non-functional transducers.

Introduction

Regular word languages form the best understood class of languages. They enjoy several characterizations, in particular by different kinds of finite-state automata. For instance, two-way finite-state automata have the same expressive power as one-way automata. This result has been established independently by Rabin and Scott [START_REF] Rabin | Finite automata and their decision problems[END_REF] and Shepherdson [START_REF] Shepherdson | The reduction of two-way automata to one-way automata[END_REF]. Besides automata, regular languages have logical and algebraic characterizations, namely through monadic second-order logic and congruences of finite index.

Transducers extend automata by producing outputs with each transition. A run generates an output word by concatenating the words produced by its transitions. A transducer thus defines a relation over words. It is called functional when this relation is a function. For finite-state transducers, expressiveness is different than for finite-state automata. As an example, two-way transducers are strictly more expressive than one-way transducers. For instance, the function that maps a word to its mirror image can be done by a back-and-forth pass over the input, but no one-way transducer can do it.

As seen above, we lose some robustness when going from automata to transducers. On the other hand, some of the classical characterizations of regular languages generalize well to transducers. An important result is the equivalence of functional two-way transducers and Ehrenfeucht-Courcelle's monadic-second order transductions [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF] over words. Another characterization of two-way transducers was provided through a new model called streaming string transducers [START_REF] Alur | Streaming transducers for algorithmic verification of single-pass list-processing programs[END_REF][START_REF] Alur | From monadic second-order definable string transformations to transducers[END_REF], that process the input one-way and store the output in write-only registers. Finally, first-order transductions are known to be equivalent to aperiodic streaming transducers [START_REF] Filiot | First-order definable string transformations[END_REF] and to aperiodic two-way transducers [START_REF] Carton | Aperiodic two-way transducers and FO-transductions[END_REF].

The question whether a functional two-way word transducer is equivalent to a one-way transducer has been solved recently in [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF]. The algorithm proposed by [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF] takes a two-way transducer S and builds a one-way transducer T that is "maximal" in the following sense: [START_REF] Alur | Streaming transducers for algorithmic verification of single-pass list-processing programs[END_REF] all accepting runs of T produce correct outputs, and (2) all runs of S that can be performed one-way are realized by T . As a consequence, the two-way transducer S has an equivalent one-way transducer if and only if the constructed one-way transducer T has the same domain as S, which is a decidable problem. The problem is that the upper bound on both the decision procedure and the size of the constructed one-way transducer is non-elementary.

The main contribution of this paper is an elementary procedure for deciding whether a functional two-way word transducer is equivalent to a one-way transducer, for the particular class of sweeping transducers. While two-way transducers can reverse their head direction at any position of the input, sweeping transducers can only reverse it at the first and last position. Unsurprisingly, sweeping transducers are strictly less expressive than two-way transducers, and the following example shows the difference: on input u 1 a u 2 a . . . a u n-1 a u n , where the words u i contain no occurrence of a, the two-way transducer produces as output u n a u n-1 a . . . a u 2 a u 1 (we assume that the alphabet contains at least two letters).

Our decision procedure works in doubly exponential space and, when it succeeds, it produces an equivalent one-way transducer of doubly exponential size. We show that the bound on the size of the transducer is tight for any decision algorithm producing an equivalent one-way transducer from a sweeping transducer. This improves the PSpace lower bound from [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF]. The non-elementary procedure described in [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF] relies on Rabin-Scott's construction for automata, and works by eliminating basic zigzags in runs. Our procedure is closer to the textbook approach (due to Shepherdson) and uses crossing sequences. This requires a decomposition of runs which is incomparable with the zigzag decomposition of [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF]. Finally, we show that the one-way definability problem becomes undecidable for non-functional transducers.

Overview

Section 2 defines transducers and related concepts. Section 3 defines decomposition of runs and gives the construction of a one-way transducer based on such decompositions. In Section 4 we show that all one-way-definable runs admit a decomposition. Section 5 provides the lower bound and the undecidability result. Some proofs are deferred to the appendix.

Preliminaries Transducers

A two-way transducer is a tuple (Σ, ∆, Q, I, F, δ), where Σ (resp., ∆) is a finite input (resp., output) alphabet, Q is a finite set of states, I (resp., F ) is a subset of Q representing the initial (resp., final) states, and δ ⊆ 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. We talk of a one-way transducer whenever δ ⊆ Q × Σ × ∆ × Q × {right}. The size of a transducer is its number of states.

According to standard practice, the states of one-way automata and transducers are usually located between the letters of the input word u = a 1 . . . a n . For this it is convenient to introduce n + 1 positions 0, 1, . . . , n and think of each position i > 0 (resp., 0) as a placeholder between the i-th and the i + 1-th symbols (resp., just before the first symbol a 1 ). Moreover, since here we deal with two-way devices, a single position can be visited several times along a run. Thus, to describe a run of a two-way transducer on input u = a 1 . . . a n , we will associate states with locations, namely, with pairs (x, y) where x is a position among 0, 1, . . . , n and y is an integer representing the number of reversals performed up to a certain point -for short, we call this number y the level of the location.

A run is a sequence of locations, labelled by states and connected by edges, called transitions. The state at 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. In addition, each transition is labelled with a pair a/v consisting of an input symbol a and an output v. There are four types of transitions:

(i -1, 2y + 1) (i, 2y + 1) (i -1, 2y) (i, 2y) (i, 2y + 1) (i, 2y + 2) (i -1, 2y) (i -1, 2y + 1) a/v a/v a/v a/v
Note that the transitions between locations at even levels are all directed from left to right, while the transitions at odd levels are directed from right to left. More precisely, the upper left (resp., upper right) transition may occur in a run ρ on u = a 1 . . . a n if ρ(i, 2y + 1), a, v, ρ(i -1, 2y + 1), left (resp., ρ(i -1, 2y), a, v, ρ(i, 2y), right ) is a valid transition rule of T and a = a i . Similarly, the lower left (resp., lower right) transition may occur if ρ(i, 2y + 1), a, v, ρ(i, 2y + 2), right (resp., ρ(i -1, 2y), a, v, ρ(i -1, 2y + 1), left ) is a valid transition rule of T and a = a i . For technical reasons (namely, to enable distinguished transitions at the extremities of the input word), we will introduce the special fresh symbols £ and ¡ and allow the lower left (resp., lower right) transition also when i = 0 and a = £ (resp., when i = |u| and a = ¡).

Given a sequence x 1 , . . . , x n , a factor denotes any contiguous subsequence x i , . . . , x j , for 1 ≤ i ≤ j ≤ n. A run on the input u = a 1 . . . a n is said to be successful if it starts at the lower left location (0, 0) with an initial state of T and ends at the upper right location (|u|, y max ) in a final state of T . The output produced by a run is the concatenation of the outputs of its transitions, and it is denoted by out(ρ). We denote by dom(T ) the language of all words u that admit a successful run of T . We order the locations along a run ρ by letting 1 < 2 if 2 is reachable from 1 following the transitions in ρ. Given two locations 1 < 2 of a run ρ, we denote by ρ[ 1 , 2 ] the factor of the run that starts in 1 and ends in 2 . Note that ρ[ 1 , 2 ] is also a run, hence the notation out ρ[ 1 , 2 ] is consistent. the same state and both either at an even level or at an odd level. Indeed, if this were not the case, say if a successful run ρ visits two locations 1 = (x, y 1 ) and 2 = (x, y 2 ) such that ρ( 1 ) = ρ( 2 ) and y 1 , y 2 are both even or both odd, then the output produced by ρ between 1 and 2 is either empty -in which case we could remove ρ[ 1 , 2 ] and obtain an equivalent successful run -or is non-empty -in which case, by repeating ρ[ 1 , 2 ], we could obtain successful runs that produces different outputs on the same input, thus contradicting the assumption that the transducer is functional.

Crossing sequences

Consider a run ρ of a transducer on input u = a 1 . . . a n . For each position x ∈ {0, 1 . . . , n}, we are interested in the sequence of states labelling the locations at position x. Formally, we define the crossing sequence of ρ at x as the tuple ρ|x = ρ(x, y 0 ), . . . , ρ(x, y h ) , where y 0 < . . . < y h are exactly the levels of the locations of ρ of the form (x, y), with y ∈ N (if the transducer is sweeping, we simply have y i = i). If the considered run ρ is successful, then the bottom and top locations at position x have even levels, and the outgoing transitions move rightward. In particular, every crossing sequence of a successful run has odd length. Moreover, if we assume that the successful run is normalized, then every crossing sequence has length at most 2|Q| -1. The crossing number of a run is the maximal length of a crossing sequence of that run. The crossing number of a transducer is the maximal crossing number of any of its normalized runs -note that this value is bounded by 2|Q| -1.

Intercepted factors

An interval of positions 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 a run ρ 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).

It is easy to see that distinct factors intercepted by the same interval I visit disjoint sets of locations. This means that a factor intercepted by I can be uniquely identified by specifying a location in it, e.g., the first or the last one. Accordingly, we will denote by ρ | I/ the factor intercepted by I that visits the location (if this factor does not exist, we simply let ρ | I/ = ε).

A loop of a run ρ is an interval L = [x 1 , x 2 ] such that the crossing sequences at positions x 1 and x 2 are equal, that is, ρ|x 1 = ρ|x 2 . Loops can be used to pump parts of runs, as explained below.

Pumping

Given a loop L = [x 1 , x 2 ] of a run ρ on u and a number m ∈ N, we can replicate m times the factor u[x 1 , x 2 ] of the input and simultaneously, on the run, we replicate m times the loop L. Formally, with β 0 , . . . , β h denoting the factors intercepted by L, we define the run obtained by replicating L as a sequence of the form

pump m L (ρ) = α 0 β m 0 γ 0 forward γ 1 β m 1 α 1 backward α 2 β m 2 γ 2 forward • • • α ymax β m h γ ymax forward (1)
where h < 2|Q| -1 is the maximum level visited by ρ, and α y (resp., β y , γ y ) is the factor of ρ at level y that is intercepted by the interval [0,

x 1 ] (resp., L = [x 1 , x 2 ], [x 2 , |u|]
). Note that each α y β y γ y (resp., γ y β y α y ) is a maximal factor of the run ρ that is forward-oriented (resp., backward-oriented). We also define

pump m L (u) = u[1, x 1 ] • u[x 1 + 1, x 2 ] m • u[x 2 + 1, |u|]
and we observe that pump m L (ρ) is a valid run on pump m L (u). We also remark that the above definition of pumped run works only for sweeping transducers, as 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.

Decompositions of one-way definable runs

The problem we consider in this paper is the one-way definability of functional, sweeping transducers: given a transducer S, we ask if there exists an equivalent one-way transducer T , namely, one such that T (u) = S(u) for all u ∈ Σ . In the answer is "yes", then we also want to compute an equivalent one-way transducer. Of course, there are sweeping transducers S, like S(u) = u • u, that are not equivalent to any one-way transducer (assuming that the alphabet Σ is not unary). Before introducing some technical concepts, let us consider an example that highlights the main idea of the proof. Fix a regular language R (not containing the empty word) and consider the transduction that maps a word on the mirror of the rightmost maximal factor belonging to R. That is, f (u v w) = mirror(v) whenever (1) v ∈ R, (2) there is no v ∈ R such that v is prefix of vw, and (3) w has no factor in R. It can be easily seen that f can be realized by a two-way transducer, but not by a one-way transducer. However, f can be realized by a one-way transducer for particular regular languages R, like the periodic language R = (ab) + : we simply guess v and output mirror(v) ∈ (ba) + from left to right, then we check w. This example shows that periodicities play an important role in deciding whether a given transduction can be realized by a one-way transducer.

We introduce in the following some notations and concepts that will help us to state a sufficient condition for the one-way definability of sweeping transducers. For simplicity, we fix for the remaining of the paper a functional, sweeping transducer S as input. We first introduce some constants: h S is the maximum number of levels visited by the normalized runs of S, c S is the maximum number of symbols produced by a single transition of S, and e S = c S • |Q| 2|Q| , where Q is the state space of S. The constant e S will be used to bound the lengths or the periods of certain parts of the output produced by S, and is related to the number of crossing sequences of S (see also Lemma 6 in Section 4).

A word v is said to have period p if v ∈ w * w for some word w of length p and some prefix w of w. For example, v = abc abc ab has period p = 3. Similarly, we say that v is almost periodic with bound p if v = w 0 w 1 w 2 for some words w 0 , w 2 of length at most p and some non-empty word w 1 of period at most p.

We will also need to identify sub-sequences of a run ρ of S that are induced by particular sets of locations. Recall that ρ[ 1 , 2 ] denotes the factor of ρ delimited by two locations 1 and 2 . Similarly, we denote by ρ | Z the sub-sequence of ρ induced by a set Z of locations -note that Z does not need to be an interval and, even though ρ | Z might not be a valid run of S, we can still refer to the number of transitions and the size of the output. Definition 2. Let ρ be a run of S on u. We define two types of pairs of locations of ρ:

A floor is a pair of locations ( 1 , 2 ) such that 1 ≤ 2 are on the same even level. A ramp is a pair of locations ( 1 , 2 ), with 1 = (x 1 , y 1 ) and 2 = (x 2 , y 2 ), such that (i) x 1 ≤ x 2 , (ii) y 1 < y 2 , (iii) both y 1 and y 2 are even, (iv) the output produced by ρ[ 1 , 2 ] has length at most (y 2 -y 1 + 1) • e S or it is almost periodic with bound 2 • e S , and (v) the output produced by the sub-sequence ρ | Z, where

Z = [ 1 , 2 ] \ [x 1 , x 2 ] × [y 1 , y 2 ], has length at most 2(y 2 -y 1 ) • e S .
Before discussing how the above definitions are used, we give some intuition. The simplest concept is that of floor, which is essentially a forward-oriented factor of a run. Ramps connect consecutive floors. An important constraint in the definition of a ramp ( 1 , 2 ) is that the output of ρ[ 1 , 2 ] is bounded or almost periodic with small bound. We will see later how this constraint eases the production of the output of ρ[ 1 , 2 ] by a one-way transducer. The last constraint on a ramp ( 1 , 2 ) bounds the length of the output produced by the sub- (represented by the hatched area). The constraint is used for those parts of the run that are not covered by floors or ramps. In particular, it guarantees that the size of the output above each floor is bounded by 2h S • e S .

sequence ρ | Z, where Z = [ 1 , 2 ] \ [x 1 , x 2 ] × [y 1 , y 2 ].
The general idea for turning S into an equivalent one-way transducer will be to guess (and check) a decomposition of the run of S into factors that are floors or ramps. Definition 3. A decomposition of a run ρ is a factorization into floors and ramps. Figure 1 gives an example of a decomposition. Note that, thanks to Definition 2, the number of symbols produced outside the segments F 1 , F 2 , . . . and the rectangles R 1 , R 2 , . . . is small (indeed, bounded by 2h S • e S ); so most of the output is produced inside these segments and rectangles. We can now state our main result: Theorem 4. A sweeping functional transducer S is one-way definable if and only if every input word has some successful run of S that admits a decomposition. Moreover, we can construct from S a one-way transducer T that maps u to v whenever there is a successful run of S on u that outputs v and admits a decomposition. The construction of T takes doubly exponential time in |S|. In particular, S is one-way definable if and only if dom(T ) = dom(S). The latter condition can be tested in polynomial space in |S| and |T |, so in doubly exponential space in |S|.

The first claim of the theorem gives the main characterization, namely, it shows that the existence of decompositions of successful runs, for all possible inputs in the domain of S, is a sufficient and necessary condition for the transduction to be one-way definable. The second claim shows a property that is slightly more general than sufficiency: it allows to compute a one-way transducer T that is somehow the "best one-way approximation" of S, in the sense that the transduction computed by T is always contained in the transduction computed by S and it is equal when S is one-way definable. The last claim deals with the effectiveness of the characterization, showing that one-way definability is decidable in 2ExpSpace. For the sake of presentation, we divide the proof of the theorem into two parts. The first part, given below, deals with the sufficiency and the effectiveness of the characterization (i.e. the second and third claims of the theorem). The second part, which is the most technical one and is deferred to Section 4, deals with the necessary part of the characterization.

Proof of Theorem 4 (sufficiency and effectiveness).

We build from S a one-way transducer T that simulates all successful runs of S that admit a decomposition. Consider one such run ρ. We begin by observing that a decomposition of ρ can be described by a sequence of locations 0 < 1 < . . . < t , where 0 = (0, 0), t = (x max , y max ), and, for all 0 ≤ i < t, ( i , i+1 ) is a floor or a ramp. In particular, the one-way transducer T will guess the crossing sequences of ρ, together with a sequence of locations ( i ) i≤t , which are intended to represent a decomposition of ρ. Below, we show how to check that the guessed sequence of locations represents a valid decomposition, and how to produce the corresponding output.

Traversing the floors of the decomposition does not pose particular problems, as these are forward-oriented factors of the run ρ, which can be directly simulated by T without reversing the head. Of course, we need to store the bounded output on the levels above the floor, and check that the output on the levels below the floor matches some stored output words. The interesting case happens when T simulates a ramp ( i , i+1 ), with i = (x i , y i ) and i+1 = (x i+1 , y i+1 ). First of all, it is easy for T to verify the first three conditions of the definition of ramp, namely, that x i ≤ x i+1 , y i < y i+1 , and both y i and y i+1 are even. Checking the remaining conditions is more difficult and requires storing some words for a total length that does not exceed 8h S •e S -in particular, this explains the doubly exponential blowup of the state space of T . More precisely, at the beginning of the computation, T guesses, for each ramp ( i , i+1 ), with i = (x i , y i ) and i+1 = (x i+1 , y i+1 ): a word v i that has length at most (y i+1 -y i +1)•e S or is almost periodic with bound 2•e S (in the latter case, in fact, the word is described by a prefix, a suffix, and a repeating pattern, each one of length at most 2 • e S ), some wordsv y andv y , that is, two words for each level y ∈ {y i + 1, . . . , y i+1 }, whose lengths sum up to at most 2h S • e S . The idea is that each word v i represents the output produced by the factor ρ[ i , i+1 ] (this output is bounded or is almost periodic, thanks to the fourth condition of the definition of ramp). Note that, by construction, there can be at most h S ramps in the decomposition, and hence the sum of the lengths of the words used to represent the v i 's does not exceed 6 • h S • e S . Similarly, each wordv y (resp.,v y ) represents the output produced by the factor of the run ρ that is at level y and to the left of the position x i (resp., right of x i+1 ), where i is the unique index such that y i < y ≤ y i+1 (resp., y i ≤ y < y i+1 ). The total length of these words is at most 2h S • e S . Overall, the sum of the lengths of all the words guessed by T never exceeds 8h S • e S .

Using the words v i ,v y ,v y and some additional pointers, the transducer T can verify that the guessed ramps satisfy the required conditions and that the decomposition is thus valid. In the same way, the words v i ,v y ,v y can be used to produce the output out(ρ[ i , i+1 ]) associated with each ramp ( i , i+1 ). For this, it is sufficient to visit the positions of the ramp ( i , i+1 ) and, at the same time, fetch blocks of symbols of appropriate length in the word v i , so as to eventually match the length of the desired output out(ρ[ i , i+1 ]) -note that this requires taking into account also the wordsv y andv y .

We just described informally a one-way transducer T that simulates any run ρ of S that admits a decomposition. The size of T is doubly exponential in the size of S and this proves the second claim of the theorem.

Assuming that the existence of decompositions of successful runs is also a necessary condition for the one-way definability of S (this will be proved in the next section), we can easily derive from the above constructions a 2ExpSpace decision procedure for testing one-way definability. More precisely, given a sweeping transducer S, one constructs T as above in doubly exponential time, and then tests whether dom(S) ⊆ dom(T ). The latter problem can be seen as a containment problem between a two-way non-deterministic finite-state automaton A and a one-way non-deterministic finite-state automaton B. Using standard constructions, one can turn A into an equivalent one-way non-deterministic finitestate automaton A (which is exponential in S), and finally decide the containment A ⊆ B in polynomial space in A and B, that is, in doubly exponential space in S.

Characterizing one-way definability

In this section we prove the harder direction of the first claim of Theorem 4: if a sweeping functional transducer is one-way definable, then every accepted input has a successful run that can be decomposed into floors and ramps. We begin by identifying some phenomena that prevent a transducer to be one-way definable. A first example is the mirror transduction, where a large number of symbols need to be generated from right to left. Another example is the doubling transduction S(u) = u • u.

Here, we have an inversion, namely large parts of the input must be generated before other large parts that are located to their left. We give a formal definition of inversions below.

Fix a successful run ρ of S and consider a loop L = [x 1 , x 2 ] of ρ. A location 1 of ρ is called entry point of L if 1 is the first location of the factor intercepted by L at level y, for some y. Similarly, a location 2 is called an exit point of L if 2 is the last location of the factor intercepted by L at level k, for some k. Note that 1 belongs to {x 1 }×(2N) ∪ {x 2 }×(2N+1), and 2 belongs to {x 2 } × (2N) ∪ {x 1 } × (2N + 1). Finally, we say that an intercepted factor ρ | I/ is captured by a loop L if I contains L (possibly, I = L) and the subfactor intercepted by L on the same level as , has non-empty output. Definition 5. An inversion of the 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:

1 is an entry point of L 1 and 2 is an exit point of L 2 , 1 < 2 and x 1 ≥ x 2 (namely, 2 strictly follows 1 along the run, but the left endpoint of L 2 precedes the left endpoint of L 1 ), for both i = 1 and i = 2, the intercepted factor ρ | L i / i is captured by the loop L i , but it is not captured by any other loop strongly contained in L i . We say that the above loops L 1 and L 2 are witnessing the inversion ( 1 , 2 ).

The left-hand side of Figure 2 gives an example of an inversion, where the entry point 1 of L 1 and the exit point 2 of are represented by white circles.

The first lemma (proved in the appendix) can be used to bound the lengths of the outputs produced by the factors ρ | L 1 / 1 and ρ | L 2 / 2 , where 1 , 2 , L 1 , L 2 are as in Definition 5:

L2 L1 1 2 X(3,3) 2 X(3,3) 1 v 1 v 1 v 1 v 2 v 2 v 2
Figure 2 To the left: an entry point 1 of L1 and an exit point 2 of L2 forming an inversion. To the right: the run obtained by pumping the loops L1 and L2. Lemma 6. If an intercepted factor ρ | I/ is not captured by any loop L strongly contained in I, then the length of its output is at most e S . In particular, for every inversion ( 1 , 2 ) witnessed by some loops L 1 and L 2 , we have

1 ≤ out(ρ | L i / i ) ≤ e S , for both i = 1 and i = 2.
The next proposition gives the crucial property for characterizing one-way definability, as it shows that the transducer S is one-way definable only if for every inversion ( 1 , 2 ), the output of ρ[ 1 , 2 ] is periodic. Proposition 7. Suppose that the sweeping transducer S is one-way definable. Then, for all inversions ( 1 , 2 ) of the run ρ witnessed by loops L 1 , L 2 and for both i = 1 and i = 2, the output of ρ[ 1 , 2 ] has period out(ρ | L i / i ) , hence, in particular, at most e S .

A key ingredient for the proof of the above proposition is Fine and Wilf's theorem [START_REF] Lothaire | Combinatorics on words[END_REF]. In short, this theorem says that, whenever two periodic words w 1 , w 2 share a sufficiently long factor, then they have the same periods. Below, we state a slightly stronger variant of Fine and Wilf's theorem, which contains an additional claim that shows how to align a common factor of the two words w 1 , w 2 so as to form a third word containing a prefix of w 1 and a suffix of w 2 . The additional claim will be exploited in the proof of Proposition 7 and Lemma 11.

Lemma 8 (Fine and Wilf).

If w 1 is a word with period p 1 , w 2 is a word with period p 2 , and w 1 and w 2 have a common factor of length at least p 1 + p 2 -gcd(p 1 , p 2 ), then w 1 and w 2 have also period gcd(p 1 , p 2 ). If in addition we have

w 1 = u 1 w v 1 , w 2 = u 2 w v 2 , and |w| ≥ gcd(p 1 , p 2 ), then w 3 = u 1 w v 2 has also period gcd(p 1 , p 2 ).
Proof of Proposition 7. Let L 1 = (x 1 , x 1 ), L 2 = (x 2 , x 2 ) be the loops witnessing the inversion ( 1 , 2 ). Note that the two loops L 1 and L 2 might not be ordered exactly as shown in Figure 2. In fact, two cases can arise: either

x 2 < x 2 ≤ x 1 < x 1 (that is, L 1 and L 2 are disjoint and L 1 is to the right of L 2 ) or x 2 ≤ x 1 < x 2 ≤ x 1 (that is, L 1 overlaps to the right with L 2 ).
We begin by pumping the loops L 1 and L 2 (see the right-hand side of Figure 2). Formally, for all positive numbers m 1 , m 2 , we define

ρ (m1,m2) = pump m2 L2 (pump m1 L1 (ρ)) and u (m1,m2) = pump m2 L2 (pump m1 L1 (u)) .
We identify the positions of u (m1,m2) that mark the endpoints of the copies of the loops L 1 and L 2 in the pumped run ρ (m1,m2) . Because L 2 precedes L 1 with respect to the ordering of positions, it is easier to define first the set of endpoints of the copies of L 2 :

X(m1,m2)

2 = {x 2 + i∆ 2 | 0 ≤ i ≤ m 2 } where ∆ 2 = x 2 -x 2 .
The set of endpoints of the copies of L 1 is defined as X(m1,m2)

1 = {x 1 + i∆ 1 + m 2 ∆ 2 | 0 ≤ i ≤ m 1 } where ∆ 1 = x 1 -x 1 .
We then exploit the hypothesis that S is one-way definable and assume that the one-way transducer T is equivalent to S. In particular, T produces the same output as S on every input u (m1,m2) . Let σ (m1,m2) be a successful run of T on u (m1,m2) . Since T has finitely many states, we can find a large enough number h > 0 and two positions x1 < x 1 ∈ X(h,h)

1
such that the crossing sequences of σ (h,h) at x1 and x 1 are the same. Similarly, we can find two positions x2 < x 2 ∈ X(h,h)

2
such that the crossing sequences of σ (h,h) at x2 and x 2 are the same. This means that L1 = (x 1 , x 1 ) and L2 = (x 2 , x 2 ) can be equally seen as loops of ρ (h,h) or as loops of σ (h,h) . In particular, there are constants k 1 , k 2 > 0, 0 ≤ h 1 < k 1 , and 0 ≤ h 2 < k 2 such that, for all positive numbers m 1 , m 2 :

u (k1•m1+h1,k2•m2+h2) = pump m2 L2 (pump m1 L1 (u (h,h) ))
and the above word has a successful run in T of the form pump m2 L2 (pump m1 L1 (σ (h,h) )). Consider the outputs v 1 and v 2 produced by the intercepted factors ρ | L 1 / 1 and ρ | L 2 / 2 , respectively. By Lemma 6, both v 1 and v 2 are non-empty. Moreover, by definition of pumped run, the output produced by ρ

(k1•m1+h1,k2•m2+h2) contains k 1 • m 1 + h 1 consecutive occurrences of v 1 followed by k 2 • m 2 + h 2 consecutive occurrences of v 2 (
see again the right-hand side Figure 2). Formally, we can write

out(ρ (k1•m1+h1,k2•m2+h2) ) = v 0 (m 1 , m 2 )•v k1•m1+h1 1 •v 3 (m 1 , m 2 )•v k2•m2+h2 2 •v 4 (m 1 , m 2 ) (2)
for some words v 0 (m 1 , m 2 ), v 3 (m 1 , m 2 ), and v 4 (m 1 , m 2 ) that may depend on m 1 and m 2 (we highlighted in bold the repeated occurrences of v 1 and v 2 and we observe that v 1 precedes v 2 ).

In a similar way, because the same output is also produced by the the one-way transducer T , i.e. by the run pump m2 L2 (pump m1 L1 (σ (h,h) )), and because the loop L 2 precedes the loop L 1 according to the natural ordering of positions, we have

out(ρ (k1•m1+h1,k2•m2+h2) ) = w 0 • w m2 2 • w 3 • w m1 1 • w 4 (3)
where w 1 (resp., w 2 ) is the output produced by the unique factor of σ (h,h) intercepted by L1 (resp., L2 ), and w 0 , w 3 , w 4 are the remaining parts of the output. Note that, differently from the previous equation, here the first repetition is produced during the loop L2 and the remaining parts w 0 , w 3 , w 4 do not depend on m 1 , m 2 . We now consider the factor

v(m 1 , m 2 ) = v k1•m1+h1 1 • v 3 (m 1 , m 2 ) • v k2•m2+h2 2
of the output produced by S. The following claim shows that this factor is periodic, with a small period that only depends on S (in particular, it does not depend on any of the indices

h, k 1 , k 2 , h 1 , h 2 , m 1 , m 2 ). Claim. For all numbers m 1 , m 2 > 0, the word v(m 1 , m 2 ) = v k1•m1+h1 1 • v 3 (m 1 , m 2 ) • v k2•m2+h2 2 is periodic with period gcd(|v 1 |, |v 2 |).
The idea for the proof of the above claim, detailed in the appendix, is to let m 1 and m 2 grow independently. We exploit Equations ( 2) and (3) to show that v k1•m1+h1 Recall that we aim at proving the periodicity of the output out(ρ[ 1 , 2 ]) of the original run ρ of S between the locations 1 and 2 . The previous arguments, however, concern the outputs v(m 1 , m 2 ), which are produced by factors of the pumped runs ρ (k1•m1+h1,k2•m2+h2) . By Equation (1) in Section 2, out(ρ[ 1 , 2 ]) can be obtained from any v(m 1 , m 2 ) by deleting some occurrences of non-empty words produced by factors intercepted by L 1 or L 2 . More precisely, the words that need to be deleted in v(m 1 , m 2 ) to obtain out(ρ[ 1 , 2 ]) are nonempty and of the form out(ρ | L i / i ), for some i ∈ {1, 2} and some location i such that

1 • v 3 (m 1 , m 2 ) • v 2 has period gcd(|v 1 |, |w 1 |), and that v 1 • v 3 (m 1 , m 2 ) • v k2•m2+h2
1 ≤ i ≤ 2 .
Let us denote by v 1 , . . . , v m these words. Note that, as m 1 and m 2 get larger, v(m 1 , m 2 ) contains arbitrarily long repetitions of each word v i , and hence long factors of period |v i |, for i = 1, . . . , m. Thus, by applying Lemma 8, we get that v(m 1 , m 2 ) has period

p = gcd(|v 1 |, |v 2 |, |v 1 |, . . . , |v m |).
Towards a conclusion, we know that out(ρ

[ 1 , 2 ]) is obtained from v(m 1 , m 2
) by removing occurrences of the words v 1 , . . . , v m whose lengths are multiple of the period p of v(m 1 , m 2 ). This implies that out(ρ[ 1 , 2 ]) is also periodic with period p, which divides out(ρ | L i / i ) for both i = 1 and i = 2.

Recall that the proof of the remaining part of Theorem 4 (necessity of the condition characterizing one-way definability) amounts at constructing a decomposition of the successful run ρ under the assumption that S is one-way definable. We begin to construct a decomposition of ρ by identifying some ramps in it. Intuitively, such ramps are obtained by considering the classes of a suitable equivalence relation: Definition 9. Let be the relation that pairs every two locations , along the run ρ whenever there is an inversion ( 1 , 2 ) of ρ such that 1 ≤ , ≤ 2 , namely, whenever and occur within the same inversion. Let be the reflexive and transitive closure of .

It is easy to see that every equivalence class of is a convex subset with respect to the natural ordering of locations of ρ. The following lemma shows that every non-singleton equivalence class of is a union of a series of inversions that are two-by-two overlapping.

Lemma 10. If two locations ≤ of ρ belong to the same non-singleton equivalence class of , then there is a sequence of locations 1 ≤ 3 ≤ 4 ≤ . . . ≤ n-3 ≤ n-2 ≤ n , for some even number n ≥ 4, such that

1 ≤ ≤ 4 and n-3 ≤ ≤ n , ( 1 , 4 ), ( 3 , 6 ), ( 5 , 8 ), . . . , ( n-5 , n-2 ), ( n-3 , n ) are inversions.
The next result uses Lemma 6, Proposition 7, and Lemma 10 to show that the output produced inside a -equivalence class is also periodic with small period, provided that S is one-way definable. Lemma 11. If S is one-way definable and ≤ are two locations of the run ρ such that , then the output out(ρ[ , ]) produced between and has period at most e S .

Below, we introduce some "bounding boxes" of non-singleton -equivalence classes. Intuitively, these bounding boxes are the smallest possible rectangles that start and end at some even levels and that cover all the locations forming an inversion inside a non-singleton -equivalence class. Subsequently, in Lemma 13 we show that these bounding boxes can be given the status of ramps in a suitable decomposition of ρ. Definition 12. Let K be a non-singleton -equivalence class and let H be the subset of K that contains all the locations , ∈ K forming an inversion ( , ). We define [K] to be the pair of locations 1 = (x 1 , y 1 ) and 2 = (x 2 , y 2 ) such that x 1 (resp., x 2 ) is the position of the leftmost (resp., rightmost) location ∈ H, y 1 (resp., y 2 ) is the highest (resp., lowest) even level such that y 1 ≤ y (resp., y 2 ≥ y) for all locations = (x, y) ∈ H.

Lemma 13. If K is a non-singleton -equivalence class, then [K] is a ramp.
For the sake of brevity, we call -ramp any ramp of the form [K], where K is a nonsingleton -equivalence class. The results obtained so far imply that every location of the run ρ covered by an inversion is also covered by a -ramp. To complete the decomposition of ρ, we need to consider the locations that are not strictly covered by -ramps, formally, the set

B = { | ( 1 , 2 ) -ramp s.t. 1 < < 2 }.
We equip B with the natural ordering of locations induced by ρ. We now consider some maximal convex subset C of B. Note that the left/right endpoint of C coincides with the first/last location of the run ρ or with the right/left endpoint of some -ramp. Below, we show how to decompose the sub-run ρ | C into a series of floors and ramps. After this, we will be able to get a full decomposition of ρ by interleaving the -ramps that we defined above with the floors and the ramps that decompose each sub-run ρ | C.

Let D C be the set of locations = (x, y) of C such that there is some loop L = [x, x ], with x ≥ x, whose intercepted factor ρ | L/ lies entirely inside C and produces non-empty output. We remark that the set D C may be non-empty. To see this, one can imagine the existence of two consecutive -ramps (e.g. R 1 and R 2 in Figure 1) and a loop between them that produces non-empty output (e.g. the factor F 2 ). In a more general scenario, one can find several loops between two consecutive -ramps that span across different levels. We can observe however that all the locations in D C are on even levels. Indeed, if this were not the case for some = (x, y) ∈ D C , then we could select a minimal loop

L = [x 1 , x 2 ] such that x 1 ≤ x ≤ x 2 and out(ρ | L/ ) = ε. Since y is odd, 1 = (x 2 , y
) is an entry point of L and 2 = (x 1 , y) is an exit point of L, and hence ( 1 , 2 ) is an inversion. Since 1 ≤ ≤ 2 and all inversions are covered by -ramps, there is a -ramp ( 1 , 2 ) such that 1 ≤ ≤ 2 . However, as 1 and 2 are at even levels, must be different from these two locations, and this would contradict the definition of D C . Using similar arguments, one can also show that the locations in D C are arranged along a "rising diagonal", from lower left to upper right.

The above properties suggest that the locations in D C identify some floors and ramps that form a decomposition of ρ | C. The following lemma shows that this is indeed the case, namely, that any two consecutive locations in D C form a floor or a ramp. Lemma 14. Let 1 = (x 1 , y 1 ) and 2 = (x 2 , y 2 ) be two consecutive locations of D C . Then, x 1 ≤ x 2 and y 1 ≤ y 2 and the pair ( 1 , 2 ) is a floor or a ramp, depending on whether y 1 = y 2 or y 1 < y 2 .

We have just shown how to construct a decomposition of the entire run ρ, assuming that the sweeping transducer S is one-way definable. This completes the proof of the only-if direction of the first claim of Theorem 4.

Lower bound and undecidability

We show now that the doubly exponential blow-up in size stated by Theorem 4, cannot be avoided.

Proposition 15. There is a family (f n ) n of functions from {0, 1} * to {0, 1} * such that:

f n can be computed by a sweeping transducer of size quadratic in n, f n can be computed by a one-way transducer, any one-way transducer computing f n has at least 2 2 n-1 states.

We exhibit such a family of function by defining the domain of f n to be the set of words of the form

a 0 bin 0 a 1 bin 1 a 2 . . . a 2 n -1 bin 2 n -1 a 2 n
where a i ∈ {0, 1} for all i ∈ {0, . . . , 2 n }. On those words, we define f n as follows:

f n a 0 bin 0 a 1 bin 1 a 2 . . . a 2 n -1 bin 2 n -1 a 2 n = w • w where w = a 0 a 1 . . . a 2 n .
We conclude the section by showing that the one-way definability problem becomes undecidable for relations computed by sweeping non-functional transducers. Note that ε-transitions are needed in order to capture the class of one-way definable relations. On the other hand, for one-way definable functions, ε-transitions can be excluded.

Proposition 16. The problem of testing whether a sweeping non-functional transducer is one-way definable is undecidable.

Conclusion

In this paper we proposed a new algorithm that decides whether a sweeping transducer is equivalent to a one-way transducer. Our decision algorithm works in doubly exponential space and produces one-way transducers of doubly exponential size. The latter bound is shown to be optimal. An open question is whether the decision problem has lower complexity if we do not build the one-way transducer.

The main open question is whether our algorithm can be extended to two-way functional transducers that are not necessarily sweeping. We conjecture that this is the case and that a similar characterization based on decompositions of runs into floors and ramps can be obtained. The main difficulty is that (de)pumping loops is more complicated because of permutations.

One-way definability is also a special case of the following open problem: given an integer k and a two-way transducer, decide if there is an equivalent k-crossing two-way transducer. Finally, note that the problem that we considered here becomes much simpler in the origin semantics of [START_REF] Bojańczyk | Transducers with origin information[END_REF]: there, the output of a transducer also includes the origin of each symbol, i.e., the input position where the symbol was generated. In the origin semantics, the oneway definability problem is PSpace-complete, and an equivalent one-way transducer has exponential size.

A Appendix

Proposition 1. Functionality of two-way transducers can be decided in polynomial space. This problem is PSpace-hard even for sweeping transducers.

Proof. Showing that the problem is PSpace-hard for sweeping transducers is easy: we reduce from the emptiness problem of the intersection of NFAs.

Given n NFAs A 1 , . . . , A n we build a sweeping transducer S which simulates the automaton A i on its i-th pass. At the end of the i-th pass, if the simulation of A i is in an accepting state, we choose non-deterministically either to stop the computation and output the number i, or to continue testing if the input is in L(A i+1 ). That way, a pair (u, i) is in the transduction defined by S if and only if A i accepts the input u. This yields exactly to the desired property of S: it is functional if and only if i≤n L(A i ) = ∅.

To show that the functionality problem is in PSpace for two-way transducers, we use a reduction similar to [START_REF] Alur | Streaming transducers for algorithmic verification of single-pass list-processing programs[END_REF], to the reachability of 1-counter machines. The latter problem belongs to Nlogspace and we will obtain an exponential-sized 1-counter machine, that can be simulated on-the-fly. Altogether this yields PSpace complexity. We recall that N = 2|Q| is the maximal crossing number of a normalized run in a functional transducer. We first show the following claim:

Claim. If S is not functional, then either there exists (1) a successful run with crossing number at most 2N and non-empty output on some repetition in a crossing sequence, or (2) two normalized runs on the same input, each with crossing number at most N , and with different outputs.

Proof. Assume there is a successful run with non-empty output on some repetition in a crossing sequence. That is, the crossing sequence contains two locations with the same state and both on even/odd level, such that the output on the factor run delimited by these locations is non-empty. We can first remove from this run all repetitions that produce empty outputs. Then, we can also remove the repetitions with non-empty outputs, obtaining other successful runs, until there remains only one non-empty repetition. The run produced is an instance of case [START_REF] Alur | Streaming transducers for algorithmic verification of single-pass list-processing programs[END_REF].

On the other hand, if all the repetitions in the crossing sequences of any successful run produce an empty output, we can find a pair of runs satisfying (2): We know by non functionality that there is pair (u, v) of outputs produced by different runs on the same input, such that u = v. As we know there is no repetition producing a non-empty output, we can remove the repetitions of the runs of u and v and obtain new successful runs producing the same u and v. As those runs do not have any repetition in their crossing sequence, they have a crossing number ≤ N .

To determine non-functionality, the 1-counter machine will guess between the two cases of the lemma: in (1) it will guess a run of S of crossing number smaller than 2N , and in (2) it will guess two runs of S on the same input of crossing number smaller than N . In the second case, we define u and v to be the two outputs of the runs, and S decides if it will check |u| = |v| or the existence of a position i such that u i = v i .

In each case, M guesses two locations in the runs and marks locations on the crossing sequences that will help to identify certain factors of runs.

In the first case M guesses two locations in the run at the same crossing sequence, that have the same state, and the same movement of the input head, and M marks all locations between those two locations. It checks then that the output produced by the factor containing marked locations is non-empty.

In the second case, when verifying that |u| = |v|, it guesses one location in the second run, and marks the locations before it in the corresponding crossing sequences. The counter is incremented by the number of letters produced in the first run, and decremented by those produced by marked locations of the second. The guessed location represents the moment in the second run where it has produced an output longer than |u|.

In the second case, when checking the existence of a position such that u i = v i , it guesses one location in each run, and marks the locations before those in the corresponding crossing sequences. The counter is incremented (resp. decremented) by the number of letters produced by marked locations of the first (resp. second) run. The machine also checks that the letters produced at the guessed locations are different, and the counter's value is 0 at the end of the run. This guarantees that the letters were produced at the same place. Lemma 6. If an intercepted factor ρ | I/ is not captured by any loop L strongly contained in I, then the length of its output is at most e S . In particular, for every inversion ( 1 , 2 ) witnessed by some loops L 1 and L 2 , we have 1 ≤ out(ρ | L i / i ) ≤ e S , for both i = 1 and i = 2.

Proof. Let I = [x 1 , x 2 ] be an interval, = (x, y) a location, with x 1 ≤ x ≤ x 2 , and α = ρ | I/ the intercepted factor. Suppose that there is no loop L strongly contained in I that captures α. We have to show that |out(α)| ≤ e S .

We first claim that the number of transitions of the factor α that produce non-empty output does not exceed the number of distinct crossing sequences of the form ρ|x, with x 1 ≤ x < x 2 . Indeed, if this were not the case, then there would exist two locations = (x , y) and = (x , y), with x 1 < x < x < x 2 , such that the crossing sequences at x and x are the same, depending on whether y is even or odd, and are either targets or sources of two distinct transitions that produce non-empty output. From the above, we derive the existence of a loop L = [x , x ] that is strongly contained in I and intercepts a factor on level y producing non-empty output, i.e. a contradiction to our hypotheses on α. Now, recall that the run ρ is normalized, and hence there are at most |Q| 2|Q| distinct crossing sequences of the form ρ|x, with x 1 ≤ x < x 2 . Together with the previous claim, this implies that the factor α = ρ | I/ contains at most |Q| 2|Q| transitions that produce non-empty output. To prove the first result stated in the lemma it is thus sufficient to recall that each of those transitions can produce at most c S symbols and e S = c S • |Q| 2|Q| .

We conclude the proof by showing the last claim of the lemma. Consider an inversion ( 1 , 2 ) witnessed by some loop L 1 and L 2 . By definition, we have that, for both i = 1 and i = 2, the intercepted factor ρ | L i / i is captured by L i , but is not captured by any loop strongly contained in L i . Together with the previous claims, this implies that

1 ≤ out(ρ | L i / i ) ≤ e S .

Claim (in the proof of Proposition 7). For all numbers m

1 , m 2 > 0, the word v(m 1 , m 2 ) = v k1•m1+h1 1 • v 3 (m 1 , m 2 ) • v k2•m2+h2 2 is periodic with period gcd(|v 1 |, |v 2 |).
Proof. The proof of this claim is based on Equations ( 2) and ( 3), which we recall here:

out(ρ (k1•m1+h1,k2•m2+h2) ) = v 0 (m 1 , m 2 ) • v k1•m1+h1 1 • v 3 (m 1 , m 2 ) • v k2•m2+h2 2 • v 4 (m 1 , m 2 ) (2) out(ρ (k1•m1+h1,k2•m2+h2) ) = w 0 • w m2 2 • w 3 • w m1 1 • w 4 (3)
We are going to use the above equations for varying parameters m 1 , m 2 . We first fix m 1 large enough so that the prefix

v 0 (m 1 , m 2 ) • v k1•m1+h1 1 is longer than |w 0 | + |v 1 |.
Then, by letting m 2 grow arbitrarily large and by using the above equations, we get that the periodic word w m2 2 covers an arbitrarily long prefix of

v 1 •v 3 (m 1 , m 2 )•v k2•m2+h2
(m1,m2) 3 •v k2•m2+h2 2 is covered by w m2 2 , we have that the word v 1 •v 3 (m 1 , m 2 )•v k2•m2+h2 2 is also periodic with period p 2 = gcd(|v 2 |, |w 2 |).
Symmetrically, by fixing m 2 large enough and letting m 1 grow, we get that the word v h1•m1+h1

1 •v 3 (m 1 , m 2 )•v 2 is periodic with period p 1 = gcd(|v 1 |, |w 1 |).
We can summarize the previous results as follows:

v(m 1 , m 2 ) = period p1 v k1•m1+h1-1 1 • period p2 v 1 • v 3 (m 1 , m 2 ) • v 2 • v k2•m2+h2-1 2 .
Finally, we observe that the words v h1•m1+h1

1 •v 3 (m 1 , m 2 )•v 2 and v 1 •v 3 (m 1 , m 2 )•v k2•m2+h2 2 share the factor v 1 • v 3 (m 1 , m 2 ) • v 2 of length at least |v 1 | + |v 2 |.
Hence, by applying the second claim of Lemma 8, we conclude that the word v(m 1 , m 2 ) is periodic with period gcd(|v 1 |, |v 2 |).

Lemma 10. If two locations ≤

of ρ belong to the same non-singleton equivalence class of , then there is a sequence of locations 1 ≤ 3 ≤ 4 ≤ . . . ≤ n-3 ≤ n-2 ≤ n , for some even number n ≥ 4, such that

1 ≤ ≤ 4 and n-3 ≤ ≤ n , ( 1 , 4 ), ( 3 , 6 ), ( 5 , 8 ), . . . , ( n-5 , n-2 ), ( n-3 , n ) are inversions.
For the sake of presentation, in Figure 3 we give an intuitive account of the structure of the series of inversions claimed in the lemma: the thick arrows represent the transitions within the equivalence class and the hatched areas mark the endpoints of the overlapping inversions (for example, ( 1 , 4 ) overlaps with ( 3 , 6 )).

Proof. We will say that an inversion ( 1 , 2 ) covers a location when 1 ≤ ≤ 2 . We prove the lemma by induction on the distance between the two locations and . The basic case is when = . Because belongs to a non-singleton -equivalence class, we know that there is an inversion ( 1 , 4 ) that covers , namely, such that 1 ≤ ≤ 4 . Thus, the claim of the lemma holds by simply letting n = 4.

To prove the induction step, we consider two locations , satisfying the hypothesis of the lemma and being at distance t > 0, and we assume that the claim holds for analogous pairs of locations at distance strictly less than t. As before, because belongs to a nonsingleton -equivalence class, we know that there is an inversion ( 1 , 4 ) that covers . Without loss of generality we can assume that 4 is the greatest location that forms an inversion covering . In particular, we have that < 4 , as otherwise we would have = 4 : the latter equality however is impossible, as all the locations in the equivalence class of would then occur before , thus contradicting > (recall that and are by hypothesis in the same equivalence class of ). If is also covered by ( 1 , 4 ), then we are done, namely, the claim holds for n = 4. Otherwise, we let = 4 and we observe that < is a pair of locations satisfying the hypothesis of the lemma and being at distance strictly less than t. By applying the inductive hypothesis, we derive the existence of a series of inversions of the form ( 3 , 6 ), ( 5 , 8 ), . . . , ( n-5 , n-2 ), ( n-3 , n ), for some n ≥ 4 and some locations 3 ≤ 5 ≤ . . . ≤ n-3 ≤ n-2 ≤ n . By prepending the pair ( 1 , 4 ) to this sequence we get the desired claim. Lemma 11. If S is one-way definable and ≤ are two locations of the run ρ such that , then the output out(ρ[ , ]) produced between and has period at most e S .

Proof. The claim for = holds trivially, so for the rest of the proof we focus only on the case < . By Lemma 10, we know that there is a series of inversions

( 1 , 4 ) ( 3 , 6 ) ( 5 , 8 ) . . . ( n-5 , n-2 ) ( n-3 , n ) for some locations 1 ≤ 3 ≤ 4 ≤ . . . ≤ n-3 ≤ n-2 ≤ n , with 1 ≤ 4 and n-3 ≤ ≤ n .
For each of the above inversions ( i-3 , i ), we denote by L i-3 and L i the two witnessing loops and by p i-3 and p i the lengths of the outputs produced by the intercepted factors ρ | L i-3 / i-3 and ρ | L i / i , respectively. Recall that, by Lemma 6, e S is an upper bound to the lengths p 1 , p 4 , p 3 , p 6 , . . . , p n-5 , p n-2 , p n-3 , p n . Therefore, in order to show that out ρ[ , ] is periodic with period at most e S , it suffices to prove the following claim by induction on i:

Claim. For all i ∈ {4, 6, . . . , n -2, n}, the output out(ρ[ 1 , i ]) produced between 1 and i is periodic with period gcd(p i-3 , p i ).

The base case i = 4 follows immediately from Proposition 7, since ( 1 , 4 ) is an inversion. For the inductive step, we assume that the claim holds for i ≤ n -2 and we prove it for i + 2. First of all, we decompose our word as follows:

out ρ[ 1 , i+2 ] = out ρ[ 1 , i-1 ] out ρ[ i-1 , i ] out ρ[ i , i+2 ] .
We then observe that, by the inductive hypothesis, the output produced between 1 and i has period gcd(p i-3 , p i ). Similarly, because ( i-1 , i+2 ) is an inversion, we know from Proposition 7 that the output produced between i-1 and i+2 has period gcd(p i-1 , p i+2 ). Now, we focus on the output out ρ[ i-1 , i ] . We first verify that ( i-1 , i ) is an inversion. Indeed, we have i-1 ≤ i . Moreover, because ( i-1 , i+2 ) and ( i-3 , i ) are inversions, we know that i-1 is an entry point of L i-1 and i is an exit point of L i . In particular, we have i-1 < i and the x-coordinate of i-1 is greater than that of i . For the same reasons, the intercepted factor ρ | L i-1 / i-1 is captured by L i-1 , but is not captured by any other loop strongly contained in L i-1 . Analogous properties holds for the intercepted factor ρ | L i / i and the loop L i . This proves that ( i-1 , i ) is an inversion. Then, by applying Proposition 7 to this inversion, we get that the the output produced between i-1 and i has period gcd(p i-1 , p i ).

We can summarize the previous results as follows:

out ρ[ 1 , i+2 ] = period pi-3 and pi out ρ[ 1 , i-1 ]
period pi-1 and pi+2

period pi-1 and pi out ρ[ i-1 , i ] out ρ[ i , i+2 ] .
To head towards the conclusion, we observe that the word out ρ[ i-1 , i ] ends with the output produced by the intercepted factor ρ | L i / i , and hence it has length at least p i . Moreover, the same word occurs as a factor of out ρ[

Z = [ 1 , 2 ] \ [x 1 , x 2 ] × [y 1 , y 2 ], has length at most 2(y 2 -y 1 ) • e S .
Suppose, by way of contradiction, that this is not the case, and that out(ρ | Z) > 2(y 2 -y 1 ) • e S . Since the set Z spans across at most y 2 -y 1 levels and does not cover the locations inside the "bounding box" [x 1 , x 2 ] × [y 1 , y 2 ], we could find a factor α that produces an output longer than e S , that lies on a single level y , and either to the left of x 1 or to the right of x 2 .

Suppose that this output is on the left (the right case is symmetric), and that α is a factor on some level y ∈ {y 1 + 1, . . . , y 2 } that is intercepted by the interval I = [1, x 1 ] and that produces an output of length strictly greater than e S . By the contrapositive of Lemma 6, the factor α is captured by some loop L = [x 1 , x 2 ] that is strongly contained in I = [1, x 1 ], namely, such that 1 ≤ x 1 < x 2 < x 1 . Let = (x , y ) be the exit point of L , where x = x 1 or x = x 2 depending on whether y is odd or even. Recall that, by the definition of [K], there is also a location = (x, y) that strictly precedes along the run and that belongs to H. This implies that forms an inversion with another location and, without loss of generality, we can assume that is the first element of this inversion. Moreover, recall that x 1 ≤ x ≤ x 2 < x 1 and x 1 ≤ x ≤ x 2 , namely, is strictly to the left of according to the ordering of the x-coordinates. This shows that ( , ) is also an inversion, and hence also belongs to H. However, this contradicts the definition of x 1 as the minimum of the x-coordinates of the locations in H. A similar contradiction can be obtained in the case where the factor that produces an output of length strictly greater than e S lies at the right of x 2 .

By the above arguments, we know that out(ρ

| Z)| ≤ 2(y 2 -y 1 ) • e S , where Z = [ 1 , 2 ] \ [x 1 , x 2 ] × [y 1 , y 2 ]
, namely, that the fourth condition of the definition of ramp is satisfied.

It remains to verify the five condition, that the output produced by ρ[ 1 , 2 ] is almost periodic with bound 2 • e S . Let 1 and 2 be the first and the last locations of the equivalence class K (note that 1 ≤ 1 ≤ 2 ≤ 2 ). Recall that Lemma 11 already shows that the output produced between 1 and 2 is periodic with period at most e S . Thus, we just need to show that the prefix out(ρ[ 1 , 1 ]) and the suffix out(ρ[ 2 , 2 ]) have length at most 2 • e S .

Suppose that the length of out(ρ[ 1 , 1 ]) exceeds 2 • e S . By the definition of [K], the two locations 1 and 1 would be either on the same level, i.e. y 1 , or on adjacent levels, i.e. y 1 and y 1 + 1. In the following, we show that none of these cases can happen, thus reaching a contradiction from the assumption out(ρ[ 1 , 1 ]) > 2 • e S . If 1 were on the same level as 1 , then clearly the factor out(ρ[ 1 , 1 ]) would lie on a single level and to the right of x 1 , and would produce an output longer than e S . Then, by using the contrapositive of Lemma 6, we could find a loop L = [x 1 , x 2 ] strongly contained in the interval I = [x 1 , n], where n is the rightmost position of the input, that captures the factor out(ρ[ 1 , 1 ]) with non-empty output. We recall that 1 is the first location of the -equivalence class K, and hence there is an inversion ( 1 , ), for some location that follows 1 along the run. We then define = (x 1 , y 1 ) and we observe that this location is an entry point of L and it strictly precedes . We thus get that ( , ) is also an inversion. This, however, is a contradiction because the inversion ( , ) intersects the -equivalence class K, without being contained in it. Let us now consider the second case, where 1 is on level y 1 and 1 is on level y 1 + 1. Since ρ[ 1 , 1 ] spans across two levels and produces an output longer than 2e S , there is a factor α of out(ρ[ 1 , 1 ]) that lies entirely on a single level -either y 1 or y 1 + 1 -and to the right of x 1 , and produces an output longer than e S . Then, by reasoning as in the previous case, we can get a contradiction by finding an inversion ( , ) that intersects K without being contained in it.

We have just shown that out(ρ[ 1 , 1 ]) ≤ 2 • e S . By using symmetric arguments, we can also prove that out(ρ[ 2 , 2 ]) ≤ 2•e S . Finally, we recall that, by Lemma 11, out(ρ[ 1 , 2 ]) ≤ e S . All together, this shows that the output produced between the locations 1 and 2 is almost periodic with bound 2 • e S , and hence [K] = ( 1 , 2 ) is a ramp. Lemma 14. Let 1 = (x 1 , y 1 ) and 2 = (x 2 , y 2 ) be two consecutive locations of D C . The pair ( 1 , 2 ) is a floor or a ramp, depending on whether y 1 = y 2 or y 1 < y 2 ..

Proof.

Recall that all the locations in D C are on even levels, so the lemma holds in particular for 1 and 2 If y 1 = y 2 , then ( 1 , 2 ) is clearly a floor. So let us assume that y 1 = y 1 . The fact that x 1 ≤ x 2 and y 1 < y 2 holds follows from the arguments given in part of the body that just preceded the lemma. The first three conditions of the definition of ramp are also satisfied because 1 and 2 are consecutive locations in D C .

Below, we verify that the output produced by the factor ρ[ 1 , 2 ] has length at most (y 2 -y 1 + 1) • e S . Note that this will prove both the fourth and the fifth conditions: for f n can be computed by a sweeping transducer of size quadratic in n, f n can be computed by a one-way transducer, any one-way transducer computing f n has at least 2 2 n-1 states.

Z = [ 1 , 2 ] \ [x 1 , x 2 ] × [y 1 , y 2 ],
Proof. In this proof we use the standard binary encodings bin i,n of the natural numbers i ∈ {0, . . . , 2 n -1} (for simplicity, hereafter we write bin i in place of bin i,n ): bin 0 = 0 n , bin 1 = 0 n-1 1, . . . , bin 2 n -1 = 1 n . Formally, bin i is the unique word of length n such that i = n-1 j=0 bin i (n -j) • 2 j . Note that the least significant bit is in the rightmost position. Let f n be the function over the binary alphabet {0, 1} defined as follows. The domain of f n is the set of words of the form

a 0 bin 0 a 1 bin 1 a 2 . . . a 2 n -1 bin 2 n -1 a 2 n
where a i ∈ {0, 1} for all i ∈ {0, . . . , 2 n }. The function f n extracts from the above word the sub-sequence a 0 . . . a 2 n and copies it twice to form the output, namely,

f n a 0 bin 0 a 1 bin 1 a 2 . . . a 2 n -1 bin 2 n -1 a 2 n = w • w where w = a 0 a 1 . . . a 2 n .
We first show that there exists a sweeping transducer S n that computes f n and has size quadratic in n. Then, we prove that there is a one-way transducer computing f n . Finally, we show that every one-way transducer computing f n has at least 2 2 n-1 states.

Let us describe the sweeping transducer S n that computes f n . A first task of the transducer S n is to check that the input contains a sub-sequence of the form bin 0 bin 1 . . . bin 2 n -1 . This can be done with n left-to-right passes, which are of course interleaved by n -1 rightto-left passes. During the j-th left-to-right pass, with j ∈ {1, . . . , n}, the transducer checks the j-th bit of each block bin i , where i ∈ {0, . . . , 2 n -1}. It does so by applying the following rule: if it reads 0 (resp., 1) at position j of bin i and if all bits after position j in bin i are set to 1, then it must read 1 (resp., 0) at position j of bin i+1 . Dually, if some bits after position j in bin i are set to 0, then the bit at position j of bin i must be the same as the bit at position j of bin i+1 . Moreover, the first pass, where j = 1, verifies two additional constraints, namely, that bin 0 = 0 n and that, after reading 1 n (= bin 2 n -1 ), the input contains exactly one letter (this is needed to avoid that the block bin 2 n -1 is followed by a new block bin 0 ). The constraints of a single left-to-right pass can be verified with a number of states that is linear in n. As there are n left-to-right passes, all the checks can be performed with a quadratic number of states. The second task of the transducer aims at producing the correct output, namely, two copies of the sub-sequence a 0 a 1 . . . a 2 n . This can be done easily, for example, during the last two passes. The transducer that we just described is sweeping, input-deterministic, has O(n 2 ) states, and computes the function f n .

Let us now prove the second item, namely that there exists a one-way transducer computing f n . Consider the transducer that performs the two following tasks. The first task is to store the word a 0 . . . a 2 n (which size only depends on n) in order to output it twice at the end. The second task is to check that the sub-sequence bin 0 . . . bin 2 n -1 is correct. This can be done by storing bin j-1 and bin j when bin j is being read and checking that they encode successive integers (this is regular). It requires to store two words of length n in the state. The transducer also checks that bin 0 follows a 0 and that a 2 n is the last letter (at that point bin 2 n -1 is stored in the state). This transducer is one-way and computes f n .

We now prove the claim in the third item. Consider a one-way transducer T n that computes the function f n and suppose, by way of contradiction, that T n has less than 2 2 n-1 states. Let w 1 , . . . , w N be an enumeration of all the words over {0, 1} of length 2 n + 1, where N = 2 2 n +1 . For all i ≤ N , let ρ i be a successful run of T that produces w i • w i as output (the corresponding input can be obtained from w i by inserting bin j immediately before each position j). We defineρ i to be the maximal prefix of ρ i that produces a prefix of w i as output. We also define (p i , v i , q i ) to be the transition that immediately followsρ i in the run ρ i , andρ i to be the remaining part of the run. We finally denote byw i (resp.,w i ) the output produced byρ i (resp.,ρ i ). To sum up, we have:

ρ i = -ρ i (p i , a i , v i , q i ) -ρ i w i • w i = -w i • v i • -w i .
Now, consider the transitions (p i , a i , v i , q i ) that we just defined. Note that the corresponding triples (p i , a i , q i ) range over the finite set Q × {0, 1} × Q, which has size smaller than 2 • 2 2 n-1 2 = 2 2 n +1 = N . Thus, there must exist two distinct indices i, j ≤ N such that (p i , a i , q i ) = (p j , a j , q j ).

Since p i = p j , the sequencesρ i andρ j end with the same state and hence we can replace ρ j withρ i inside the run ρ j . This results in the successful runρ i (p j , a j , v j , q j )ρ j that produces the outputw i • v j •w j . Moreover, because every output produced by T n must be of the form w k • w k , for some 1 ≤ k ≤ N , and because v j •w j contains w j as a suffix, we can write

-w i • v j • -w j = w j • w j = -w j • v j • -w j .
From the above equation we immediately derivew i =w j .

As concerns the pieces v i and v j , we observe the following. By construction,w i •v i (resp., w j • v j ) contains w i (resp., w j ) as a prefix. Thus, since w i = w j andw i =w j , we have that v i = v j . We also know that (p i , a i , q i ) = (p j , a j , q j ). In particular, substituting in the run ρ i the transition (p i , a i , v i , q i ) with the transition (p j , a j , v j , q j ) would result in a new successful run on the same input w i • w i that produces the outputw i • v j •w i . However, since the latter output is different from w i • w i , this is in contradiction with the functionality of T n . We must conclude that every one-way transducer that computes f n has at least 2 2 n-1 states.

Proposition 16. The problem of testing whether a sweeping non-functional transducer is one-way definable is undecidable.

Proof. The proof uses some ideas and variants of constructions provided in [START_REF] Ibarra | unsolvability of the equivalence problem for epsilon-free NGSM's with unary input (output) alphabet and applications[END_REF], concerning the proof of undecidability of the equivalence problem for one-way non-functional transducers.

We show a reduction from the Post Correspondence Problem (PCP). A PCP instance is described by two finite alphabets Σ and ∆ and two morphisms f, g : Σ * → ∆ * . A solution of such an instance is any non-empty word w ∈ Σ + such that f (w) = g(w). We recall that the problem of testing whether a PCP instance has a solution is undecidable.

Below, we fix a tuple τ = (Σ, ∆, f, g) describing a PCP instance and we show how to reduce the problem of testing the non-existence of solutions of τ to the problem of deciding one-way definability of a relation computed by a sweeping transducer. Roughly, the idea is to construct a relation B τ between words over a suitable alphabet Γ that encodes all the non-solutions to the PCP instance τ (this is simpler than encoding solutions because the presence of errors can be easily checked). The goal is to have a relation B τ that (i) can be computed by a sweeping transducer and (ii) coincides with a trivial one-way definable relation when τ has no solution.

We begin by describing the encodings for the solutions of the PCP instance. We assume that the two alphabets of the PCP instance, Σ and ∆, are disjoint and we use a fresh symbol # ∈ Σ ∪ ∆. We define the new alphabet Γ = Σ ∪ ∆ ∪ {#} that will serve both as input alphabet and as output alphabet for the transduction. We call encoding any pair of words over Γ of the form (w • u, w • v), where w ∈ Σ + , u ∈ ∆ * , and v ∈ {#} * . We will write the encodings as vectors to improve readability, e.g., as

w • u w • v .
We denote by E τ the set of all encodings and we observe that E τ is computable by a one-way transducer (note that this transducer needs ε-transitions). We then restrict our attention to the pairs in E τ that are encodings of valid solutions of the PCP instance. Formally, we call good encodings the pairs in E τ of the form w • u w • # |u| where u = f (w) = g(w) .

All the other pairs in E τ are called bad encodings. Of course, the relation that contains the good encodings is not computable by any transducer. On the other hand, we can show that the complement of this relation w.r.t. E τ is computable by a sweeping transducer. Let B τ be the set of all bad encodings. Consider (w • u, w • # m ) ∈ E τ , with w ∈ Σ + , u ∈ ∆ * , and m ∈ N, and we observe that this pair belongs to B τ if and only if one of the following conditions is satisfied:

1. m < |u|, 2. m > |u|,
1 ≤ n 1 ≤ |Q|. We claim that the output produced by the factor ρn,m must coincide with the consumed part w n1 of the input. Indeed, if this were not the case, then deleting the factor ρn,m from ρ n,m would result in a new successful run that reads w n-n1 • u m and produces w n-n2 • # m•|u| as output, for some n 2 = n 1 . This however would contradict the fact that, by definition of encoding, the possible outputs produced by T on input w n-n1 • u m must agree on the prefix w n-n1 . We also remark that, even if we do not annotate this explicitly, the number n 1 depends on the choice of the pair (n, m) ∈ I. This number, however, range over the fixed finite set J = 1, |Q| .

We can now pump the factor ρn,m of the run ρ n,m any arbitrary number of times. In this way, we obtain new successful runs of T that consume inputs of the form w n+k•n1 • u m and produce outputs of the form w n+k•n1 • # m , for all k ∈ N. In particular, we know that B τ contains all pairs of the form α n+k•n1,m . Summing up, we can claim the following:

Claim. There is a function h : I → J such that, for all pairs (n, m) ∈ I,

(n + k • h(n, m), m) k ∈ N ⊆ I .
We can now head towards a contradiction. Let ñ be the maximum common multiple of the numbers h(n, m), for all (n, m) ∈ I. Let m = n + ñ and observe that n = m, whence (n, m) ∈ I. Since ñ is a multiple of h(n, m), we derive from the above claim that the pair (n + ñ, m) = (m, m) also belongs to I. However, this contradicts the definition of I, since we observed earlier that α n,m is a bad encoding if and only if n = m. We conclude that B τ is not one-way definable when τ has a solution.

2 R 3 Figure 1

 231 Figure 1 Decomposition of a run into floors and ramps.

1 2

 1 As shown by the figure to the right, this sub-sequence (represented by bold arrows) can be obtained from the factor ρ[ 1 , 2 ] by removing the factors intercepted by [x 1 , x 2 ]

2

  has period gcd(|v 2 |, |w 2 |). A last application of Fine and Wilf's theorem (Lemma 8) gives the desired periodicity.

2 , 2 .m2 2 and v k2•m2+h2 2 are

 2222 and in particular an arbitrarily long infix of v k2•m2+h2 Hence, by Fine-Wilf's Theorem (first claim of Lemma 8), the words w periodic with period p 2 = gcd(|v 2 |, |w 2 |). Moreover, because an arbitrary long prefix of v 1 •v

Figure 3 A

 3 Figure 3 A-equivalence class seen as a series of overlapping inversions.

  1 , i-1 ] out ρ[ i-1 , i ] .Hence, by Lemma 8, the two words out ρ[ i-1 , i ] and out ρ[1 , i-1 ] out ρ[ i-1 , i ] have period gcd(p i-3 , p i-1 , p i ).In a similar way, by observing that out ρ[ i-1 , i ] has length at least p i-1 and occurs as a factor of out ρ[ i-1 , i ] out ρ[ i , i+2 ] , we derive that out ρ[ i-1 , i ] and out ρ[ i-1 , i ] out ρ[ i , i+2 ] have period gcd(p i-3 , p i-1 , p i , p i+2 ).A third application of Lemma 8 allows us to conclude that the entire word out ρ[ 1 , i+2 ] has period gcd(p i-3 , p i-1 , p i , p i+2 ), which clearly divides gcd(p i-1 , p i+2 ). This proves the inductive step of the claim.Finally, we recall that the lemma follows from the above claim and from Lemma 6 by letting i = n (note that out ρ[ , ] is a factor of out ρ[ 1 , n ] ). Let H be the subset of K that contains all the locations , ∈ K forming an inversion ( , ). Recall from Definition 12 that we have [K] = ( 1 , 2 ), where 1 = (x 1 , y 1 ),2 = (x 2 , y 2 ), x 1 = min{x | (x, y) ∈ H}, x 2 = max{x | (x,y) ∈ H}, and y 1 (resp., y 2 ) is the even number among min{y | (x, y) ∈ H} and min{y | (x, y) ∈ H} -1 (resp., among max{y | (x, y) ∈ H} and max{y | (x, y) ∈ H} + 1). We verify that [K] = ( 1 , 2 ) satisfies all the conditions of the definition of ramp.Clearly, we have x 1 ≤ x 2 , y 1 < y 2 , and both y 1 and y 2 are even. We now prove that the output produce by the sub-sequence ρ | Z, where

	Lemma 13. If K is a non-singleton	-equivalence class, then [K] is a ramp.
	Proof.

  the sub-sequence ρ | Z produces an output that is clearly shorter than that of ρ[ 1 , 2 ], and in addition we have (y 2 -y 1 + 1) < 2(y 2 -y 1 ).Suppose, by way of contradiction, that out(ρ[ 1 , 2 ]) > (y 2 -y 1 + 1) • e S . Since between 1 and 2 there are y 2 -y 1 + 1 levels, there is a factor α of ρ[ 1 , 2 ] that produces an output longer than e S and that lies on a single level y, for some y 1 ≤ y ≤ y 2 . The contrapositive of Lemma 6 implies that the factor α is captured by some loopL = [x 1 , x 2 ] such that x 1 > x 1 if y = y 1 , and x 2 < y 2 if y = y 2 .In particular, the location = (x 1 , y) is an entry point of L and it belongs to D C . We have just shown that there is ∈ D C such that 1 < < 2 . However, this contradicts the hypothesis that 1 and 2 were consecutive locations in D C . We must conclude that the output produced by the infix ρ[ 1 , 2 ] has length at most (y 2 -y 1 + 1) • e S , and hence ( 1 , 2 ) is a ramp. There is a family (f n ) n of functions from {0, 1} * to {0, 1} * such that:

	Proposition 15.

This work was partially supported by the ExStream project (ANR-13-JS02-0010) and the Technische Universität München -Institute for Advanced Study, funded by the German Excellence Initiative and the European Union Seventh Framework Programme under grant agreement n°291763.

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

One-way definability of sweeping transducers 3. u = f (w), 4. u = g(w). We explain how to construct a sweeping transducer S τ that computes B τ . Essentially, S τ guesses which of the above conditions holds and processes the input accordingly. More precisely, if S τ guesses that the first condition holds, then it performs a single left-to-right pass, first copying the prefix w to the output and then producing a block of occurrences of the symbol # that is shorter than the suffix u. This task can be easily performed while reading u: it suffices to emit at most one occurrence of # for each position in u, and at the same time guarantee that, for at least one such position, no occurrence of # is emitted. The second condition can be dealt with by a similar strategy: first copy the prefix w, then output a block of # that is longer than the suffix u. To deal with the third condition, the transducer S τ has to perform two left-to-right passes, interleaved by a backward pass that brings the head back to the initial position. During the first left-to-right pass, S τ copies the prefix w to the output. During the second left-to-right pass, it reads again the prefix w, but this time he guesses a factorization of it of the form w 1 a w 2 . On reading w 1 , S τ will output # |f (w1)| . After reading w 1 , S τ will store the symbol a and move to the position where the suffix u begins. From there, it will guess a factorization of u of the form u 1 u 2 , check that u 2 does not begin with f (a), and emit one occurrence of # for each position in u 2 . Note that the described behaviour does not immediately guarantee that u = f (w). Indeed, it may still happen that u = f (w), but in this case the length of u will not match the number m of occurrences of # produced in output. However, this case is already covered by the first and second condition, so the computation is still correct in the sense that it produces only bad encodings. On the other hand, if the number m of occurrences of # produced in output happens to be the same as u, then the computation of S τ guarantees that u = f (w). A similar behaviour can be used to deal with the fourth condition.

We have just shown that there is a sweeping non-functional transducer S τ that computes the relation B τ containing all the bad encodings. Note that, if the PCP instance τ admits no solution, then all encodings are bad, i.e., B τ = E τ , and hence B τ is one-way definable. It remains to show that when τ has a solution, B τ is not one-way definable. Suppose that τ has solution w ∈ Σ * and let w • u, w • # |u| be the corresponding good encoding, where u = f (w) = g(w). Note that every exact repetition of w is also a solution, and hence the pairs w n • u n , w n • # n•|u| are also good encodings, for all n ≥ 1.

Suppose, by way of contradiction, that there is a one-way transducer T that computes the relation B τ . For every n, m ∈ N, we define the encoding

and we observe that α n,m ∈ B τ if and only if n = m (recall that w is the solution of the PCP instance τ and u = f (w) = g(w)). Below, we consider bad encodings like the above ones, where the parameter n is supposed to be large enough. Formally, we define the set I of all pairs of indices (n, m) ∈ N 2 such that (i) n = m (this guarantees that α n,m ∈ B τ ) and (ii) n is larger than the number |Q| of states of T . We consider some pair (n, m) ∈ I and we choose a successful run ρ n,m of T that witnesses the membership of α n,m in B τ , namely, that reads the input w n •u m and produces the output w n • # m•|u| . We can split the run ρ n,m into a prefixρ n,m and a suffixρ n,m in such a way thatρ n,m consumes the prefix w n andρ n,m consumes the remaining suffix u m . Since n is larger than the number of state of T , we can find a factor ρn,m ofρ n,m that starts and ends with the same state and consumes a non-empty exact repetition of w, say w n1 , for some