Emmanuel Filiot
email: efiliot@ulb.ac.be

Olivier Gauwin
email: olivier.gauwin@labri.fr

Nathan Lhote
email: nlhote@labri.fr

First-order definability of rational transductions: An algebraic approach *

Keywords: F.4.2 [Mathematical Logic and Formal Languages]: Formal Languages rational word transductions, definability problems, first-order logic, algebraic characterizations

The algebraic theory of rational languages has provided powerful decidability results. Among them, one of the most fundamental is the definability of a rational language in the class of aperiodic languages, i.e., languages recognized by finite automata whose transition relation defines an aperiodic congruence. An important corollary of this result is the first-order definability of monadic second-order formulas over finite words.

Our goal is to extend these results to rational transductions, i.e. word functions realized by finite transducers. We take an algebraic approach and consider definability problems of rational transductions in a given variety of congruences (or monoids).

The strength of the algebraic theory of rational languages relies on the existence of a congruence canonically attached to every language, the syntactic congruence. In a similar spirit, Reutenauer and Schützenberger have defined a canonical device for rational transductions, that we extend to establish our main contribution: an effective characterization of V-transductions, i.e. rational transductions realizable by transducers whose transition relation defines a congruence in a (decidable) variety V. In particular, it provides an algorithm to decide the definability of a rational transduction by an aperiodic finite transducer.

Using those results, we show that the FO-definability of a rational transduction is decidable, where FO-definable means definable in a first-order restriction of logical transducers à la Courcelle.

Introduction

A key aspect of formal language theory is the relationship between logic, automata and algebra, established on a number of structures Rational languages Rational languages of finite words form a robust class that enjoys computational, logical and algebraic characterizations. They correspond for instance to languages defined by finite automata, monadic second-order logic (MSO), and finite monoids. These powerful connections have also been established for subclasses of rational languages: at the computational level, by imposing structural restrictions on finite automata, at the logical level, by putting restrictions on the use of quantifiers and predicates e.g., and at the algebraic level, by considering varieties (sometimes called pseudo-varieties) of finite monoids. Most notably, first-order definable languages are known to correspond to languages defined by counter-free automata, and to languages recognized by aperiodic finite monoids (see (Diekert and Gastin 2008) for a survey on first-order definable languages). More generally, a whole theory relating monoid varieties and logical fragments has been established in [START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF]. There is a tight correspondence between the notions of recognizability by monoid and recognizability by congruence, through their quotient. In this paper, for convenience, we choose the congruence view. Roughly speaking, a congruence variety is a class of congruences of finite index with reasonable closure properties: e.g. the classes of congruences of finite index, aperiodic congruences, commutative congruences are congruence varieties.

A powerful tool in this context is the existence of a canonical minimal deterministic automaton for each rational language, whose states are equivalence classes of the so called right syntactic congruence (or Myhill-Nerode congruence), a congruence canonically attached to each language. The right syntactic congruence ∼L of a language L has a strong property with respect to varieties V: If L is recognized by some V-automaton, i.e. a finite automaton whose transition relation defines a congruence in V, called the transition congruence, then ∼L belongs to V. In other words, the minimal deterministic automaton that recognizes L is a V-automaton. This well-known result provides a way to decide whether an automaton A is equivalent to some V-automaton, as long as V is a decidable variety, i.e. a variety with decidable membership problem. It suffices to construct the minimal deterministic automaton for the language recognized by A and check whether its transition congruence belongs to V. As an application, it yields for instance the decidability of FO in MSO on finite words: given an MSO sentence ϕ, it is decidable whether ϕ is equivalent to some FO formula. More generally, fragments of MSO that are characterized by decidable varieties have, through automata minimization, a decidable definability problem in MSO [START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF].

Our goal is to extend these decidability results, considered as jewels of theoretical computer science, to rational transductions. Rational transductions Transductions are functions from (finite) words to words. Rational transductions are the transductions realized by finite state transducers, i.e. automata extended with outputs. Figure 1 depicts three examples of transducers. Initial states are states with source-free incoming arrow, and final states are states with a target-free outgoing arrow. In transducer 1(a), both p0 and p1 are final but only p0 is initial. When reading a sequence of a, the left transducer outputs a half the time, and the empty word the other half. This transducer maps any word of the form a n to a n2 , for all n ≥ 0. Transducer 1(b) simply realizes the identity function on a n for all n ≥ 0, and transducer 1(c) maps any word of the form (ab) n to (aab) n , and the transduction is undefined for other input words.

Transition congruence of a transducer To define the transition congruence ≈T of a transducer T over an alphabet Σ, one only considers the input symbols: it is the transition congruence of its underlying input automaton (obtained by erasing the output). Informally, a word u defines a binary relation on the states of T -(p, q) are in the relation if there is a run from p to q on uand two words are equivalent if they define the same relation. For the transducer 1(a), e.g., the word a is equivalent to aaa: both send state p0 to p1 and state p1 to p0. There are in fact two equivalence classes, that of (equal to { , aa, a 4 , . . . }) and that of a (equal to {a, a 3 , a 5 , . . . }).

Contributions A transducer is aperiodic if its transition congruence ≈T is aperiodic, i.e. u n ≈T u n+1 for all words u ∈ Σ * and all n larger than some bound that depends only on T . Transducer 1(c) is aperiodic, but not transducers 1(a) and 1(b).

Despite their non-aperiodicity, are transducers 1(a) and 1(b) equivalent to some aperiodic transducer? In this paper, one objective is to automatize this question, for the class of aperiodic congruences but more generally for any decidable variety V of congruences. Due to non-determinism, an input word can have possibly many output words by a transducer. In this paper, we consider the class of unambiguous transducers, which defines exactly the class of rational transductions [START_REF] Eilenberg | Automata, Languages, and Machines[END_REF]. In other words, one wants to decide whether a rational function, given by a transducer, realizes a V-transduction, i.e. a transduction definable by some unambiguous transducer whose transition congruence belongs to V (we call it a V-transducer). As our first main result, we answer this question positively: Theorem 1. Let V be a decidable variety. It is decidable whether a given transducer realizes a V-transduction.

While it is clear that transducer 1(b) is equivalent to a single state aperiodic transducer, it turns out that transducer 1(a) is not, although its domain, the set of words of the form a n for all n ≥ 0, is an aperiodic language. As a matter of facts, the tools needed to prove Theorem 1 are not simple extensions of what is known from the theory of languages. In general, there is no minimal transducer for rational transductions. However, for a subclass of transductions, the sequential transductions, minimization exists.

Sequential transductions are the rational transductions realized by sequential transducers, the subclass of transducers whose underlying input automaton is deterministic. There exists a minimal sequential transducer for any sequential transduction f [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF], based on a congruence relation introduced by Choffrut, that takes into account the output words. We show that this congruence belongs to a variety V if and only if f is realized by a sequential V-transducer.

For rational transductions in general, there is no unique minimal transducer. However, canonicity is available for another device, bimachines [START_REF] Schützenberger | A remark on finite transducers[END_REF][START_REF] Eilenberg | Automata, Languages, and Machines[END_REF]. Roughly speaking, a bimachine is a sequential transducer with a deterministic regular look-ahead. It consists of a left deterministic automaton, reading words from left to right, and a deterministic right automaton (the look-ahead), reading words from right to left. The output words are then computed based on the information given by the two automata. If both the left and right automata are V-automata, then the bimachine they define is called a V-bimachine. Given a rational function f , represented as a transducer, [START_REF] Reutenauer | Minimization of rational word functions[END_REF] have shown how to compute a canonical bimachine for f . Unfortunately, even if f is V-rational, this canonical bimachine may not be a V-bimachine. However, we show how to canonically attach to f a finite and computable set of bimachines, among which one is a V-bimachine iff f is a V-transduction. This addresses the conjecture stated in [START_REF] Reutenauer | Minimization of rational word functions[END_REF], Section 5.3, that "there are only a finite number of minimal bimachines computing (a function) α".

On the logical side, we take Courcelle's logical transducers as a formalism to define word transductions [START_REF] Courcelle | Monadic second-order definable graph transductions: A survey[END_REF], based on first-order logic over the predicates for labels, and the natural order between positions. Intuitively, an FO-transducer is a finite set of FO formulas that define the predicates of the output word, interpreted on a bounded number of copies of the input word structure. If one takes MSO instead of FO, it is known that MSO-transducers correspond to transductions definable with deterministic two-way transducers [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF], and therefore are much beyond the expressiveness of rational transductions. They can for instance copy the input word, or swap unbounded subwords of it. To capture rational transductions, MSO-transducers have been restricted to their order-preserving variant [START_REF] Bojanczyk | Transducers with origin information[END_REF][START_REF] Filiot | Logic-automata connections for transformations[END_REF]. We consider the same restriction on FO-transducers, that we call FOop-transducers. We show that aperiodic transductions are exactly the transductions realized by FOop-transducers, and, as a consequence of Theorem 1, we obtain our second result: Theorem 2. It is decidable whether a rational transduction (as a finite transducer) is FOop-definable.

Related work

