Emmanuel Filiot

Olivier Gauwin

Pierre-Alain Reynier

Frederic Servais

Frédéric Servais

Streamability of Nested Word Transductions

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Memory analysis is an important tool for ensuring system robustness. In this paper we focus on the analysis of programs processing nested words [START_REF] Alur | Adding nesting structure to words[END_REF], i.e., words with a recursive structure, like program traces, XML documents, or more generally unranked trees. On huge inputs, a streaming mode is often used, where the nested word is read only once, from left to right. This corresponds to a depth-first left-to-right traversal when the nested word is considered as a tree. For such programs, dynamic analysis problems have been addressed in various contexts. For instance, runtime verification detects dynamically, and as early as possible, whether a property is satisfied by a program trace [START_REF] Kupferman | Model checking of safety properties[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]. On XML streams, some algorithms outputting nodes selected by an XPath expression at the earliest possible event have also been proposed [START_REF] Benedikt | Efficient and expressive tree filters[END_REF][START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF]. These algorithms allow minimal buffering [START_REF] Bar-Yossef | Buffering in query evaluation over XML streams[END_REF].

In this paper, we investigate static analysis of memory usage for a special kind of programs on nested words, namely programs defined by transducers. We assume that the transducers are functional and non-deterministic. Non-determinism is required as input words are read from left to right in a single pass and some actions may depend on the future of the stream. For instance, the XML transformation language XSLT [START_REF] Clark | XSL Transformations (XSLT) version 1.0, W3C recommendation[END_REF] uses XPath for selecting nodes where local transformations are applied, and XPath queries relies on non-deterministic moves along tree axes, such as a move to any descendant. We require our transducers to be functional, as we are mainly interested by transformation languages like XSLT [START_REF] Clark | XSL Transformations (XSLT) version 1.0, W3C recommendation[END_REF], XQuery [START_REF] Boag | XQuery 1.0: An XML query language[END_REF] and XQuery Update Facility, [20], for which any transformation maps each XML input document to a unique output document.

Visibly pushdown transducers (VPTs) form a subclass of pushdown transducers adequate for dealing with nested words and streaming evaluation, as the input nested word is processed from left to right. They are visibly pushdown automata [START_REF] Alur | Adding nesting structure to words[END_REF] extended with arbitrary output words on transitions. VPTs capture interesting fragments of the aforementioned XML transformation languages that are amenable to efficient streaming evaluation, such as all editing operations (insertion, deletion, and relabeling of nodes, as used for instance in XQuery Update Facility) [20]) under all regular tests. Like for visibly pushdown automata, the stack behavior of VPTs is imposed by the type of symbols read by the transducer. Those restrictions on stack operations allow to decide functionality and equivalence of functional VPTs in PTime and ExpTime respectively [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF]. Some transductions defined by (functional and non-deterministic) VPTs cannot be evaluated efficiently in streaming. For instance, swapping the first and last letter of a word can be defined by a VPT as follows: guess the last letter and transform the first letter into the guessed last letter, keep the value of the first letter in the state, and transform any value in the middle into itself. Any deterministic machine implementing this transformation requires to keep the entire word in memory until the last letter is read. It is not reasonable in practice as for instance XML documents can be very huge.

Our aim is thus to identify decidable classes of transductions for various memory requirements that are suitable to space-efficient streaming evaluation. We first consider the requirement that a transducer can be implemented by a program using a bounded memory (BM), i.e. computing the output word using a memory independent of the size of the input word. However when dealing with nested words in a streaming setting, the bounded memory requirement is quite restrictive. Indeed, even performing such a basic task as checking that a word is well-nested or checking that a nested word belongs to a regular language of nested words requires a memory dependent on the height (the level of nesting) of the input word [21]. This observation leads us to the second question: decide, given a transducer, whether the transduction can be evaluated with a memory that depends only on the size of the transducer and the height of the word (but not on its length). In that case, we say that the transduction is height bounded memory (HBM). This is particularly relevant to XML transformations as XML documents can be very long but have usually a small depth [START_REF] Barbosa | Studying the XML web: Gathering statistics from an xml sample[END_REF]. HBM does not specify how memory depends on the height. A stronger requirement is thus to consider HBM transductions whose evaluation can be done with a memory that depends polynomially on the height of the input word.

Contributions First, we give a general space-efficient evaluation algorithm for functional VPTs. After reading a prefix of an input word, the number of configurations of the (nondeterministic) transducer as well as the number of output candidates to be kept in memory may be exponential in the size of the transducer and the height of the input word (but not in its length). Our algorithm produces as output the longest common prefix of all output candidates, and relies on a compact representation of sets of configurations and remaining output candidates (the original output word without the longest common prefix). We prove that it uses a memory linear in the height of the input word, and linear in the maximal length of a remaining output candidate.

We prove that BM is equivalent to subsequentiability for finite state transducers (FSTs), which is known to be decidable in PTime. BM is however undecidable for arbitrary pushdown transducers but we show that it is decidable for VPTs in coNPTime.

Like BM, HBM is undecidable for arbitrary pushdown transductions. We show, via a nontrivial reduction to the emptiness of pushdown automata with bounded reversal counters, that it is decidable in coNPTime for transductions defined by VPTs. In particular, we show that the previously defined algorithm runs in HBM iff the VPT satisfies some property, which is an extension of the so called twinning property for FSTs [START_REF] Choffrut | Une Caractérisation des Fonctions Séquentielles et des Fonctions Sous-Séquentielles en tant que Relations Rationnelles[END_REF] to nested words. We call it the horizontal twinning property, as it only cares about configurations of the transducers with stack contents of identical height. This property only depends on the transduction, i.e. is preserved by equivalent transducers.

When a VPT-transduction is height bounded memory, the memory needed may be exponential in the height of the word. We introduce a refinement of the twinning property that takes the height of the configurations into account, hence called matched twinning property. A VPT satisfying this property is called twinned. We prove that the evaluation of twinned transductions with our algorithm uses a memory quadratic in the height of the input word. We show that it is decidable in coNPTime whether a VPT is twinned. Moreover, the most challenging result of this paper is to show that being twinned depends only on the transduction and not on the VPT that defines it. Thus, this property indeed defines a class of transductions. As a consequence of this result, all subsequentializable VPTs are twinned, because subsequential VPTs trivially satisfy the matched twinning property. The class of twinned transductions captures a strictly larger class than subsequentializable VPTs while staying in the same complexity class for evaluation, i.e. polynomial space in the height of the input word when the transducer is fixed.

Related Work

In the XML context, visibly pushdown automata based streaming processing has been extensively studied for validating XML streams [START_REF] Kumar | Visibly pushdown automata for streaming XML[END_REF][START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF]21]. The validation problem with bounded memory is studied in [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF] when the input is assumed to be a wellnested word and in [21] when it is assumed to be a well-formed XML document (this problem is still open). Querying XML streams has been considered in [START_REF] Grohe | Tight lower bounds for query processing on streaming and external memory data[END_REF]. It consists in selecting a set of tuples of nodes in the tree representation of the XML document. For monadic queries (selecting nodes instead of tuples), this can be achieved by a functional VPT returning the input stream of tags, annotated with Booleans indicating selection by the query. However, functional VPTs cannot encode queries of arbitrary arities. The setting for functional VPTs is in fact different to query evaluation, because the output has to be produced on-the-fly in the right order, while query evaluation algorithms can output nodes in any order: an incoming input symbol can be immediately output, while another candidate is still to be confirmed. This makes a difference with the notion of concurrency of queries, measuring the minimal amount of candidates to be stored, and for which algorithms and lower bounds have been proposed [START_REF] Bar-Yossef | Buffering in query evaluation over XML streams[END_REF]. VPTs also relate to tree transducers [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF], for which no comparable work on memory requirements is known. However, the height of the input word is known to be a lower bound for Core XPath filters [START_REF] Grohe | Tight lower bounds for query processing on streaming and external memory data[END_REF]. As VPTs can express them, this lower bound also applies when evaluating VPTs. When allowing two-way access on the input stream, space-efficient algorithms for XML validation [START_REF] Konrad | Validating XML documents in the streaming model with external memory[END_REF] and querying [START_REF] Madhusudan | Query automata for nested words[END_REF] have been proposed.

Visibly Pushdown Languages and Transductions

Words and nested words In this paper, we consider nested words accessed in streaming. Their nesting structure is thus discovered on-the-fly, so we consider a finite alphabet Σ partitioned into three disjoint sets Σ c , Σ r and Σ ι , denoting respectively the call, return and internal alphabets. We denote by Σ * the set of (finite) words over Σ and by ǫ the empty word. The length of a word u is denoted by |u|. For all words u, v ∈ Σ * , we denote by u ∧ v the longest common prefix of u and v. More generally, for any non-empty finite set of words V ⊆ Σ * , the longest common prefix of V , denoted by lcp(V ), is inductively defined by lcp({u}) = u and lcp(V ∪ {u}) = lcp(V ) ∧ u. The set of well-nested words Σ * wn is the smallest subset of Σ * such that Σ * ι ⊆ Σ * wn and for all c ∈ Σ c , all r ∈ Σ r , all u, v ∈ Σ * wn , cur ∈ Σ * wn and uv ∈ Σ * wn . Let u = α 1 . . . α n ∈ Σ * be a prefix of a well-nested word. A position i ∈ {1, . . . , n} is a pending call if α i ∈ Σ c and for all j ≥ i, α i . . . α j ∈ Σ * wn . The height of u is the maximal number of pending calls on any prefix of u, i.e.

h(u) = max 1≤i≤n |{k | 1 ≤ k ≤ i, α k is a pending call of α 1 . . . α i }| For instance, h(crcrcc) = h(ccrcrr) = 2.
In particular, for well-nested words, the height corresponds to the usual height of the nesting structure of the word.

Given two words u, v ∈ Σ * , the delay of u and v, denoted by ∆(u, v), is the unique pair of words (u ′ , v ′ ) such that u = (u ∧ v)u ′ and v = (u ∧ v)v ′ . For instance, ∆(abc, abde) = (c, de). Informally, in a word transduction, if there are two output candidates u and v during the evaluation, we are sure that we can output u ∧ v and ∆(u, v) is the remaining suffixes we still keep in memory.

Visibly pushdown transducers (VPTs)

As finite-state transducers extend finite-state automata with outputs, visibly pushdown transducers extend visibly pushdown automata [START_REF] Alur | Adding nesting structure to words[END_REF] with outputs [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF]. To simplify notations, we suppose that the output alphabet is Σ, but our results still hold for an arbitrary output alphabet. Informally, the stack behavior of a VPT is similar to the stack behavior of visibly pushdown automata (VPA). On a call symbol, the VPT pushes a symbol on the stack and produces some output word (possibly empty), on a return symbol, it must pop the top symbol of the stack and produce some output word (possibly empty) and on an internal symbol, the stack remains unchanged and it produces some output word. Formally:

◮ Definition 1. A visibly pushdown transducer (VPT) on finite words over Σ is a tuple T = (Q, I, F, Γ, δ) where Q is a finite set of states, I ⊆ Q is the set of initial states, F ⊆ Q the set of final states, Γ is the stack alphabet, δ = δ c ⊎ δ r ⊎ δ ι the (finite) transition relation, with δ c ⊆ Q × Σ c × Σ * × Γ × Q, δ r ⊆ Q × Σ r × Σ * × Γ × Q, and δ ι ⊆ Q × Σ ι × Σ * × Q. A configuration of a VPT is a pair (q, σ) ∈ Q×Γ * . A run of T on a word u = a 1 . . . a l ∈ Σ * from a configuration (q, σ) to a configuration (q ′ , σ ′ ) is a finite sequence ρ = {(q k , σ k )} 0≤k≤l such that q 0 = q, σ 0 = σ, q l = q ′ , σ l = σ ′ and for each 1 ≤ k ≤ l, there exist v k ∈ Σ * and γ k ∈ Γ such that either (q k-1 , a k , v k , γ k , q k ) ∈ δ c and σ k = σ k-1 γ k or (q k-1 , a k , v k , γ k , q k ) ∈ δ r and σ k-1 = σ k γ k , or (q k-1 , a k , v k , q k ) ∈ δ ι and σ k = σ k-1 . The word v = v 1 . . . v l is
called an output of ρ. We write (q, σ) u/v --→ (q ′ , σ ′ ) when there exists a run on u from (q, σ) to (q ′ , σ ′ ) producing v as output. We denote by ⊥ the empty word on Γ. A configuration (q, σ) is accessible (resp. is co-accessible) if there exist u, v ∈ Σ * and q 0 ∈ I (resp. q f ∈ F ) such that (q 0 , ⊥)

u/v --→ (q, σ) (resp. such that (q, σ) u/v --→ (q f , ⊥))
. A transducer T is reduced if every accessible configuration is co-accessible. Given any VPT, computing an equivalent reduced VPT can be performed in polynomial time [START_REF] Caralp | A polynomial procedure for trimming visibly pushdown automata[END_REF] 1 . A transducer T defines the binary

word relation T = {(u, v) ∈ Σ * × Σ * | ∃q ∈ I, q ′ ∈ F, (q, ⊥) u/v --→ (q ′ , ⊥)}. A transduction is a binary relation R ⊆ Σ * × Σ * .
We say that a transduction R is a VPT-transduction if there exists a VPT T such that R = T . For any input word u ∈ Σ * , we denote by R(u) the set {v | (u, v) ∈ R}. Similarly, for a VPT T , we denote by T (u) the set T (u). A transduction R is functional if for all u ∈ Σ * , R(u) has size at most one. If R is functional, we identify R(u) with the unique image of u if it exists. A VPT T is functional if T is functional, and this can be decided in PTime [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF]. The class of functional VPTs is denoted by fVPT. The domain of T (denoted by Dom(T )) is the domain of T . The domain of T contains only well-nested words, which is not necessarily the case of the codomain.

◮ Example 2. Consider the VPT T of Fig. 1 represented in plain arrows. The left and right parts accept the same input words except for the last letter of the word. The domain of T is 1 The reduction of VPAs in [START_REF] Caralp | A polynomial procedure for trimming visibly pushdown automata[END_REF] trivially extends to VPTs.

