Etienne Simon-Loriere

Ousmane Faye

Matthieu Prot

Isabelle Casademont

Gamou Fall

Maria Fernandez-Garcia

Moussa M Diagne

Autochthonous Japanese Encephalitis with Yellow Fever Coinfection in Africa

Autochthonous Japanese encephalitis with Yellow fever coinfection in Africa

Authors: Etienne Simon-Loriere 1,2,* , Ousmane Faye 3 , Matthieu Prot 1,2 , Isabelle Casademont 1,2 , Gamou Fall 3 , Maria Dolores Fernandez-Garcia 3 , Moussa Moise Diagne 3 , Jean-Marie Kipela [START_REF] Chen | A fatal yellow fever virus infection in China: description and lessons[END_REF] , Ibrahima Socé Fall 5 , Edward C. Holmes 6 , Anavaj Sakuntabhai 1,2 and Amadou A. Sall [START_REF] Matranga | Enhanced methods for unbiased deep sequencing of Lassa and Ebola RNA viruses from clinical and biological samples[END_REF] .

Affiliations:

1 Institut Pasteur, Functional Genetics of Infectious Diseases Unit, 75724 Paris Cedex 15, France. To the Editor: Japanese encephalitis virus and yellow fever virus are mosquito-borne flaviviruses that circulate in disjunct geographic areas with different mosquito vectors. Japanese encephalitis is endemic to most of Asia and the Western Pacific, whereas yellow fever occurs in tropical areas of Africa and South America. Both viruses lead to a wide spectrum of disease severities that include asymptomatic infection and mild illness with influenza-like symptoms. However, severe yellow fever disease can be fatal in 20 to 60% of cases 1 , whereas symptomatic Japanese encephalitis virus can progress to severe encephalitis, with case fatality rates of up to 30%. Survivors often have long-term neuropsychological sequelae [START_REF] Who | Encephalitis Vaccines: WHO position paper -February 2015[END_REF] . In March 2016, during the yellow fever outbreak in Angola, a 19-yearold man was admitted to the Cunene Provincial Hospital with a 5-day history of fever, headache, and jaundice. The patient, who survived, worked in the capital city of Luanda at the onset of disease and had not traveled abroad. A blood sample was obtained, and a test for yellow fever virus was positive. The sample was later processed for high-throughput RNA sequencing. Because the protocol followed made use of randomly primed cDNA synthesis, it provided a more complete and quantitative view of all RNA present in the sample than would have otherwise been possible, enabling the characterization of potential coinfecting viruses [START_REF] Matranga | Enhanced methods for unbiased deep sequencing of Lassa and Ebola RNA viruses from clinical and biological samples[END_REF] . Surprisingly, de novo assembly of the sample revealed a Japanese encephalitis virus genome in addition to the expected yellow fever virus genome. Phylogenetic analysis revealed that this Japanese encephalitis virus variant belongs to genotype III, clustering closely with variants sampled in Asia (Fig. 1A, and Supplementary Appendix). The yellow fever virus sequence was closely related to both a sequence from the 1971 yellow fever virus outbreak in Angola and the recently reported yellow fever virus sequence detected in a sample from a Chinese traveler returning from Angola 4 (Fig. 1B).The likelihood of sample contamination is small, since neither the Institut Pasteur of Dakar, Senegal, where the RNA extracted from the samples in Angola was delivered, nor the laboratory at the Institut Pasteur, Paris, where the libraries were constructed and sequenced, has ever had any material containing Japanese encephalitis virus. In addition, none of the 15 additional RNA samples from patients with yellow fever virus who were treated at the same time provided reads that corresponded to Japanese encephalitis virus. Leftover sera from the Angola samples were later extracted at Institut Pasteur of Dakar, and only sample C17 was positive for Japanese encephalitis virus RT-qPCR. We found evidence of locally acquired infection with Japanese encephalitis virus in Africa in addition to coinfection with yellow fever virus, which raises the issue of the risk of circulation of the Japanese encephalitis virus and human infection in Africa. Since both the vectors and suitable hosts (e.g., pigs) for Japanese encephalitis virus are present in Angola, more studies of this virus in this locality, including serosurveillance, are needed. Increased levels of population movement between Asia and Africa may provide opportunities for pathogens to expand their geographic range. These data also highlight the potential usefulness of high-throughput sequencing, particularly untargeted approaches, for pathogen surveillance 5 .