In [START_REF] Schützenberger | On finite monoids having only trivial subgroups[END_REF], Schützenberger proved that languages definable by an aperiodic deterministic finite-state automaton are exactly star-free languages (see [START_REF] Diekert | Omega-rational expressions with bounded synchronization delay[END_REF] for a simplified version). Star-free languages were proved to be captured by first-order logic (with the order predicate) in [START_REF] Mcnaughton | Counter-free automata[END_REF]. This provides a way to decide first-order definability of a regular language, through aperiodicity (see e.g. (Diekert and Gastin 2008)).

For word functions, a recent work [START_REF] Cadilhac | A circuit complexity approach to transductions[END_REF] shows that it is decidable whether a deterministic rational transduction is definable in the circuit class AC 0 (resp. ACC 0 ), also using an algebraic approach. Other results relate transduction classes, but without definability procedures. We briefly present some of them, and refer the reader to [START_REF] Filiot | Logic-automata connections for transformations[END_REF] for a more complete picture.

One of these relations has been established in [START_REF] Lautemann | The descriptive complexity approach to LOGCFL[END_REF]): Aperiodic functional non-deterministic length-preserving transducers capture length-preserving FO-transducers. Here, aperiodicity of a non-deterministic transducer is defined as the aperiod-icity of the deterministic automaton obtained after subset construction on the input automaton of the transducer. In [START_REF] Mckenzie | The many faces of a translation[END_REF] this result is generalized to group varieties (beyond aperiodic monoids), and also to two-way transducers and bimachines, but always on length-preserving functions.

Streaming string transducers and two-way transducers both capture MSO-transducers. Aperiodic streaming string transducers capture FO-translations [START_REF] Filiot | First-order definable string transformations[END_REF], where aperiodicity applies on the transition monoid and the variable dependencies. Aperiodic two-way transducers also capture FO-transducers [START_REF] Carton | Aperiodic two-way transducers and FOtransductions[END_REF]. Here aperiodicity only applies to the transition monoid.

Another non-effective characterization of aperiodic rational transductions is established in [START_REF] Reutenauer | Variétés et fonctions rationnelles[END_REF], by relating the period of any rational language with the period of its inverse image by the transduction.

Organization Section 2 gathers the definitions of languages, transductions and related concepts used in this paper. Section 3 is devoted to algebraic characterizations of transductions, and Section 4 to applications in logics. Hence Theorem 1 is proved in Section 3, and Theorem 2 in Section 4. Finally, Section 5 contains discussions on these results and related open problems.

Rational languages and transductions

Rational languages

Words and languages An alphabet Σ is a finite set. A word over Σ is an element of the free monoid Σ * . We denote by the empty word. For w ∈ Σ * , |w| denotes its length. In particular | | = 0. The set of positions of w is pos(w) = {1, . . . , |w|}, and in particular, pos( ) = ∅. For a word w and i, j ∈ pos(w) such that i ≤ j, w[i] denotes the i-th letter of w, w[i:j] the factor of w from position i to position j (both included), and we set w[:i] = w[1:i] and w[i:] = w[i:|w|]. The prefix order on words is defined by u v if u = , or u = v[:i] for some i ∈ pos(v) (if it exists). If u v, we denote by u -1 v the word v such that v = uv . By u ∧ v we denote the longest common prefix of any two words u and v, and by u, v the value |u| + |v| -2|u ∧ v|. It is well-known that ., . defines a distance. Finally, a language L ⊆ Σ * is a set of words, and the prefix of L is the set P (L) of all prefixes of words of L.

Finite automata A finite automaton (or just automaton for short) over an alphabet Σ is a tuple A = (Q, I, F, ∆) where Q is a finite set of states, I ⊆ Q (resp. F ⊆ Q) is a set of initial (resp. final) states, and ∆ ⊆ Q × Σ × Q is a transition relation. A is deterministic if I is a singleton and for any two rules (p, σ, q1), (p, σ, q2) ∈ ∆, it holds that q1 = q2. A run r of an automaton A = (Q, I, F, ∆) on a word w ∈ Σ * of length n is a word r = q0 . . . qn over Q such that (qi, w[i+1], qi+1) ∈ ∆ for all i ∈ {0, . . . , n-1}. It is accepting if q0 ∈ I and qn ∈ F . A word w is accepted by A if there exists an accepting run of A over it. The language recognized by A is the set A of words accepted by A. We often write p w -→A q (or simply p w -→ q) whenever there exists a run r on w such that r[1] = p and r[|r|] = q. A state q is accessible if there is a word w and an initial state q0 such that q0 w -→ q, and an automaton is accessible if all its states are accessible. If for any word there exists at most one accepting run on A, we say that A is unambiguous. Finally, the class of rational languages over Σ is defined as the class of languages recognized by finite automata.

Congruences and recognizability Let Σ be an alphabet and let ∼ be an equivalence relation on Σ * . We say that ∼ is a right congruence if it satisfies u ∼ v ⇒ uσ ∼ vσ for all u, v ∈ Σ * , σ ∈ Σ. Symmetrically we define a left congruence (u ∼ v ⇒ σu ∼ σv), and a congruence is defined as both a left and a right congruence. For u ∈ Σ * , we denote by [u]∼ (or [u] if clear from the context) its equivalence class, and by Σ * /∼ the quotient of Σ * by ∼, i.e. Σ * /∼ = {[u]∼ | u ∈ Σ * }. We say that ∼ has finite index if Σ * /∼ is finite. Concatenation naturally extends to congruence classes as follows: for all u, v ∈ Σ * , [u]∼[v]∼ = [uv]∼. Since ∼ is a congruence, the latter is well-defined as it does not depend on the choices of u and v. With this operation, Σ * /∼ forms a monoid whose neutral element is [ ]∼.

Central examples of congruences in this paper are the syntactic congruence ≡L of a language L and the transition congruence ≈A of an automaton A, defined as follows:

u ≡L v ⇔ (∀x, y ∈ Σ * , xuy ∈ L ⇔ xvy ∈ L) u ≈A v ⇔ (∀p, q ∈ Q, p u -→A q ⇔ p v -→A q)
We say that a language L is recognized by a congruence ∼ if there exists

P ⊆ Σ * /∼ such that L = {u ∈ Σ * | [u] ∈ P }.
For example, by taking P = L/≡ L , one can see that L is recognized by ≡L. It is also well-known that a language L is rational iff it is recognized by a congruence of finite index.

Another useful example is the right transition congruence ∼A of a deterministic automaton A, defined as follows:

u ∼A v ⇔ (∀q ∈ Q, q0 u -→A q ⇔ q0 v -→A q)
Let ∼1 and ∼2 be two equivalence relations on Σ * . We say that ∼1 is finer than ∼2, or that ∼2 is coarser than ∼1, denoted by ∼1

∼2 if for all u, v ∈ Σ * we have u ∼1 v ⇒ u ∼2 v. For instance, ≡L is the coarsest congruence recognizing L, for any language L. If ∼1 and ∼2 are congruences of finite index then ∼1 ∼2 (seen as the set intersection) is a congruence of finite index, finer than both ∼1 and ∼2. Let A1 and A2 be two deterministic automata, we will say by extension that A1 is finer than A2 if we have ∼A 1 finer than ∼A 2 , and we write A1 A2. We consider right congruences because they are naturally equivalent to (accessible) deterministic automata.

Algebraic characterization of classes of regular languages

Congruence varieties We say that a set V of congruences of finite index is a congruence variety (variety for short) if it is closed under intersection of congruences (on the same alphabet) and the taking of coarser congruences. Let V be a variety and let Σ be an alphabet. An automaton with transition letters in Σ is a Vautomaton if its transition congruence is in V. A language over Σ is a V-language if it is recognized by a V-automaton. Since a variety is stable by taking coarser congruences, a language is a Vlanguage if and only if its syntactic congruence is in V. We denote by L(V) the set of V-languages. Remark 1. The notion of recognizability by a congruence of finite index ∼ is equivalent to the already studied notion of recognizability by a stamp (i.e. a morphism from a free monoid to a finite monoid) ϕ : Σ * → M by setting u ∼ v iff ϕ(u) = ϕ(v) for one direction, and by taking M = Σ * /∼ and ϕ : u → [u]∼ for the other direction. In this paper we have chosen the congruence approach for simplicity reasons. Furthermore, the notion of congruence variety we define here is more general than the one of C-variety of [START_REF] Pin | Some results on C-varieties[END_REF], indeed a C-variety of stamps is in particular a congruence variety. We make this choice simply because our results still hold in this more general framework.

Definability problem Given a class of languages Λ, the Λdefinability problem asks, given an automaton recognizing a language L whether L ∈ Λ.

Decidable variety Let Σ be an alphabet. A congruence of finite index over Σ can be given as a morphism ϕ : Σ * → M , with M a finite monoid, by taking u ∼ v iff ϕ(u) = ϕ(v). The morphism ϕ can itself be given explicitly by a function φ : Σ → M . Let V be a variety. The membership problem for V asks, for a congruence of finite index, given explicitly, whether it is in V. In particular the L(V)-definability problem reduces to the membership problem for V. We say that V is decidable if its membership problem is decidable. Example 1. Let A denote the variety of aperiodic congruences, i.e. of congruences ∼ verifying: ∃n > 0 ∀w ∈ Σ * w n ∼ w n+1 . This property is stable by intersection and taking coarser congruences hence A is indeed a variety. The A-definability problem is PSPACE-complete [START_REF] Cho | Finite-automaton aperiodicity is pspace-complete[END_REF].