i p 3 p 2 p 1 q 3 q 1 q 2 c/a, γ r/c, γ r/c, γ c/b, γ r/c, γ r ′ /c, γ c/a, γ r/c, γ c/b, γ r/c, γ c/b, γ c/a, γ
Dom(T ) = {c n r n | n ≥ 2} ∪ {cc n r n r ′ | n ≥ 1}.
Any word c n r n is translated into a n c n , and any word cc n r n r ′ is translated into b n+1 c n+1 . Therefore the translation of the first sequence of calls depends on the last letter r or r ′ . This transformation cannot be evaluated with a bounded amount of memory, but with a memory which depends on the height n of the input word.

Finite state transducers (FSTs)

A finite state transducer (FST) on an alphabet Σ is a tuple (Q, I, F, δ) where Q is a finite set, I, F ⊆ Q and δ ⊆ Q × Σ × Σ * × Q with the standard semantics. This definition corresponds to the usual definition of real-time FSTs, as there is no ǫ-transitions. We always consider real-time FSTs in this paper, so we just call them FSTs.

A subsequential FST (resp. VPT) is a pair (T, Ψ) where T is an (input) deterministic FST (resp. VPT) and Ψ : F → Σ * . The outputs of u by (T, Ψ) are the words v.Ψ(q) whenever there is a run of T on u producing v and ending up in some accepting state q.

Given an integer k ∈ N and a VPT T , one can define an FST, denoted by FST(T, k), which is the restriction of T to input words of height less than k. The transducer is naturally constructed by taking as states the configurations (q, σ) of T such that |σ| ≤ k.

Turing Transducers

In order to formally define the complexity classes for evaluation that we target, we introduce a deterministic computational model for word transductions that we call Turing Transducers. Turing transducers have three tapes: one read-only left-toright input tape, one write-only left-to-right output tape, and one standard working tape. Such a machine naturally defines a transduction: the input word is initially on the input tape, and the result of the transduction is the word written on the output tape after the machine terminates in an accepting state. We denote by M the transduction defined by M . The space complexity is measured on the working tape only.

Online Evaluation Algorithm of VPT-Transductions

We present an online algorithm LcpIn to evaluate functional word transductions defined by fVPTs. For clarity, we present this algorithm under some assumptions, without loss of generality. First, input words of our algorithms are words u ∈ Σ * concatenated with a special symbol $ / ∈ Σ, denoting the end of the word. Second, we only consider input words without internal symbols, as they can easily be encoded by successive call and return symbols. Third, input words are supposed to be valid, in the sense that they produce an output. It is indeed easy to extend our algorithms in order to raise an error message when the input is not in the domain, i.e. when no run of the VPT applies on the input.

The core task of this algorithm is to maintain the configuration for each run of the fVPT T on the input u, and produce its output on-the-fly. Therefore, the algorithm LcpIn only applies on reduced fVPTs. Indeed, as T is reduced, functionality ensures that, for a given input word u, and for every accessible configuration (q, σ) of T , there is at most one v such that (q i , ⊥) u/v --→ (q, σ) with q i ∈ I. Hence, a configuration is a triple (q, σ, w) where q is the current state of the run, σ its corresponding stack content, and w the part of the output that has been read but not output yet. We call such a configuration d-configuration and write Dconfs(T ) = Q × Γ * × Σ * for the set of d-configurations of T . Algorithm LcpIn relies on two main features.

q 0 q 1 c/a, γ 1 c/b, γ 2 r 1 /ε, γ 1 r 1 /ε, γ 1 r 2 /ε, γ 2 (
Compact representation First, the set of current d-configurations is stored in a compact structure that shares common stack contents. Consider for instance the VPT T 1 in Fig. 2a. After reading cc, current d-configurations are {(q 0 , γ 1 γ 1 , aa), (q 0 , γ 1 γ 2 , ab), (q 0 , γ 2 γ 1 , ba), (q 0 , γ 2 γ 2 , bb)}. Hence after reading c n , the number of current d-configurations is 2 n . However, the transition used to update a d-configuration relates the stack symbol and the output word. For instance, the previous set is the set of tuples (q 0 , η

1 η 2 , α 1 α 2 ) where (η i , α i ) is either (γ 1 , a) or (γ 2 , b).
Based on this observation, we propose a data structure avoiding this blowup. As illustrated in Fig. 2b to 2d, this structure is a directed acyclic graph (DAG). Nodes of this DAG are tuples (q, γ, i) where q ∈ Q, γ ∈ Γ and i ∈ N is the depth of the node in the DAG. Each edge of the DAG is labelled with a word, so that a branch of this DAG, read from the root # to the leaf, represents a d-configuration (q, σ, v): q is the state in the leaf, σ is the concatenation of stack symbols in traversed nodes, and v is the concatenation of words on edges. For instance, in the DAG of Fig. 2c, the branch # -→ (q 0 , ⊥, 0) b -→ (q 0 , γ 2 , 1) a -→ (q 0 , γ 1 , 2) encodes the d-configuration (q 0 , γ 2 γ 1 , ba) of the VPT of Fig. 2.(a). However, this data structure cannot store any set of accessible dconfigurations of arbitrary functional VPTs: at most one delay w has to be assigned to a d-configuration. This is why we need T to be reduced.

Computing outputs Second, after reading a prefix u ′ of a word u, LcpIn will have output the common prefix of all corresponding runs, i.e. lcp in (u ′ , T ) = lcp(reach(u ′ )) where

reach(u ′ ) = {v | ∃(q 0 , q, σ) ∈ I × Q × Γ * , (q 0 , ⊥) u ′ /v ---→ (q, σ)}.
When a new input symbol is read, the DAG is first updated. Then, a bottom-up pass on this DAG computes lcp in (u ′ , T ) in the following way. For each node, let ℓ be the largest common prefix of labels of outgoing edges. Then ℓ is removed from these outgoing edges, and concatenated at the end of labels of incoming edges. At the end, the largest common prefix of all output words on branches is the largest common prefix of words on edges outgoing from the root node #.

Let out = (u ′ ) be the maximal size of outputs of T on u ′ where their common prefix is removed: out = (u ′ ) = max v∈reach(u ′ ) |v| -|lcp in (u ′ , T )| and out max = (u) its maximal value over prefixes of u: out max = (u) = max u ′ prefix of u out = (u ′ ). To summarize, one can in polynomial time reduce T if necessary, and then build the Turing transducer associated with the algorithm LcpIn. We prove the following complexity result: ◮ Proposition 3. Given an fVPT T , one can build in PTime a Turing transducer, denoted LcpInTT(T ), which, on an input stream u ∈ Σ * , runs in space complexity O((h(u) + 1) • out max = (u)).

In addition, when T is reduced, we can detail how the constant depends on the size of T . The space used by LcpInTT(T ) for computing

T (u) is in O(|Q| 2 • |Γ| 2 • (h(u) + 1) • out max = (u)).

Bounded Memory Evaluation Problems

Bounded Memory Transductions

We first consider transductions that can be evaluated with a constant amount of memory if we fix the machine that defines the transduction:

◮ Definition 4. A (functional) transduction R ⊆ Σ * × Σ * is bounded memory (BM)
if there exists a Turing transducer M and K ∈ N such that M = R and on any input word u ∈ Σ * , M runs in space complexity at most K.

It is not difficult (see Appendix B) to verify that for FST-transductions, bounded memory is characterized by subsequentializability, which is decidable in PTime [22]. Moreover, BM is undecidable for pushdown transducers, since it is as difficult as deciding whether a pushdown automaton defines a regular language. For VPTs, BM is quite restrictive as it imposes to verify whether a word is well-nested by using a bounded amount of memory. This can be done only if the height of the words of the domain is bounded by some constant which depends on the transducer only: ◮ Proposition 5. Let T be a functional VPT with n states.

1. T is BM iff (i) for all u ∈ Dom(T ), h(u) ≤ n 2 , and (ii) FST(T, n 2 ) is BM; 2. It is decidable in coNPTime whether T is BM.
Sketch. The first assertion is obvious by using simple pumping techniques to show that bounded memory implies bounded height. In the sequel, we define the class of height bounded memory transductions, and show it is decidable in coNPTime. On words of bounded height, this class collapses with bounded memory transductions. ◭

Height Bounded Memory Transductions

As we have seen, bounded memory is too restrictive to still benefit from the extra expressiveness of VPT compared to FST, namely the ability to recognize nested words of unbounded height. In this section, we define a notion of bounded memory which is well-suited to VPTs.

◮ Definition 6. A (functional) transduction R ⊆ Σ * × Σ * is height bounded memory (HBM)
if there exists a Turing transducer M and a function f : N → N such that M = R and on any input word u ∈ Σ * , M runs in space at most f (h(u)).

Note that this definition ensures that the machine cannot store all the input words on the working tape in general. The VPT in Fig. 2a is not in BM, but is in HBM: the stack content suffices (and is necessary) to determine the output. When the structured alphabet contains only internal letters, HBM and BM coincide, thus it is undecidable whether a pushdown transducer is HBM. The remainder of this section is devoted to the proof that HBM is decidable for fVPTs.

BM functional FST-transductions (or equivalently subsequentializable FSTs) are characterized by the so called twinning property [START_REF] Choffrut | Une Caractérisation des Fonctions Séquentielles et des Fonctions Sous-Séquentielles en tant que Relations Rationnelles[END_REF], which is decidable in PTime [22]. We introduce a similar characterization of HBM fVPTs-transductions, called the horizontal twinning property (HTP). The restriction of the horizontal twinning property to FSTs is equivalent to the usual twinning property for FSTs (see Appendix C.1). Intuitively, the HTP requires that two runs on the same input cannot accumulate increasing output delay on loops. ◮ Definition 7. Let T be an fVPT. T satisfies the horizontal twinning property (HTP) if for all u 1 , u 2 , v 1 , v 2 , w 1 , w 2 ∈ Σ * such that u 2 is well-nested, for all q 0 , q ′ 0 ∈ I, for all q, q ′ ∈ Q, and for all σ, σ ′ ∈ Γ * such that (q, σ) and (q ′ , σ ′ ) are co-accessible, if

   (q 0 , ⊥) u1/v1 ----→ (q, σ) u2/v2 ----→ (q, σ) (q ′ 0 , ⊥) u1/w1 ----→ (q ′ , σ ′ ) u2/w2 ----→ (q ′ , σ ′ ) (1) then ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ).
◮ Example 8. Consider the VPT of Fig. 1 (including dashed arrows). It does not satisfy the HTP, as the delays increase when looping on crcr... Without the dashed transitions, the HTP is satisfied.

◮ Lemma 9. The HTP is decidable in coNPTime for fVPTs.

Proof. First, let us show that an fVPT T does not satisfy the HTP if and only if there exist

u 1 , u 2 , v 1 , v 2 , w 1 , w 2 ∈ Σ * , q 0 , q ′ 0 ∈ I, q, q ′ ∈
Q, and σ, σ ′ ∈ Γ * such that (q, σ) and (q ′ , σ ′ ) are co-accessible, satisfy [START_REF] Alur | Streaming tree transducers[END_REF], and such that either we have (i)

|v 2 | = |w 2 |, or (ii) |v 2 | = |w 2 |, |v 1 | ≤ |w 1 | and not v 1 v 2 w 1 w 2 .
Indeed, one can easily check that it is a necessary condition. To prove that it is a sufficient condition, suppose we have elements that satisfy (1) with ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ) but conditions (i) and (ii) do not hold. Wlog, we can assume that

|v 1 | ≤ |w 1 |, therefore we have |v 2 | = |w 2 |, |v 1 | ≤ |w 1 |, v 1 v 2 w 1 w 2 and ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 )
. One can verify that there exists k ∈ N such that replacing u 2 with u ′ 2 = u 2 k yields a system that satisfies (ii). We refer the reader to Appendix C.2 for the details.

Second, let T be an fVPT, we define a pushdown automaton with bounded reversal counters [START_REF] Harju | Some decision problems concerning semilinearity and commutation[END_REF], A, such that the language of A is empty if and only if T satisfies the HTP. More precisely, A accepts the words u = u 1 u 2 u 3 ∈ Dom(T ) such that there exist v 1 , v 2 , w 1 , w 2 ∈ Σ * , q 0 , q ′ 0 ∈ I, q, q ′ ∈ Q, and σ, σ ′ ∈ Γ * that satisfy (1) and either (i) or (ii). A simulates in parallel any two runs of T on the input word (product automaton). It guesses the end of u 1 and stores the states q and q ′ of the first and second run (in order to be able to check that the simulated runs of T are in state q, resp. q ′ after reading u 2 ). Non-deterministically, it checks whether (i) or (ii) holds. To check (i), it uses two counters, one for each run. It does so by, after reading u 1 , increasing the counters by the length of the output word of each transition of the corresponding run. Then, when reaching the end of u 2 it checks that both counters are different (by decreasing in parallel both counters and checking they do not reach 0). Similarly, using two other counters, A checks that (ii) holds as follows. Note that condition (ii) implies that there is a position p such that the p-th letter a 1 of v 1 v 2 and the p-th letter a 2 of w 1 w 2 are different. The automaton A guesses the position p ∈ N of the mismatch, and initializes both counters to the value p. Then, while reading u 1 u 2 , it decreases each counter by the length of the output words of the corresponding run. When a counter reaches 0, A stores the output letter of the corresponding run. Finally, A checks that a 1 = a 2 , and that both configurations are co-accessible. T satisfies the HTP iff the language of A is empty. The latter is decidable in coNPTime [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF].

◭

We now show that HTP characterizes HBM fVPTs-transductions and therefore by Lemma 9 we get:

◮ Theorem 10. Let T be an fVPT. Then T is HBM iff the HTP holds for T , which is decidable in coNPTime. In this case, the Turing transducer LcpInTT(T ) runs, on an input stream u, in space complexity exponential in the height of u.

We can state more precisely the space complexity of LcpInTT(T ) when T is reduced. In this case, it is in