Figure 1 .

 1 Figure 1. Maximum likelihood phylogenetic trees of representative full-length (A) JEV and (B) YFV sequences. The isolates newly sequenced here are shown in bold, italic font. Viruses are identified by GenBank accession numbers, country of sampling and isolation date and viral genotypes are indicated. All horizontal branch lengths are scaled to the number of nucleotide substitutions per site and the trees were mid-point rooted for clarity only. Bootstrap values are shown for key nodes.

  2 CNRS URA3012, Paris 75015, France. 3 Institut Pasteur de Dakar, Arbovirus and Viral Hemorrhagic Fever Unit, BP220 Dakar, Senegal. 4 World Health Organization Country Representative Office, Luanda, Angola. 5 World Health Organization, Country Representative Office, Bamako, Mali. 6 Marie Bashir Institute for Infectious Diseases and Biosecurity, Charles Perkins Centre, School of Life and Environmental Sciences and Sydney Medical School, The University of Sydney, Sydney, NSW 2050, Australia.


Olivier Carton

Léo Exibard

Olivier Serre

Two-way Two-tape Automata

Keywords: Alternating, Multi-tape automata, Complementation

In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternating automata are not closed under composition.

Introduction

In this article we consider two-way two-tape (alternating) automata that are designed to recognize binary relations between finite words. Although these automata are quite natural as read-only Turing machines, almost no work has been devoted to this model of computation. We study their properties, with a special focus on their closure properties, in particular under complementation and composition.

Finite states machines with inputs and outputs are widely used in many different areas like coding [START_REF] Lind | An Introduction to Symbolic Dynamics and Coding[END_REF], computer arithmetics [START_REF] Lothaire | Algebraic Combinatorics on Words[END_REF], natural language processing [START_REF] Roche | Finite-State Language Processing[END_REF] and program analysis [START_REF] Cohen | Instance-wise reaching definition analysis for recursive programs using context-free transductions[END_REF]. The simplest model is obtained by adding outputs to a classical finite-state (non)-deterministic one-way automaton to get a machine known as a transducer. In a transducer, the input word is only scanned once by a one-way head and the output is produced by the transitions used along the reading. A transducer can equivalently be seen as a machine with two tapes, one for the input and the other for the output, that are scanned once by two one-way heads. Relations realized by this kind of machines are called rational. They have been intensively studied since the early days of automata theory [START_REF] Elgot | On relations defined by generalized finite automata[END_REF] and they enjoy some nice properties [START_REF] Sakarovitch | Elements of Automata Theory[END_REF]. They are, for instance, closed under composition, but not under complementation.

Rational relations turn out to form a rather small class, hence classes of stronger transducers have been introduced by enriching transducers with extra features like two-wayness and/or alternation. A well studied class is that of twoway transducers in which the input word is scanned by a two-way head and the output is produced (or equivalently scanned) by a one-way head. In that class, deterministic machines are of special interest as they are equivalent to MSO-transductions and turn out to be closed under composition [START_REF] Engelfriet | MSO definable string transductions and two-way finite-state transducers[END_REF].

In this article, we consider machines with two tapes which are both scanned by two-way heads. In this model, it is important to consider the output word as already written, and not produced on some output tape to ensure consistency, as it is scanned several times.

Another key feature, used to increase either the expressive power or the succinctness of finite state machines, is alternation, which allows the machine to spawn several copies of itself. Alternation often provides for free closure under complementation for machines on finite structures like words or trees. Indeed, the dual machine obtained by swapping existential and universal states and complementing the acceptance condition accepts the complement language as long as all computations terminate: if the run of a machine may loop, the closure under complementation of alternating machines may no longer hold.

Picture automata introduced in [1] scan a 2-dimensional array of symbols with moves in the four cardinal directions to either accept or reject it. As in the case of two-way automata, the border of the array is marked by special symbols. A run of such an automaton may loop as it can scan the same position twice with the same control state. These picture automata differ from classical word or tree automata where all variants (deterministic, non-deterministic, alternating) are equivalent. Indeed, it has been shown by Kari and Moore that alternating picture automata are not closed under complementation as soon as the alphabet size is greater than 1 [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF]. This means that loops are inherent to the model and that they cannot be removed.