Rational transductions

Transductions A transduction over a finite alphabet Σ is a partial function of Σ * → Σ * . In the literature a transduction is, generally speaking, a binary relation over Σ * , however in this paper we only consider functional relations. We denote by dom(f ) the domain of a transduction f . Finite transducers A finite transducer1 (or just transducer for short) over an alphabet Σ is a tuple

T = (A, o, i , t ) where A = (Q, I, F, ∆) is a finite automaton, o : ∆ → Σ * is the output function, i : I → Σ *
(resp. sequential) if A is unambiguous (resp. deterministic).
In both cases T is a transduction and we denote (u, w) ∈ T by T (u) = w. The class of rational transductions (resp. sequential transductions) is defined as the class of transductions realized by unambiguous (resp. sequential) finite transducers. Remark 2. It is decidable in polynomial time whether a transducer realizes a transduction (i.e. is functional) and in that case there exists an unambiguous transducer realizing the same transduction (see e.g. [START_REF] Berstel | Transductions and context-free languages[END_REF]).

V-transductions Let V be a variety. A finite transducer is called a V-transducer if its automaton is a V-automaton. A transduction is called V-rational (resp. V-sequential) if it is realized by an unambiguous (resp. sequential) V-transducer.

Algebraic characterizations of transductions

In this section we establish algebraic characterizations, for a given variety V, of V-sequential and V-rational transductions based on notions of canonical congruences associated with a given transduction. These characterizations are effective whenever V is decidable.

In the first subsection we show that, for a given variety V, the minimal sequential transducer defined in [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF]) is a Vtransducer if and only if its transduction is definable by a sequential V-transducer, which provides a way to decide if a sequential transducer realizes a V-sequential transduction.

In the other two subsections, we deal with the more difficult case of rational transductions. Refining the methods of [START_REF] Reutenauer | Minimization of rational word functions[END_REF], we obtain this time not one minimal transducer but a finite set of transducers such that, for a given variety V, one of these transducers is a V-transducer if and only if the transduction is realizable by some unambiguous V-transducer.

Thus we obtain a way to decide if a transducer realizes a V-rational transduction, as stated in Theorem 1.

Sequential Transductions

In order to decide if a given rational language belongs to some variety, one only has to consider the syntactic congruence of the language which is coarser than any congruence recognizing the language. In the same spirit, sequential transductions can be minimized by writing the outputs as soon as possible and the resulting minimal transducer has the coarsest congruence of any sequential transducer realizing the transduction. We describe the construction given in [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF] of this minimal transducer and show that its transition congruence is indeed the coarsest. For a proof of correctness of the construction we refer the reader to the original paper.

Minimization Let T = (A, o, i , t ) be a sequential transducer with A = (Q, I, F, ∆), and let f = T . Let us define the transducer T f = (A f , o f , i f , t f ) which depends only on f . The construction of T f is based on a notion of syntactic congruence for f , that we now define. Intuitively, two words u and v are equivalent if they are equivalent for the Myhill-Nerode right congruence of dom(f ), and if for any suffix w such that both uw and vw are in dom(f ), the outputs f (uw) and f (vw) have a common suffix which only depends on w. In other words, the effect of u and v on the translation of w is the same.

Formally, f is defined on P (dom(f )) by:

f (u) = ∧{f (uw) | uw ∈ dom(f )} for u ∈ P (dom(f )). The syntactic congruence of f is denoted by ∼ f and defined as: for u, v ∈ Σ * , u ∼ f v if for all w ∈ Σ * , uw ∈ dom(f ) ⇔ vw ∈ dom(f ) and if u, v ∈ dom( f ), f (u) -1 f (uw) = f (v) -1 f (vw).
Then we define:

• Q f = {[u] | u ∈ dom( f )} • I f = {[ ]} (we assume that the domain of f is non empty) • F f = {[u] | u ∈ dom(f )} • ∆ f = {([u], σ, [uσ]) | uσ ∈ dom( f )} • o f ([u], σ, [uσ]) = f (u) -1 f (uσ) • i f ([ ]) = f (ε) • t f ([u]) = f (u) -1 f (u)
Theorem 3. Let V be a decidable variety. Given a sequential transduction f : Σ * → Σ * (as a transducer T ), it is decidable whether f is V-sequential.

Before proving the theorem we consider the following property.

Proposition 1. Let V be a variety, let A1, A2 be two deterministic automata such that A1 A2 and A2 is accessible. If A1 is a V-automaton, then A2 is a V-automaton.

Proof. Let A1, A2 be two deterministic automata such that A2 is accessible. We only need to show that ≈A 1 ≈A 2 since any variety is stable by the taking of coarser congruences. Let us assume that ∼A 1 ∼A 2 and let u ≈A 1 v. Then, for any word w, we have that wu ∼A 1 wv, hence for any w, wu ∼A 2 wv. Since A2 is accessible, we have that u ≈A 2 v. Hence, if A1 is a V-automaton, then A2 is a V-automaton.

Proof of Theorem 3. Let us show that T f is a V-sequential transducer iff there exists a V-sequential transducer realizing f . This will entail the result because T f is effectively computable from any sequential transducer realizing f [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF]. Let T = (A, o, i , t ) be a V-transducer realizing f . We want to show that A f is a V-automaton, since by definition A f is accessible, it suffices to show according to Proposition 1 that A A f . Let u ∼A v and let us show that u ∼ f v. Let w be a word such that p u -→A q w -→A r such that p ∈ I, r ∈ F . This implies that p v -→A q w -→A r. Hence we have that for all w ∈ Σ * , uw ∈ dom(f

) ⇔ vw ∈ dom(f ). Let 0 1 2 a | a | a a | a | Figure 2. I-transducer.
w be a word such that p u|x --→ q w|y --→ r and p v|x --→ q w|y --→ r with p ∈ I, r ∈ F . Let us define fq the transduction realized by Tq = ((Q, q, F, ∆), o, q → , t ). We have

f (u) = i (p)xxq and f (v) = i (p)x xq with xq = fq( ). We also have f (uw) = i (p)xyt (r) and f (vw) = i (p)x yt (r). Hence we have f (u) -1 f (uw) = x -1 q yt (r) = f (v) -1 f (vw)
which means that u ∼ f v and concludes the proof.

Remark 3. In general, for a given variety V, a sequential transduction that is V-rational may not be necessarily V-sequential, and we give an example of this below.

Let I be the variety of idempotent congruences, i.e. for ∼ in I, w ∈ Σ * we have w ∼ w 2 . In Figure 2 we show a sequential function which is I-rational yet not I-sequential. The transduction f realized is obviously sequential. Let us show by contradiction that it cannot be realized by a sequential I-transducer. Let us assume there exists a sequential I-transducer realizing f . We have p a| --→ q with p ∈ I and q ∈ F . We also have i (p) = t (q) = . Since f (aa) = a and a ∼ aa, we must have q a|a --→ q, and then we obtain f (aaa) = aa which is a contradiction.

It is important however to note that in the particular case of A, a sequential transduction that is A-rational is necessarily Asequential. The proof of the following proposition is quite technical and is given in the Appendix.

Proposition 2. A sequential transduction is A-sequential if and only if it is A-rational.

Rational Transductions

For rational transductions, V-rationality is also decidable, as stated in Theorem 1. This section is devoted to proving this result.

Since rational transductions cannot, in general, be realized by a sequential transducer, a unique congruence is not enough to characterize a transduction. Let us consider the example of the transduction f : wσ → σw, with σ ∈ Σ and w ∈ Σ * . This transduction is not sequential (if Σ has more than one letter), and if we apply the construction of [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF] we obtain a right congruence with infinite index, because in order to obtain the image of wσ in a sequential fashion, one has to remember the whole word w before outputting σ. In this case, by adding a lookahead information about the last letter of the input, one can output the image of wσ sequentially. It is the main idea of [START_REF] Reutenauer | Minimization of rational word functions[END_REF] to get a canonical object for rational transductions. They prove indeed that for rational transductions, a finite amount of look-ahead information is sufficient to realize the transduction in a sequential manner, knowing that information.

In particular, in [START_REF] Reutenauer | Minimization of rational word functions[END_REF], it is shown that rational transductions can be characterized by pairs of congruences: a left congruence which gives look-ahead information on the suffix of the word and a Choffrut-like right congruence which depends on the left one. Based on those congruences, they define a computational model called bimachines.

Bimachines A bimachine is a model of computation introduced by [START_REF] Schützenberger | A remark on finite transducers[END_REF]) and shown to be equivalent to (func- tional) transducers. A bimachine is composed of two automata, a left automaton, which is just a deterministic automaton, and a right automaton. A right automaton is an automaton reading words from right to left deterministically. A bimachine can be seen as a transducer with look-ahead where the look-ahead at some position of the word is given by the state of the right automaton.

The runs of a right automaton R are defined as the runs of a left one. Let r be a run on a right automaton, it is accepting if r[1] is final and r[|r|] is initial. We write s2 w ← -R s1 whenever there is a run r of R on w such that r[1] = s2 and r[|r|] = s1. Furthermore, the transitions of a right automaton are deterministic, i.e. it has only one initial state and for any two transitions (p1, σ, q), (p2, σ, q) it holds that p1 = p2. The transition congruence ≈R of a right automaton R with a set of states R is defined as

