Emmanuel Filiot

Frédéric Servais

Visibly Pushdown Transducers with Look-Ahead

Visibly Pushdown Transducers (VPT) form a subclass of pushdown transducers. In this paper, we investigate the extension of VPT with visibly pushdown look-ahead (VPT la ). Their transitions are guarded by visibly pushdown automata that can check whether the well-nested subword starting at the current position belongs to the language they define. First, we show that VPT la are not more expressive than VPT, but are exponentially more succinct. Second, we show that the class of deterministic VPT la corresponds exactly to the class of functional VPT, yielding a simple characterization of functional VPT. Finally, we show that while VPT la are exponentially more succinct than VPT, checking equivalence of functional VPT la is, as for VPT, EXPTIME-C. As a consequence of these results, we show that for any functional VPT there is an equivalent unambiguous one.

Introduction

Visibly pushdown transducers (VPT) [START_REF] Staworko | Equivalence of deterministic nested word to word transducers[END_REF][START_REF] Filiot | Properties of visibly pushdown transducers[END_REF] form an interesting subclass of pushdown transducers (PT). Several problems that are undecidable for PT are decidable for VPT, noticeably: functionality is decidable in PTIME, k-valuedness in NPTIME and equivalence of functional VPT is EXPTIME-C [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF].

Visibly pushdown machines [START_REF] Alur | Visibly pushdown languages[END_REF], automata or transducers, are pushdown machines such that the behavior of the stack, i.e. whether it pushes or pops, is visible in the input word. Technically, the input alphabet is partitioned into call, return and internal symbols. When reading a call the machine must push a symbol on the stack, when reading a return symbol it must pop and when reading an internal symbol it cannot touch the stack. The partitioning of the input alphabet induces a nesting structure of the input words [START_REF] Alur | Adding nesting structure to words[END_REF]. A call symbol delimits an additional level of nesting, while a return symbol is a position in the word that ends a level of nesting. A word is well-nested if each call, respectively each return, has a matching return, respectively a matching call. Visibly pushdown transductions are transductions can be defined by VPT 1 .

In this paper, one of our motivations is to give a simple characterization of functional VPT that can be checked easily. Deterministic VPT are not expressive enough to capture all functional VPT, as for instance swapping the first and last letters of a word cannot be done deterministically. Instead of non-determinism, we show that some limited inspection of the longest well-nested subword starting at the current position (called the current well-nested prefix) is required to capture (non-deterministic) functional VPT. More precisely, we show that functional VPT-transductions are captured by deterministic VPT extended with visibly pushdown look-aheads that inspect the current well-nested prefix. Moreover, inspecting the current well-nested prefix is somehow the minimal necessary information to capture all functional VPT.

In this paper, we therefore introduce and investigate the class of VPT with visibly pushdown look-ahead. A VPT with visibly pushdown look-ahead (VPT la ) is a VPT such that call transitions are guarded with visibly pushdown automata (VPA). When reading a call at position i, a VPT la can apply a call transition provided the longest well-nested word starting at position i is included in the language of the VPA of the transition. Our main contributions are the following:

1. VPT la are as expressive as VPT, but exponentially more succinct.

For this we present an exponential construction that shows how a VPT can simulate look-aheads. Moreover we show this exponential blow-up is unavoidable.

2. Deterministic VPT la and functional VPT are equally expressive.

This equivalence is obtained by a construction (which is also exponential) that replaces the non-determinism of the functional VPT with deterministic look-ahead. This also yields an elegant and simple characterization of functional VPT.

3. Equivalence of functional VPT la is, as for VPT, EXPTIME-C. Therefore even though VPT la are exponentially more succinct than VPT, testing equivalence of functional VPT la is not harder than for functional VPT. This is done in two steps. First one checks equivalence of the domains. Then one checks that the union of the two transducers is still functional. We show that testing functionality is EXPTIME-C for VPT la : get rid of the look-aheads with an exponential blow-up and test in PTIME the functionality of the constructed VPT. To verify that the domains are equivalent, the naive technique (removing the look-aheads and then verifying the mutual inclusion of the domains) yields a doubly exponential algorithm. Instead, we show that the domains of VPT la are linearly reducible to alternating top-down tree automata. Testing the equivalence of such automata can be done in EXPTIME [START_REF] Comon | Tree automata techniques and applications[END_REF]. [START_REF] Eilenberg | Automata, Languages, and Machines[END_REF]. functional VPT and unambiguous VPT are equally expressive.

As an application of look-aheads, we show that a nice consequence of the constructions involved in contributions 1 and 3 is that functional VPT are effectively characterized by unambiguous VPT. This result was already known for finite-state transducers [START_REF] Eilenberg | Automata, Languages, and Machines[END_REF][START_REF] Schützenberger | Sur les relations rationnelles entre monoides libres[END_REF][START_REF] Elgot | On relations defined by generalized finite automata[END_REF] and here we extend it to VPT with rather simple constructions based on the concept of look-aheads. This characterization of functional finite-state transducers has been generalized to k-valued and k-ambiguous finite-state transducers [START_REF] Weber | Decomposing finite-valued transducers and deciding their equivalence[END_REF] and recently with a better upper-bound [START_REF] Sakarovitch | Lexicographic decomposition of k -valued transducers[END_REF] based on lexicographic decomposition of transducers.

Finally, we discuss slightly different look-aheads. First, we consider look-aheads that are allowed to inspect the whole current prefix until the end. We show this does not add expressivity nor succinctness. Second, we show that restricting the look-ahead to the current prefix in between the current call and its matching return is not sufficient to have a characterization of functional VPT by deterministic VPT la . All these results are new indications that the class of VPT is robust, and they show that the class of VPT la is interesting in itself.

Related Works Regular look-aheads have been mainly considered for classes of tree transducers, where a transition can be fired provided the current subtree belongs to some regular tree language. For instance, regular look-aheads have been added to topdown (ranked) tree transducers in order to obtain a robust class of tree transducers that enjoys good closure properties wrt composition [START_REF] Engelfriet | Top-down tree transducers with regular look-ahead[END_REF], or to macro tree transducers (MTT) [START_REF] Engelfriet | Macro tree transducers[END_REF]. For top-down tree transducers, adding regular look-ahead strictly increases their expressive power while MTT are closed by regular look-ahead [START_REF] Engelfriet | Macro tree transducers[END_REF].

Trees over an alphabet Σ can be linearized as well-nested words over the structured alphabet Σ c = {c a | a ∈ Σ}, Σ r = {r a | a ∈ Σ}. It is well-known that unranked trees can be represented by binary trees via the classical first-child next-sibling encoding (fcns). Top-down (ranked) tree transducers can thus be used as unranked tree transducers on fcns encodings of unranked trees. Inspecting a subtree in the fncs encoding corresponds to inspecting the first subtree and its next-sibling subtrees in an unranked tree, which in turn corresponds to inspecting the current longest well-nested prefix in their linearization. However as explained in [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF], top-down tree transducers and VPT are incomparable: top-down tree transducers can copy subtrees while VPT cannot, and VPT support concatenation of tree sequences while top-down tree transducers cannot.

Modulo those encodings, MTT subsume VPT [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF] and as we said before, there is a correspondence between the two notions of look-aheads, for VPT and MTT respectively. However it is not clear how to derive our results on closure by look-aheads from the same result on MTT, as the latter highly relies on parameters and it would require back-and-forth encodings between the two models. The direct construction we give in this paper is self-contained and allows one to derive the characterization of functional VPT as unambiguous VPT by a careful analysis of the construction.

Visibly Pushdown Languages and Transductions

All over this paper, Σ denotes a finite alphabet partitioned into two disjoint sets2 Σ c , Σ r , denoting respectively the call and return 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|. 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 . A visibly pushdown automaton (VPA) [START_REF] Alur | Visibly pushdown languages[END_REF] on finite words over Σ is a tuple A = (Q, I, F, Γ, δ) where Q is a finite set of states, I ⊆ Q the set of initial states, F ⊆ Q the set of final states, Γ the (finite) stack alphabet, and

δ = δ c ⊎ δ r where δ c ⊆ Q × Σ c × Γ × Q are the call transitions, δ r ⊆ Q × Σ r × Γ × Q are the return transitions.
On a call transition (q, a, γ, q ′ ) ∈ δ c , γ is pushed onto the stack and the control goes from q to q ′ . On a return transition (q, a, γ, q ′ ) ∈ δ r , γ is popped from the stack.