In this article, we show that two-tape two-way alternating automata are not closed under complementation either. Picture automata are actually very close to the model that we consider. In particular they coincide for unary alphabets. Indeed, over a unary alphabet, a pair of words is merely a pair of integers (their lengths) and this is equivalent to a two-dimensional array on a unary alphabet. However, as soon as the alphabets have cardinality at least 2, the models are distinct. Indeed, for an alphabet of size k, the number of m × n-arrays is k mn while the number of pairs of words is only k m+n .

The fact that the two models coincide for unary alphabets allows us to recover immediately some separation and undecidability properties. For instance, it has been shown that such deterministic picture automata are strictly less powerful than non-deterministic ones which are, in turn, less powerful than alternating automata [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF]. These results carry over the two-tape two-way automata that we consider.

To prove that alternating automata are not closed under complementation, we use a counter-example that is close to the one in [START_REF] Kari | Rectangles and squares recognized by two-dimensional automata[END_REF] for picture automata. However, since our coding is different, we need some extra arguments to show that it is accepted by an alternating automaton and, to show that its complement cannot, we use a more direct proof.

Two-way Two-tape Automata

In this article, Σ is a finite alphabet and Σ * denotes the set of finite words over Σ. For a word u ∈ Σ * , we denote its length by |u|, and for each 1 ≤ i ≤ |u| we denote by u i its i-th letter. From now on, ⊢ (begin) and ⊣ (end) are reserved characters not belonging to Σ and marking word boundaries. For simplicity of notation, we let Σ ⊣ ⊢ = Σ ∪ {⊢, ⊣}. For u ∈ Σ * , we let u ⊣ ⊢ = ⊢u⊣, with u ⊣ ⊢0 = ⊢, u ⊣ ⊢|u|+1 = ⊣ and u ⊣ ⊢i = u i for each 1 ≤ i ≤ |u|. A (non-deterministic) two-way two-tape finite automaton is a tuple A = (Q, Σ, ∆, I, F ), where Q is the set of states, and I, F ⊆ Q are respectively the sets of initial and final states. We call -------→ q for (p, a 1 , a 2 , q, d 1 , d 2 ) ∈ ∆. We require that the reading heads cannot cross the words boundaries, i.e. for every transition p a1,a2|d1,d2