u ≈R v ⇔ (∀p, q ∈ R, p u ← -R q ⇔ p v ← -R q).
A bimachine over an alphabet Σ is a tuple B = (L, R, ω, λ, ρ) where L = (L, {l0}, FL, ∆L) is a deterministic left automaton (or just left automaton), R = (R, {r0}, FR, ∆R) is a deterministic right automaton (or right automaton), ω : L × Σ × R → Σ * is the output function, λ : FR → Σ * is the left final function and ρ : FL → Σ * is the right final function. Let u be a word such that the runs of L and of R on u, l = l0 . . . ln and r = rn . . . r0 are both accepting. We write

B (u) = λ(rn)ω(l0, u[1], rn-1) . . . ω(ln-1, u[n], r0)ρ(ln)
and we say that B is the transduction realized by B. Example 2. In Figure 3 we give the automata of a bimachine B = (L, R, ω, λ, ρ) realizing the transduction fswap : σwτ → τ wσ for σ, τ ∈ Σ, w ∈ Σ * and Σ = {a, b} and maps words of length less than two to themselves. For l ∈ L, r ∈ R and σ ∈ Σ we define:

λ(r) = ρ(l) = and ω(l, σ, r) =      σ if l = l0 and
u ∼R v ⇔ (∀r ∈ R, r u ← -R r0 ⇔ r u ← -R r0).
As for left automata, we say that R1 is finer than R2 or write R1 R2 if ∼R 1 ∼R 2 . Notice that for simplicity we use the same notations for left and right automata and we rely on the context to differentiate between them. Remark 4. One can easily see that a bimachine with a trivial right automaton (one state, accepts all words) is equivalent to a sequential transducer.

Canonical bimachine

The construction of a canonical bimachine associated with a rational transduction was given in [START_REF] Reutenauer | Minimization of rational word functions[END_REF]. The idea is to refine the minimization of sequential transducers using what can be seen as a look-ahead. For a fixed right automaton, a minimal left automaton can be defined, like for sequential transducers, by producing the outputs as early as possible, given the look-ahead information of the right automaton. A canonical right automaton is defined in [START_REF] Reutenauer | Minimization of rational word functions[END_REF], which gives a construction of a completely canonical machine. Let us define this canonical machine.

Let f be a rational transduction on Σ. The left congruence of f is defined by ∀u, v ∈ Σ * , u f v if:

• ∀w ∈ Σ * , wu ∈ dom(f ) ⇔ wv ∈ dom(f ). • sup{ f (wu), f (wv) | wu, wv ∈ dom(f )} < ∞
The finiteness of the index of f is a powerful characterization of rational transductions and we refer the interested reader to [START_REF] Reutenauer | Minimization of rational word functions[END_REF].

We define the canonical right automaton R f = (R, {r0}, F, ∆). For the rest of this section [w] denotes the class of w in Σ * / f . We take

R = Σ * / f , r0 = [ ], F = {[w] | w ∈ dom(f )} and ∆ = {([σw], σ, [w]) | σ ∈ Σ, w ∈ Σ * }.
Minimal left automaton Let f be a rational transduction and let R be a right automaton finer than R f . Our goal here is to construct a canonical bimachine B f (R) = (Left f (R), R, ω, λ, ρ), which realizes f , as described in [START_REF] Reutenauer | Minimization of rational word functions[END_REF] but we refer the reader to the original paper for a proof of correctness. We first give the construction of a canonical left automaton Left f (R) (or simply Left(R) when it is clear from the context). For simplicity, we will write [w]R instead of [w]∼ R for any word w ∈ Σ * . Let w be a word and let u ∈ P (dom(f )), we define

f [w] R (u) = ∧{f (uv) | v ∈ [w]R} and if u / ∈ P (dom(f )), f [w] R
is not defined. This word is the longest possible output upon reading u, knowing that the suffix is in [w]R. To define the left automaton Left f (R), we need a right congruence: u ∼L v if for any letter σ, any w, z ∈ Σ * we have:

• uz ∈ dom(f ) ⇔ vz ∈ dom(f ) • f [ ] R (uz) -1 f (uz) = f [ ] R (vz) -1 f (vz), if uz, vz ∈ dom(f ) • f [σw] R (uz) -1 f [w] R (uzσ) = f [σw] R (vz) -1 f [w] R (vzσ)
Intuitively, congruence classes of ∼L will be the states of Left f (R). Then, the second line ensures that for the states reached after reading uz and vz, the final output is the same. The third line states that the output of a transition reading σ is the same for the states reached after reading uz and vz.

From ∼L we define the automaton Left

f (R) = (L, {l0}, F, ∆) where L = Σ * /∼ L , l0 = [ ]∼ L , F = {[w]∼ L | w ∈ dom(f )} and ∆ = {([w]∼ L , σ, [wσ]∼ L ) | σ ∈ Σ, w ∈ Σ * }.
Now that we have the automata of the bimachine, the output functions are defined naturally:

• ω([u]∼ L , σ, [v]R) = f [σv] R (u) -1 f [v] R (uσ) • λ([v]R) = f [v] R ( ) • ρ([u]∼ L ) = f [ ] R (u) -1 f (u)
Theorem 4. [START_REF] Reutenauer | Minimization of rational word functions[END_REF] Let f be a rational transduction. Let R be a right automaton finer than R f . Then the bimachine B f (R) = (Left f (R), R, ω, λ, ρ) realizes f . Remark 5. The important result of [START_REF] Reutenauer | Minimization of rational word functions[END_REF] is that the bimachine B f (R f ) is completely canonical i.e. does not depend on any description of f , and is computable. We can define symmetrically the right congruence of f by

u f v if ∀w, uw ∈ dom(f ) ⇔ vw ∈ dom(f ) and sup{ f (uw), f (vw) | uw, vw ∈ dom(f )} < ∞. We can then define L f = (L, {l0}, F, ∆) by L = Σ * / f , l0 = [ ] f , F = {[w] f | w ∈ dom(f )} and ∆ = {([w] f , σ, [wσ] f ) | σ ∈ Σ, w ∈ Σ * }.
For L finer than L f one can also define symmetrically Right f (L) and B f (L) with L and Right f (L) as its left and right automata. Note also that for a total sequential transduction f , the automaton R f is trivial and B f (R f ) is exactly the minimal transducer of [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF].

V-rational transductions

In this section we naturally define V-bimachines as bimachines with V-automata and show they exactly capture V-rational transductions. Since we have, thanks to [START_REF] Reutenauer | Minimization of rational word functions[END_REF], a canonical bimachine one could hope that it suffices to compute this canonical device to decide if a transduction is Vrational. Unfortunately the canonical bimachine is not necessarily a V-bimachine even for a V-rational transduction. The case of the transduction given in Figure 2 is a good example of this: It is I-rational, however the canonical bimachine is not. Indeed, since the outputs of this transduction f are of bounded length, all words are congruent with respect to f . This means that the right automaton of R f is trivial, which is consistent with the fact that f is sequential (and total). However, as we have seen in Remark 3, f is not I-sequential hence the canonical bimachine cannot be an I-bimachine. We have to refine the construction of [START_REF] Reutenauer | Minimization of rational word functions[END_REF], and we show that a rational transduction admits not one but a finite set of minimal (i.e. pairwise incomparable) bimachines, in the strong sense that if there exists a V-bimachine realizing a transduction then one of the minimal bimachines is a V-bimachine. However we only get this result for total functions, but we show that the V-rationality problem for partial functions can easily be reduced to the problem for total functions. Proposition 3. Let V be a variety. A transduction is V-rational if and only if it is realized by a V-bimachine.

Proof. Let f be a transduction realized by T = (A, o, i , t ) an unambiguous V-transducer. We will define a V-bimachine B = (L, R, ω, λ, ρ) realizing the same transduction. We consider the congruence ≈A which is by definition in V. Then we define L = (L, {l0}, FL, ∆L) with:

L = Σ * /≈ A , l0 = [ ], FL = {[w] | w ∈ dom(f )} and ∆L = {([w], σ, [wσ]) | ∃v, wσv ∈ dom(f )}.
Similarly we define R = (R, {r0}, FR, ∆R) with: R =

Σ * /≈ A , r0 = [ ], FR = {[w] | w ∈ dom(f )} and ∆R = {([σw], σ, [w]) | ∃v, vσw ∈ dom(f )}. Let ([u], σ, [v]) ∈ L×Σ×R. If uσv ∈ dom(f ) then there exists a unique tuple (by unambiguity) (p1, p2, q1, q2) ∈ I × Q × Q × F such that p1 u -→ p2, (p2, σ, q1) ∈ ∆ and q1 v -→ q2. In that case we set ω([u], σ, [v]) = o(p2, σ, q1). Otherwise the value of ω([u], σ, [v]
) does not matter and can be set to for instance. If u ∈ dom(f ), we define λ([u]) = i (p) with p being the first state of the unique accepting run on u which is, again, well defined. It is well defined since any word equivalent to u has an accepting run beginning with p. Similarly, ρ([u]) = t (p) with p being the last state of the unique accepting run on u.