A configuration of a VPA 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 exists γ k ∈ Γ such that either

(q k-1 , a k , γ k , q k ) ∈ δ c and σ k = σ k-1 γ k or (q k-1 , a k , γ k , q k ) ∈ δ r and σ k-1 = σ k γ k .
The run ρ is accepting if q 0 ∈ I, q l ∈ F and σ 0 = σ l = ⊥ 3 . A word w is accepted by A if there exists an accepting run of A over w. L(A), the language of A, is the set of words accepted by A. A language L over Σ is a visibly pushdown language if there is a VPA A over Σ such that L(A) = L. Finally, a VPT is unambiguous if there is at most one accepting run per input word. In particular, any unambiguous VPT is functional. Unambiguity can be checked in PTIME [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF].

As finite-state transducers extend finite-state automata with outputs, visibly pushdown transducers extend visibly pushdown automata 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 and not necessarily wellnested), 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. 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.
Configurations and runs are defined similarly as VPA. Given a word u = a 1 . . . a l ∈ Σ * and a word v ∈ Σ * , v is an output of u by T if there exists an accepting run ρ = {(q k , σ k )} 0≤k≤l on u and l words v 1 , . . . , v l such that v = v 1 . . . v l and for all 0 ≤ k < l, there is a transition of T from (q k , σ k ) to (q k+1 , σ k+1 ) that produces the output v k+1 on input letter a k+1 . We write (q, σ) u/v --→ (q ′ , σ ′ ) when there exists a run on u from (q, σ) to (q ′ , σ ′ ) producing v as output. 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 . A transduction R is functional if for all u ∈ Σ * , there exists at most one v ∈ Σ * such that (u, v) ∈ R. A VPT T is functional if T is functional. Two transducers T 1 , T 2 are equivalent if T 1 = T 2 .
It is known [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF] that functionality is decidable in PTIME for VPT and equivalence of functional VPT is EXPTIME-C.

The class of functional VPT is denoted by fVPT. 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). If R is functional, we confound R(u) (which is at most of cardinality 1) and the unique image of u if it exists. The domain of T (denoted by Dom(T )) is the domain of T . Note that the domain of T contains only well-nested words, which is not necessarily the case of the codomain. Example 1. Let Σ c = {c, a}, Σ r = {r} be the call and return symbols of the alphabet. The following VPT T transforms a word as follows: (i) a and r are mapped to a and r respectively; (ii) c is mapped either to c if no a appears in the longest well-nested word starting just after c, and to a if an a appears. E.g. ccrarrcr is mapped to acrarrcr, and cccarrcrcarrrr to aaaarrcraarrrr.

The

VPT T = (Q, I, F, Γ, δ) is defined by Q = {q, q a }, I = {q}, F = Q, Γ = {(a,
a), (a, ¬a), (¬a, a), (¬a, ¬a), (-, a)} and δ contains the following transitions:

q c/c,(¬a,¬a) -------→ q q c/a,(a,¬a)
-------→ q q a/a,(-,a)

------→ q q a c/c,(¬a,a)

------→ q q a c/a,(a,a)

------→ q q a a/a,(-,a)

------→ q q r/r,(¬a,¬a)

-------→ q q r/r,(a,¬a)

------→ q a q r/r,(-,a)

------→ q a q a r/r,(a,¬a)

------→ q a q a r/r,(a,a)

-----→ q a q a r/r,(-,a)

------→ q a If T is in state q a it means that there is an a in the longest well-nested word that ends at the current position, otherwise it is in state q. Consider an element (α, β) of the stack. If α = a, respectively ¬a, it means that the call was a c and the automaton translated it into an a, respectively translated into a c, i.e. it guesses there is an a, respectively there is no a, in the well-nested word starting just after c. If α =then the call was an a. The second component β, carry over the fact that there is or not an a in the well nested word ending at the current call.

VPT with Visibly Pushdown Look-Ahead

Given a word w over Σ we denote by pref wn (w) the longest well-nested prefix of w. E.g. pref wn (ccrcr) = ǫ and pref wn (crc) = cr. We define a VPT T with visibly pushdown look-ahead (simply called look-ahead in the sequel) informally as follows. The lookahead is given by a VPA A without initial state. On a call symbol c, T can trigger the look-ahead from a state p of the VPA (which depends on the call transition). The lookahead tests membership of the longest well-nested prefix of the current suffix (that starts by the letter c) to L(A, p), where (A, p) is the VPA A with initial state p. If the prefix is in L(A, p) then the transition of T can be fired. When we consider nested words that encode trees, look-ahead correspond to inspecting the subtree rooted at the current node and all right sibling subtrees (in other words, the current hedge). Formally:

Definition 2. A VPT with look-ahead (VPT la ) is a pair T la = (T, A) where A is a VPA A = (Q la , F la , Γ la , δ la ) without initial state and T is a tuple T = (Q, q 0 , F, Γ, δ) such that Q is a finite set of states, q 0 ∈ Q is an initial state, F ⊆ Q is a set of final states, Γ is a stack alphabet, and δ = δ c ⊎ δ r is a transition relation such that δ c ⊆ Q × Σ c × Σ * × Q la × Γ × Q and δ r ⊆ Q × Σ r × Σ * × Γ × Q. Let u ∈ Σ * . A run of T la on u = a 1 . . . a l is a sequence of configurations ρ = {(q k , σ k )} 0≤k≤l such that there exist γ ∈ Γ and v k+1 ∈ Σ * such that (i) if a k+1 ∈ Σ r , then σ k+1 γ = σ k and (q k , a k+1 , v k+1 , γ, q k+1 ) ∈ δ r ; (ii) if a k+1 ∈ Σ c , then σ k+1 = σ k γ,
and there exists p ∈ Q la such that (q k , a k+1 , v k+1 , p, γ, q k+1 ) ∈ δ c and pref wn (a k+1 . . . a l ) ∈ L(A, p). The run ρ is accepting if σ 0 = σ l =⊥ and q l ∈ F . The word v 1 . . . v l is an output of u.

The VPT la T la is deterministic if for all transitions (q, c, v

1 , p 1 , γ 1 , q 1 ) ∈ δ c and (q, c, v 2 , p 2 , γ 2 , q 2 ) ∈ δ c , if v 1 = v 2 or γ 1 = γ 2 or q 1 = q 2 or p 1 = p 2 , then L(A, p 1 ) ∩ L(A, p 2 ) = ∅;
and for all transitions (q, r, v 1 , γ 1 , q 1 ) ∈ δ r and (q, r, v 2 , γ 2 , q 2 ) ∈ δ r we have v 1 = v 2 , γ 1 = γ 2 and q 1 = q 2 . Note that deciding whether some VPT la is deterministic can be done in PTIME. One has to check that for each state q and each call symbol c, the VPL guarding the transition from state q and reading c are pairwise disjoint. The number of states of a VPT la is the number of states of the transducer plus the number of states of the look-ahead.

Example 2. A VPT la is represented in Figure 1. The look-ahead automaton is depicted on the right, while the transducer in itself is on the left. It defines the transduction of Example 1. When starting in state q a , respectively q ¬a , the look-ahead automaton accepts well-nested words that contains an a, respectively does not contain any a. When starting in state q f it accepts any well-nested word. The transducer rewrites c symbols into a if the well-nested word starting at c contains an a (transition on the top), otherwise it just copy a c (transition on the right). This is achieved using the q a and q ¬a states of the look-ahead automaton. Other input symbols, i.e. a and r, are just copied to the output (left and bottom transitions).

The next theorem states that adding look-aheads to VPT does not add expressiveness. The main difficulty is to simulate an unbounded number of look-aheads at the same time. Indeed, a look-ahead is triggered at each call and is life until the end of the wellnested subword starting at this call. We use summaries [START_REF] Alur | Visibly pushdown languages[END_REF] to handle look-aheads that started at a strictly less deeper nesting level and a subset construction for those that started at the same nesting level.

Theorem 1. For all VPT la T la with n states, one can construct an equivalent VPT T ′ with O(n2 n 2 +1 ) states. Moreover, if T la is deterministic, then T ′ is unambiguous.

Proof. Let T la = (T, A) with T = (Q, q 0 , F, Γ, δ) and A = (Q la , F la , Γ la , δ la ). We construct T ′ = (Q ′ , q ′ 0 , F ′ , Γ ′ , δ ′ ) as follows (where Id Q la denotes the identity relation on Q la ):