O(|Q| 4 •|Γ| 2h(u)+2 •(h(u)+1)•M ), where M = max{|v| | (q, a, v, γ, q ′ ) ∈ δ}.
Sketch. We prove that T is HBM iff the HTP holds for T . To prove that the HTP is a necessary condition to be in HBM, we proceed by contradiction. We find a counter-example for the HTP and we let K be the height of the input word of this counter-example. It implies that the twinning property for FSTs does not hold for FST(T, K), and therefore FST(T, K) is not BM by Proposition 5. In particular, T is not HBM.

For the converse, it can easily be shown that when T satisfies the HTP, the procedure of [START_REF] Caralp | A polynomial procedure for trimming visibly pushdown automata[END_REF] that reduces T preserves the HTP satisfiability. In particular, there is a one-to-one mapping between the runs of T and the runs of its reduction that preserves the output words. We then show that for any input word u ∈ Σ * , the maximal delay out max = (u) between the outputs of u is bounded by (|Q| • |Γ| h(u) ) 2 M . This is done by a pumping technique "by width" that relies on the property ∆(vv ′ , ww ′ ) = ∆(∆(v, w) • (v ′ , w ′ )) for any words v, v ′ , w, w ′ . Thus for an input word for which there are two runs that pass by the same configurations twice at the same respective positions, the delay of the output is equal to the delay when removing the part in between the identical configurations. Finally we apply Proposition 3.

◭ HBM is tight Theorem 10 shows that the space complexity of a VPT in HBM is at most exponential. We give here an example illustrating the tightness of this bound. The idea is to encode the tree transduction

f (t, a) → f (t, a) ∪ f (t, b) → f (t, b
) by a VPT, where t is a binary tree over {0, 1} and t is the mirror of t, obtained by replacing the 0 by 1 and the 1 by 0 in t. Thus taking the identity or the mirror depends on the second child of the root f . To evaluate this transformation in a streaming manner, one has to store the whole subtree t in memory before deciding to transform it into t or t. The evaluation of this transduction cannot be done in polynomial space as there are a doubly exponential number of trees of height n, for all n ≥ 0.

HBM vs Subsequentializable fVPTs

We have seen that a functional transduction defined by an FST T is BM iff T is subsequentializable. We give an example illustrating that for VPTs, being subsequentializable is too strong to characterize HBM. Consider the VPT of Fig. 1 defined by the plain arrows. The transduction it defines is in HBM by Proposition 3, as at any time the delay between two outputs is bounded by the height of the input: out max = (u)≤2h(u). However it is not subsequentializable, as the transformation of c into a or b depends on the last return.

Quadratic Height Bounded Memory Evaluation

In the previous section, we have shown that a VPT-transduction is in HBM iff the horizontal twinning property holds, and if it is in HBM, the algorithm of Section 3 uses a memory at most exponential in the height of the word, and this bound is tight. To avoid this exponential cost, we identify in this section a subclass of HBM containing transductions for which the evaluation algorithm of Section 3 uses a memory quadratic in the height of the word. Therefore, we strengthen the horizontal twinning property by adding some properties for well-matched loops. Some of our main and challenging results are to show the decidability of this property and that it depends only on the transduction, i.e. is preserved by equivalent transducers. We show that subsequential VPTs satisfy this condition and therefore our class subsumes the class of subsequentializable transducers. The property is a strengthening of the horizontal twinning property that we call the matched twinning property (MTP). Intuitively, the MTP requires that two runs on the same input cannot accumulate increasing output delay on well-matched loops. They can accumulate delay on loops with increasing stack but this delay has to be caught up on the matching loops with descending stack. ◮ Definition 11. Let T = (Q, I, F, Γ, δ) be an fVPT. T satisfies the matched twinning property (MTP) if for all u i , v i , w i ∈ Σ * (i ∈ {1, . . . , 4}) such that u 3 is well-nested, and u 2 u 4 is well-nested, for all i, i ′ ∈ I, for all p, q, p ′ , q ′ ∈ Q, and for all σ 1 , σ 2 ∈ ⊥.Γ * , for all σ ′ 1 , σ ′ 2 ∈ Γ * , such that (q, σ 1 ) and (q ′ , σ 2 ) are co-accessible:

if    (i, ⊥) u1/v1 ----→ (p, σ 1 ) u2/v2 ----→ (p, σ 1 σ ′ 1 ) u3/v3 ----→ (q, σ 1 σ ′ 1 ) u4/v4 ----→ (q, σ 1 ) (i ′ , ⊥) u1/w1 ----→ (p ′ , σ 2 ) u2/w2 ----→ (p ′ , σ 2 σ ′ 2 ) u3/w3 ----→ (q ′ , σ 2 σ ′ 2 ) u4/w4 ----→ (q ′ , σ 2 ) then ∆(v 1 v 3 , w 1 w 3 ) = ∆(v 1 v 2 v 3 v 4 , w 1 w 2 w 3 w 4 )
. We say that a VPT T is twinned whenever it satisfies the MTP.

Note that any twinned VPT also satisfies the HTP (with

u 3 = u 4 = ǫ).
◮ Example 12. The VPT of Fig. 1 with plain arrows does not satisfy the MTP, as the delay between the two branches increases when iterating the loops. Consider now the VPT obtained by replacing r by r ′ in the transition (q 1 , r, c, γ, q 2 ). It is obviously twinned, as we cannot construct two runs on the same input which have the form given in the premises of the MTP. However this transducer is not subsequentializable, as the output on the call symbols cannot be delayed to the matching return symbols.

As for the HTP, we can decide the MTP using a reduction to the emptiness of a pushdown automaton with bounded reversal counters. A complete proof can be found in Appendix D.

◮ Lemma 13. The matched twinning property is decidable in coNPTime for fVPTs.

The most challenging result of this paper is to show that the MTP only depends on the transduction and not on the transducer that defines it. The proof relies on fundamental properties of word combinatorics that allow us to give a general form of the output words v 1 , v 2 , v 3 , v 4 , w 1 , w 2 , w 3 , w 4 involved in the MTP, that relates them by means of conjugacy of their primitive roots. The proof gives a deep insight into the expressive power of VPTs which is also interesting on its own. As many results of word combinatorics, the proof is a long case study, so that we give it in Appendix D.2 only.

◮ Theorem 14. Let T 1 , T 2 be fVPTs such that T 1 = T 2 . T 1 is twinned iff T 2 is twinned.
Sketch. We assume that T 1 is not twinned and show that T 2 is not twinned either. By definition of the MTP there are two runs of the form

   (i 1 , ⊥) u1/v1 ----→ (p 1 , σ 1 ) u2/v2 ----→ (p 1 , σ 1 β 1 ) u3/v3 ----→ (q 1 , σ 1 β 1 ) u4/v4 ----→ (q 1 , σ 1 ) (i ′ 1 , ⊥) u1/v ′ 1 ----→ (p ′ 1 , σ ′ 1 ) u2/v ′ 2 ----→ (p ′ 1 , σ ′ 1 β ′ 1 ) u3/v ′ 3 ----→ (q ′ 1 , σ ′ 1 β ′ 1 ) u4/v ′ 4 ----→ (q ′ 1 , σ ′ 1 )
such that (q 1 , σ 1 ) and (q ′ 1 , σ ′ 1 ) are co-accessible and ∆(v

1 v 3 , v ′ 1 v ′ 3 ) = ∆(v 1 v 2 v 3 v 4 , v ′ 1 v ′ 2 v ′ 3 v ′ 4
). We will prove that by pumping the loops on u 2 and u 4 sufficiently many times we will get a similar situation in T 2 , proving that T 2 is not twinned. It is easy to show that there exist

k 2 > 0, k 1 , k 3 ≥ 0, w i , w ′ i ∈ Σ * , i ∈ {1, . . . , 4}, some states i 2 , p 2 , q 2 , i ′ 2 , p ′ 2 , q ′ 2 of T 2 and some stack contents σ 2 , β 2 , σ ′ 2 , γ ′ 2 of T 2 such that we have the following runs in T 2 :    (i2, ⊥) u 1 u k 1 2 /w 1 ------→ (p2, σ2) u k 2 2 /w 2 -----→ (p2, σ2β2) u k 3 2 u 3 u k 3 4 /w 3 ---------→ (q2, σ2β2) u k 2 4 /w 4 -----→ (q2, σ2) (i ′ 2 , ⊥) u 1 u k 1 2 /w ′ 1 ------→ (p ′ 2 , σ ′ 2 ) u k 2 2 /w ′ 2 -----→ (p ′ 2 , σ ′ 2 β ′ 2 ) u k 3 2 u 3 u k 3 4 /w ′ 3 ---------→ (q ′ 2 , σ ′ 2 β ′ 2 ) u k 2 4 /w ′ 4 -----→ (q ′ 2 , σ ′ 2 )
such that (q 1 , σ 1 ) and (q 2 , σ 2 ) are co-accessible with the same input word u 5 , and (q ′ 1 , σ ′ 1 ) and (q ′ 2 , σ ′ 2 ) are co-accessible with the same input word u ′ 5 . Now for all i ≥ 0, we let

V (i) = v 1 (v 2 ) k1+ik2+k3 v 3 (v 4 ) k1+ik2+k3 W (i) = w 1 (w 2 ) i w 3 (w 4 ) i V ′(i) = v ′ 1 (v ′ 2 ) k1+ik2+k3 v ′ 3 (v ′ 4 ) k1+ik2+k3 W ′(i) = w ′ 1 (w ′ 2 ) i w ′ 3 (w ′ 4 ) i D 1 (i) = ∆(V (i) , V ′(i) ) D 2 (i) = ∆(W (i) , W ′(i) )
In other words, D 1 (i) (resp. D 2 (i)) is the delay in T 1 (resp. T 2 ) accumulated on the input word u 1 (u 2 ) k1+ik2+k3 u 3 (u 4 ) k1+ik2+k3 by the two runs of T 1 (resp. T 2 ). There is a relation between the words V (i) and W (i) . Indeed, since T 1 and T 2 are equivalent and (q 1 , σ 1 ) and (q 2 , σ 2 ) are both co-accessible by the same input word, for all i ≥ 1, either

V (i) is a prefix of W (i) or W (i) is a prefix of V (i) .
We have a similar relation between V ′(i) and W ′(i) . We prove in Appendix the following intermediate results: (i) there exists i 0 ≥ 0 such that for all i, j ≥ i 0 such that i = j, D

1 (i) = D 1 (j); (ii) for all i, j ≥ 1, if D 1 (i) = D 1 (j), then D 2 (i) = D 2 (j).
The proofs of those results rely on fundamental properties of word combinatorics and a non-trivial case study that depends on how the words v 1 (v 2 ) k1+ik2+k3 v 3 (v 4 ) k1+ik2+k3 and w 1 (w 2 ) i w 3 (w 4 ) i are overlapping. Thanks to (i) and (ii), we clearly get that D 2 (i 0 ) = D 2 (i 0 + 1), which provides a counter-example for the matched twinning property. ◭ Subsequential transducers have at most one run per input word, so we get the following:

◮ Corollary 15. Subsequentializable VPTs are twinned.
The MTP is not a sufficient condition to be subsequentializable, as shown for instance by Example 12. Therefore the class of transductions defined by transducers which satisfy the MTP is strictly larger than the class of transductions defined by subsequentializable transducers. However, these transductions are in the same complexity class for evaluation, i.e. polynomial space in the height of the input word for a fixed transducer: ◮ Theorem 16. Let T be an fVPT. If T is twinned, then the Turing transducer LcpInTT(T ) runs, on an input stream u, in space complexity quadratic in the height of u.

We can state more precisely the space complexity of LcpInTT(T ) when T is reduced. In this case, it is in

O |Q| 4 • |Γ| 2|Q| 4 +2 • (h(u) + 1) 2 • M , where M = max{|v| : (q, a, v, γ, q ′ ) ∈ δ}.
Sketch. Like for the HTP, when T satisfies the MTP, also does the reduced VPT returned by the reduction procedure of [START_REF] Caralp | A polynomial procedure for trimming visibly pushdown automata[END_REF]. We use a pumping technique to show that for any word u ∈ Σ * on which there is a run of T , we have out max = (u) ≤ (h(u) + 1)q(T ) for some function q, whenever the MTP holds for T . This is done as follows: any such word can be uniquely decomposed as u = u 0 c 1 u 1 c 2 . . . c n u n with n ≤ h(u), each u i is well-nested and each c i is a call. Then if the u i are long enough, we can pump them vertically and horizontally without affecting the global delay, by using the property ∆(vv ′ , ww ′ ) = ∆(∆(v, w).(v ′ , w ′ )). Then we can apply Proposition 3. ◭

Conclusion and Remarks

This work investigates the streaming evaluation of nested word transductions, and in particular identifies an interesting class of VPT-transductions which subsumes subsequentializable transductions and can still be efficiently evaluated. The following inclusions summarize the relations between the different classes of transductions we have studied:

BM fVPTs Subsequentializable VPTs twinned fVPTs HBM fVPTs fVPTs Moreover, we have shown that BM, twinned and HBM fVPTs are decidable in coNPTime.

Further Directions An important asset of the class of twinned fVPTs w.r.t. the class of subsequentializable VPTs is that it is decidable. It would thus be interesting to determine whether or not the class of subsequentializable VPTs is decidable. In addition, we also plan to extend our techniques to more expressive transducers, such as those recently introduced in [START_REF] Alur | Streaming tree transducers[END_REF], which extend VPTs with global variables and are as expressive as MSO-transductions, and can therefore swap or reverse sub-trees. Another line of work concerns the extension of our evaluation procedure, which holds for functional transductions, to finite valued transductions.

A Online Evaluation Algorithm of Visibly Pushdown Transductions

All over this section we assume an implementation of VPTs such that the set S of transitions with a given left-hand side can be retrieved in time O(|S|). Recall also that for the presentation of this algorithm, the VPT must be reduced. We define the current height of a prefix of a nested word in the following way: hc(u) = 0 if u is well-nested, and hc(ucv) = hc(u) + 1 if c ∈ Σ c and v is well-nested.