B is by definition a V-bimachine which is by construction equivalent to T . For a word of this domain, one can check that the two transductions coincide.

Let f be a transduction realized by B = (L, R, ω, λ, ρ) a Vbimachine. We will define an unambiguous V-transducer T = (A, o, i , t ) realizing the same transduction. This transducer simultaneously simulates the runs of L and the runs of R but backwards. We define A = (Q, I, F, ∆) with:

Q = L × R, I = {l0} × FR, F = FL × {r0} and ∆ = ((l1, r1), σ, (l2, r2)) | (l1, σ, l2) ∈ ∆L (r1, σ, r2) ∈ ∆R
It is easily shown that ≈A is coarser than ≈L ≈R, hence, since V is a variety it is closed under these operations, A is a V-automaton. We define o((l1, r1), σ, (l2, r2)) = ω(l1, σ, r2), i (l0, r) = λ(r) and t (l, r0) = ρ(l). T is an unambiguous Vtransducer which is by construction equivalent to B.

Partial functions Let f be a rational transduction over Σ. The completion of f , denoted by f is defined by:

f : Σ * → (Σ {⊥}) * w → f (w) if w ∈ dom(f ) ⊥ otherwise
where ⊥ / ∈ Σ is a fresh alphabet symbol.

Proposition 4. Let Σ be an alphabet, let V be a variety. Then we have an equivalence:

• f is a V-rational transduction.

• f is a V-rational transduction and dom(f ) is a V-language.

Proof. Let T be an unambiguous V-transducer realizing f . Since f is V-rational, its domain is a V-language and thus we can define A a deterministic automaton recognizing Σ * \ dom(f ). This can be done because modifying the initial and final states of an automaton does not affect the transition congruence. Hence we can define T an unambiguous V-transducer that outputs ⊥ on any word not in dom(f ) and rejects otherwise. The union of T and T is unambiguous since their domains do not intersect. The transition congruence of the obtained transducer is coarser than the intersection of the transition congruences of T and T , and since V is a variety it is closed under these operations, we obtain an unambiguous V-transducer realizing f . Conversely let T be an unambiguous V-transducer realizing f . Since the domain of f is a V-language, we can construct an unambiguous V-transducer behaving as T but rejecting any word outside of dom(f ): Let A be the automaton of T and let A be an unambiguous V-automaton recognizing dom(f ). We construct the transducer whose automaton is the product of A and A and behaves as T but only accepts when A reaches an accepting state. The transition congruence of the product is coarser than the intersection of the congruences of the automata, hence,since V is a variety, we obtain an unambiguous V-automaton realizing f . Towards a finite set of automata Let us now give an overview of the proof of Theorem 1, for a total transduction f . The main idea is the following: If f is V-rational, realized by some Vbimachine B = (L, R, ω, λ, ρ), then there exists a bimachine B = (L , R , ω , λ , ρ ) that realizes f , of which we can bound the granularity of the left and right automata by canonical and computable automata, and such that L L and R R . In particular, we can construct L such that it satisfies Left(R f ) L L f , and R such that it satisfies Right(L f ) R R f . There is only a finite number of automata L and R in these intervals. Moreover, since we take them such that L L and R R , and since by assumption L and R are V-automata, so are L and R . In other words, B is a V-bimachine.

We prove that it suffices to take L = Left(R) and R = Right(Left(R)). The relations between these automata are depicted on Figure 5. The main objective of the rest of this section is to establish the relations depicted on this figure.

First, we establish the upper bounds:

Proposition 5. Let f be a total transduction, and let B = (L, R, ω, λ, ρ) be a bimachine realizing f . Then L L f and R R f . Proof. Let f be a total transduction and let B = (L, R, ω, λ, ρ) be a bimachine realizing f . We will show that R is finer than R f and the proof for L L f is exactly symmetrical. Let u ∼R v, we want to show that u f v. We have obviously for any word w, that wu ∈ dom(f ) ⇔ wu ∈ dom(f ) since f is total. Let w be a word and let l = l0 . . . l |wu| and r = r |wu| . . . r0 the runs (they exist since f is total) on wu of L and R, respectively. Similarly, let l = l 0 . . . l |wv| and r = r |wv| . . . r 0 the runs on wv of L and R, respectively. Since u ∼R v and R is deterministic, the ends (from right to left) of the runs r and r are identical, i.e. for 0 ≤ i ≤ |w| we have r i+|u| = r i+|v| . Hence for x = f (wu) ∧ f (wv) we have

x -1 f (wu) = ω(l |w| , u[1], r |u|-1 ) . . . ω(l |wu|-1 , u[|u|], r0)ρ(l |wu| ) x -1 f (wv) = ω(l |w| , v[1], r |v|-1 ) . . . ω(l |wv|-1 , v[|v|], r0)ρ(l |wv| ) Finally we obtain f (wu), f (wv) ≤ k(|u| + |v| + 2)
where k is the maximum length of any word in the ranges of ω, λ and ρ, which proves that u f v.

To establish the lower bounds, we first state a useful result from [START_REF] Reutenauer | Minimization of rational word functions[END_REF] for total transductions, which gives us a minimality result for the automaton Left(R) when the right automaton R is fixed. Proposition 6. [START_REF] Reutenauer | Minimization of rational word functions[END_REF] Let f be a total transduction. Let B = (L, R, ω, λ, ρ) be a bimachine realizing f . Then L Left(R) and R Right(L) .

From this proposition, we derive an important corollary which will give us the lower bounds:

Corollary 1. Let f be a total transduction and R R f a right automaton. Then Left(R f ) Left(R). Symmetrically, if L L f then Right(L f ) Right(L).
Proof. Let f be a total transduction and R R f . We can assume that R is accessible and still have R R f . According to Theorem 4, there is a bimachine realizing f with Left(R f ) and R f as its automata. This means that there is a bimachine with Left(R f ) and R as its automata which realizes f , by discarding the extra information given by the finer automaton R in the following way: We have a well-defined function

π : Σ * /∼ R → Σ * / f [w]∼ R → [w]
Since R is accessible, we also have a function:

α : R → Σ * /∼ R r → [w] ∼ R such that r w ← -R r0
Hence we have the function π • α : R → Σ * / f such that for any word w if r w ← -R r0 then π • α(r) = [w], hence the behaviour of R f can be simulated by R.

Then according to Proposition 6, Left(R f ) Left(R). The symmetric part of the result is shown in the exact same way. We are now able to establish the relations of Figure 5, as stated by the following lemma, which gives a sufficient and necessary condition for a total transduction to be V-rational.

L Left(R f ) L = Left(R) L f R f R = Right(Left(R)) Right(L f ) R Right L e f t
Lemma 1. Let f be a total transduction. f is a V-rational transduction if and only if there exists an automaton L , with

Left(R f ) L L f such that B f (L ) is a V-bimachine. Proof. If there exists a V-automaton L coarser than Left(R f ) such that Right(L ) is a V-automaton, then f is clearly V-rational.
Conversely, let us assume that f is realized by a V-bimachine B = (L, R, ω, λ, ρ). According to Theorem 4 there is a bimachine realizing f with Left(R f ) and R f as its automata. According to Proposition 6 we know that L Left(R) which means that Left(R) is in V. By Proposition 5, R is finer than R f , we also have according to Corollary 1 that Left(R f )

Left(R). From Theorem 4 and Proposition 6, we have that

R Right(Left(R)) hence Right(Left(R)) is a V-automaton and B f (Left(R)) is a V-bimachine which concludes the proof.
We have proven the key lemma towards the procedure to decide if a transduction is V-rational. Since there are only a finite number of left automaton coarser than a given left automaton, we are able to define a canonical finite set of bimachines, such that a transduction is V-rational if and only if one of those is a V-bimachine.

Proof of Theorem 1 Let T be a transducer and V a decidable congruence variety. First we check in PTime whether T defines a transduction, i.e. is functional [START_REF] Gurari | A note on finite-valued and finitely ambiguous transducers[END_REF]. Second, we check if dom(f ) is a V-language. If it is not then f is not V-rational. If it is then we construct an unambiguous transducer realizing f using the construction given in Proposition 4.

Then we construct the right automaton R f and the left automaton Left f (R f ). They are computable from T as shown in [START_REF] Reutenauer | Minimization of rational word functions[END_REF]. Then we compute all the V-automata L coarser than Left f (R f ), of which there is a finite number, and check if Right f (L ) is a V-automaton. According to Lemma 1, if there does not exist such a pair of V-automata, then f is not V-rational. Otherwise the bimachine B f (L ) is a Vbimachine realizing f .

From Proposition 3 we obtain an unambiguous V-transducer realizing f . Finally, from Proposition 4 we can construct an unambiguous V-transducer realizing f .

First-order definability problems for transductions