∆ ⊆ Q × Σ ⊣ ⊢ × Σ ⊣ ⊢ × (Q × {⊳, ▽, ⊲ } × {⊳, ▽,
-------→ q and every i = 1, 2 if

a i = ⊢ (resp. a i = ⊣) then d i = ⊳ (resp. d i = ⊲).
An automaton A is said to be deterministic whenever for every state p ∈ Q and every letters a 1 , a 2 ∈ Σ, there exists at most one q ∈ Q, d 1 , d 2 ∈ {⊳, ▽, ⊲} such that p a1,a2|d1,d2

-------→ q. Note that extending the model to more than two tapes is straightforward. Note also that if we restrict the model to a single tape we retrieve the classical notion of two-way automata on finite words. A configuration is a triple (q, i, j) ∈ Q × N × N, where q is the current state, and i (resp. j) is the position of the reading head on the first (resp. second) tape (recall that the ⊢ marker is by convention at position 0).

Q ⊢ u1 • • • ui • • • um ⊣ First Tape ⊢ v1 • • • vj • • • vn ⊣ Second Tape
We say that a configuration (q 2 , i 2 , j 2 ) is a successor of a configuration (q 1 , i 1 , j 1 ) with regard to input (u, v), written (q 1 , i 1 , j 1 ) (u,v) (q 2 , i 2 , j 2 ), when automaton A can go from one configuration to the next in a single step, i.e. if

q 1 (u ⊣ ⊢ )i 1 ,(v ⊣ ⊢ )j 1 |d,e
-----------→ q 2 , and if

i 2 = i 1 + χ(d) and j 2 = j 1 + χ(e), where χ(⊳) = -1, χ(▽) = 0 and χ(⊲) = 1. A run of A on input (u, v) ∈ Σ * × Σ * is a (possibly infinite) sequence (p k , i k , j k ) 1≤k<n , where n ∈ N ∪ {∞}, of successive configurations: for every 1 ≤ k < n, one has (p k , i k , j k ) (u,v) (p k+1 , i k+1 , j k+1 ).
An initial run is a run starting with an initial configuration, i.e. one such that p 0 ∈ I and i 0 = j 0 = 0. It is accepting when it is moreover finite and contains a final state f ∈ F , i.e. there exists k ≤ n such that p k ∈ F .

The relation R (A) accepted by a two-way two-tape automaton A is the set of pairs (u, v) such that there exists an accepting run of A on input (u, v).

We now introduce alternating automata, which generalize non-deterministic automata. An alternating automaton is an automaton whose set of control states is partitioned into existential (Q ∃ ) and universal (Q ∀ ) states. A configuration is defined as in the non-deterministic setting and it is existential (resp. universal) if the control state is.

Runs of alternating automata are (possibly infinite) trees whose nodes are labeled by configurations, and such that each inner node u labeled by a configuration C satisfies the following conditions:

-If C is existential then u has a single son that is labeled by a successor configuration of C. -If C is universal and if {C 1 , . . . , C k } denotes all successor configurations of C, then u has k sons each of them labeled by a different C i for 1 ≤ i ≤ k.
A run is accepting if it is finite, its root is labeled by an initial configuration and all its leaves are labeled either by accepting configurations, or by universal configurations that have no successor configuration. Again, we define the relation accepted by an alternating automaton as those pairs of words over which there is an accepting run. Note that non-deterministic automata correspond to the case where Q ∀ = ∅.

First we remark that if we restrict the model by forbidding the reading heads to go to the left, we obtain a 1-way model that recognizes the rational relations, i.e. those realized by transducers [START_REF] Sakarovitch | Elements of Automata Theory[END_REF]. Not surprisingly this is a restriction as two-way two-tape automata can, for instance, recognize deterministically the relation {(u, ũ) | u ∈ Σ * }, where ũ denotes the reverse of u. The corresponding automaton is depicted in Figure 2. This relation cannot be recognized by classical one-way transducers.

qi q q f ⊢, Σ ⊢ | ▽, ⊲ ⊢, ⊣ | ⊲, ⊳ a, a | ⊲, ⊳ b, b | ⊲, ⊳ ⊣, ⊢ | ▽, ▽ Fig. 2. Automaton recognizing {(u, ũ) | u ∈ Σ * } when Σ = {a, b}
Our model captures much more complex relations. It is shown in the next section that two-way two-tape automata can recognize the relation Coprime = {(a p , a q ) | p ∧ q = 1}, where p ∧ q denotes the greatest common divisor of p and q, by implementing a variant of the Euclidean algorithm.

Picture Languages

For brevity we simply recall here some key notions on picture languages: we refer the reader to [START_REF] Giammarresi | Recognizable picture languages[END_REF] for an excellent survey on the topic with complete definitions of all objects discussed below.

A picture p of dimensions m × n is a matrix over a finite alphabet Σ. For every 1 ≤ i ≤ m and 1 ≤ j ≤ n, we write p i,j for the content of the cell at position (i, j). To recognize pictures, we add a special marker # / ∈ Σ all around the picture p, i.e. we adopt the convention that for all 0 ≤ i ≤ m + 1 and 0 ≤ j ≤ n + 1, p 0,j = p m+1,j = p i,0 = p i,n+1 = #. We write Σ * * for the set of all pictures over Σ. A picture language is thus a subset of Σ * * .

In order to recognize picture languages, 4-way automata were first introduced in [START_REF] Blum | Automata on a 2-dimensional tape[END_REF]. Such an automaton has a single head which is able to move on a twodimensional array of symbols (surrounded by markers) in the four directions (up, down, left, right) and accepts when reaching a final state. A schema is provided in Figure 3. The link between two-way two-tape automata and picture automata is provided by special pictures, called products of words, that we now define. For u, v ∈ Σ * , we define the picture

Q # # # # # # # # # # # # # # # # # # # # # # # # ui,j
u ⊗ v = ((u i , v j )) 1 ≤ i ≤ |u| 1 ≤ j ≤ |v| over the product alphabet Σ × Σ. Thus, any relation R ⊆ Σ * × Σ * is mapped to a picture language L ⊗ R ⊆ (Σ × Σ)
* * . Moreover, over unary alphabets, pictures languages and binary relations over words are in one-to-one correspondance as the pair (a m , a n ) unambiguously represents an image of dimensions m × n and conversely. Consequently, for L ⊆ {a} * * , L is recognizable by a 4-way deterministic (resp. nondeterministic, alternating) automaton iff R is recognizable by a deterministic (resp. non-deterministic, alternating) two-way two-tape automaton where R is the unique relation such that L = L ⊗ R . Thus, all the results known for unary picture languages also hold in our model when |Σ| = 1. In particular, in [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF], it is shown that determinism is strictly weaker than non-determinism, the latter being weaker than alternation: DFA NFA AFA where DFA (resp. NFA, AFA) is the class of relations recognized by deterministic (resp. non-deterministic, alternating) two-way two-tape automata.

The relation R = {(a w , a h ) | ∃i, j ∈ N, w = ih + j(h + 1)} is such that R / ∈ DFA, R ∈ NFA, R /
∈ NFA, R ∈ AFA, where R denotes the complement of R in Σ * × Σ * . In [START_REF] Kari | A survey on picture-walking automata[END_REF], it is shown that the emptiness problem is undecidable even for a unary alphabet.

(p, 1) The following examples from [START_REF] Kari | Rectangles and squares recognized by two-dimensional automata[END_REF] show that picture automata and two-way two-tape automata are really expressive. The relation Coprime = {(a p , a q ) | p ∧ q = 1} can be recognized by a deterministic automaton implementing a variant of the Euclidean algorithm. The automaton follows diagonals until it reaches either one of (p, 1) or (1, q) or one of (0, 0), (p, 0), (0, q) or (p, q). In the former case, it accepts and in the latter case, it rejects.

(1, q) p q 2 n 2 n
A more sophisticated deterministic automaton can recognize the relation {(2 n , 2 n ) | n ∈ N} following the schema in Figure 4 (right). The automaton moves with a ratio of 1/2 as long as it is possible (i.e. while the remaining length is divisible by 2), and it accepts if it reaches the bottom-right square. An even more sophisticated deterministic automaton can accept the relation

{(2 2 n , 2 2 n ) | n ∈ N}.
4 Alternating Two-way Two-tape Automata Are Not

Closed under Complementation

Our main result is the following. Note that the case of unary alphabets is still an open problem.

Theorem 1. The class of relations recognized by alternating two-way two-tape automata is not closed under complementation as soon as the alphabet is not unary.

In this proof we denote by AFA the class of relations recognized by alternating two-way two-tape automata, and by co-AFA the class of relations whose complement is recognized by alternating two-way two-tape automata. Hence, we aim to prove that AFA and co-AFA are distinct, and this is achieved by defining a well-chosen relation P and show that P ∈ AFA but P / ∈ co-AFA. The first point is proved by giving an explicit alternating two-way two-tape automaton recognizing P (Lemma 2); the second point is proved by contradiction using a game-theoretic approach combined with a combinatorial argument (Lemma 3).

The proof is inspired by the one in [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF] establishing that the set of picture languages recognized by alternating 4-way automata is not closed under complementation. One difference is that the counter-example they exhibit cannot be used in our setting as the images that are considered are not product of words (as defined in Section 3). Hence, even if the general idea -coding a permutation to build a counter-example -is similar to the one in [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF], our coding is different and therefore new ideas are needed to prove that we can accept this relation with an alternating two-way two-tape automaton. The proof that the complement is not recognizable by an alternating two-way two-tape automaton, even if it shares ideas with the one in [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF], is somehow more direct as it does not appeal to an intermediate class.

In the following, if c 1 , . . . , c n are n words of length n over alphabet {0, 1} we identify the tuple (c 1 , . . . , c n ) with the n × n matrix whose i-th column is c i . We define the relation P by

P = {(a n , c 1 # • • • #c n $c 1 # • • • #c n ) | n ∈ N, (c 1 , . . . , c n ) ∈ S n }
where S n denotes the set of all (n × n {0, 1}-matrix coding) permutations over {1, . . . , n}. See Figure 5 for an example. As announced, we start by showing that P ∈ AFA. Lemma 2. There exists an alternating two-way two-tape automaton recognizing P.

Proof. We describe below how to check whether a pair (a n , c) ∈ a * ×{0, 1, $, #} * is in P. As the a n word is used only to store position we sometimes refer to the content of the first tape as the counter.

To decide if (a n , c) ∈ P, we have to check two things. The first one is whether c is of the form σ 1 $σ 2 , where σ 1 , σ 2 are the encodings of two permutations of dimension n and the second one is whether

σ 1 = σ 2 .
For the first step, we only explain how to check the property for σ 1 as the case of σ 2 is checked in the same way. Assume σ 1 = c 0 #c 1 # • • • #c n (checking that there are n block is easy). We first need to check that each c i (i.e. each column) has length n and contains exactly one 1: this is easy (the length condition being checked thanks to the first tape). We then need to check that for each k = 1, . . . , n there is exactly one c i whose k-th letter is a 1 (i.e. each row contains exactly one 1). This property is checked for each k = 1, . . . , n in increasing order starting from k = 1, and at the beginning of step k the head in the counter in the first tape is at position k and the head in the second tape is at the beginning of σ 1 : now going left on the counter and right on the second tape at the same speed the k-th symbol of c 1 is reached (just before the left marker is read on the first tape); then the automaton goes back to the beginning of c 1 and the counter is increased back to k; finally the second head goes to the beginning of c 2 (going to the right until reading a #), then c 2 is processed in the same way, and so on until reading a $ meaning that c n was processed and that one can go back to the beginning of the second tape and start again but now for k + 1.

We are now left with checking that σ 1 = σ 2 knowing that both σ 1 and σ 2 encode a permutation. For that we use the same approach as the one in [8, Lemma 2, Condition (*)]. More precisely, we use the following property: two permutations are different iff there exists an inversion i.e. there exists

i = i ′ , σ 1 (i) < σ 1 (i ′ ) but σ 2 (i) > σ 2 (i ′
). This can be checked by trying all possible way of moving in the associated picture (as illustrated in Figure 5) in the following fashion (see Figure 6): from a 1 move right to another column but stay on the same side of the column of $s. Find the 1 on that column. Then move to the other 1 that is on the same row, on the opposite side of the column of $s, and repeat: then, the machine enters an infinite loop iff it finds an inversion [START_REF] Kari | New results on alternating and non-deterministic twodimensional finite-state automata[END_REF].

$ $ $ $ $ $ $ $ $ 1 1 1 1

Fig. 6. Loop corresponding to an inversion

The first step (finding a 1) is easy and done using universal states (which ensures that we do the check for all possible 1). Moving to another column on the right is easy: simply use a universal state and keep moving the head to the right passing one or more # but stopping before reading the $. Finding the 1 on the column is easy (look for it in between the left and right #). Finally, moving to the other 1 on the same row on the opposite side of the $ is achieved by using the counter to keep in memory the row number j, and then go to the other side and check every column until finding the one with a 1 on the j-th row (this is done with the same trick used previously to check that each row contains a single 1). If at some point when moving to a column to the right the automaton hit a $ then it goes to a final state. The automaton accepts the desired language for the following reason: if an inversion exists, it is found (thanks to universal choices) and leads to a looping hence, rejecting, computation; if not, whatever the universal choices are the automaton is getting closer and closer to the $ and eventually hit it thus reaching a final state.

Therefore, we built an alternating two-way two-tape automaton recognizing P. More generally, the ideas used in the first part of the proof can be used to prove the following: for any picture language L recognizable by a 4-way automaton, the relation

{(a max(n,m) , c 1 # • • • #c m ) | (c 1 , . . . , c m ) is an n × m picture in L} is
recognizable by a two-way two-tape automaton.

⊓ ⊔

We now show that the complement of P cannot be recognized by an alternating two-way two-tape automaton.

Lemma 3. Relation P / ∈ co-AFA.
Proof. The proof is by contradiction assuming the existence of an alternating two-way two-tape automaton A = (Q, Σ, ∆, I, F ) such that a pair (u, v) is accepted by A iff (u, v) / ∈ P. Hence, a pair (a n , c) is rejected by A iff if belongs to P.

We now rephrase the fact that (a n , c) is rejected by A, to that end we use a game-theoretic flavoured argument. Indeed, another way of thinking about a run of an alternating automaton is as a two-player games where the existential player is in charge of choosing the transition in existential configurations while the universal player takes care of universal configurations. The winning condition for the existential player is that a final configuration is eventually reached. In particular A rejects its input iff the universal player has a winning strategy, i.e. a playing policy ensuring no final state is ever reached whatever the existential player does. Moreover, this strategy can be chosen to be positional, i.e. only depending on the configuration, not on how it was reached (see e.g. [START_REF]Automata, Logics, and Infinite Games: A Guide to Current Research[END_REF]).

Fix an input of the form (a n , σ$σ) ∈ P. A strategy for the universal player and the proof that it is a winning one can be described as follows. For each position 0 ≤ j ≤ 2n + 2 on the second tape (including the markers) we associate a n + 2 tuple τ j = (τ 0,j , . . . , τ n+1,j ) of functions describing what configurations can appear when the heads are at position (i, j) and for universal ones what the strategy of the universal player is. Hence for each 0 ≤ i ≤ n + 1, τ i,j is a map from Q such that:

-if q ∈ Q ∃ , τ i,j (q) is either ⊥ (meaning (q, i, j) is not reachable) or ⊤ (reach- able) -if q ∈ Q ∀ , τ i,j (
q) is either ⊥ (not reachable) or a transition in ∆ starting with (q, x, y) where x (resp. y) is the letter at position i (resp. j) in the first (resp. second) tape, including markers. The latter case means that configuration (q, i, j) can appear and gives the corresponding move in the universal player strategy.

Such an object τ 0 , . . . , τ 2n+2 is a proof of reject if it satisfies the following four conditions. 1. For each initial state q ∈ I, τ 0,0 (q) = ⊥ (all initial configurations are allowed). 2. For each final state q ∈ F and each i, j, τ i,j (q) = ⊥ (no final configuration can be reached). 3. For each existential state q and each i, j such that τ i,j (q) = ⊤, for each possible successor (q ′ , i ′ , j ′ ) of (q, i, j) one has that τ i ′ ,j ′ (q ′ ) = ⊥ (all successors of allowed existential configurations are allowed). 4. For each universal state q and each i, j such that τ i,j (q) = ⊥, if one denotes by (q ′ , i ′ , j ′ ) the configuration reached from (q, i, j) applying transition τ i,j (q) then τ i ′ ,j ′ (q ′ ) = ⊥ (an allowed universal configurations has its successor described by the strategy allowed).

It is then standard to notice that A has no accepting run over (a n , σ$σ) iff there is a proof of reject for it. Now, for a fixed n, consider the number of possible values for the central part (τ n , τ n+1 , τ n+2 ) of a proof: it is smaller than ((|∆| + 1) |Q| ) 3n . Hence, for n large enough it is smaller than n!. For such n it means that there are two distinct permutations σ = σ ′ such that the proofs of reject for σ$σ and for σ ′ $σ ′ coincide on their central part: hence, they can be combined (glue the left part of the first proof with the right part of the second), leading a proof of reject for σ$σ ′ . But this leads a contradiction as σ$σ ′ / ∈ P and therefore is accepted by A. ⊓ ⊔

Union, Intersection and Composition

In this section, we study the closure under union, intersection and composition of two-way two-tape automata.

Closure under Union and Intersection

Concerning closure under union and intersection we have the following picture.

Lemma 4. Relations recognized by deterministic ( resp. non-deterministic, resp. alternating) two-way two-tape automata are closed under union and intersection.

Proof (sketch). For non-deterministic automata union is for free; intersection is simply obtained by simulating the first automaton, and if it reaches an accepting state, simulating the second automaton. For alternating automata both closures are for free. For deterministic automata, intersection can be obtained as in the non-deterministic case. Concerning union, one can no longer use nondeterminism and hence, one needs to simulate successively the two automata. However this does not work in general as a two-way two-tape automaton can reject by entering an infinite loop. Hence, one must first get rid of such phenomenon: this can be achieved thanks to a method due to Sipser [START_REF] Sipser | Halting space-bounded computations[END_REF], which ensures that a deterministic two-way two-tape automaton never rejects by looping.

⊓ ⊔

Remark that preventing deterministic two-way two-tape automata from rejecting by looping can be used to prove that the class of relations they recognize is also closed under complementation, and therefore forms a Boolean algebra.

Non-closure under Composition

In this section, we prove that the class of relations recognized by two-way twotape automata is not closed under composition, even in the deterministic case.

Theorem 5. Relations recognized by deterministic ( resp. non-deterministic, resp. alternating) two-way two-tape automata are not closed under composition.

Proof. The proof works the same way for all three models. One first establishes (see Lemma 6 below) an elementary bound on the growth of the functions recognized by our model, and then exhibit (see Lemma 7 below) a recognizable relation breaking this bound when self-composed.

⊓ ⊔

We now give the lemmas used in the proof of Theorem 5. The following lemma bounds the growth of the functions, that is functional relations recognized by two-way two-tape automata (a similar statement can easily be obtained for alternating two-way two-tape automata with a doubly exponential bound instead). Lemma 6. If f is a function recognized by a two-way two-tape automaton, then there exists k ∈ N such that for all n ∈ N and u ∈ Σ n , one has |f (u)| ≤ 2nk nk+1 , where n k denotes the binomial coefficient. Proof. Let A be a two-way two-tape automaton recognizing a function f . Let n ∈ N, and u ∈ Σ n . Finally, let k be the size of A. Fixing u, we easily build from A a two-way automaton with nk states accepting the singleton language {f (u)}. Now, thanks to a result by Kapoutsis [START_REF] Kapoutsis | Removing bidirectionality from nondeterministic finite automata[END_REF] establishing that any m-state two-way automaton can be transformed into an equivalent equivalent non-deterministic finite automaton with 2m m+1 states, we have that {f (u)} is accepted by a nondeterministic finite automaton with 2nk nk+1 states. As the shortest word accepted by an m-state non-deterministic finite automaton has length at most m, it concludes the proof.

⊓ ⊔

For i ∈ N and n ≥ log 2 (i) let i n ∈ {0, 1} n be the writing of i in base 2 on n bits, with the less significant bit on the left (possibly padded with zeros). For example, 6 5 = 01100. We are now ready to exhibit a function with an exponential growth and recognized by a deterministic two-way two-tape automaton. The proof is based on the concept of so-called synchronous relations. A relation is synchronous if it is recognized by a synchronous transducer, which can be simulated by a two-way two-tape automaton whose two heads always move simultaneously to the right and which accepts once the two inputs words are entirely scanned. An example of such a relation is I = {( i n , i + 1 n ) | n ≥ 1 and 0 ≤ i ≤ 2 n -1} since an integer can deterministically be incremented starting from its less significant digit. Note that a synchronous transducer can always be made deterministic as it is a classical automaton over the product alphabet. Finally, E is recognized by iterating the methods for J (this is made possible thanks to the presence of #) and stopping once the second word is only composed of 1s.

  ⊲}) the transition relation. We use the notation p a1,a2|d1,d2

Fig. 1 .

 1 Fig. 1. Schema of a two-way two-tape finite automaton

Fig. 3 .

 3 Fig. 3. Schema of a 4-way automaton

Fig. 4 .

 4 Fig. 4. Euclidean algorithm (left) and Squares of size 2 n (right)

(a 3 ,Fig. 5 .

 35 Fig. 5. Two identical permutations separated by $s and the corresponding encoding

Lemma 7 .

 7 The functionE = {(w, #w 0 #w 1 # . . . #w 2 |w| -1 #) | w i = i |w| } isrecognizable by a deterministic two-way two-tape automaton.

Lemma 8 .

 8 Let R be a synchronous relation. Then {(w, #u#v#) | (u, v) ∈ R, |w| = |u| = |v|} is recognized by a deterministic two-way two-tape automaton.The rough idea to prove Lemma 8 is to use the first tape to keep track of the position when alternatively reading the u and v part of the word written on the second tape. Now, using Lemma 8 with relation I we conclude that the relationJ = {(w, # i |w| # i + 1 |w| # | 0 ≤ i ≤ 2 |w| -1}is recognizable by a deterministic two-way two-tape automaton.

⋆ funded by the DeLTA project (ANR-16-CE40-0007)