A.1 Naive algorithm

We start with the algorithm Naive, that we will later improve to obtain LcpIn. The algorithm Naive simply computes all the runs (with their respective outputs) of the fVPT T on the input word u, stores them in a data structure and, at the end of u, outputs the only output word: it will be the same in all accepting runs, as T is functional.

Naive consists in maintaining the set of d-configurations corresponding to the runs of T on the input word u. Hence, it is based on the operation update(C, a) that returns the set of d-configurations obtained after applying rules of T using input symbol a to each d-configuration of C. The function update : Dconfs(T ) × Σ → Dconfs(T ) maps a set of d-configurations and an input symbol to another set of d-configurations. For call symbols

c ∈ Σ c , update(C, c) = (q,σ,v)∈C {(q ′ , σγ, vv ′ ) | (q, c, v ′ , γ, q ′ ) ∈ δ c } and for return symbols r ∈ Σ r , update(C, r) = (q,σγ,v)∈C {(q ′ , σ, vv ′ ) | (q, r, v ′ , γ, q ′ ) ∈ δ r }
The function update can be considered as the transition function of a transition system with states Dconfs(T ) (i.e. an infinite number of states). We can easily turn it into an infinite state transducer, i.e. an FST with infinitely many states: this transducer returns ǫ at every input symbol, except for the last one $, where it returns the output word. This is illustrated in Fig. 3. Formally, an infinite state transducer t (IST for short) is defined

q 0 q 1 c/a, γ 1 c/b, γ 2 r 1 /ε, γ 1 r 1 /ε, γ 1 r 2 /ε, γ 2 (a) A VPT T1.
(q 0 , ⊥, ε) exactly like an FST, except that its number of states may be infinite (but countable). In particular, the acceptance condition remains the same, so that the transduction t is still a set of pairs of finite words (u, v).

(q 0 , γ 1 , a) (q 0 , γ 2 , b) (q 0 , γ 1 γ 1 , aa) (q 0 , γ 1 γ 2 , ab) (q 0 , γ 2 γ 1 , ba) (q 0 , γ 2 γ 2 , bb) (q 1 , γ 1 , aa) (q 1 , γ 2 , ba) (q 1 , ⊥, ba) q f c/ε c/ε r 1 /ε r 2 /ε $/ba
Given the functional VPT T = (Q, I, F, Γ, δ), consider the IST t = (Dconfs(T )⊎{q f }, I t , {q f }, δ t ) where I t = {{(q 0 , ⊥, ǫ) | q 0 ∈ I}}. To deal with the last symbol $, we have to characterize the sets of d-configurations reached after reading words in Dom(T ). T being functional, each of these sets of d-configurations C comes with a single output word v:

C = (C, v) ∈ Dconfs(T ) × Σ * | ∃q ∈ F. (q, ⊥, v) ∈ C and ∀(q ′ , ⊥, v ′ ) ∈ C, q ′ ∈ F =⇒ v ′ = v
Rules in δ t are:

C a/ǫ --→ update(C, a) for C ∈ Dconfs(T ) and a ∈ Σ C $/v --→ q f for (C, v) ∈ C ◮ Lemma 17. (u, v) ∈ T iff (u$, v) ∈ t .
Proof. It can be checked easily by induction on |u| that for every u ∈ Σ * , the current state of

t after reading u is q0∈I {(q, σ, v) | (q 0 , ⊥) u/v
--→ (q, σ)}. Let us check whether reading the last symbol $ leads to a correct state. Let u ∈ Σ * . If u / ∈ Dom(T ), then there is no run of T on u of the form (q, ⊥)

u/v
--→ (q ′ , ⊥) with q ∈ I and q ′ ∈ F . Hence, the state C reached by t after reading u, if it exists, is such that

(C, v) / ∈ C for all v ∈ Σ * , so u / ∈ Dom(t). If u ∈ Dom(T ),
then the state of t reached after reading

u is C = q0∈I {(q, ⊥, v) | (q 0 , ⊥) u/v
--→ (q, ⊥)}. As T is functional, there is a unique v for all (q, ⊥, v) ∈ C such that q ∈ F , and such elements of C exist, so that (C, v) ∈ C, and (u$, v) ∈ t . ◭

As t is deterministic, the algorithm Naive only consists in computing the unique run of t on the input word u. Let out(u) = max v∈reach(u) |v|, and let out max (u) be its maximal value over prefixes: out max (u) = max u ′ prefix of u out(u ′ ). Proof. As T is functional, there cannot exist two distinct d-configurations (q, σ, v) and (q, σ, v ′ ) that are both accessible and co-accessible. As we suppose that T is reduced, any accessible configuration is co-accessible. As a consequence, if there are two d-configurations (q, σ, v) and (q, σ, v ′ ) in C, then we have v = v ′ . This remark proves the space complexity. For time complexity, updating a d-configuration is just a research of rules to apply. Each of them will generate a new d-configuration, and is retrieved in constant time. ◭

A.2 Compact representation of runs of fVPTs: Naive compact .