Q ′ = Q × 2 Q la ×Q la × 2 Q la q ′ 0 = (q 0 , Id Q la , ∅) F ′ = {(q, R, L) ∈ Q ′ | q ∈ F, L ⊆ F la } Γ ′ = Γ × 2 Q la ×Q la × 2 Q la × Σ c
The transducers T ′ simulates T and its running look-aheads. A state of T ′ is a triple (q, R, L). The first component is the state of T . The second and third components are used to simulate the running look-aheads. When taking a call c, T ′ non-deterministically chooses a new look-ahead triggered by T . This look-ahead is added to all running lookaheads that started at the same nesting level. T ′ ensures that the run will fail if the longest well-nested prefix starting at c is not in the language of the triggered lookahead. The L component contains the states of all running look-aheads triggered at the current nesting level. The R component is the summary (see [START_REF] Alur | Visibly pushdown languages[END_REF]) necessary to update the L-component. When reading a call the L component is put on the stack. When reading a return, T ′ must check that all look-ahead states in L are final, i.e. T ′ ensures that the chosen look-ahead are successful.

After reading a well-nested word w if T ′ is in state (q, R, L), with q ∈ Q, R ⊆ Q la × Q la and L ⊆ Q la , we have the following properties. The pair (p, p ′ ) ∈ R iff there exists a run of A from p to p ′ on w. If some p ′′ is in L, there exists a run of a look-ahead that started when reading a call symbol of w at depth 0 which is now in state p ′′ . Conversely, for all look-aheads that started when reading a call symbol of w at depth 0, there exists a state p ′′ ∈ L and a run of this look-ahead that is in state p ′′ .

w c w ′ r L new l-a p0 push c, R, L ∪ {p0} pop c, R, L ∪ {p0} R L ′′ ⊆ F la R ′′ L ′ R ′ Fig. 2.
Let us consider a word wcw ′ r for some well-nested words w, w ′ (depicted on Fig. 2). Assume that T ′ is in state (q, R, L) after reading w (on the figure, the relation R is represented by dashed arrows and the set L by big points, and other states by small points). We do not represent the T -component of the states on the figure but rather focus on R and L. The information that we push on the stack when reading c is the necessary information to compute a state (q ′ , R ′ , L ′ ) of T ′ reached after reading wcw ′ r. After reading the call symbol c, we go in state (q ′ , Id Q la , ∅) and produce the output v for some q ′ , v such that q c|v,p0,γ -----→ q ′ ∈ δ c , where p 0 ∈ Q la is the starting state of a new look-ahead. Note that determinism of T is preserved. On the stack we put the tuple (γ, R, L ∪ {p 0 }, c) where γ, R, L, p 0 , c have been defined before. Now, suppose that after reading wcw ′ the transducer T ′ is in state (q ′′ , R ′′ , L ′′ ). It means that T is in state q ′′ after reading wcw ′ , and (p, p ′ ) ∈ R ′′ iff there exists a run of A from p to p ′ on w ′ , and L ′′ is some set of states reached by the look-aheads that started at the same depth as w ′ . Therefore we first impose that any transition from (q ′′ , R ′′ , L ′′ ) reading r must satisfy L ′′ ⊆ F la . Clearly, R ′ can be constructed from c, R and R ′′ . Finally, L ′ is a set which satisfies for all p ∈ L ∪ {p 0 }, there exists p ′ ∈ L ′ such that there exists a run of A from p to p ′ on cw ′ r. If such an L ′ does not exist, there is no transition on r. The set L ′ can be constructed from L ∪ {p 0 } and R ′′ .

We now define the transitions formally. First, for all q, R, L, c, γ, we have:

(q, R, L) c|u,(γ,R,L∪{p0},c) ------------→ (q ′ , Id Q la , ∅) ∈ δ ′ c whenever q c|u,p0,γ -----→ q ′ ∈ δ c
Then, for all R, L, r, γ, q ′′ , R ′′ , L ′′ , q ′ , R ′ , L ′ we have:

(q ′′ , R ′′ , L ′′ ) r|u,(γ,R,L,c) --------→ (q ′ , R ′ , L ′ ) ∈ δ ′ r
if the following conditions hold:

(i) q ′′ r|u,γ ---→ q ′ ∈ δ r , (ii) L ′′ ⊆ F la (iii) R ′ = {(p, p ′ ) | ∃s c,γ --→ s ′ ∈ δ la c • ∃(s ′ , s ′′ ) ∈ R ′′ • (p, s) ∈ R and s ′′ r,γ --→ p ′ ∈ δ la r } (iv) for all p ∈ L, there exist p ′ ∈ L ′ , γ ∈ Γ , s, s ′ ∈ Q la such that (s, s ′ ) ∈ R ′′ , p c,γ --→ s ∈ δ la c , s ′ r,γ --→ p ′ ∈ δ la r .
The proof of correctness is sketched in Appendix. If T is deterministic, then T ′ is unambigous. Indeed, it is deterministic on return transitions. If there are two possible transitions q c|u1,p1,γ1

------→ q 1 and q c|u2,p2,γ2

------→ q 2 on a call symbol c, as T is deterministic, we know that either the look-ahead starting in p 1 or the look-ahead starting in p 2 will fail. In T ′ , there will be two transitions that will simulate both look-aheads respectively, and therefore at least one continuation of the two transitions will fail as well. Therefore there is at most one accepting computation per input word in T .

⊓ While there is no known syntactic restriction on VPT that captures all functional VPT, we show that the class of deterministic VPT la captures all functional VPT. As there may be an unbounded number of accepting runs, the equivalent VPT la has to choose only one of them by using look-aheads. This is done by ordering the states and extending this order to runs. The main difficulty is to cope with nesting. Indeed, when the transducer enters an additional level of nesting, its look-ahead cannot inspect the entire suffix but is limited to the current nesting level. When reading a call, choosing (thanks to some look-ahead) the smallest run on the current well-nested prefix is not correct because it may not be possible to extend this run to an accepting run on the entire word. Therefore the transducer has to pass some information from one to the next level of nesting about the chosen global run.

Theorem 2. For all functional VPT T , one can construct a deterministic VPT la T la with exponentially many more states such that T = T la .

Proof. It is clear that deterministic VPT la are functional VPT. For the converse, we order the states of T and use look-aheads to choose the smallest runs wrt to an order on runs that depends on the structure of the word. Let T = (Q, q 0 , F, Γ, δ) be a functional VPT. Wlog we assume that for all q, q ′ ∈ Q, all α ∈ Σ, there is at most one u ∈ Σ * and one γ ∈ Γ such that (q, α, u, γ, q ′ ) ∈ δ. A transducer satisfying this property can be obtained by duplicating the states with transitions, i.e. by taking the set of states Q × ∆.

We construct an equivalent deterministic VPT la (T ′ , A) where

T ′ = (Q ′ , q 0 , F ′ , Γ ′ , δ ′ ) with Q ′ = {q 0 } ∪ Q 2 , F ′ = F × Q if q 0 ∈ F otherwise F ′ = (F × Q) ∪ {q 0 }.
The look-ahead A is defined later. Before defining δ ′ formally, let us explain it informally. There might be several accepting runs on an input word w, each of them producing the same output, as T is functional. To ensure determinism, T ′ has to choose exactly one transition when reading a symbol. The idea is to order the states by a total order < Q and to extend this order to runs. The look-ahead will be used to choose the next transition of T that has to be fired, so that the choice will ensure that T follows the smallest accepting run on w. However the look-ahead can only visit the current longest well-nested prefix, and not the entire word. Therefore the "parent" of the call c has to pass some information about the global run to its child c. In particular, when T ′ is in state (q, q ′ ) for some state q ′ , it means that T is in state q and the state reached after reading the last return symbol of the longest-well nested current prefix must be q ′ . Consider a word of the form w = c 1 w 1 r 1 w 2 c 3 w 3 r 3 where w i are well-nested, depicted on Fig. 3. Suppose that before evaluating w, T ′ is in state (q 1 , q 3 ). It means that the last transition T has to fire when reading r 3 has a target state q 3 . When reading the call symbol c 1 , T ′ uses a look-ahead to determine the smallest triple of states (q ′ 1 , q ′ 2 , q 2 ) such that there exists a run on w that starts in q 1 and such that after reading c 1 it is in state q ′ 1 , before reading r 1 it is in state q ′ 2 , after reading r 1 it is in state q 2 and after reading r 3 it is in state q 3 . Then, T ′ fires the call transition on c 1 that with source and target states q 1 and q ′ 1 respectively (it is unique by hypothesis), put on the stack the states (q 2 , q 3 ) and passes to w 1 (in the state) the information that the chosen run on w 1 terminates by the state q ′ 2 , i.e. it goes to the state (q ′ 1 , q ′ 2 ). (see Fig. 3). On the figure, we do not explicit all the states and anonymous components are denoted by . When reading r 1 , T ′ pops from the stack the tuple (γ, q 2 , q 3 ) and therefore knows that the transition to apply on r 1 has target state q 2 and the transition to apply on r 3 has target state q 3 . Then it passes q 3 to the current state.