The theory of rational languages is rich with results linking automata, logics and algebra, and there have already been successful attempts to lift some of these results to transductions: a monadic second-order logic based transducer model introduced by Courcelle (MSO-transducers) has been shown to be equivalent to deterministic two-way transducers [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF] and, recently, to a one-way deterministic model with registers [START_REF] Alur | Expressiveness of streaming string transducers[END_REF]. More recently, equivalences have been shown between FO-transducers and deterministic two-way transducers with an aperiodic transition monoid [START_REF] Carton | Aperiodic two-way transducers and FOtransductions[END_REF]. However, the expressiveness of MSO-transducers, which are equivalent to deterministic two-way transducers, lies way above that of rational transductions. Indeed, two-way transducers can define transductions that do not preserve the order between input symbols: e.g., they can mirror an input word, or copy it twice. Therefore, in this paper, we consider the order-preserving restriction of MSO-transducers, which we call MSOop-transducers, and is known to capture exactly the class of rational transductions [START_REF] Bojanczyk | Transducers with origin information[END_REF][START_REF] Filiot | Logic-automata connections for transformations[END_REF]. The first-order fragment of MSOoptransducers is defined as MSOop-transducers but with first-order formulas instead of second-order ones.

We show decidability of the following problem: given a rational transduction, is it definable by some FOop-transducer? In particular, we prove that a transduction is realizable by an FOop-transducer iff it is A-rational, and we use Theorem 1 to decide A-rationality. Since our translations are effective, we get the decidability of the following definability problem: given an MSOop-transducer, is it equivalent to some FOop-transducer ?

Our result relies on the correspondence between languages defined in the variety of aperiodic congruences, and first-order definable languages. Similar correspondences exist for other varieties and logical fragments of MSO [START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF], and as seen in the previous section, V-rationality of transductions is decidable for all decidable varieties V. This raises the question of whether one could get decidability of the definability of an MSOop-transducer by an Fop-transducer, for logical fragments F other than FO. We discuss this question at the end of this section.

Monadic second-order and first-order logics on words

We first recall the definition of MSO and FO.

Words as logical structures To express properties of words in logics, one sees a word w over an alphabet Σ as a logical structure2 w over the signature ΞΣ = {(σ(x))σ∈Σ, x y} where σ(x) is a unary predicate interpreted as the positions of a word labelled by σ ∈ Σ, and is a binary predicate interpreted as the order of the word positions. The domain of the structure w is dom(w), the set of positions of w. From now on, we write w instead of w when it is clear from the context.

Monadic second-order and first-order logics Monadic secondorder formulas (MSO-formulas) over ΞΣ are defined over a countable set of first-order variables x, y, . . . and a countable set of second-order variables X, Y, . . . by the following grammar:

φ ::= ∃X φ | ∃x φ | (φ ∧ φ) | ¬φ | x ∈ X | σ(x) | x y
Universal quantifier and other boolean connectives are defined as usual: ∀x φ := ¬∃x ¬φ, ∀X φ := ¬∃X ¬φ, (φ1 ∨ φ2) := ¬(¬φ1 ∧ ¬φ2), (φ1 → φ2) := ¬φ1 ∨ φ2. We also define the formulas and ⊥ as being respectively always and never satisfied. First-order formulas (FO-formulas) are the MSO-formulas in which no second-order variable occurs. We do not define the semantics of MSO, nor the standard notion of free and bound variables, but rather refer the reader to [START_REF] Ebbinghaus | Finite model theory[END_REF] or [START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF] for formal definitions. We recall that a closed formulas (or sentence), is a formula without free variables.

Let φ be an MSO formula without free second-order variables, we write φ(x1, . . . , xm) to denote that the free first-order variables of φ are x1, . . . , xm. Given an MSO formula φ(x1, . . . , xm) and w ∈ Σ * , we write w |= φ(i1, . . . , im) to denote that w, together with the interpretations of xj by ij, j ∈ {1, . . . , m} satisfies φ.

The language defined by a closed MSO-formula (or FOformula) φ is the set φ = {w | w |= φ}. Example 3. As a (well-known) example, we show that the language (ab) * is FO-definable. It suffices to express that the first position is labeled a, the last one is labeled b, and for any position labeled a, the next one is labeled b, and the next next one is labeled a. First, we define the formula for first, last, and successor:

x ≺ y ≡x y ∧ x = y first(x) ≡¬∃y, y ≺ x last(x)≡¬∃y, x ≺ y S(x, y)≡x ≺ y ∧ ¬∃z, x ≺ z ≺ y

Then, the formula defining (ab) * is:

∀x, (first(x) → a(x)) ∧ (last(x) → b(x))∧ ∀y∀z[a(x) ∧ S(x, y) → (b(y) ∧ (S(y, z) → a(z)))]

Logical transducers

Logical transducers have been defined in [START_REF] Courcelle | Monadic second-order definable graph transductions: A survey[END_REF]; Courcelle and Engelfriet 2012) as a logical way of defining transductions of arbitrary structures. We cast this definition to word transductions. Intuitively, the domain of the output word is defined from a fixed number k of copies of the input word. Then the predicates of the output word structure are defined as formulas with free firstorder variables (one for unary label predicates and two for the binary order predicate) interpreted over the input word. In particular, a closed formula φdom defines the domain of the transduction. For all σ ∈ Σ and all copies c, a formula φ c σ (x) defines the label of the c-th copy of the input position x. For all copies d, a formula φ c,d (x, y) defines the order between the c-th copy of x and the dth copy of y. One may want to filter out some copies of the input positions. According to Courcelle's definition, this is done by having formulas φ c filter (x) which holds false if the c-th copy of x is not part of the output word. To shorten our definition, we assume that the c-th copy of x does not belong to the output word iff it has no label, i.e. none of the formula φ c σ (x) holds true.

MSOand FO-transducers An MSO-transducer (resp. FOtransducer) over ΞΣ is a tuple:

T = (k, φdom, (φ c σ (x)) 1≤c≤k,σ∈Σ , (φ c,d (x, y)) 1≤c,d≤k )
where k is an integer, φdom, φ c σ and φ c,d for all c, d ∈ {1, . . . , k} and σ ∈ Σ are MSO-formulas (resp. FO-formulas) over ΞΣ. The MSO-transducer T defines a function T of domain φdom ⊆ Σ * , from words to structures in ΞΣ. For w ∈ φdom , we let the output structure T (w) = N = (D N , (σ N )σ∈Σ, N ) with:

• D N = {(i, c) ∈ dom(w) × {1, . . . , k} | w |= σ∈Σ φ c σ (i)} • σ N = {(i, c) ∈ D N | w |= φ c σ (i)}, for σ ∈ Σ • N = {((i, c), (j, d)) ∈ D N × D N | w |= φ c,d (i, j)}
Observe that nothing guarantees that the output structure is isomorphic to a word structure. However in this paper, we assume that MSO-transducers T always produce structures that are isomorphic to a word structure, i.e., T is word to word transduction. This property is decidable [START_REF] Filiot | Logic-automata connections for transformations[END_REF]. Example 4. As an example, we consider the transduction f : (ab) n → (aab) n defined by the transducer of Fig. 1(c). This transduction can be defined by an FO-transducer with only two copies of the input word. The first two a are produced while reading the first a and the b is produced while reading the b. The transduction of a particular input word by the FO-transducer we are going to construct is depicted on Fig. 6. The domain of f is (ab) * , which is well-known to be FO-definable (see Example 3). Then, one defines the label formulas as follows:

1,2 φ 2,1 φ 1,1 φ 1,2 φ 2,1 φ 1,1 φ 1,2 φ 2,1 φ 1,1 φ 1,2 φ 2,1
φ 1 a (x) ≡ φ 2 a (x) ≡ a(x) φ 1 b (x) ≡ b(x) φ 2 b (x) ≡ ⊥ Note that φ 2 b (x)
is false and φ 2 a (x) ≡ a(x), and therefore the second copy of input position labeled b is not used in the output word. The order predicate is defined by:

φ 1,1 (x, y) ≡ φ 2,2 (x, y) ≡ x y φ 2,1 (x, y) ≡ x y ∧ x = y φ 1,2 (x, y) ≡ (x = y ∧ a(x)) ∨ (x y ∧ x = y)
In the figure, only the successor relation of the order is depicted.

As we have said, MSO-transducers are much more expressive than rational transductions. To capture rational transductions, the following restriction can be imposed:

Order-preserving transducers An MSO-transducer (resp. FOtransducer) is called order-preserving (denoted by MSOop and FOop resp.) if the sentence ∀x, y 1≤c,d≤k (φ c,d (x, y) → x y) is valid in Σ * . E.g. the FO-transducer defined in Example 4 and depicted in Figure 6 is an FOop-transducer. The following is known: Theorem 5. [START_REF] Bojanczyk | Transducers with origin information[END_REF][START_REF] Filiot | Logic-automata connections for transformations[END_REF]) A transduction f is rational iff it is realizable by an MSOop-transducer.

FOop-transducers and aperiodicity

The proof is similar to the one from [START_REF] Filiot | Logic-automata connections for transformations[END_REF] that MSOoptransducers capture exactly the rational transductions and is given in the Appendix. Proposition 7. A transduction is A-rational iff it is definable by an FOop-transducer.

We are ready to prove Theorem 2 of Introduction.

Proof of Theorem 2. A is a decidable variety [START_REF] Cho | Finite-automaton aperiodicity is pspace-complete[END_REF]. By Theorem 1, A-rationality of transducers is decidable, and so is FO-definability by Proposition 7.

Theorem 2 has interesting consequences. Since MSOop-transducers and rational transductions coincide, the FOop-in-MSOop definability problem is decidable:

Corollary 2. Given an MSOop-transducer, it is decidable whether there exists an FOop-transducer realizing the same transduction.

For sequential transductions, Proposition 2 stated that aperiodicity of the transduction can be decided by testing the aperiodicity of the minimal sequential transducer from [START_REF] Choffrut | Minimizing subsequential transducers: a survey[END_REF]. From Theorem 2, this also provides a way to decide FOop-definability: Corollary 3. A sequential transduction is FOop-definable if and only if it is A-sequential.

FO-transducers are easily seen to be closed under composition, i.e. for any two FO-transducers T1, T2, there exists an FOtransducer T such that T = T1 • T2 . The main idea is to substitute the atoms occurring in the formulas of T1 by the formulas of T2 defining these atoms. We refer the reader to [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF]) for more details. It is easily shown that the order-preserving restriction is preserved by the latter transformation whenever T1 and T2 are order-preserving. Therefore we get, as a consequence of Proposition 7, the following corollary.

Corollary 4. Aperiodic rational transductions are closed under composition.

Let us mention that in [START_REF] Carton | Aperiodic two-way transducers and FOtransductions[END_REF], it is shown that deterministic two-way aperiodic transducers are closed under composition. By inspecting the construction of [START_REF] Carton | Aperiodic two-way transducers and FOtransductions[END_REF], applied to aperiodic one-way transducers, one can see that this construction yields an aperiodic one-way transducer, thus proving the latter corollary, in a different way.

Remark on other fragments of MSO Concerning languages, there are other results that link F a logical fragment of MSO to an algebraic variety V, and the question is: does the same link hold between Fop-transducers and V-transducers? Two examples are FO 2 , first-order logic with only two variables, and BΣ1, first order logic with no quantifier alternation, which both have an equivalent in terms of algebraic varieties (see e.g. (Diekert et al. 2008)). Unfortunately, the proof of Theorem 7 (in Appendix B)linking order-preserving FO-transducers to A-transducers cannot be simply transferred to these logics. Indeed for an FO 2 formula φ one cannot construct the formula φ |<x without possibly adding a third variable. On the other hand, for a BΣ1 formula with a free variable, one cannot freely quantify to obtain a closed formula. For FO 2 and other logics where this problem arises, one could consider interpretations on pointed words, i.e. logics with an additional predicate of arity 0 (i.e. a constant), which is trivially equivalent to considering formulas with a free variable when the number of variables is unbounded. For BΣ1 and other logics with restricted quantification, the difficult part is to avoid additional quantification when getting rid of the constant symbol, but this problem should be discussed elsewhere.

Conclusion

Discussion on Theorem 1 Recall that a V-transduction is a transduction defined by an unambiguous V-transducer. What happens if we change the target class, say, to functional V-transducer (not necessarily unambiguous)? It is known that any transduction can be defined by some unambiguous transducer, see for instance [START_REF] Eilenberg | Automata, Languages, and Machines[END_REF][START_REF] Berstel | Transductions and context-free languages[END_REF] for a lexicographic disambiguation construction. However, the lexicographic disambiguation does not necessarily preserve the V-membership in general. This raises the question of whether there exists a disambiguation construction that preserves varieties and more generally, whether Theorem 1 still holds if one targets functional V-transducers instead of unambiguous V-transducers.

FO in MSO definability problem We proved that for any rational transduction described by a transducer (thus MSOop-definable), one can decide whether it is FOop-definable. Hence we solve the FOop in MSOop definability problem.

A possible extension is the FO in MSOop definability problem: given a transducer, is it FO-definable? We conjecture that for rational functions, FO = FOop. Indeed, for deterministic two-way transducers, first-order definability and aperiodicity coincide [START_REF] Carton | Aperiodic two-way transducers and FOtransductions[END_REF]. It remains to prove that a rational transduction given by an aperiodic two-way transducer is also definable by an aperiodic one-way transducer. This would be true if, for instance, the procedure in [START_REF] Filiot | From two-way to one-way finite state transducers[END_REF]

preserves aperiodicity.

A more involved question is the FO in MSO definability: given a two-way transducer, is its transduction FO-definable? For deterministic two-way transducers, a notion of transition monoid is defined and studied in [START_REF] Carton | Aperiodic two-way transducers and FOtransductions[END_REF], but no canonical object is known.

Figure 1 .

 1 Figure 1. Finite state transducers.

  is the initial function and t : F → Σ * is the final function. Let r = q0 . . . qn be a run of A on the word u.We write q0 u|v --→T qn (or simply q0 u|v --→ qn) whenever q0 u -→A qn and v = o(q0, u[0], q1) . . . o(qn-1, u[n], qn). If r is an accepting run and w = i (q0)vt (qn) then we say that (u, w) is realized by T . Then the relation realized by T is the set of pairs of words realized by T and denoted by T . The transducer T is called unambiguous

Figure 3 .Figure 4 .

 34 Figure 3. Automata of bimachine B.

  r = r0 σ if l = l0 and r = r0 τ if l = lτ and r = r0 τ if l = l0 and r = rτ Figure 4 illustrates the execution of B on the word aaab.Left transition congruence For a given right automaton R = (R, {r0}, FR, ∆R), we define the left transition congruence ∼R as

Figure 5 .

 5 Figure 5. Relations between automata

Figure 6 .

 6 Figure 6. FOop-transducer defining the transduction of Fig. 1(c)

2016/4/27

2016/4/27

This type of transducer is sometimes called real-time(Sakarovitch

2009).In the general case, a transition of a transducer may be labelled by any word, however such a transducer is always equivalent to a real-time one.

2016/4/27

2016/4/27

2016/4/27

2016/4/27

For a definition of logical structures see for instance[START_REF] Ebbinghaus | Finite model theory[END_REF] or[START_REF] Straubing | Finite Automata, Formal Logic, and Circuit Complexity[END_REF].82016/4/27

2016/4/27

2016/4/27

Acknowledgments

The authors warmly thank Anca Muscholl for her contribution in early stages of this work.

* This work was partially supported by the ExStream project (ANR-13-JS02-0010), the ARC project Transform (French speaking community of Belgium) and the Belgian FNRS PDR project Flare. Emmanuel Filiot is research associate at F.R.S.-FNRS.

A. Determinization of aperiodic transducers

Proof of Proposition 2. In order to prove Proposition 2 we use the determinization algorithm of [START_REF] Béal | Determinization of transducers over finite and infinite words[END_REF] and show that it preserves the aperiodicity of the transition congruence.

The idea of the algorithm is similar to the subset construction for automata, but taking the outputs into account: on a transition from a subset to another, the output is the longest common prefix for all the possible transitions. The rest of the outputs have to be remembered in the states themselves. Since not all rational transductions are sequential, the algorithm may not terminate. However it is shown in [START_REF] Béal | Determinization of transducers over finite and infinite words[END_REF] that if the transduction is sequential, the algorithm does terminate. Now let us describe the algorithm: Let T = (A, o, i , t ) be a transducer realizing a sequential transduction f . Let us assume that A = (Q, I, F, ∆) is an A-automaton. We give a construction of T = (A , o , i , t ) a transducer realizing f , with A = (Q , S0, F , ∆ ) being deterministic. Let j = ∧{i (q) | q ∈ I}. Then S0 = {(q, w) | q ∈ I and i (q) = jw}.

From the initial state we build the states and the transitions of A inductively. Let S1 be a state already constructed and let σ ∈ Σ.

We define R2 = {(p, vu) | (q, v) ∈ S1 and p σ|u --→T q}. Let s = ∧{w | (q, w) ∈ R2}. Then we define a new state of Q , S2 = {(q, w) | (q, sw) ∈ R2} and add the transition to ∆ and the output of the transition: S1 σ|s --→ T S2. Since f is sequential, the construction must terminate, and we only have left to describe:

The definition of t may seem ambiguous but since f is functional it is well-defined.

Let us show that this construction preserves the aperiodicity of T . We will show that A is counter-free i.e. for any state S, any word u, any integer n > 0, if S u n --→ A S then S u -→ A S. This condition is sufficient for an automaton to be aperiodic (see e.g. (Diekert and Gastin 2008)). For two words u, v, let us denote by u < v that u is a suffix of v and by u ≶ v that either u < v or v < u.

Let R0 ∈ Q , let u ∈ Σ + and let k > 0 such that R0 u k --→ A R0 and we can assume that k is the smallest of such integers. We have to show that k = 1. Let

be the corresponding sequence of transitions of T . Since A is aperiodic, there is an integer n such that for any word w, w n ≈A w n+1 . Let us remark that if we have S w -→ A R then the states of R are, by construction, exactly the states reachable in A from the a state of S. The states reachable in A from a state of R0 by reading u kn+j are the same for any 0 ≤ j < k, hence all the Rj's contain the same states. Let Rj = {(q1, v1,j), . . . , (qm, vm,j)} be pairwise distinct for 0 ≤ j < k. Let us assume not all the x j s are empty otherwise the conclusion is immediate. Let qi u|x i,i ----→T q i denote, when they exist, the transitions of T for 1 ≤ i, i ≤ m. By construction of T , we have for any 0 ≤ j < k: vi,jx i,i = xj+1v i ,j+1