We present the data structure S T u representing all d-configurations stored by Naive on the VPT T after reading u, i.e., the state of t reached after reading u. This structure is illustrated in Fig. 2. This first improvement avoids the exponential blowup in h(u). The structure S T u is a labeled DAG (directed acyclic graph) whose nodes are configurations of T (with an additional root node #, and each node has a depth) and edges are labeled by delays:

nodes(S T u ) = {#} ⊎ Q × (Γ ∪ {⊥}) × N and edges(S T u ) ⊆ nodes(S T u ) × Σ * × nodes(S T u )
. This DAG will have as leaves (nodes without outgoing edges) current configurations. The structure S T u is defined inductively on u according to the following algorithms.

edges(S

T ǫ ) = {# ǫ ֒-→ (q, ⊥, 0) | q ∈ I}
When a call letter c ∈ Σ c is read, the structure S T u is updated such that, for every leaf of S T u , a child is added for every way of updating the corresponding configuration according to a rule of T . If a leaf cannot be updated, it is removed, and also the possible new generated leaves (procedure remove_edges). Algorithm 1 describes how S T uc is computed from S T u . For a return letter r ∈ Σ r , we try to pop every leaf: if it is possible, the leaf is removed and

Algorithm 1

Updating structure S with a call symbol. procedure update_call(S, c)

2: newEdges ← ∅ orphans ← ∅ 4: for (q, γ, i) ∈ leaves(S) do if ∃v, γ ′ , q ′ | (q, c, v, γ ′ , q ′ ) ∈ δ then 6: for (v, γ ′ , q ′ ) | (q, c, v, γ ′ , q ′ ) ∈ δ do newEdges.add((q, γ, i) v ֒-→ (q ′ , γ ′ , i + 1)) 8:
else orphans.add((q, γ, i))

10:

edges(S) ← edges(S) ∪ newEdges

12: procedure remove_edges(S, orphans) while orphans = ∅ do 14:

n ← orphans.pop() for m | ∃v, m v ֒-→ n do 16: remove(S, m v ֒-→ n) if ∄n ′ , v ′ , m v ′ ֒-→ n ′ then orphans.add(m)
the new leaves updated, otherwise we remove the leaf and propagate the removal upwards (procedure remove_edges). This is described in Algorithm 2. Only edges and reachable nodes need to be stored, so that |S T u | ≤ (hc(u) + 1) • |Q| 2 • |Γ| 2 • out(u, T ). We prove the correctness of this construction using the transition function = ⇒ u based on edges of S T u , that gathers the stack content and delay. The relation =

⇒ u is the smallest relation in (Q × Γ * × N) × Σ * × (Q × Γ * × N) containing ֒-→ such that: if (q 0 , σ 0 , i) v = ⇒ u (q 1 , σ 1 γ, j) and (q 1 , γ, j) v ′ ֒-→ (q 2 ,
γ ′ , j + 1) then (q 0 , σ 0 , i)

vv ′ = = ⇒ u (q 2 ,
σ 1 γγ ′ , j + 1) (we may have σ = ǫ and γ = ⊥). The set of d-configurations stored in S T u is defined by: C(S T u ) = {(q, σ, v) | ∃i, (q, σ, i) ∈ leaves(S T u ) and # v = ⇒ u (q, σ, i)}. The following lemma shows that S T u exactly encodes the d-configurations computed by the IST t.

◮ Lemma 19. C(S T u

) is the state of the IST t after reading u. Proof. As mentioned in the proof of Lemma 17, the current state of t after reading u is

qi∈I {(q, σ, v) | (q i , ⊥) u/v
--→ (q, σ)}. Hence proving the following invariant is sufficient to prove this lemma:

For every 0 ≤ i ≤ hc(u), # v = ⇒ u (q, σ, i) iff there exists q i ∈ I such that (q i , ⊥) u1•••u k /v ------→ (q, σ) where k = max{j | hc(u 1 • • • u j ) = i}.
We prove it by induction on |u|. If |u| = 0, then i = 0 and the equivalence holds, as we can assume ǫ-loops (without output) on initial states.

Assume that the property holds for a given u, we prove that if also holds for the wellnested prefix uc. Let orphans be the set of leaves collected by the outermost for-loop of

Algorithm 2

Updating structure S with a return symbol. procedure update_return(S, r)

2: newEdges ← ∅ orphans ← ∅ 4:
for (q ℓ , γ ℓ , i) ∈ leaves(S) do if ∃v, q | (q ℓ , r, v, γ ℓ , q) ∈ δ then 6:

for (v, q) | (q ℓ , r, v, γ ℓ , q) ∈ δ do for (q 0 , γ 0 , v 0 ) | (q 0 , γ 0 , i -1) v0 ֒-→ (q ℓ , γ ℓ , i) ∈ edges(S) do 8:

for (n, v 1 ) | n v1 ֒-→ (q 0 , γ 0 , i -1) ∈ edges(S) do newEdges.add(n v1v0v ֒---→ (q, γ 0 , i -1)) 10:
else orphans.add((q ℓ , γ ℓ , i))

12:

remove_edges(S, orphans) remove_leaves(S)

for (m, v) | m v ֒-→ n ∈ edges(S) do remove(S, m v ֒-→ n)
update_call. These are the leaves (q, γ, hc(u)) of S T u such that no rule (q, c, v, γ ′ , q ′ ) exists in δ. Hence, corresponding configurations are blocked, and can be removed. The procedure remove_edges propagates these deletions, so that after the call to this procedure, the structure exactly contains configurations that can be updated by c. Hence, by induction hypothesis, the equivalence holds for 0 ≤ i ≤ hc(u).

For i = hc(uc) = hc(u) + 1, let k = max{j | hc(u 1 • • • u j ) = i}. We have: # vv ′ = = ⇒ uc (q, σγγ ′ , i) iff ∃q 1 , # v = ⇒ uc (q 1 , σγ, i -1) and (q 1 , γ, i -1) v ′ ֒-→ (q, γ ′ , i) (1) iff ∃q 1 , ∃q i ∈ I, (q i , ⊥) u/v
--→ (q 1 , σγ) and (q 1 , γ, i -1)

v ′ ֒-→ (q, γ ′ , i) (2) iff ∃q 1 , ∃q i ∈ I, (q i , ⊥) u/v --→ (q 1 , σγ) and (q 1 , c, v ′ , γ ′ , q) ∈ δ (3) iff ∃q i ∈ I, (q i , ⊥) uc/vv ′ ----→ (q, σγγ ′ ) (1) is by definition of = ⇒ uc .
(2) holds because, as mentioned above, remove_edges removes non-accessible configurations, and by induction hypothesis. Here, we also have

k -1 = max{j | hc(u 1 • • • u j ) = i -1}, as uc ends with a call symbol: so u 1 • • • u k-1 = u and u 1 • • • u k = uc.
(3) is due to the way update_call operates: it adds children to leaves according to rules of δ. Now we show that the property holds for the well-nested prefix ur, if it holds for u. Let h = hc(u). Procedure update_return checks, for each leaf, whether a rule can be applied. If not, the leaf is removed, and orphaned edges too, as explained for call symbols. Then, the hth level is removed and the (h -1)th updated, according to rules of T . Hence the property remains true for 0 ≤ i ≤ h -2. We have:

# v = ⇒ ur (q, σγγ 0 , h -1) iff ∃q 0 , q 1 , q ℓ , γ ℓ , v ′ , v 0 , v 1 , # v ′ = ⇒ u (q 1 , σγ, h -2) and (q 1 , γ, h -2) v1 ֒-→ (q 0 , γ 0 , h -1) ∈ edges(S T u ) and (q 0 , γ 0 , h -1) v0 ֒-→ (q ℓ , γ ℓ , h) ∈ edges(S T u ) and (q ℓ , r, v ′′ , γ ℓ , q) ∈ δ and v = v ′ v 1 v 0 v ′′ (1) iff ∃q 0 , q ℓ , γ ℓ , v ′ , v 0 , # v ′ = ⇒ u (q 0 , σγγ 0 , h -1) and (q 0 , γ 0 , h -1) v0 ֒-→ (q ℓ , γ ℓ , h) ∈ edges(S T u ) and (q ℓ , r, v ′′ , γ ℓ , q) ∈ δ and v = v ′ v 0 v ′′ (2) iff ∃q ℓ , γ ℓ , v ′ , # v ′ = ⇒ u (q ℓ , σγγ 0 γ ℓ , h) ∈ edges(S T u ) and (q ℓ , r, v ′′ , γ ℓ , q) ∈ δ and v = v ′ v ′′ (3) iff ∃q ℓ , γ ℓ , v ′ , q i ∈ I (q i , ⊥) u/v ′ ---→ (q ℓ , σγγ 0 γ ℓ ) and (q ℓ , r, v ′′ , γ ℓ , q) ∈ δ and v = v ′ v ′′ (4)
iff ∃q i ∈ I, (q i , ⊥)

ur/v ---→ (q, σγγ 0 )
Equivalence (1) reflects how update_return generates the new leaves. ( 2) and ( 3) come from the definition of = ⇒ u . ( 4) is obtained by induction hypothesis and the fact that, if

k = max{j | hc(u 1 • • • u j ) = h}, then u 1 • • • u k = u. ◭
The depth of the DAG obtained after reading u is the current height of u plus 1, each level has at most |Q| • |Γ| nodes, and each edge is labelled with a word of length less than out(u).

◮ Proposition 20. The maximal amount of memory used by Naive

compact on u ∈ Σ * is in O(|Q| 2 • |Γ| 2 • (h(u) + 1) • out max (u)).

A.3 LcpIn algorithm

We extend the definition of the largest common prefix to sets of d-configurations: if C ⊆ Dconfs(T ), then lcp(C) = lcp({v | (q, σ, v) ∈ C}). Let rem_lcp be the function that removes the largest common prefix to a set of d-configurations:

rem_lcp(C) = {(q, σ, v ′ ) ∈ Dconfs(T ) | (q, σ, lcp(C) • v ′ ) ∈ C}.
From an fVPT T , we define the IST τ = (Dconfs(T ) ⊎ {q f }, I τ , {q f }, δ τ ) where I τ = {{(q 0 , ⊥, ǫ) | q 0 ∈ I}}. We keep the same definition of C as in Naive, and rules of δ τ are: -----------→ rem_lcp(update(C, a)) for C ∈ Dconfs(T ) and a ∈ Σ

C a/lcp(update(C,a))
C $/v --→ q f for (C, v) ∈ C
We start by proving the correctness of the definition of the IST τ . This definition is illustrated in Fig. 5. ◭ (q 0 , ⊥, ǫ) We now provide algorithms for the second step of the computation performed by LcpIn on an input symbol a. Recall that the first step is the same as in Naive compact , i.e. Algorithm 1 if a is a call symbol, and Algorithm 2 if it is a return symbol, which transforms S T u to a new structure S ′ . The second step is the computation of lcp(C(S ′ )), which is output, and removed from every branch of S ′ , using Algorithm 3.

◮ Lemma 21. (u, v) ∈ T iff (u$, v) ∈ τ .
c 1 /df c, γ 1 c 3 /ab, γ 3 r 3 /ε, γ 3 c 1 /d, γ 1 c 3 /f, γ 3 r 3 /cab, γ 3 r 1 /gh, γ 1 r 1 /gh, γ 1 c 2 /ε, γ 2 r 2 /cabcab, γ 2 c 2 /abc, γ 2 r 2 /cab, γ 2
(q 1 , γ 1 , ǫ) (q 4 , γ 2 , f c) (q 2 , γ 1 γ 3 , ǫ) (q 5 , γ 2 γ 3 , cab) (q 3 , γ 1 , ǫ) (q 6 , γ 2 , ǫ) (q 7 , ⊥, ǫ) q f c 1 /d c 3 /f r 3 /cab r 1 /gh $/ǫ
Algorithm 3 starts with the procedure factorize, that processes every nodes in a bottomup manner (from leaves to the root #). For every node, the lcp of all outgoing edges is moved to all incoming edges. This is illustrated in Fig. 6.

For every node n ∈ nodes(S T u ), let S n be the structure obtained from S T u just after returning from factorize(S, n, done), and let = ⇒ n be the relation defined like = ⇒ u , but on S n . Note that the structure has the same set of nodes and edges after being processed by Algorithm 3, only the labels of edges are updated. Let B n be the set of branches from node n to a leaf:

B n0 = {(n 0 , n 1 , . . . , n k ) | ∀0 ≤ i < k, ∃v i , n i vi ֒-→ n i+1 and n k ∈ leaves(S T u )}.
For a branch b, we write V n (b) for its output in the structure S n , and V (b) for its output in S T u :

V n ((n 0 , . . . , n k )) = v 0 • • • v k-1 where n i vi ֒-→ n i+1 for all 0 ≤ i < k in S n .
We extend this definition to sets of branches:

V n (B) = {V n (b) | b ∈ B}. Note also that each node

Algorithm 3

Compute lcp(C(S)), and update S to the structure encoding rem_lcp(C(S)).

procedure output_lcp(S)

2: f actorize(S, #, ∅) ℓ ← lcp({v | ∃n, # v ֒-→ n}) 4: output ℓ for m, v | # v ֒-→ m do 6: let p be such that v = ℓ • p replace # v ֒-→ m by # p ֒-→ m in S 8:
function factorize(S, n, done)

f actor ← lcp({v | ∃m, n v ֒-→ m}) for m, v | n v ֒-→ m do 16: let p be such that v = f actor • p replace n v ֒-→ m by n p ֒-→ m in S 18: for p, v | p v ֒-→ n do replace p v ֒-→ n by p v•f actor ֒-----→ n in S 20:
return done ∪ {n} is processed once using factorize, and in a bottom-up way: when processing node n, all its descendants have been updated before (cf lines 11 and 12). The following property is the main invariant proving the correctness of Algorithm 3.

◮ Lemma 22. For every node n = #, let ℓ = lcp(V (B n )). Then,

1. for every branch b ∈ B n , V (b) = ℓ • V n (b) 2. for every p, v such that p v ֒-→ n in S n , v = v ′ ℓ with p v ′ ֒-→ n in S T u
Proof. We prove the following property by bottom-up induction on the structure. This property is true on leaves, as factorize does not modify their incoming edges. Assume that the property holds for all descendants of a node n. Let ℓ = lcp(V (B n )), and consider a branch b ∈ B n . The function factorize applied at n computes the lcp of edges outgoing from n and removes it on every branch. Hence, if n ′ be the node processed by factorize before n, then:

V n ′ (b) = lcp({v | ∃p, n v ֒-→ p in S n ′ }) • V n (b) (1)
Let p be the second node in branch b = (n, p, . . .). As p and all its descendants are processed before n ′ and not modified until the call of factorize on p, we have

V n ′ (b) = V p (b). Let us decompose V p (b) according to p: V p (b) = v 0 • V p (b p )
where n v0 ֒-→ p in S p and b p is the branch obtained from b by removing n. Using the induction hypothesis applied at p, we get

v 0 = v 1 ℓ ′ with ℓ ′ = lcp(V (B p )), n v1 ֒-→ p in S T u , and V (b p ) = ℓ ′ • V p (b p ). Thus V p (b) = v 1 • ℓ ′ • V p (b p ) = v 1 • V (b p ) = V (b). Equation (1) becomes: V (b) = lcp({v | ∃p, n v ֒-→ p in S n ′ }) • V n (b) (2) Let us write ℓ ′′ = lcp({v | ∃p, n v ֒-→ p in S n ′ }).
It remains to prove that ℓ ′′ = ℓ. Notice that this will prove both parts of the lemma. We have ℓ ′′ = lcp({v | ∃p, n v ֒-→ p in S p }) because p and its descendants are unchanged between calls of factorize on p and n ′ . Using the induction hypothesis on each p, we obtain:

ℓ ′′ = lcp({v • lcp(V (B p )) | n v ֒-→ p in S T u }) = lcp(V (B n )) = ℓ
This concludes the proof. ◭

The next lemma ensures that factorize preserves the semantic of the structure, i.e. the set of encoded configurations.

◮ Lemma 23. C(F (S T u )) = C(S T u ).
Proof.

(q, σ, v) ∈ C(S T u ) iff ∃i, (q, σ, i) ∈ leaves(S T u ) and # v = ⇒ u (q, σ, i) iff ∃i, (q, σ, i) ∈ leaves(S T u ) and ∃p, # v0 ֒-→ p and p v1 = ⇒ u (q, σ, i) with v = v 0 v 1 iff ∃i, (q, σ, i) ∈ leaves(S T u ) and ∃p, # v0 ֒-→ p and v = v 0 V (b) where b is a branch p = ⇒ u (q, σ, i) iff ∃i, (q, σ, i) ∈ leaves(S T u ) and ∃p, # v0 ֒-→ p and v = v 0 • lcp(V (B p )) • V n (b) where b is a branch p = ⇒ u (q, σ, i) (1) iff (q, σ, v) ∈ C(F (S T u ))
Equivalence ( 1 Let T be a functional FST.

1. T is BM iff T is subsequentializable; 2. It is decidable in PTime if T is BM [29].
Proof. Statement 2 is proved in [START_REF] Weber | Economy of description for single-valued transducers[END_REF] (it is proved that subsequentializability is decidable in PTime). We prove statement 1. Clearly, if T is definable by a subsequential transducer T d , then evaluating T d on any input word u can be done with a space complexity that depends on the size of T d only.

Conversely, if T is BM, there exists K ∈ N and a TT M that transforms any input word u into T (u) in space complexity K. Any word on the working tape of M is of length at most K. As M is deterministic, we can therefore see M as a subsequential FST, whose states are pairs (q, w) where q is a state of T and w a word on the working tape (modulo some elimination of ǫ-transitions).

◭

B.2 Bounded Memory pushdown transductions

◮ Proposition 25. It is undecidable whether a pushdown transduction is BM.

Proof. We reduce the problem of deciding whether the language of a pushdown automaton P over an alphabet A is regular to BM. Any letter of A is seen as an internal symbol. We associate with P a pushdown transducer I P which defines the identity on L(P ). Clearly, if L(P ) is regular, it is defined by a finite automaton which can easily be turned into a Turing transducer defining I P and which uses a memory that depends on the size of the automaton only. Conversely, if I P is BM, there exists a function f and a TT M equivalent to I P and which uses at most f (1, |M |) bits of memory, i.e. an amount of memory which depends on the size of M only. The machine M can easily be turned into a finite automaton which defines P , whose states are the configurations of the working tape of M . ◭

B.3 Proof of Proposition 5

Proof. If T is BM, there exist K and a TT M such that M evaluates any input word in space at most K. We can easily extract from M a finite automaton that defines Dom(T ), whose number of states m only depends on M and K. By a simple pumping argument, it is easy to show that the words in Dom(T ) have a height bounded by m. If the height of the words in Dom(T ) is bounded, then their height is bounded by n 2 . Indeed, assume that there exists a word u ∈ Dom(T ) whose height is strictly larger than n 2 . Then there exists a run of T on u of the following form:

(i, ⊥) u1/v1 ----→ (q, σ) u2/v2 ----→ (q, σσ ′ ) u3/v3 ----→ (p, σσ ′ ) u4/v4 ----→ (p, σ) u5/v5 ----→ (f, ⊥)
such that u = u 1 u 2 u 3 u 4 u 5 , σ ′ is not empty, and i (resp. f ) is an initial (resp. final) state of T . The existence of this decomposition follows from the consideration of the set of pairs of positions in u corresponding to matching calls and returns of well-nested subwords of u.

Then one can iterate the matching loops around q and p to generate words in Dom(T ) with arbitrarily large heights, yielding a contradiction. Therefore FST(T, n 2 ) is equivalent to T . As in the proof of Proposition 24, we can regard M as a subsequential FST T M whose set of states are configurations of the machine. The FST T M is equivalent to T , and therefore to FST(T, n 2 ). Since T M is subsequential, FST(T, n 2 ) is subsequentializable and therefore by Proposition 24, FST(T, n 2 ) is BM. The converse is obvious. Therefore to check whether T is BM, we first decide if the height of all input words accepted by T is less or equal than n 2 . This can be done in PTime O(|T | • n 2 ) by checking emptiness of the projection of T on the inputs (this is a visibly pushdown automaton) extended with counters up to n 2 + 1 that counts the height of the word. Then we check in coNPTime whether evaluating T can be done in constant memory if we fix both the transducer and the height of the word (Theorem 10). Since here the height is bounded by n 2 , it is equivalent to checking bounded memory. ◭

C On deciding height bounded memory for VPTs

Before going into the proofs of the results of this section, we first prove that our horizontal twinning property, when restricted to FSTs, is equivalent to the twinning property for FSTs defined in [START_REF] Béal | Determinization of transducers over finite and infinite words[END_REF].

C.1 Twinning properties for FSTs

Since we use results on the twinning property for FSTs in this paper, we clarify the definition of twinning property for FSTs. In the core of the paper, it is said that restricting the horizontal twinning property to FSTs correspond to the usual twinning property of FSTs.

By "usual" we mean the following definition, taken from [START_REF] Béal | Determinization of transducers over finite and infinite words[END_REF].

◮ Definition 26 (Twinning property for FSTs of [START_REF] Béal | Determinization of transducers over finite and infinite words[END_REF]). Let T = (Q, I, F, δ) be a reduced FST. T satisfies the twinning property if for all q 0 , q ′ 0 ∈ I, for all q, q ′ ∈ Q, for all words

u 1 , v 1 , w 1 , u 2 , v 2 , w 2 ∈ Σ * , if: q 0 u1/v1 ----→ q u2/v2 ----→ q q ′ 0 u1/w1 ----→ q ′ u2/w2 ----→ q ′
Then either v 2 = w 2 = ǫ, or the following holds:

(i) |v 2 | = |w 2 | (ii) v 1 (v 2 ) ω = w 1 (w 2 ) ω
Our twinning property for FSTs is obtained by restricting the horizontal twinning property of VPTs to FSTs. By restricting we mean the following: ◮ Definition 27 (Twinning property for FSTs of this paper). Let T = (Q, I, F, δ) be a reduced FST. T satisfies the twinning property if for all q 0 , q ′ 0 ∈ I, for all q, q ′ ∈ Q, for all words

u 1 , v 1 , w 1 , u 2 , v 2 , w 2 ∈ Σ * , if: q 0 u1/v1 ----→ q u2/v2 ----→ q q ′ 0 u1/w1 ----→ q ′ u2/w2 ----→ q ′ Then ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ).
The two definitions are equivalent, as shown by the next lemma:

◮ Lemma 28. Definitions 26 and 27 are equivalent.

Proof. First suppose that Definition 26 holds. If

v 2 = w 2 = ǫ, then clearly ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ). Otherwise |v 2 | = |w 2 | and v 1 (v 2 ) ω = w 1 (w 2 ) ω . Then necessarily v 1 w 1 (i.e. v 1 is a prefix of w 1 ) or w 1 v 1 . Wlog suppose that v 1 w 1 , i.e. w 1 = v 1 w ′ 1 for some w ′ 1 . Therefore ∆(v 1 , w 1 ) = (ǫ, w ′ 1 ), and ∆(v 1 v 2 , w 1 w 2 ) = ∆(v 2 , w ′ 1 w 2 ). We now prove that ∆(v 2 , w ′ 1 w 2 ) = (ǫ, w ′ 1 ). Since v 1 (v 2 ) ω = w 1 (w 2 ) ω , we have (v 2 ) ω = w ′ 1 (w 2 ) ω . Therefore v 2 w ′ 1 (w 2 ) ω = v ω 2 = w ′ 1 (w 2 ) ω . Since |v 2 | = |w 2 |, we get v 2 w ′ 1 = w ′ 1 w 2 , from which we have ∆(v 2 , w ′ 1 w 2 ) = ∆(v 2 , v 2 w ′ 1 ) = (ǫ, w ′ 1 )
. Conversely, suppose that Definition 27 holds and

v 2 w 2 = ǫ. Since ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ), we have either v 1 w 1 or w 1 v 1 . Wlog suppose that v 1 w 1 , i.e. w 1 = v 1 w ′ 1 for some w ′
1 . Therefore we have:

∆(v 1 , w 1 ) = (ǫ, w ′ 1 ) = ∆(v 1 v 2 , w 1 w 2 ) = ∆(v 2 , w ′ 1 w 2 )
Consequently, v 2 w ′ 1 w 2 , and in particular, w ′ 1 w 2 = v 2 w ′ 1 , which gives us the following series of equalities:

w 1 (w 2 ) ω = v 1 w ′ 1 (w 2 ) ω = v 1 v 2 w ′ 1 (w 2 ) ω = v 1 (v 2 ) 2 w ′ 1 (w 2 ) ω = • • • = v 1 (v 2 ) ω ◭ C.2 HTP is decidable ◮ Lemma 29.
Let T be an fVPT, T does not satisfy the HTP if and only if there exist

q 0 , q ′ 0 ∈ I, q, q ′ ∈ Q, σ, σ ′ ∈ Γ * and u 1 , v 1 , w 1 , u 2 , v 2 , w 2 ∈ Σ * , with either v 2 = ǫ or w 2 = ǫ and: (q 0 , ⊥) u1/v1 ----→ (q, σ) u2/v2 ----→ (q, σ) (q ′ 0 , ⊥) u1/w1 ----→ (q ′ , σ ′ ) u2/w2 ----→ (q ′ , σ ′ )
and either (i)

|v 2 | = |w 2 | or (ii) |v 2 | = |w 2 |, |v 1 | ≤ |w 1 | and v 1 v 2 w 1 w 2 .
Proof. Let suppose that there exist q 0 , q ′ 0 ∈ I, q, q ′ ∈ Q, σ, σ ′ ∈ Γ * and u 1 , v 1 , w 1 , u 2 , v 2 , w 2 ∈ Σ * , with either v 2 = ǫ or w 2 = ǫ and :

(q 0 , ⊥) u1/v1 ----→ (q, σ) u2/v2 ----→ (q, σ) (q ′ 0 , ⊥) u1/w1 ----→ (q ′ , σ ′ ) u2/w2 ----→ (q ′ , σ ′ )
And let show that if (i) or (ii) hold so does ∆(v

1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ). First suppose that (i) holds. Let x = v 1 ∧ w 1 and z = v 1 v 2 ∧ w 1 w 2 , clearly there exists y ∈ Σ * such that z = xy. By definition, we have ∆(v 1 , w 1 ) = (x -1 v 1 , x -1 w 1 ) and ∆(v 1 v 2 , w 1 w 2 ) = ((xy) -1 v 1 v 2 , (xy) -1 w 1 w 2 ). Therefore if (i) holds then either |x -1 v 1 | = |(xy) -1 v 1 v 2 | or |x -1 w 1 | = |(xy) -1 w 1 w 2 )|. Indeed, suppose the first inequality does not hold, we have |x -1 v 1 | = |v 1 | -|x| = |(xy) -1 v 1 v 2 | = |v 1 | + |v 2 | -|x| -|y|, that is 0 = |y| -|v 2 |.
Therefore one can check that the second inequality must hold. We have shown that (i) implies ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ). Now, suppose (ii) holds and let us show that we also have ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ). We have (ii

) |v 2 | = |w 2 |, |v 1 | ≤ |w 1 | and v 1 v 2 w 1 w 2 .
Note that for any u, v, x, y ∈ Σ * with ∆(u, v) = (x, y) we have u v if and only if x = ǫ and y = ǫ. Therefore, if we pose (y 1 , y 2 ) = ∆(v 1 v 2 , w 1 w 2 ), we have, by hypothesis, v 1 v 2 w 1 w 2 and so y 1 = ǫ and y 2 = ǫ.

Let pose (x 1 , x 2 ) = ∆(v 1 , w 1 ), if (x 1 , x 2 ) = (y 1 , y 2 ) then x 1 = ǫ and x 2 = ǫ, that is v 1 w 1 , but then ∆(v 1 v 2 , w 1 w 2 ) = ∆(v 1 , w 1 ) • (v 2 ,
w 2 ) which cannot be equal to ∆(v 1 , w 1 ) (because, by hypothesis, one of v 2 and w 2 is not the empty word). Now let suppose the HTP does not hold and let show that (i) or (ii) is satisfied for some words (as above). So there exist q 0 , q ′ 0 ∈ I, q, q ′ ∈ Q, σ, σ ′ ∈ Γ * and u 1 , v 1 , w 1 , u 2 , v 2 , w 2 ∈ Σ * with :

(q 0 , ⊥) u1/v1 ----→ (q, σ) u2/v2 ----→ (q, σ) (q ′ 0 , ⊥) u1/w1 ----→ (q ′ , σ ′ ) u2/w2 ----→ (q ′ , σ ′ ) such that ∆(v 1 , w 1 ) = ∆(v 1 v 2 ,
| = |w 2 k |, |v 1 | ≤ |w 1 | and v 1 v 2 k w 1 w 2 k
. We now prove that this implies ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ), which is a contradiction with the hypothesis. On the one hand, if for all k we have v 1 v 2 k w 1 w 2 k then we have

w 1 = v 1 v 2 a v ′ 2 for some a ∈ N and some v ′ 2 v 2 . So, ∆(v 1 , w 1 ) = ∆(v 1 , v 1 v 2 a v ′ 2 ) = (ǫ, v 2 a v ′ 2 ). On the other hand, v 1 v 2 k w 1 w 2 k and |v 2 | = |w 2 | implies that we have w 1 w 2 = v 1 v 2 a+1 v ′ 2 . So we have ∆(v 1 v 2 , w 1 w 2 ) = ∆(v 1 v 2 , v 1 v 2 a+1 v ′ 2 ) = (ǫ, v 2 a v ′ 2 ). Therefore ∆(v 1 , w 1 ) = ∆(v 1 v 2 , w 1 w 2 ). This concludes the proof. ◭ ∆(v 1 v 3 , v ′ 1 v ′ 3 )
. As v 1 v 3 and v ′ 1 v ′ 3 are possible output words for the input word u 1 u 3 , whose length is strictly smaller than |u|, we obtain |w| ≤ out = (u 1 u 3 ) and the result holds by induction.

We now consider the second case: s ∈ Dom(T ). Let s ′ be the longest prefix of s such that there exists s ′′ such that s ′ s ′′ ∈ Dom(T ). Since T is reduced (w.l.o.g., as explained in preliminaries), s ′ correspond to the longest prefix of s on which there exist a run of T . Therefore we have out max = (s) ≤ out max = (s ′ ) and we can apply the proof of the first case (as s ′ is a prefix of a word that belongs to Dom(T )) and we get out max = (s Let T be a fVPT. We construct in polynomial time a pushdown automaton with s counters 2 (one reversal) that accepts any word u = u 1 u 2 u 3 u 4 that satisfies the premise of the MTP but such that ∆(v 1 v 3 , w 1 w 3 ) = ∆(v 1 v 2 v 3 v 4 , w 1 w 2 w 3 w 4 ) (i.e. the MTP is not verified). Therefore the MTP holds if and only if no word is accepted by the automaton. This can be checked in coNPTime [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF].

′ ) ≤ (|Q| • |Γ| h(s ′ ) ) 2 M . Moreover, h(s ′ ) ≤ h(s), therefore out max = (s) ≤ out max = (s ′ ) ≤ (|Q| • |Γ| h(s) ) 2 M
The automaton simulates any two runs, and guesses the decomposition u 1 u 2 u 3 u 4 (it checks that the decomposition is correct by verifying that each run is in the same state after reading u 1 and u 2 , and in the same state after reading u 3 and u 4 ). With two counters it can check that |v 2 v 4 | = |w 2 w 4 |, if it is not the case then it accepts u (indeed the MTP is therefore not verified). The automaton checks that ∆(v We detail how to check the first condition, the others can be checked with the same technique. The automaton guesses the value k and with two counters verifies that a l-k = b l-k as follows. First it initializes both counters to lk (e.g. with an epsilon loop that increments both counters). Then it counts the letters of both words A and B up to lk and records a l-k and b l-k and verifies that they are not equal. Finally it must verify that either (i) or (ii) is satisfied. The verification of (i) is easy. To verify (ii), i.e.

1 v 3 , w 1 w 3 ) = ∆(v 1 v 2 v 3 v 4 ,

By hypothesis we have a

l-k = b l-k therefore |A ′ | ≥ k + 1 (as a l-k ∈ A ′ ) and |B ′ | ≥ k + 1 -(l -m) (as b l-k ∈ B ′ ). Thus |C ′ | ≥ k + 1 and |D ′ | ≥ k + m -l + 1.
In particular, this implies that we are in case (ii) as

|C| ≥ |C ′ | ≥ k + 1. We consider two cases: (a) if a l-k = c n-k we have A ′ = C ′ (because a l-k ∈ A ′ and c n-k ∈ C ′ and are at the same position in A ′ and C ′ as |A ′ | = |C ′ |), or (b) if a l-k = c n-k this means that b l-k = d n-k (because a l-k = b l-k and c n-k = d n-k ), and so B ′ = D ′ (because b l-k ∈ B ′ and d n-k ∈ D ′ because |B ′ | = |D ′ |). 2. Similar to proof of 1. 3. We prove that condition (i) implies ∆(A, B) = ∆(C, D). Condition (ii) is proved sim- ilarly. We know that |A ′ | ≥ |A| -|B| = l -m > k therefore a l-k ∈ A ′ . Similarly, |C ′ | = |A ′ | > k, so c n-k ∈ C ′ . By hypothesis a l-k = c n-k , therefore, as |A ′ | = |C ′ |,
′ | > |C ′ | (this implies |B ′ | > |D ′ |): take k = |A ′ | -1, we have a l-k = b l-k and c n-k = d n-k (existence of b l-k and d n-k is ensured by ( † B ) and ( † D )): condition 1.(ii) is satisfied. |C ′ | > |A ′ | (this implies |D ′ | > |B ′ |): take k = |C ′ | -1, then condition 2.(ii) is satisfied. |A ′ | = |C ′ | (this implies |B ′ | = |D ′ |),
V (i) = v 1 (v 2 ) i v 3 (v 4 ) i W (i) = w 1 (w 2 ) i w 3 (w 4 ) i .
If there exist K ≥ 0 and X ∈ Σ * such that for all i ≥ K, V (i) = W (i) X, then for all i ≥ 0,

V (i) = W (i) X.
Proof. First note that we have |v 2 v 4 | = |w 2 w 4 |, this is a straight consequence from the fact that for all i ≥ K, V (i) = W (i) X. We consider two cases:

|v 2 | = |v 4 |:
in that case we can show that the primitive roots of v 2 , v 4 , w 2 , w 4 are conjugate (see for example [START_REF] Filiot | On functionality of visibly pushdown transducers[END_REF]) and therefore have the same length. Therefore we can apply Theorem 1 of [START_REF] Holub | On systems of word equations with simple loop sets[END_REF] which yields the result.

i ≥ K we have v 1 v 2 i = w 1 w 2 i Y and Y v 3 v 4 i = w 3 w 4 i X.
Therefore we can apply Theorem 2 of [START_REF] Holub | On systems of word equations with simple loop sets[END_REF] which shows that these equalities hold for any i. For any i we have

V (i) = v 1 v 2 i v 3 v 4 i = w 1 w 2 i Y v 3 v 4 i = w 1 w 2 i w 3 w 4 i X = W (i) X. ◭ ◮ Lemma 36. Let v 1 , v 2 , v 3 , v 4 , w 1 , w 2 , w 3 , w 4 ∈ Σ *
and for all i ≥ 0, let 1) , W (1) ), then there exists i 0 ≥ 1 such that for all i, j ≥ i 0 , if i = j then ∆(V (i) , W (i) ) = ∆(V (j) , W (j) ).