(q 1 ,q 3 ) (q ′ 1 ,q ′ 2 ) (q ′ 2 ,q ′ 2 ) (q 2 ,q 3 ) ( ,q 3 ) ( , ) ( , )
( ,q 3 ) l.a. to choose the smallest

(q ′ 1 , q ′ 2 , q 2 ) i i+1 c 1 w 1 r 1 w 2 c 3 w 3 r 3
push (γ,q 2 ,q 3 ) pop (γ,q 2 ,q 3 ) Fig. 3.

When the computation starts in q 0 , we do not know yet what return transition has to be fired at the end of the hedge. This case can be easily treated separately by a lookahead on the first call symbol that determine the smallest 4-tuple of states (q 1 , q ′ 2 , q 2 , q 3 ) which satisfies the conditions described before, but to simplify the proof, we assume that the VPT accepts only words of the form cwr, where w is well-nested, so that one only needs to consider triples of states.

We now define the transition relation formally. Let < be a total order on states, extended lexicographically to tuples. For all states q 1 , q ′ 1 , q ′ 2 , q 2 , q 3 ∈ Q, it is easy to define a VPA A q1,q ′ 1 ,q ′ 2 ,q2,q3 whose size is polynomial in the size of T that accepts a word w iff it is of the form c 1 w 1 r 1 w 3 where w 1 , w 3 are well-nested and there exists a run of T on w that starts in state q 1 and is state q ′ 1 after reading c 1 , in state q ′ 2 before reading r 1 , in state q 2 after reading r 1 and in state q 3 after reading w 3 . Note that if w 3 = ǫ then if q 3 = q 2 , then w ∈ L(A q1,q ′ 1 ,q ′ 2 ,q2,q3 ). We denote by A q1,q ′ 1 ,q ′ 2 ,q2,q3 the complement of A q1,q ′ 1 ,q ′ 2 ,q2,q3 . We let B q1,q ′ 1 ,q ′ 2 ,q2,q3 a VPA with initial state p q1,q ′ 1 ,q ′ 2 ,q2,q3 that defines the language:

L(B q1,q ′ 1 ,q ′ 2 ,q2,q3 ) = L(A q1,q ′ 1 ,q ′ 2 ,q2,q3 ) ∩ (s1, s ′ 2 , s2) ∈ Q 3 (s1, s ′ 2 , s2) < (q1, q ′ 2 , q2) L(A q1,s1,s ′ 2 ,s2,q3 )
Such a VPA exists as VPA are closed by intersection and complement. Its size however may be exponential in |Q|. We define the look-ahead VPA as the union of all those VPA, A la = B q1,q ′ 1 ,q ′ 2 ,q2,q3 . We now define the call and return transitions of T ′ as follows, for all c ∈ Σ c , r ∈ Σ r , γ ∈ Γ, q 1 , q ′ 1 , q ′ 2 , q 3 , q ∈ Q, u ∈ Σ * :

(q 1 , q 3 ) c|u, (γ,q2,q3), p q 1 ,q ′ 1 ,q ′ 2 ,q 2 ,q 3 ------------------→ (q ′ 1 , q ′ 2 ) if (q 1 c|u,γ ---→ q ′ 1 ) ∈ δ c q 0 c|u, (γ,q3,q3), p q 0 ,q ′ 1 ,q ′ 2 ,q 3 ,q 3 ------------------→ (q ′ 1 , q ′ 2 ) if (q 0 c|u,γ ---→ q ′ 1 ) ∈ δ c (q ′ 2 , q) r|u,(γ,q2,q3) --------→ (q 2 , q 3 ) if (q ′ 2 r|u,γ ---→ q 2 ) ∈ δ r
The transducer T ′ is deterministic: return transitions are fully determined by the states q ′ 2 , q 2 , q 3 and the input letter r (by our first assumption there is at most one transition in T from q ′ 2 to q 2 ). For call transitions, suppose that from (q 1 , q 3 ) there are two possible look-aheads p q1,q ′ 1 ,q ′ 2 ,q2,q3 and p q1,s ′ 1 ,s ′ 2 ,s2,s3 . By definition of the look-aheads, we have L(B q1,q ′ 1 ,q ′ 2 ,q2,q3 )∩L(B q1,q ′ 1 ,q ′ 2 ,q2,q3 ) = ∅. Moreover, there cannot be two transitions with the same look-ahead as transitions are fully determinied by q 1 , q 3 , q 2 , q ′ 2 , q ′ 1 (there is at most one call transition by our assumption with source and target states q 1 and q ′ 1 respectively). A simple analysis of the complexity shows that the look-ahead A has exponentially many more states than T (the exponentiation comes from the complement in the definition of B q1,q ′ 1 ,q ′ 2 ,q2,q3 ).

⊓ ⊔

This construction, followed by the construction of Theorem 1 that removes the lookaheads, yields a nice characterization of functional VPT: Theorem 3. For all functional VPT T , one can effectively construct an equivalent unambigous VPT T ′ .

Functionality and Equivalence of VPT la

In this section, we study the problems of functionality of VPT la and equivalence of functional VPT la . In particular, we prove that while being exponentially more succinct than VPT, the equivalence of functional VPT la remains decidable in EXPTIME, as equivalence of functional VPT. Theorem 4. Functionality of VPT la is EXPTIME-C, even for deterministic look-aheads.

Proof. For the EXPTIME upper-bound, we first apply Theorem 1 to remove the lookaheads. This results in a VPT possibly exponentially bigger. Then functionality can be tested in PTIME [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF]. For the lower-bound, we reduce the problem of deciding emptiness of the intersection of n deterministic top-down tree automata, which is known to be EXPTIME-C when n is part of the input [START_REF] Comon | Tree automata techniques and applications[END_REF]. The full proof is in Appendix.

We know that the equivalence of two functional VPT is EXPTIME-C [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF]. To decide the equivalence of two functional VPT la , one can first remove the look-aheads, modulo an exponential blow-up, and use the procedure for VPT. This would yield a 2-EXPTIME procedure for the equivalence of functional VPT la . However, it is possible to decide it in EXPTIME: Theorem 5. Equivalence of functional VPT la is EXPTIME-C, even if the transducers and the look-aheads are deterministic.

Proof. The lower bound is obtained similarly as for functionality (see Appendix). For the upper-bound, in a first step we check equivalence of the respective domain of two VPT la (we show how to do it in EXPTIME). Then we check the equivalence as follows: transform each VPT la into an equivalent VPT with at most an exponential blow-up, take the union and verify (in PTIME) that the resulting VPT is still functional.

We now show how to check the equivalence of the domain of two VPT la . Let T 1 , T 2 be two VPT la . Their domains are defined by VPA extended with visibly pushdown look-aheads: it suffices to project away the output words in T 1 and T 2 respectively. We do not formally define VPA with look-aheads, but they can be defined as VPT la without considering output words. Let us denote A 1 , A 2 the VPA with look-ahead that define Dom(T 1 ) and Dom(T 2 ) respectively. We show how to check L(A 1 ) = L(A 2 ) in EXPTIME. The idea is to reduce the problem to equivalence of finite alternating tree automata, which is known to be in EXPTIME [START_REF] Comon | Tree automata techniques and applications[END_REF]. Well-nested words over the alphabet Σ = Σ c ⊎ Σ r can be translated as unranked trees over the alphabet Σ = Σ c × Σ r . Those unranked trees can be again translated as binary trees via the classical first-child next-sibling encoding [START_REF] Comon | Tree automata techniques and applications[END_REF]. VPA over Σ can be translated into equivalent top-down tree automata over first-child next-sibling encodings on Σ of well-nested words over Σ in PTIME [START_REF] Gauwin | Streaming Tree Automata and XPath[END_REF]. Look-aheads of VPA inspect the longest well-nested prefix of the current suffix. This corresponds to subtrees in first-child next-sibling encodings of unranked trees. Therefore VPA with look-aheads can be translated into top-down tree automata with look-aheads that inspect the current subtree. Top-down tree automata with such look-aheads can be again translated into alternating tree automata: triggering a new look-ahead corresponds to a universal transition towards two states: the current state of the automaton and the initial state of the look-ahead. This again can be done in PTIME. Since equivalence of finite alternating tree automata is in EXPTIME [START_REF] Comon | Tree automata techniques and applications[END_REF], one gets an EXPTIME upper-bound for testing equivalence of the domains of two VPT la .