Let qi 0 u -→A qi 1 . . . qi t-1 u -→A qi t be a sequence of transitions in A such that t is a multiple of k. Then we obtain for any 0 ≤ j, j < k:

2016/4/27

In particular, the two words have a common suffix which means that vi t ,j and v i t ,j have a common suffix. This suffix can be arbitrarily large since t can be chosen arbitrarily large. Hence vi t ,j ≶ v i t ,j for any such i, j, j (any state qt is reachable by a long enough sequence).

Let

---→A qi and we can assume that t is a multiple of k, t = sk. Let i = i1, i2, . . . , it, i and i = i 1 , i 2 , . . . , i t+1 , i be the index sequences corresponding with these two runs. Let

We know that vi,j ≶ vi,j+1, let us first assume that vi,j < vi,j+1 and write vi,j+1 = wvi,j+1. We obtain: Let q l be another looping state state such that q l u t --→A q l . Again, since A is aperiodic, by taking t large enough we can assume, t = t . If v l,j < v l,j+1 then v l,j+1 = w l v l,j . However, it also implies that (xjw) k = (xjw l ) k , hence w l = w. On the other hand, let us assume v l,j > v l,j+1 with w l v l,j+1 = v l,j . Let Y l and Y l correspond this time to sequences associated with q l u t -→A q l and q l u t-1 ---→A q l , respectively.

As above, the first two equations give: (Xj) s w l = w l (Xj+1) s From the third equation we have:

Let us remark that:

Hence:

From this we obtain (xj+1

Now from above we can write:

Hence by length, we obtain w = w l = ε. Let q l be a state reachable from qi (any state is reachable from some such looping state). Then it can be reached by a sequence of length t and there is a corresponding sequence of outputs denoted by Z l such that: vi,jZ l = (Xj) s v l,j wvi,jZ l = (Xj+1) s vi,j+1

Hence wv l,j = v l,j+1 .

Finally, w is a common prefix to all v i ,j+1 (j fixed and i ∈ {1, • • • , m}) and must by definition be empty. The reasoning is the same if we assume vi,j > vi,j+1. Hence v i ,j = v i ,j+1 and therefore k = 1, which means that A is counter-free and thus is aperiodic. We have shown that determinization of an aperiodic transducer realizing a sequential transduction preserves the aperiodicity of the transition congruence.

B. Equivalence between A-transducers and FO op -transducers

Proof of Proposition 7. We use the proof from [START_REF] Filiot | Logic-automata connections for transformations[END_REF]) that MSOop-transducers capture exactly the rational transductions and adapt it to the aperiodic/FO case. We give the general idea and mainly focus on the parts that are relevant for the specific aperiodic case. For a more complete proof we refer the reader to the original paper.

Let φ(x1, . . . , x k ) be an FO formula, and let x be a variable which does not appear in φ. Then we define by induction φ(x1, . . . , x k , x) |<x a formula with one more free variable such that for any word u, for any tuple n in dom(u) k , for any word v = , we have:

Let f be a transduction realized by an unambiguous aperiodic transducer T = (A, o, i , t ) with A = (Q, I, F, ∆). Up to the image of the empty word, we can assume that the functions i and t are constant such that for any q ∈ Q, i (q) = t (q) = . Let q ∈ Q, we define the automata Aq = (Q, {q}, F, ∆) and A q = (Q, I, {q}, ∆), which are all aperiodic since they have the same transition congruence as A. Using the Schützenberger, McNaughton-Papert theorem, we also define φ, φq and φ q firstorder formulas recognizing the same languages as A, Aq and A q , respectively.

Let t = (p, σ, q) be a transition of A. We can define the formula ψt(x) = φ p |<x ∧ σ(x) ∧ φ q|<x . A word u satisfies ψt(i) if and only if there is an accepting run r of A on u such that t = (r[i], u[i], r[i + 1]). From this we can define formally T = (k, φdom, (φ c σ (x)) 1≤c≤k,σ∈Σ , (φ c,d (x, y)) 1≤c,d≤k ).

12 2016/4/27

where c ≤ d is a boolean constant or ⊥. T is indeed orderpreserving and one can check that T = T .

Conversely, consider the FOop-transducer T = (k, φdom, (φ c σ (x)) 1≤c≤k,σ∈Σ , (φ c,d (x, y)) 1≤c,d≤k ) realizing a transduction f . Let n be an integer and let u = σ1 . . . σn ∈ Σ n be a word in the domain of f . Let v = f (u) and since T is order-preserving, v can be decomposed as v = v1 . . . vn such that for |vi| ≤ k for any i ≤ n. The word vi is the subword of v induced by the copies of the i th position of u, i.e. the set k) denote the set of words of length less than or equal to k. It means that for any word w ∈ Σ (k) , one can define an FO formula ψw(x) such that for any word u ∈ dom(f ) and i ≤ n, u |= ψw(i) if and only if w = vi according to the decomposition given above. Now we can define an automaton A on the alphabet Γ = Σ × Σ (k) which accepts all words (σ1, v1) . . . (σn, vn) such that σ1 . . . σn |= φdom and for any i, vi is the unique word such that σ1 . . . σn |= ψv i (i). From this we can construct T an unambiguous transducer such that for any transition p (σ,v) ---→A q of A, we have a transition p σ|v --→ T q in T . In order to construct an aperiodic automaton A we use the Schützenberger, McNaughton-Papert theorem since the language of A is FO-definable:

where [φ]Γ is the formula over ΞΓ obtained from a formula over ΞΣ by replacing every atomic formula σ(x) by w∈Σ (k) (σ, w)(x). One can check that T = T . Now we only have left to show that the automaton A of T is aperiodic. We will show that it is counter-free. Let u = σ1 . . . σn be a word of length n, let q be a state of A and let p be a positive integer such that q u p --→ A q. This means that for any i ≤ n, j ≤ p there is a word vi,j ∈ Σ (k) such that q U -→A q with U = (σ1, v1,1) . . . (σn, vn,1)(σ1, v1,2) . . . (σn, vn,p). Without loss of generality we can assume that q is both accessible and co-accessible. Let w1, w2 be words such that q0 w 1 --→A q and q w 2 --→A qF where q0 and qF respectively are an initial state and a final state of A. Since the formulas ψw(x) are FO, we can show using Ehrenfeucht-Fraïssé games (see e.g. [START_REF] Libkin | Elements of Finite Model Theory[END_REF])) that there exists an integer m such that for any words x, y, z, (y being nonempty) and for i ≤ |y| we have xy m yy m z |= ψ(|x| + |y| m + i) ⇒ xy m yy m z |= ψ(|x| + |y| m+1 + i). Since we have for any i ≤ n, j ≤ p, w1u km u k u km w2 |= ψv i,j (|w1| + |u| km+(j-1) + i), we get that w1u km u k u km w2 |= ψv i,j (|w1| + |u| km+j + i). This means that we have vi,j = vi,j+1 for any 1 ≤ j < p, so let vi = vi,j. Hence, q ((σ 1 ,v 1 )...(σn,vn)) p -------------→A q. However, A is a deterministic and aperiodic automaton and is thus counter-free, hence q (σ 1 ,v 1 )...(σn,vn) -----------→A q. Finally we obtain that q u -→ A q which means that A is counter-free and T is an unambiguous Vtransducer.

C. Closure of FO op -transducers under composition

Proof of Corollary 4. We want to show that FOop-transducers are closed under composition. It is well-known that MSO-transducers, as well as FO-transducers, are closed under composition [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF]. Let us give the overall idea. If the set of copies of T1 is {1, . . . , k1} and the one of T2 is {1, . . . , k2}, then the set of copies of T , which realizes the composition, is {1, . . . , k1} × {1, . . . , k2}, which is isomorphic to {1, . . . , k1k2}.

Then, an output position of the image of a word w by T is a triple (i, c1, c2) where i ∈ dom(w), c1 is a copy of T1 and c2 is a copy of T2. Then, to give a very high-level idea, the formulas of T are obtained by substituting atomic propositions in the formulas of T1 by formulas of T2, and by restraining the quantifiers of the formulas of T1 to positions that exist by T2. We refer the reader to [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF]) for all the details, but extract the main argument that will allow us to show that the orderpreserving restriction is preserved: the construction of [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF] preserves origin information, in the sense of [START_REF] Bojanczyk | Transducers with origin information[END_REF]. Given (w, w ) ∈ T1 , the origin mapping is a function o from dom(w ) to dom(w), defined as follows: every position in w is a pair (i, c) where i ∈ dom(w) and c is a copy of T1. Then, the origin of node (i, c) is defined as i, i.e. o(i, c) = i. Moreover, T1 is order-preserving iff o is order-preserving, in the sense that for any two elements α, β in the range of o, if α β, then o(α) o(β). Now, it is easily seen that the construction of (Courcelle and Engelfriet 2012) preserves origin, in the following sense: if (w1, w3) ∈ T with origin mapping o, then there exists w2 such that (w1, w2) ∈ T2 with origin mapping o2 and (w2, w3) ∈ T1 with origin mapping o1, such that o = o2 • o1. Finally, since o1 and o2 are order-preserving, so is o: Indeed, take two elements α β in the range of o, since o1 is order-preserving, o1(α) o1(β) and since o2 is order-preserving, o2(o1(α)) o2(o1(β)), i.e. o(α) o(β).