V (i) = v 1 (v 2 ) i v 3 (v 4 ) i W (i) = w 1 (w 2 ) i w 3 (w 4 ) i . If ∆(V (0) , W (0) ) = ∆(V (
Proof. First note that since ∆(V (0) , W (0) ) = ∆(V (1) , W (1) ), we clearly have

|v 2 v 4 | = ǫ or |w 2 w 4 | = ǫ, We write u v if u is a prefix of v,
and u||v if u and v are incomparable, i.e. u ∧ v = ǫ. We consider several cases:

1. there is K ≥ 1 such that for all i ≥ K, V (i) W (i) or W (i) V (i) . Consider the lengths of V (i) and W (i) . When K is large enough, one of V (i) and W (i) is always the prefix of the other, for i ≥ K: V

(i) W (i) if |v 2 v 4 | ≤ |w 2 w 4 |, and
W (i) V (i) otherwise. Let us assume that |v 2 v 4 | ≤ |w 2 w 4 |, i.e., for all i ≥ K, there exists X i such that W (i) = V (i) X i . The other case is symmetric. We have |W (i+1) | -|W (i) | = |w 2 w 4 | = |V (i+1) | + |X i+1 | -|V (i) | -|X i |, i.e. |w 2 w 4 | = |V (i) | + |v 2 v 4 | + |X i+1 | -|V (i) | -|X i |, i.e. |X i+1 | -|X i | = |w 2 w 4 | -|v 2 v 4 |. We again consider several cases: 1.1 |w 2 w 4 | > |v 2 v 4 |. We have |X K | < |X K+1 | < |X K+2 | . . .,
and by definition of the delay, ∆(V (i) , W (i) ) = (ǫ, X i ). Therefore the delay always increases in size as i icreases and we get the result; 1.2 |w 2 w 4 | = |v 2 v 4 |. We show that this case is not possible. Indeed, it implies that

|X K | = |X K+1 | = |X K+2 | . . .
. Therefore by definition of V (i) and W (i) , there exists K ′ ≥ K and X ∈ Σ * such that X = X K ′ = X K ′ +1 = X K ′ +2 . . . . By Lemma 35, we get W (0) = V (0) X and W (1) = V (1) X, which contradicts ∆(W (0) , V (0) ) = ∆(W (1) , V (1) ). 2. for all K ≥ 1, there is i ≥ K such that V (i) ||W (i) . We show in this case that one of the two components of the delay always increases in size when i increases. We consider several cases depending on where the first difference between V (i) and W (i) occurs. The cases we consider also depend on K. In particular, by taking a large K it can reduce the number of cases we have to consider. For some α 1 , α 2 , α 3 ∈ Σ * and a, b ∈ Σ such that a = b, and for a K large enough, one of the following condition holds:

2.1 there is i ≥ K such that v 1 (v 2 ) i = α 1 aα 2 and w 1 (w 2 ) i = α 1 bα 3 , as illustrated below.

V (i) v1(v2) i v3(v4) i α1 α2 W (i) w1(w2) i w3(w4) i α1 α3 a b
Then for all j ≥ i:

∆(V (j) , W (j) ) = (aα 2 (v 2 ) j-i v 3 (v 4 ) j , bα 3 (w 2 ) j-i w 3 (w 4 ) j )
Since |v 2 v 4 | = ǫ or |w 2 w 4 | = ǫ, some of the two components of the delays is always increasing in size as j icreases, which proves the result; 2.2 w 2 = ǫ and v 1 = α 1 aα 2 and there is i ≥ K such that w 1 w 3 (w 4 ) i = α 1 bα 3 , as illustrated below.

V (i) v1 (v2) i v3(v4) i α1 α2 W (i) w1w3(w4) i α1 α3 a b
Then for all j ≥ i:

∆(V (j) , W (j) ) = (aα 1 v j 2 v 3 (v 4 ) j , bα 3 (w 4 ) j-i )
Since v 2 v 4 = ǫ or w 4 = ǫ, one of the two components of the delays is always increaing in size; 2.3 there is

i ≥ K such that v 1 (v 2 ) i = α 1 aα 2 and w 1 (w 2 ) i w 3 = α 1 bα 3 , with |α 1 | ≥ |v 1 | and |α 1 | ≥ |w 1 (w 2 ) i | (otherwise it is case 2.1
). We also assume that w 2 = ǫ (otherwise it can be proved similarly as case 2.1). Therefore v 2 = ǫ. This case is illustrated below:

V (i) v1 (v2) i v3(v4) i α1 α2
W (i) w1(w2) i w3 (w4) i α1 α3 a b

We have taken K large enough, so that v i 2 and w i 2 have a common factor of length at least |v 2 | + |w 2 |. The strong theorem of Fine and Wilf [START_REF] Lothaire | Combinatorics on words[END_REF] implies that the primitive roots of v 2 and w 2 are conjugate: there are t 1 , t 2 ∈ Σ * and n, p ≥ 1 such that v 2 = (t 1 t 2 ) n and w 2 = (t 2 t 1 ) p . It can be shown (see for instance [START_REF] Filiot | On functionality of visibly pushdown transducers[END_REF]) that we can choose t 1 and t 2 such that there exist k 1 , k 2 ≥ 0 verifying:

v 1 = (v 1 ∧ w 1 )(t 2 t 1 ) k1 t 2 w 1 = (v 1 ∧ w 1 )(t 2 t 1 ) k2
Let α ′ 1 be such that α 1 = w 1 (w 2 ) i α ′ 1 . There exist k 3 , X and Y such that α ′ 1 = (t 2 t 1 ) k3 X with t 2 t 1 = XaY , and w 3 = α ′ 1 bα 3 , as illustrated below (we assume that |w 1 | < |v 1 | on the picture).

V (i) v1 (v2) i v3(v4) i α1 α2 W (i) w1 (w2) i w3 (w4) i α1 α3 α ′ 1 a b t2t1t2t1t2t1t2t1t2t1t2t1t2t1t2t1t2t1t2t1t2t1t2t1t2
We have for all j ≥ i: ∆(V (j) , W (j) ) = ∆(v 1 (v 2 ) j v 3 (v 4 ) j , w 1 (w 2 ) j w 3 (w 4 ) j ) = ∆((v 1 ∧ w 1 )(t 2 t 1 ) k1 t 2 (t 1 t 2 ) jn v 3 (v 4 ) j , w 1 (w 2 ) j w 3 (w 4 ) j ) = ∆((v 1 ∧ w 1 )t 2 (t 1 t 2 ) k1+jn v 3 (v 4 ) j , w 1 (w 2 ) j w 3 (w 4 ) j ) = ∆((v 1 ∧ w 1 )t 2 (t 1 t 2 ) k1+jn v 3 (v 4 ) j , (v 1 ∧ w 1 )(t 2 t 1 ) k2 (w 2 ) j w 3 (w 4 ) j ) = ∆(t 2 (t 1 t 2 ) k1+jn v 3 (v 4 ) j , (t 2 t 1 ) k2+jp w 3 (w 4 ) j ) = ∆((t 2 t 1 ) k1+jn t 2 v 3 (v 4 ) j , (t 2 t 1 ) k2+jp w 3 (w 4 ) j )

We now consider the following subcases: 2.3.1 |v 2 | > |w 2 |. As a consequence, n > p, and we can assume that K is big enough, so that k 1k 2 + j(np) > 0. We get:

∆(V (j) , W (j) ) = ∆((t 2 t 1 ) k1-k2+j(n-p) t 2 v 3 (v 4 ) j , w 3 (w 4 ) j ) = ∆((t 2 t 1 ) k1-k2+j(n-p) t 2 v 3 (v 4 ) j , α ′ 1 bα 3 (w 4 ) j ) = ∆((t 2 t 1 ) k1-k2+j(n-p) t 2 v 3 (v 4 ) j , (t 2 t 1 ) k3 Xbα 3 (w 4 ) j )

We can take j such that k 1k 2 + j(np) > k 3 , and therefore we finally have: ∆(V (j) , W (j) ) = ∆((t 2 t 1 ) k1-k2+j(n-p)-k3 t 2 v 3 (v 4 ) j , Xbα 3 (w 4 ) j ) = ∆(XaY (t 2 t 1 ) k1-k2+j(n-p)-k3-1 t 2 v 3 (v 4 ) j , Xbα 3 (w 4 ) j ) = (aY (t 2 t 1 ) k1-k2+j(n-p)-k3-1 t 2 v 3 (v 4 ) j , bα 3 (w 4 ) j ) Since t 2 t 1 = ǫ, we get that the first component of the delay always increases in size when j increases; 2.3.2 |v 2 | < |w 2 |. We can take K large enough such that this case never happens, i.e.

(v 2 ) i and w 3 do not overlap. 2.3.3 |v 2 | = |w 2 |. Therefore n = p, and we have for all j ≥ i: ∆(V (j) , W (j) ) = ∆((t 2 t 1 ) k1 t 2 v 3 (v 4 ) j , (t 2 t 1 ) k2 w 3 (w 4 ) j ) As case 2.3.1, since by hypothesis there is an overlap between (v 2 ) i and w 3 , we have k 1 > k 2 + k 3 , and we get: ∆(V (j) , W (j) ) = ∆((t 2 t 1 ) k1-k2 t 2 v 3 (v 4 ) j , w 3 (w 4 ) j ) = ∆((t 2 t 1 ) k1-k2 t 2 v 3 (v 4 ) j , (t 2 t 1 ) k3 Xbα 3 (w 4 ) j ) = ∆((t 2 t 1 ) k1-k2-k3 t 2 v 3 (v 4 ) j , Xbα 3 (w 4 ) j ) = ∆(XaY (t 2 t 1 ) k1-k2-k3-1 t 2 v 3 (v 4 ) j , Xbα 3 (w 4 ) j ) = (aY (t 2 t 1 ) k1-k2-k3-1 t 2 v 3 (v 4 ) j , bα 3 (w 4 ) j )

Therefore if v 4 = ǫ and w 4 = ǫ, we are done as one of the two components of the delay will increase in size when j increases. If v 4 = w 4 = ǫ we can explicitly give the form of ∆(V (0) , W (0) ) and ∆(V (1) , W (1) ):

∆(V (0) , W (0) ) = ∆((t 2 t 1 ) k1 t 2 v 3 , (t 2 t 1 ) k2+k3 Xbα 3 ) = ∆((t 2 t 1 ) k1-k2-k3 t 2 v 3 , Xbα 3 ) = ∆((t 2 t 1 ) k1 t 2 (t 1 t 2 ) n v 3 , (t 2 t 1 ) k2+k3+n Xbα 3 ) = ∆(V (1) , W (1) ) This is excluded by hypothesis, so this case is not possible.

2.4 the other cases (the first difference occurs between (v 2 ) i and (w 4 ) i , or between v 3 and w 3 , or between v 3 and (w 4 ) i , or between (v 4 ) i and (w 4 ) i ) are proved similarly as case 2.3 by decomposing the words as power of their primitive roots. For instance, if the first difference occurs between v 3 and w 3 , then either v 2 = w 2 = ǫ and it is the same as case 2.1, or v 2 = ǫ and w 2 = ǫ but we can take K large enough so that this case is impossible, or v 2 = ǫ and w 2 = ǫ. In this latter case we can take K large enough so that the primitive roots of v 2 and w 2 are conjugate. We have again to distinguish several cases on the relative lengths of v 2 and w 2 (as for 2.3) but the proofs are similar. Similar techniques were already applied to prove that functionality is decidable for VPTs [START_REF] Filiot | On functionality of visibly pushdown transducers[END_REF].

◭

D.3 Proof of Theorem 16

We can use the same proof as the proof of back direction of Theorem 10, the only difference is the lemma that bounds the maximal difference between outputs of T . We prove the following lemma, which states that the MTP implies that in the evaluation algorithm, the delays stored by the algorithm can be bounded linearly in the height of the input word.

◮ Lemma 37. Let T be an fVPT. If the MTP holds for T , then for any word s ∈ Σ * , we have out max = (s) ≤ (h(s) + 1) • (|Q| • |Γ| |Q| 4 ) 2 + 1 • M , where M = max{|t| | (q, a, t, γ, q ′ ) ∈ δ}.

Proof. Let s ∈ Σ * . We assume that s ∈ Dom(T ) (we can handle the case s ∈ Dom(T ) as in the proof of Lemma 31 for the HTP). We use the notion of current height hc(u) of a prefix u of s as defined at the beginning of Appendix A. Consider a word u prefix of s. There exists a unique decomposition of u as follows: u = u 0 c 1 u 1 c 2 . . . u n-1 c n u n , where n = hc(u), and for any i, we have c i ∈ Σ c and u i is well-nested. Indeed, as n = hc(u), the word u contains exactly n pending calls, that correspond to c i 's, and other parts of u can be gathered into well-nested words. If each of the u i 's is such that |u i | ≤ (|Q| • |Γ| |Q| 4 ) 2 , then the property holds as length of word u can be bounded by (hc(u) + 1)

• (|Q| • |Γ| |Q| 4 ) 2 + 1 .
Otherwise, we prove that there exists a strictly shorter input word that produces the same delays as u when evaluating the transduction on it. Therefore, consider a word w such that (q 0 , ⊥) u/w ---→ (q, σ) for some q 0 ∈ I. Then there exist runs ̺, ̺ ′ in T producing respectively as output words v and v ′ , such that v = (v ∧ v ′ ) • w. Consider the smallest index i such that |u i | > (|Q| • |Γ| |Q| 4 ) 2 . We distinguish two cases: 4 , then we can reduce the length of u i using the HTP by exhibiting two configurations occurring twice in runs ̺ and ̺ ′ . This yields an input word u ′ , strictly shorter than u, that produces the same delays as u (see the proof of Lemma 31). 2. if h(u i ) > |Q| 4 , then we prove that we can "pump vertically" u i , and then reduce its length too. Indeed, let k be the first position in word u i at which height h(u i ) is obtained.

1. if h(u i ) ≤ |Q|
As u i is well-nested, we can define for each 0 ≤ j < h(u i ) the unique position lef t(j) (resp. right(j)) as the largest index, less than k (resp. the smallest index, larger than k), whose height is j (see Figure 7). As h(u i ) > |Q| 4 , there exist two heights j and j ′ such that configurations reached at positions lef t(j), lef t(j ′ ), right(j) and right(j ′ ) in runs ̺ and ̺ ′ satisfy the premises of the matched twinning property, considering the prefix u 0 c 1 . . . c i u i of u. Thus, one can replace in this prefix u i by a shorter word u ′ i and hence reduce its length, while preserving the delays reached after it. Let u ′ be the word obtained from u by substituting u ′ i to u i , hence |u ′ | < |u|. By Lemma 33, this entails that the delays reached after u and u ′ are the same, proving the result. ◭ height length (p, q) (p, q) (p ′ , q ′ ) (p ′ , q ′ ) j j ′ lef t(j ′ ) lef t(j) right(j) right(j ′ )

Figure 7 Vertical pumping in a well-nested word

Figure 1 A

 1 Figure 1 A functional VPT with Σc = {c}, Σr = {r, r ′ } and Σι = {a, b}

  After reading ccr1.

Figure 2

 2 Figure 2 Data structure used by LcpIn.

( b )

 b Part of the IST t corresponding to T1, computed on ccr1r2.

Figure 3

 3 Figure 3 Illustration of the computations of Naive on an input word.

◮ Proposition 18 .

 18 The maximal amount of memory used by Naive for processing u ∈ Σ * is in O(|Q| • |Γ| h(u) • out max (u)). The preprocessing time, and the time used by Naive to process each symbol of u are both polynomial in |Q|, |Γ|, |δ|, h(u), out max (u) and |Σ|.

  The preprocessing time, and the time used by Naive to process each symbol of u are both polynomial in |Q|, |Γ|, |δ|, h(u), out max (u) and |Σ|.

Proof.

  By an induction on |u|, it can be checked that C 0 u/lcpin(u,T ) -------→ τ C where C 0 is the only element in I τ and C is obtained from the run of t on u: C = rem_lcp(C ′ ) with C 0 u/ǫ --→ t C ′ . The remainder of the proof is similar to the proof of Lemma 17.

Figure 4 A

 4 Figure 4 A functional VPT on Σc = {c1, c2, c3} and Σr = {r1, r2, r3}.

Figure 5

 5 Figure 5 Part of the IST τ corresponding to the VPT in Fig. 4, computed by LcpIn on input c1c3r3r1.

  Internal node n of the DAG.

  Node n after update by factorize.

Figure 6

 6 Figure 6 Changes performed by factorize on a node.

Proposition 3 .

 3 ) is by Lemma 22. ◭ Let us first show that given a reduced fVPT T , Algorithm LcpIn runs, on an input word u, in space complexity O(|Q| 2• |Γ|2• (h(u) + 1) • out max = (u)). Correctness of Algorithm 3 is ensured by Lemma 22, and the fact that at the root node, it uses the same technique to factorize and output the lcp. In terms of memory requirement, the number of nodes of S T u remains bounded as before, while words on edges have length at most out max = (u), as each of them participate in a d-configuration in C(S T u ), as proved by Lemma 23 and Lemma 19.Consider now an arbitrary fVPT T . If T is not reduced, then we reduce it in polynomial time. Then, we can consider the Turing Transducer associated with algorithm LcpIn. It can be constructed in polynomial time, by correction of Algorithm LcpIn it computes the transduction T , and by the above property of Algorithm LcpIn, it runs in space complexity O((h(u) + 1) • out max = (u)).

  w 1 w 2 w 3 w 4 ) with the hypothesis (checked in parallel) that |v 2 v 4 | = |w 2 w 4 |. Let A, B, C, D be four words with A = a 1 . . . a l , B = b 1 . . . b m , C = c 1 . . . c n , D = d 1 . . . d p , l ≥ m. We show in Lemma 32 below, that ∆(A, B) = ∆(C, D) holds if, and only if, at least one out of four simple conditions is true. For example, the first condition states that there exists k such that a l-k = b l-k and either (i) k ≥ |C|, or (ii) c n-k = d n-k . The automaton guesses which condition holds and verifies it with the help of counters.