⊓ ⊔

Discussion and Conclusion

Discussion We discuss several variants of visibly pushdown look-aheads. Instead of inspecting the longest well-nested current prefix, one could visit only the current wellnested prefix of the form cwr. This would correspond to the first subtree of the current hedge in encodings of unranked trees as well-nested words. While VPT would still be closed by such look-aheads, we would not have a correspondence between deterministic VPT la and functional VPT anymore. For instance, the class of transductions defined in Prop. 1 would not be definable by a deterministic VPT la , although it is a functional transduction. In some sense, our definition of look-ahead is the minimal requirement to get the equivalence between deterministic VPT la and functional VPT.

One could also allow look-aheads on return transitions. Such look-aheads would inspect the longest well-nested prefix starting just after the current return symbol. This could be easily simulated by look-aheads on call transitions in PTIME, and it would preserve determinism. Therefore our results still hold in this setting.

Another way of adding look-aheads is to allow them to inspect the whole current suffix. Such look-aheads can be defined by visibly pushdown automata where return transitions on empty stack are allowed, as originally defined in [START_REF] Alur | Visibly pushdown languages[END_REF]. The construction of Theorem 1 can be slightly modified to show that VPT are still closed by such lookaheads. The idea is to extend the states with a new component L ⊥ ⊆ Q la that corre-sponds to states of look-aheads that started at a deeper position than the current position. For those states we apply only return transitions on empty stack when reading a return symbol. See Appendix for a formal construction. Obviously, VPT with such look-aheads still satisfy the correspondence between functional VPT and deterministic VPT with look-ahead. However, the proof of the EXPTIME upper-bound for functional equivalence cannot be adapted as we cannot reduce the problem of testing equivalence of the domains to equivalence of alternating tree automata. We let the question of finding the exact complexity of functional equivalence for VPT with visibly pushdown look-ahead that inspect the whole suffix as future work.

Finally, note that most of our results also hold for VPA extended with visibly pushdown look-aheads: closure of VPA by visibly pushdown look-aheads, succinctness of VPA with look-aheads, and EXPTIME-completeness of equivalence of VPA with lookahead (even for deterministic VPA and look-aheads).

Future Work It is unknown whether k-valued VPT are equivalent to k-ambiguous VPT la . This question seems more difficult than for functional VPT. Indeed, let us assume that the look-aheads can visit the whole suffix (this setting is more powerful but already allows us to give some insights on the difficulty of this problem). For functional VPT, when several transitions are possible, we know that any of them that can be completed into an accepting run can be triggered. Therefore one just has to order the transitions and, by using a look-ahead, trigger the smallest satisfying this property. For k-valued VPT, among a set of possible transitions it is necessary to choose for each output word (among at most k output words) exactly one transition, in order to turn k-valuedness into k-ambiguity. It is not clear how to use look-aheads to make such choices.

A VPT with Visibly Pushdown Look-Ahead Proof (Correctness of the construction of Theorem 1). We sketch the proof of correctness of the construction. Let w ∈ Σ * such that w is a prefix of well-nested word. We define sh(w) as the longest well-nested suffix of w, we call sh(w) the subhedge of w. For instance, if w = c 1 c 2 r 2 c 3 r 3 , then sh(w) = c 2 r 2 c 3 r 3 . However if w = c 1 c 2 , then sh(w) = ǫ.

First, one can check (e.g. by induction on the length of w) that the successive computations of the R component of the state ensures that the following property holds: for all words w ∈ Σ * prefix of a well-nested word, if there is a run of T ′ from q ′ 0 to (q, R, L) on w, then for all p, p ′ ∈ Q la , (p, p ′ ) ∈ R iff there is a run of A on sh(w) from p to p ′ .

With this last property it is easy to show that the following property also holds: let w = c 1 w 1 r 1 c 2 w 2 r 2 . . . c n w n r n where all w i are well-nested. A run of T on w will trigger a new look-ahead at each call c i , all these look-ahead will still be 'live' until r n . These look-aheads are simulated by the L component of the state of T ′ . If there is a run of T on w, it means that all look-aheads accepts the respective remaining suffixes of w, and therefore after reading r i there are i accepting runs of the previous look-aheads. Suppose that those accepting runs are in the states Q i after reading r i . By suitable choices of L-components (T ′ is non-deterministic on L-components), we can ensure that there is an accepting run of T ′ such that after reading r i the L-component of the states is Q i , for all i. Conversely, if there is an accepting run of T ′ on w, then one can easily reconstruct accepting runs of the look-aheads.

⊓ ⊔ Proof (Proof of Proposition 1). We show that the exponential blow-up already holds with finite state automaton with regular look-ahead. This same blow-up is then obtained for VPT la accepting only flat words, i.e. words in (Σ c Σ r ) * (in that case the stack is useless). On such words each look-ahead visits the suffix of the whole word starting at the position it is triggered. More precisely, we can construct a VPT la such that any VPT needs an exponential number of states to have the same domain of the given VPT.

We now show how the exponential blow-up is obtained on finite state automata with look-ahead.

Let n ∈ N and L n = {vuv | |v| = n}. L n is definable by a finite state automaton with look-ahead A n with O(n) states. Let w = a 1 . . . a n w ′ and m = |w|. For all 1 ≤ i ≤ n, when reading a i , A uses a look-ahead to check that the (mn + i)-th letter of w is equal to a i . The look-ahead starts in a state q ai,n-i , non-deterministically guesses that the current position is the mn + i-th letter of u, verifies that it is equal to a i and decreases a counter from ni to 0 (the counter is implemented with ni states) to check that the guess was correct. A n as O(n) states.

Without a regular look-ahead, an automaton has to store the n-th first letters of w in its states, then it guesses the mn-th position and checks that the prefix of size n is equal to the suffix of size n. A simple pumping argument shows that the automaton needs at least |Σ| n states.

⊓ ⊔ .

B Closure by Visibly Pushdown Look-Ahead Inspecting the Whole Suffix

We consider in this section VPA that can trigger return transitions on empty stack. Such a VPA is a tuple (Q, q 0 , F, Γ, δ = δ r ⊎ δ c ⊎ δ ⊥ ) where δ ⊥ ⊆ Q × Σ r × Q denotes the set of those new transitions. We denote by VPT + la the set of visibly pushdown transducers with look-aheads that can inspect the whole suffix. We prove that VPT are closed by such look-aheads. The construction is done by a slight modification of the construction given in the proof of Theorem 1.

The idea is extend the states a the constructed VPT with a new component L ⊥ ⊆ Q la that corresponds to states of look-aheads that started at a deeper position than the current position., and such that any position in between the position at which they started and the current position is not above the current position. For instance, let us consider a well-nested word of the form wcc 1 w 1 r 1 . . . c n w n r n rw ′ where w i is wellnested. After reading r i , L ⊥ contains current states of look-aheads that started when reading the words w 1 , . . . , w n . We therefore have two L-components: the look-aheads that started when reading c 1 , . . . , c n and the new look-ahead component. When reading c, we push on the stack this new component. Let us formally define the construction. From a VPT + la T = (Q, q 0 , F, Γ, δ) with look-ahead A = (Q la , q la 0 , F la , Γ la , δ la ), we construct an equivalent VPT T ′ = (Q ′ , q ′ 0 , F ′ , Γ ′ , δ ′ ) possibly exponentially bigger as follows:

-Q ′ = Q × 2 Q la ×Q la × 2 Q la × 2 Q la ; -Γ ′ = Γ × 2 Q la ×Q la × 2 Q la × 2 Q la × Σ c ; -F ′ = {(q, R, L, L ⊥ ) ∈ Q ′ | q ∈ F, L ⊆ F la , L ⊥ ⊆ F la }.
q ′ 0 = (q 0 , Id Q la , ∅, ∅).