◮ 1 .2 3 .

 13 c n-k = d n-k , it uses two additional counters and proceeds similarly as for checking a l-k = b l-k , but checks equality instead of inequality. ◭ Lemma 32. Let A, B, C, D ∈ Σ * , such that A = a 1 . . . a l , B = b 1 . . . b m , C = c 1 . . . c n , D = d 1 . . . d p , and lm = np ≥ 0. We have that ∆(A, B) = ∆(C, D) if and only if one of the following conditions is satisfied: there exists k such that a l-k = b l-k and either (i) k ≥ |C|, or (ii) c n-k = d n-k ; 2. there exists k such that c n-k = d n-k and either (i) k ≥ |A|, or (ii) a l-k = b l-k ; The number s does not depend on the transducer T . there exists k such that a l-k = c n-k and either (i) k < lm, or (ii) there exists k ′ with a k ′ = b k ′ and k + k ′ ≤ l; 4. there exist k, k ′ such that b m-k = d p-k and a k ′ = b k ′ and k + k ′ ≤ m. Proof. Let us define E = A ∧ B and F = C ∧ D, and also A ′ , B ′ , C ′ , D ′ ∈ Σ * such that A = EA ′ , B = EB ′ , C = F C ′ and D = F D ′ , i.e. (A ′ , B ′ ) = ∆(A, B) and (C ′ , D ′ ) = ∆(C, D). We first prove that each condition implies ∆(A, B) = ∆(C, D), i.e. that (A ′ , B ′ ) = (C ′ , D ′ ). If |A ′ | = |C ′ | or |B ′ | = |D ′ | then the result is immediate. Now, assume that |A ′ | = |C ′ | and |B ′ | = |D ′ |.

4 .

 4 A ′ and C ′ differ on their kth letter from the right. Similar to proof of 3. Now suppose that ∆(A, B) = ∆(C, D) and let us show that one of the conditions is satisfied. First note that if B ′ = ε, then B is a prefix of A, and thus |A ′ | = lm. In particular, we obtain |A ′ | ≤ |C ′ | ≤ |C|. We call this property ( † B ). Similarly, D ′ = ε entails |C ′ | ≤ |A ′ | ≤ |A|, what we denote by ( † D ). We prove the property by considering several cases: |A ′ | > |C|: take k = |A ′ | -1, we have a l-k = b l-k . Note that b l-k does not exist iff lk > m, i.e. B ′ = ε. By property ( † B ), this can not occur. In addition, by definition of k, we have k ≥ |C| and thus condition 1.(i) is satisfied. |C ′ | > |A|: take k = |C ′ | -1, we have c n-k = d n-k (as above, ( † D ) ensures that d l-k is well defined) and k ≥ |A|: condition 2.(i) is satisfied. |A ′ | ≤ |C| and |C ′ | ≤ |A|: |A

◭ 6 .◭◮

 6 we suppose A ′ = C ′ and prove that condition 3 holds (the case B ′ = D ′ is similar with condition 4 holding). Because A ′ = C ′ and they have the same size, there must be a k < |A ′ | with a l-k = c n-k , we consider two cases:* |A ′ | ≤ |A| -|B|, this implies that k < |A| -|B| = lm therefore condition 3.(i) is satisfied. * |A ′ | > |A| -|B|, take k ′ = l -|A ′ | + 1 (the first position of A ′ in A).Then we have a k ′ = b k ′ and thus condition 3.(ii) is satisfied. A = ǫ and C = ǫ. This case is not possible since we have assumed A = C; 7. A = ǫ and D = ǫ (C = ǫ). We have ∆(Aw, Bw ′ ) = ∆(w, Bw ′ ) and ∆(Cw, Dw ′ ) = ∆(Cw, w ′ ). Suppose that E = G and F = H. Then there exists Z, Z ′ such that w = ZE, Bw ′ = ZF , Cw = Z ′ E and w ′ = Z ′ F . Therefore Bw ′ = BZ ′ F = ZF , and BZ ′ = Z, so that w = BZ ′ E and Cw = CBZ ′ E = Z ′ E, i.e. CB = ǫ, which contradicts C = ǫ; 8. B = ǫ and C = ǫ. This case is symmetric to the previous case; 9. B = ǫ and D = ǫ. Then we have ∆(Aw, Bw ′ ) = ∆(Aw, w ′ ) and ∆(Cw, Dw ′ ) = ∆(Cw, w ′ ). Again suppose that E = G and F = H, therefore there exists Z, Z ′ such that Aw = ZE, w ′ = ZF , Cw = Z ′ E and w ′ = Z ′ F . Therefore Z = Z ′ , which implies Aw = Cw. This contradicts A = C. Lemma 35. Let v 1 , v 2 , v 3 , v 4 , w 1 , w 2 , w 3 , w 4 ∈ Σ * and for all i ≥ 0, let

|v 2 |

 2 = |v 4 |: in that case we also have |w 2 | = |w 4 |, and suppose |v 1 | ≥ |w 1 | (the case |v 1 | < |w 1 | is similar). There exists Y ∈ Σ * , such that for any

  w 1 w 2 ). Moreover, let us suppose, by contradiction, that for all k ∈ N, if we replace u 2 by u 2 k (and thus v 2 and w 2 are replaced by v 2 k and w 2

		k
	respectively), we get a system such that neither (i) nor (ii) do hold, that is for all k ∈ N
	we have |v 2	k

Acknowledgements

The authors would like to thank Jean-François Raskin and Stijn Vansummeren for their comments on a preliminary version of this work.

* Partially supported by the ESF project GASICS, by the FNRS, by the ANR project ECSPER (JC09-472677), by the PAI program Moves funded by the the Federal Belgian Government and by the FET project FOX (FP7-ICT-233599). © Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier and Frédéric Servais; licensed under Creative Commons

C.3 Proof of Theorem 10

Let T be an fVPT. We show that T is HBM iff T satisfies the HTP.

If T is HBM, then the HTP holds for T by Lemma 30 (proved in this section). Conversely, if T satisfies the HTP, then we apply Lemma 31 (proved this section) which bounds the maximal difference between outputs of T , and then Proposition 3 gives the complexity the evaluation algorithm.

◮ Lemma 30. Let T be an fVPT. If T is HBM, then the HTP holds for T .

Proof. By definition of HBM and BM, if T is HBM and there exists K ∈ N such that for all u ∈ Dom(T ), h(u) ≤ K, then T is BM. Now suppose that the HTP does not hold for T . Therefore there are words u 1 , u 2 , u 3 , u ′ 3 , v 1 , v 2 , v 3 , w 1 , w 2 , w 3 , w 3 ∈ Σ * , stacks σ, σ ′ and states q, q ′ ∈ Q, q 0 , q ′ 0 ∈ I and q f , q ′ f ∈ F such that:

. By definition of FST(T, K) (states are configurations of T ) and of the twinning property for FSTs, the twinning property for FSTs does not hold for FST(T, K). Therefore FST(T, K) is not subsequentializable [START_REF] Choffrut | Une Caractérisation des Fonctions Séquentielles et des Fonctions Sous-Séquentielles en tant que Relations Rationnelles[END_REF] and by Proposition 24 FST(T, K) is not BM. Therefore T is not HBM, otherwise T could be evaluated in space complexity f (h(u)) on any input word u, for some function f . That corresponds to bounded memory if we fix the height of the words to K at most.

◭

For the converse, we can apply the evaluation algorithm of Section 3, whose complexity depends on the maximal delay between all the candidate outputs of the input word. We first prove that this maximal delay is exponentially bounded by the height of the word.

◮ Lemma 31. Let T be an fVPT. If the HTP holds for T , then for all s ∈ Σ * we have

, where M = max{|t| | (q, a, t, γ, q ′ ) ∈ δ}.

Proof. Let s ∈ Σ * . We consider two cases. We first assume that s ∈ Dom(T ). Let u ∈ Σ * be a prefix of s, we will prove that out = (u) ≤ (|Q| • |Γ| h(u) ) 2 M . Note that there exist N = |Q| • |Γ| h(u) configurations reachable by words of height less than h(u). The proof is similar to that of [START_REF] Béal | Determinization of transducers over finite and infinite words[END_REF] for FST. It proceeds by induction on the length of u. If |u| ≤ N 2 , then the result is trivial. Otherwise, assume that |u| > N 2 and let (q, σ, w), (q

we can decompose these two runs as follows:

In addition, we have

Indeed, by the choice of N , there must exist a pair of configurations that occurs twice. By the HTP property, we obtain ∆(v

. By Lemma 33 (see Appendix D.2), this entails the equality ∆(v

D.2 MTP is preserved by equivalent transducers

In this section we prove Theorem 14. We extend the concatenation to pairs of words and denote it by

Proof of Theorem 14

Proof. We assume that T 1 is not twinned and show that T 2 is not twinned either. By definition of the MTP there are two runs of the form

such that (q, σ 1 ) and (q ′ , σ ′ 1 ) are co-accessible and ∆(v

). We will prove that by pumping the loops on u 2 and u 4 sufficiently many times we will get a similar situation in T 2 , proving that T 2 is not twinned. It is easy to show that there exist

of T 2 such that we have the following runs in T 2 :

such that (q 1 , σ 1 ) and (q 2 , σ 2 ) are co-accessible with the same input word u 5 , and (q ′ 1 , σ ′ 1 ) and (q ′ 2 , σ ′ 2 ) are co-accessible with the same input word u ′ 5 . Now for all i ≥ 0, we let

In other words, D 1 (i) (resp. D 2 (i)) is the delay in T 1 (resp. T 2 ) accumulated on the input word u 1 (u 2 ) k1+ik2+k3 u 3 (u 4 ) k1+ik2+k3 by the two runs of T 1 (resp. T 2 ).

There is a relation between the words V (i) and W (i) . Indeed, since T 1 and T 2 are equivalent and (q 1 , σ 1 ) and (q 2 , σ 2 ) are both co-accessible by the same input word, for all i ≥ 1, either V (i) is a prefix of W (i) or W (i) is a prefix of V (i) , i.e. there exist X ∈ Σ * such that: for all i ≥ 1,

We now prove the following key result: for all i, j ≥ 1,

We consider two cases (the other ones being symmetric):

Then we have: ℓ) . Then we have:

Now by Lemma 36, since ∆(v

In particular since k 2 ≥ 1, we have D 1 (i) = D 1 (j) for all i, j ≥ i 0 and i = j. By the last intermediate result, we get D 2 (i 0 ) = D 2 (i 0 + 1). Therefore the MTP does not hold for

Proof. Let X = uu ′ ∧ vv ′ and Y = u ∧ v. There exists A, B, C, D such that A ∧ B = ǫ, C ∧ D = ǫ, and:

We have necessarily |X| ≥ |Y | since X is the longest common prefix of uu ′ and vv ′ and Y is the longest common prefix of u and v. Now we have Y Cu ′ = XA and Y Dv ′ = XB, i.e.

Proof. There exists A, B, C, D and X, Y such that: We can apply the same argument as case 2; 4. A = ǫ and C = cC ′ and D = dD ′ . This case is symmetric to case 2; 5. B = ǫ and C = cC ′ and D = dD ′ . This case is symmetric to case 2;