The transitions are defined as follows:

First, for all q, R, L, L ⊥ , c, γ, we have:

(q, R, L, L ⊥ ) c|u,(γ,R,L∪{p0},L ⊥ ,c)

---------------→ (q ′ , Id Q la , ∅, ∅) ∈ δ ′ c whenever q c|u,p0,γ -----→ q ′ ∈ δ c

Then, for all R, L, L ⊥ , r, γ, q ′′ , R ′′ , L ′′ , L ′′ ⊥ , q ′ , R ′ , L ′ , L ′ ⊥ we have:

(q ′′ , R ′′ , L ′′ , L ′′ ⊥ )

r|u,(γ,R,L,L ⊥ ,c)

-----------→ (q ′ , R ′ , L ′ , L ′ ⊥ ) ∈ δ ′ r if the following conditions hold:

(i) q ′′ r|u,γ ---→ q ′ ∈ δ r ; (ii) R ′ = {(p, p ′ ) | ∃s c,γ --→ s ′ ∈ δ la c • ∃(s ′ , s ′′ ) ∈ R ′′ • (p, s) ∈ R and s ′′ r,γ --→ p ′ ∈ δ la r } (iii) for all p ∈ L (resp. L ⊥ ), there exist p ′ ∈ L ′ (resp. L ′ ⊥ ), γ ∈ Γ , s, s ′ ∈ Q la such that (s, s ′ ) ∈ R ′′ , p c,γ --→ s ∈ δ la c , s ′ r,γ --→ p ′ ∈ δ la r ; (iv) for all p ∈ L ′′ ⊥ , there exist p ′ ∈ L ′ ⊥ , such that p r -→ p ′ ∈ δ la ⊥ .

C Decisions Problems

Proof of Theorem 4, Lower Bound Given n deterministic top-down binary tree automata T 1 , . . . , T n over an alphabet ∆, one can construct in linear-time n deterministic VPA A 1 , . . . , A n that define the same languages as T 1 , . . . , T n respectively, modulo the natural encoding of trees as nested words over the structured alphabet ∆ = {c a | a ∈ ∆} ⊎ {r a | a ∈ ∆} [START_REF] Gauwin | Streaming Tree Automata and XPath[END_REF]. The encoding corresponds to a depth-first left-to-right traversal of the tree. For instance, enc(f (f (a, b), c)) = c f c f c a r a c b r b r f c c r c r f . We now construct a VPT la T over the alphabet ∆ such that T is functional iff i L(T i ) = ∅. The domain of T are words of the form w n,t = c 1 r 1 . . . c n r n enc(t) for some ranked tree t over ∆. It is easy to define a VPA that accepts such words and whose size is polynomial in n and ∆. The n first call symbols are used to run n look-aheads. When the i-th call c i is read, a look-ahead B i checks that enc(t) ∈ L(A i ): it first count that 2(ni + 1) symbols have been read and go to the initial state of A i . The output words of T are produced as follows: when reading c i , there are two possible transitions, that both push the same symbol on the stack, launch the same look-ahead, and goes to the same state, but output two different words, let say c a and r a respectively. If the look-ahead is not accepting the suffix, then none of these transitions can be fired and the computation stops. Any run of T on the word w n,t is accepting. Therefore there is an accepting run of T on w n,t iff enc(t) ∈ i L(A i ), and in that case there are 2 n accepting runs whose output words are of the form α 1 . . . α n respectively where α i ∈ {c a , r a }. Therefore T is not functional iff there is a tree t such that enc(t) ∈ i L(A i ), iff there is a tree t such that t ∈ i L(T i ). Note that the look-aheads are deterministic.

⊓ ⊔

Proof of the lower bound for Theorem 5 Lower bound The lower-bound in the case where both the transducer and the look-ahead are deterministic is obtained similarly as the lower-bounds for functionality, i.e. by reduction of the emptiness of n deterministic top-down tree automata T 1 , . . . , T n . We construct two deterministic VPT la T 1 , T 2 with deterministic look-aheads as in the proof of the lower-bound of Theorem 4, except that the output words are produced differently. On the word c 1 r 1 . . . c n r n enc(t), the transducer T 1 (resp. T 2 ) outputs c a (resp. r a ) when reading c i and only if the lookahead is accepting, i.e. t ∈ L(T i ). Both transducers are deterministic and as we saw, the look-aheads are also deterministic. Now, the image of T 1 (resp. T 2 ) is non-empty iff L(T i ) = ∅ iff there exists a tree t such that (w n,t , c n a ) ∈ T 1 (resp. (w n,t , r n a ) ∈ T 2 ). Therefore T 1 and T 2 are equivalent iff L(T i ) = ∅.

Fig. 1 .

 1 Fig. 1. A VPT la (left) and its look-ahead (right) on Σc = {c, a} and Σr = {r}

⊔

  Proposition 1. Let Σ be a finite alphabet with at least two letters. There exists a family of transductions (T n ) n over Σ such that for all n ≥ 0, T n is definable by a VPT la with O(n) states and any VPT defining L n has at least O(2 n ) states.Proof (sketch). We show that the result already holds for finite state automata with regular look-ahead, which yields a construction for VPT la . VPT on flat words (in (Σ c Σ r ) * ) can indeed simulate finite state automata (in that case the stack is useless). For all n, we define the language L n = {vuv | |v| = n}. We show that L n can be recognized by a finite state automaton with regular look-ahead with O(n) states while without regular look-ahead any automaton would need at least |Σ| n states.

⊓ ⊔ 4 Functional VPT and VPT la

In this paper when it is clear from the context, we also use VPT to denote visibly pushdown transductions

In contrast to[START_REF] Alur | Visibly pushdown languages[END_REF], we do not consider internal symbols i, as they can be simulated by a (unique) call ci followed by a (unique) return ri. All our results extend trivially to alphabets with internal symbols. We make this assumption to simplify notations.

[START_REF] Comon | Tree automata techniques and applications[END_REF] Note that, in contrast to[START_REF] Alur | Visibly pushdown languages[END_REF] and to ease notations, we do not allow return transition on ⊥ and we require the final stack to be empty. This implies that all accepted words are well-nested.


Agostino ; Baldacci

Paolo Stoppa
email: stoppa@unive.it

Santi Giorgianni

René Larsen

R Wugt Larsen

High resolution FTIR spectrum of CH2D79Br: the ground, v5 = 1 and v9 = 1 state constants

Keywords: Monodeutero methyl bromide, CH2D79Br, Rovibrational analysis, FTIR spectroscopy Monodeutero methyl bromide, CH 2 D 79 Br, Rovibrational analysis, FTIR spectroscopy

The first high resolution infrared spectrum of CH 2 D 79 Br has been investigated in the range 710 -1080 cm -1 by Fourier transform infrared spectroscopy employing a synchrotron radiation source at an unapodized resolution of 0.0025 cm -1 . This spectral region accounts for the fundamental bands ν 5 (ν 0 = 768.809 cm -1 ) and ν 9 (ν 0 = 930.354 cm -1 ) having the structure of hybrid a-/b-and c-type bands of near prolate asymmetric tops, respectively. The rovibrational analysis has been performed over a wide range of transitions with quantum numbers J ≤ 72 and K a ≤ 16. The experimentally determined ground state constants including four sextic coefficients have been obtained for the first time by merging the ground state combination-differences of the two bands. The Areduced Watson Hamiltonian in the I r representation has been adopted to fit the data.

Only weak interaction effects ascribed to a-type Coriolis coupling were influencing the K a = 10 -14 stacks of the bands. The residuals were adjusted by including in a dyad model one higher order interaction term.

Methyl bromide, CH 3 Br, is currently object of experimental [1][2][3] and theoretical [4] investigations due to environmental problems connected to the atmospheric transformation processes involving photolysis and chemical reactions with ozone, hydroxyl and nitrate radicals [5,[START_REF]Scientific Assessment of Ozone Depletion: 2006 Global Ozone Research and Monitoring Project Report[END_REF]. Harmonic and ab initio anharmonic force fields were performed by Schneider and Thiel [START_REF] Schneider | [END_REF][8][9]. The molecular parameters calculated ab initio at different levels of theory, including the symmetric and asymmetric deuterium isotopologues, were given by Venkatraman et al. [10]. Absolute integrated infrared intensities of the fundamental bands were determined by Van Staten and Smit [11].

Raman and microwave data of the partially deuterium isotopologues are unavailable from literature whereas IR measurements were mainly confined to the regions of the fundamental bands [12]. Only very recently IR studies on CH 2 DBr, performed in a large spectral range, provided the assignment of an extensive number of vibrational states with the support of an improved anharmonic force field [13]. From the partially resolved rotational structure of b-and c-type bands, a number of spectroscopic parameters was also evaluated.

In this paper, we report for the first time the results obtained from the high resolution IR spectrum of the ν 5 and ν 9 fundamental bands of CH 2 D 79 Br. The pure sample has been prepared in our laboratory for spectroscopic purposes. The choice of selecting one of the 79/81 bromine species is motivated by the near coincidence of the band origins which produce high density spectral lines in particular near the band centres. The ground state constants were obtained through suitable combination in the last fits a high order interaction term was introduced in a dyad model to take into account the systematic displacements observed in the higher K a stacks of both bands.

Experimental details

Synthesis of the sample

CH 2 D 79 Br was prepared by brominating CH 2 DOH (CDN Isotopes, 99.2 atom % D) using Na 79 Br (O.R.N.L., 98.82 atom % 79 Br) and dilute H 2 SO 4 [14]. The reaction took place in an evacuated Pyrex tube, provided with a HP Rotaflo stopcock placed in a oven at 250 °C for 24 h. The product was separated from the excess of CH 2 DOH by low temperature distillation under dynamic vacuum. No evidence of organic impurities was found in the sample by standard IR techniques. However the high resolution spectrum showed weak lines due to the perpendicular band ν 6 (955 cm -1 ) of CH

Recording of the spectrum

The high resolution (0.0025 cm -1 ) infrared absorption spectrum of the isotopically enriched CH 2 D 79 Br sample has been recorded at 296 K in the spectral region between 650 and 1100 cm -1 with the Bruker IFS 120 HR Fourier transform infrared spectrometer located at the infrared beam-line at MAX-lab (Lund University, Sweden). The highly brilliant synchrotron radiation source offered from the MAX-I electron storage ring was employed as an external radiation source [15,16]. MAX-I is a 550 MeV electron storage ring with a 300 mA maximum ring current and a mean lifetime of about 4 h. The synchrotron beam is practically an infrared point source and an aperture was solely employed to limit the amount of thermal background radiation.

The Michelson interferometer was equipped with a Ge/KBr beam splitter, the detector was a narrowband MCT and selected optical and electronic filters were employed to reduce the photonic noise level, detector nonlinearity effects and eliminate aliasing. The sample of 0.433 kPa CH 2 D 79 Br was kept in 0.5-L multipass absorption cell with a total optical path length of 184 cm. The collected interferograms (210 co-added scans) were post-zerofilled and the absorption line positions were fitted using the Microcal Origin Pro 8 software package. The absolute wave number scale of the resulting transmittance spectrum was subsequently calibrated against absorption lines of CO 2 reported by V.-M.

Horneman [17]. The accuracy of the line positions is estimated to ~0.0015 cm -1 for unblended lines.

Results and discussion

The CH 2 D 79 Br molecule is a near prolate asymmetric rotor (κ = -0.997)

belonging to the C s point group. All nine fundamental modes (six of A' and three of A" symmetry species) are infrared-active. The bands arising from the normal vibrations are summarized in Table 1. The survey IR spectrum of the region investigated is shown in Figure 1. The ν 5 hybrid band exhibits a prominent central Q-branch typical of an a-type contour and a rotational profile in the wings of the P, R branches due to the weaker btype component whereas ν 9 manifests the rotational structure of a c-type band. On the whole the contours approach to the parallel (a-type) and perpendicular bands (b-and ctype) of prolate symmetric rotors. In order to interpret the well resolved rovibrational structure, initial spectral predictions were performed using the spectroscopic parameters of [13] obtained from the analysis of the partially resolved structure identified in the IR spectrum of CH 2 DBr in natural abundance.

The rovibrational analysis of ν 5 begun by considering the a-type component.

From a preliminary scrutiny of the spectrum it was found, as expected from the medium resolution data [13], that the Q-branch is moving to the blue and within each multiplet a series of lines degrading to lower wavenumbers could be followed until they merge into the next one. Correspondingly group of regularly spaced lines decreasing their intensity were also readily apparent in the P-and R-branches near the band centre. The assigned transitions were used for initial calculation of the ground state constants through GSCDs then fixed for a rough evaluation of the upper state parameters. Correlation diagrams, which combine P, Q, and R-transitions reaching the same upper sublevels, were adopted according to the method early described by Nakagawa and Overend [18]. These plots display line position and relative intensity for each K a subband occurring in the P, Q, and R branches. When significant and systematic deviations from a vertical set of transitions were reproduced, the progression of assignment was provided by refining the spectroscopic constants of the ground and upper levels. Figure 2 displays a picture of the rotational structure of the q Q K (J)-subbranches. The assignment was performed from the weak lines with K a = 2 and proceeded up to K a = 15 with J ≤ 25 for the stronger subbranches. Conversely the sequences of the q (P,R) K (J) multiplets are almost completely mixed up. In this case the assignment reached K a = 14 and J ≤ 71. Lines undergoing to asymmetry splitting were found up to K a = 3 with the even (K a " + K c " = J") component located at lower and higher wavenumbers in the P-and R-branches, respectively, compared to the odd (K a " + K c " = J" + 1) one. At this point of analysis the identified transitions provided comparable centrifugal distortion constants for the lower and upper states.

In As a result the r (R,Q) K (J) and p (P,Q) K (J) subbranches up to K a ' = 15 and 8, respectively, with J ≤ 60 were positively identified.

The rovibrational analysis of ν 9 was accomplished in a similar fashion to that described for the b-type component of ν 5 . Predictions were performed using the information of Ref. [13] together with the determined ground state constants from ν 5 .

Just as for the perpendicular component of ν 5 , the p,r Q-subbranches are evenly spaced and approximately separated by the term value 2(A -B ) = 7.36 cm -1 , where B = (B + C) / 2. The rotational structure, with partial exclusion of the p Q 1 (J) manifold, is fully resolved. In absence of asymmetry splitting each K a manifold degrades to lower wavenumbers as J increases thus indicating that, as for ν 5 , B of v 9 = 1 is comparatively smaller than that of the ground state. An example of a typical multiplet is illustrated in Figure 3. The p P K (J) and r R K (J)-subbranches widely spread out all over the spectral region where the P-wing merges into the R-branch extremity of ν 5 . Within each sequence, the J lines are regularly spaced by about 2 B = 0.59 cm -1 . The weaker r P K (J)

and p R K (J) transitions with K a values up to medium quantum numbers were also identified and included in the dataset. Asymmetry splitting was observed up to K a ' = 5. Assignment was extended up to K a = 16 and J ≤ 72 in both P-and R-branches which show comparable line intensity.

As mentioned the ground state spectroscopic constants of CH 2 D 79 Br are unavailable in the literature. However they can be provided with an high level of accuracy by merging the large number of GSCDs produced from the dataset of ν 5 and ν 9 . This was done by excluding the transitions ascribed to broad lines due to overlapping or to partially unresolved features for the asymmetry splitting. More than 12400 GSCDs (K a ≤ 16 and J ≤ 71) with ∆K a = 0, ±1, ±2 were calculated and weighted were weighted with the reciprocal of the number of differences carried out in each group [19]. In the least-squares procedure the ground state constants were determined by computing the rotational energy levels with Watson's A-reduction Hamiltonian in the I r representation [START_REF] Watson | Vibrational Spectroscopy and Structure[END_REF]. The preliminary fits were performed by varying the constants up to fourth order; then a number of higher order centrifugal distortion terms were tested to take into account the significant systematic deviations in the residuals. The determined ground state constants which include four sixth order term values are listed in Table 2.

The rovibrational structure of the ν 5 and ν 9 bands could be fitted separately within the accuracy of measurements for a large number of transitions. However The excited state spectroscopic parameters are included in Table 2. They represent the best set of constants obtained with a standard deviation of 0.44 x 10 -3 cm -1 .

Statistically only five randomly distributed assigned transitions revealed displacements higher than ±0.0020 cm -1 from the calculated values. The standard deviation of the fit is more than three times lower than the estimated accuracy of measurements. The quartic centrifugal distortion constants are all comparable with the ground state values as well as the less accurate sextic terms with exclusion of the Φ KJ constant of ν 5 . The observed discrepancy is probably due to the existence of further weak Coriolis resonances between v 5 = 1 and v 6 = 1 levels. The comparison of the vibration-rotation interaction constants of ν 5 and ν 9 with the computed values predicted from the anharmonic force field [23], given in Table 3, shows a general good agreement thus indicating that additional interactions are only marginal. It should be lastly mentioned that many weak unassigned features are present in the spectrum. Most of them belong to transitions due to hot bands from the low lying v 6 = 1 state: the Boltzmann population at room temperature of this level is predicted about 6% of the ground vibrational state.

The list of assigned transitions and the (obs.-calc.) values resulting from the spectroscopic parameters of Table 2 are available upon request from one of the authors (P.S.).

  ) from the rovibrational transitions of ν 5 (a / b-hybrid band) and ν 9 (c-type band) fundamentals. The dataset of each band was initially treated using the classical Hamiltonian model of Watson for asymmetric top molecules. Indeed these levels, separated by about 160 cm -1 , are weakly perturbed by Coriolis resonance. Only

  the b-type component the p,r Q K (J) clusters regularly degrade to lower wavenumbers. They can be easily distinguished in spectral regions where the a-type lines show negligible line strength. In absence of asymmetry splitting, observed for transitions with K a ' ≤ 4, the clusters are completely resolved even at the band heads. The rovibrational assignment was computer assisted by graphical correlation plots where in this case a large number of transitions showing different line intensities, sharing a common upper state sublevel, can be combined. When the new data were added in a bootstrap procedure by refining the lower and upper state parameters, the A rotational and the ∆ K centrifugal distortion constants greatly improved in accuracy. However, as also shown in Figure1, the line strengths in the P-and R-branches differ significantly.

  number of transitions sharing a common upper level. In detail they

  systematic deviations from the calculated values were observed for K a ' = 12 of ν 5 and K a ' = 10 of ν 9 . The residuals (observed -calculated values) of the transitions involving the two sublevels increasing with J were similar in magnitude but different in sign. This suggested the presence of a local perturbation between the upper states. The ν 5 and ν 9 levels are of A' and A" symmetry species, respectively; hence they can interact through a-(∆K a = 0, ±2,…) and / or b-type (∆K a = ±1, ±3,…) Coriolis resonance. The approximate energy level diagram shows that in our range of assignment the perturbation can locally affect sublevels differing by two units in K a ; the interaction is therefore of a-type Coriolis with ∆K a = ±2.Taking into account the perturbation term, about 14000 assigned transitions were simultaneously fitted by fixing the ground state constants at the values determined in the present work. Calculation was carried out using the ATIRS package software[START_REF] Tasinato | [END_REF] and in particular the VCALPGM program, a graphical interface to the Pickett's SPFIT / apparently unperturbed transitions whereas the initial estimated value of the a-type Coriolis term (η bc 9 , 5 = 0.79 x 10 -4 cm -1 ) was calculated by considering the maximum energy shift observed for K a ' = 10 and J' = 62 of ν 5 . In the least squares fit only apparently single lines were considered.

  resolution IR study of the ν 5 and ν 9 fundamentals of the near prolate asymmetric top CH 2 D 79 Br has been performed. The fully resolved rotational structure of the a-, b-hybrid ν 5 and c-type ν 9 bands allowed an accurate determination of the ground state constants through GSCDs. They should be of great help in studies concerning more complex band systems of the molecule. The precise value of the rotational constant A 0 is important for the structure determination whereas the evaluation of the centrifugal distortion constants of the asymmetric species are useful for an improvement of the force field of methyl bromide. A local perturbation affecting the ν 5 and ν 9 bands due to the near coincidence of the K a sublevels differing by two units has been detected. The upper state spectroscopic parameters have been obtained by fixing the ground state constants and using a higher order a-type Coriolis interaction term in a dyad model. The unassigned weak lines mainly belong to hot bands with v 6 = 1 as lower state. In order to interpret this additional structure, the rovibrational analysis of the low lying fundamental is in progress.

Fig. 1 Fig. 2

 12 Fig. 1 Overview of the medium resolution (0.2 cm -1 ) transmission spectrum of CH 2 D 79 Br in the region of the ν 5 and ν 9 fundamentals (room temperature,

Fig. 3

 3 Fig.3The r Q 9 (J) subbranch of the ν 9 fundamental of CH 2 D 79 Br. This typical line

15 Table 1 .

 151 Gas Phase Infrared Fundamental Bands of CH 2 D 79 Br a a Ref.13. Abbreviations used are as follows: s = strong, m = medium, w = weak. The experimental error in parentheses is on the last significant digit.

	Symmetry species	Mode	Wavenumber / cm -1 Relative Intensity b Approximate description
		Α'	ν 1	3001.04(1) c	s	CH 2 sym. stretch
			ν 2	2243.80(1)	m	CD stretch
			ν 3	1424.94(1)	s	CH 2 deformation
			ν 4	1225.21(5)	s	CH 2 wag
	F o r	Α"	ν 5 ν 6 ν 7	768.80852(8) 595.0(2) 3052.96(2)	m s m	D-C-Br deformation CBr stretch CH 2 antisym. stretch
	P		ν 8 ν 9	1252.55(3) 930.35379(8)	w m	CH 2 twist CH 2 rock
	e
	e r
		R
		e
			v i e
				w
				O n l
				y

b c

Table 2 .

 2 Spectroscopic constants (cm -1 ) for the ground, v 5 = 1 and v 9 = 1 states of CH 2 D 79 Br a

			Molecular Physics
			Ground state	v 5 = 1	v 9 = 1
		ν 0		768.808516(82)	930.353789(82)
		A	3.97445755(114)	3.9862648(39)	4.0006428(31)
		B	0.29756678(20)	0.29658963(29)	0.29668616(32)
		C	0.29232654(20)	0.29128939(29)	0.29137974(35)
	∆ J	× 10 6	0.272868(92)	0.272223(99)	0.273700(104)
	∆ JK × 10 5	0.330164(113)	0.31944(31)	0.35180(25)
	∆ K × 10 4	0. 562090(102)	0.56476(44)	0.59830(27)
	δ J	× 10 8	0.47691(84)	0.4290(27)	0.5160(33)
	δ K	× 10 6	0.5525(154)	0.445(65)	0.617(77)
	Φ J × 10 13	-0.764(128)	-0.914(147)	-0.827(160)
	Φ JK × 10 11	0.347(28)	0.258(67)	0.478(52)
	Φ KJ × 10 10	0.517(38)	-0.460(127)	0.902(84)
	Φ K × 10 8	0.2727(28)	0.2288(137)	0.3465(65)
	η bc 9 , 5	× 10 4		0.8182(100)
	No. of data	12462	6765	7070
	J max		71	71	72
	K a max		16	15	16
	σ	× 10 3	0.472	0.439

a Quoted uncertainties in parenthesis are one standard deviation in units of the last significant digits.

Page 16 of 21 URL: http://mc.manuscriptcentral.com/tandf/tmph

Table 3 .

 3 Vibration-rotation interaction constants α (cm -1 ) for CH 2 D 79 Br

		Molecular Physics
		ν 5		ν 9
		Experimental	Calculated a	Experimental	Calculated a
	α A × 10 3	-11.807	-11.891	-26.185	-26.821
	α B × 10 3	0.977	0.935	0.880	0.857
	α C × 10 3	1.037	1.000	0.947	0.907

a Calculated from the anharmonic force field predicted from coupled cluster CCSD(T) with cc-pVTZ basis set

[23]

. Page 17 of 21 URL: http://mc.manuscriptcentral.com/tandf/tmph

Acknowledgments

The authors thank the Financial support by PRIN 2007 (project: "Trasferimenti di energia, carica e molecole in sistemi complessi") and the University of Ca' Foscari Venice (FRA funds). They are also grateful to A. Baldan who kindly prepared the high purity sample of the 79 Br isotopologue of CH 2 DBr. Support by the European Community -Research Infrastructure Action under the FP6 "Structuring the European Research Area" Programme (through the Integrated Infrastructure Initiative "Integrating Activity on Synchrotron and Free Electron Laser Science") is acknowledged. One of the authors (R.W.L.) acknowledges a fellowship grant from the Carlsberg Foundation.