key: cord-0043830-o2jk06pz
authors: Löbel, Raphaela; Luttenberger, Michael; Seidl, Helmut
title: On the Balancedness of Tree-to-Word Transducers
date: 2020-05-26
journal: Developments in Language Theory
DOI: 10.1007/978-3-030-48516-0_17
sha: 1e0f9080fa69840c160678b7f200345179cc148a
doc_id: 43830
cord_uid: o2jk06pz

A language over an alphabet [Formula: see text] of opening ([Formula: see text]) and closing ([Formula: see text]) brackets, is balanced if it is a subset of the Dyck language [Formula: see text] over [Formula: see text], and it is well-formed if all words are prefixes of words in [Formula: see text]. We show that well-formedness of a context-free language is decidable in polynomial time, and that the longest common reduced suffix can be computed in polynomial time. With this at a hand we decide for the class 2-TW of non-linear tree transducers with output alphabet [Formula: see text] whether or not the output language is balanced.

Structured text requires that pairs of opening and closing brackets are properly nested. This applies to text representing program code as well as to XML or HTML documents. Subsequently, we call properly nested words over an alphabet B of opening and closing brackets balanced. Balanced words, i.e. structured text, need not necessarily be constructed in a structured way. Therefore, it is a non-trivial problem whether the set of words produced by some kind of text processor, consists of balanced words only. For the case of a single pair of brackets and context-free languages, decidability of this problem has been settled by Knuth [3] where a polynomial time algorithm is presented by Minamide and Tozawa [9] . Recently, these results were generalized to the output languages of monadic second-order logic (MSO) definable tree-to-word transductions [8] . The case when the alphabet B consists of multiple pairs of brackets, though, seems to be more intricate. Still, balancedness for context-free languages was shown to be decidable by Berstel and Boasson [1] where a polynomial time algorithm again has been provided by Tozawa and Minamide [13] . Whether or not these results for B can be generalized to MSO definable transductions as e.g. done by finite copying macro tree transducers with regular look-ahead, remains as an open problem. Reynier and Talbot [10] considered visibly pushdown transducers and showed decidability of this class with well-nested output in polynomial time.

Here, we provide a first step to answering this question. We consider deterministic tree-to-word transducers which process their input at most twice by calling in their axioms at most two linear transductions of the input. Let 2-TW denote the class of these transductions. Note that the output languages of linear deterministic tree-to-word transducers is context-free, which does not need to be the case for 2-TW transducers. 2-TW forms a subclass of MSO definable transductions which allows to specify transductions such as prepending an XML document with the list of its section headings, or appending such a document with the list of figure titles. For 2-TW transducers we show that balancedness is decidable-and this in polynomial time. In order to obtain this result, we first generalize the notion of balancedness to the notion of well-formedness of a language, which means that each word is a prefix of a balanced word. Then we show that well-formedness for context-free languages is decidable in polynomial time. A central ingredient is the computation of the longest common suffix of a contextfree language L over B after reduction i.e. after canceling all pairs of matching brackets. While the proof shares many ideas with the computation of the longest common prefix of a context-free language [7] we could not directly make use of the results of [7] s.t. the results of this paper fully subsume the results of [7] . Now assume that we have verified that the output language of the first linear transduction called in the axiom of the 2-TW transducer and the inverted output language of the second linear transformation both are well-formed. Then balancedness of the 2-TW transducer in question, effectively reduces to the equivalence of two deterministic linear tree-to-word transducers-modulo the reduction of opening followed by corresponding closing brackets. Due to the well-formedness we can use the equivalence of linear tree-to-word transducers over the free group which can be decided in polynomial time [5] .

This paper is organized as follows. After introducing basic concepts in Sect. 2, Sect. 3 shows how balancedness for 2-TW transducers can be reduced to equivalence over the free group and well-formedness of LT Δ s. Section 4 considers the problem of deciding well-formedness of context-free languages in general.

Missing proofs can be found in the extended version of this paper [4] .

As usual, N (N 0 ) denotes the natural numbers (including 0). The power set of a set S is denoted by 2 S . Σ denotes some generic (nonempty) alphabet, Σ * and Σ ω denote the set of all finite words and the set of all infinite words, respectively. Then Σ ∞ = Σ * ∪Σ ω is the set of all countable words. Note, that the transducers considered here output finite words only; however, for the operations needed to analyze the output infinite words are very helpful. We denote the empty word by ε. For a finite word w = w 0 . . . w l , its reverse w R is defined by w R = w l . . . w 1 w 0 ; as usual, set L R := {w R | w ∈ L} for L ⊆ Σ * . A is used to denote an alphabet of opening brackets with A = {a | a ∈ A} the derived alphabet of closing brackets, and B := A ∪ A the resulting alphabet of opening and closing brackets.

Longest Common Prefix and Suffix. Let Σ be an alphabet. We first define the longest common prefix of a language, and then reduce the definition of the longest common suffix to it by means of the reverse. We write p to denote the prefix relation on Σ ∞ , i.e. we have u p w if either (i) u, w ∈ Σ * and there exists v ∈ Σ * s.t. w = uv, or (ii) u ∈ Σ * and w ∈ Σ ω and there exists v ∈ Σ ω s.t. w = uv, or (iii) u, w ∈ Σ ω and u = w. We extend Σ ∞ by a greatest element

which is called the longest common prefix of L, abbreviated by lcp(L). Further, define ε ω := , R := , and w := =: w for all w ∈ Σ ∞ .

In Sect. 4 we will need to study the longest common suffix ( lcs) of a language L. For L ⊆ Σ * , we can simply set lcs(L) := lcp(L R ) R , but also certain infinite words are very useful for describing how the lcs changes when concatenating two languages (see e.g. Example 2). Recall that for u, w ∈ Σ * and w = ε the ω-regular expression uw ω denotes the unique infinite word uwww . . . in k∈N0 uw k Σ ω ; such a word is also called ultimately periodic. For the lcs we will use the expression w ω u to denote the ultimately left-periodic word . . . wwwu that ends on the suffix u with infinitely many copies of w left of u; these words are used to abbreviate the fact that we can generate a word w k u for unbounded k ∈ N 0 . As we reduce the lcs to the lcp by means of the reverse, we define the reverse of w [4] we derive further equalities for lcs that allow to simplify its computation. In particular, the following two equalities (for x, y ∈ Σ * ) are very useful: Involutive Monoid. We briefly recall the basic definitions and properties of the finitely generated involutive monoid, but refer the reader for details and a formal treatment to e.g. [11] . Let A be a finite alphabet (of opening brackets/letters). From A we derive the alphabet A := {a | a ∈ A} (of closing brackets/letters) where we assume that A ∩ A = ∅. Set B := A ∪ A . We use roman letters p, q, . . . to denote words over A, while Greek letters α, β, γ, . . . will denote words over B.

We extend · to an involution on B * by means of ε := ε, a := a for all a ∈ A, and αβ := β α for all other α, β ∈ B * . Let ρ → be the binary relation on B * defined by αaa β ρ → αβ for any α, β ∈ B * and a ∈ A, i.e. ρ → cancels nondeterministically one pair of matching opening and closing brackets. A word α ∈ B * is reduced if it does not contain any infix of the form aa for any a ∈ A, i.e. α is reduced if and only if it has no direct successor w.r.t. ρ →. For every α ∈ B * canceling all matching brackets in any arbitrary order always results in the same unique reduced word which we denote by ρ(α); we write α

Well-Formed Languages and Context-Free Grammars. We are specifically interested in context-free grammars (CFG) G over the alphabet B. We write → G for the rewrite rules of G. We assume that G is reduced to the productive nonterminals that are reachable from its axiom S. For simplicity, we assume for the proofs and constructions that the rules of G are of the form

for nonterminals X, Y, Z and u, v ∈ A * . We write L X := {α ∈ B * | X → * G α} for the language generated by the nonterminal X. Specifically for the axiom S of G we set L := L S . The height of a derivation tree w.r.t. G is measured in the maximal number of nonterminals occurring along a path from the root to any leaf, i.e. in our case any derivation tree has height at least 1. We write L ≤h X for the subset of L X of words that possess a derivation tree of height at most h s.t.:

1. Let Δ(α) := |α| A − |α| A be the difference of opening brackets to closing brack-

Note that d X ≥ 0 as we can always choose α = ε in the definition of d X .

As already mentioned in the abstract and the introduction, we have that L is wf iff Prf(L) is wf iff L is a subset of the prefix closure of the Dyck language generated by S → ε, S → SS, S → aSa (for a ∈ A). We state some further direct consequences of above definition: (i) L is nonnegative iff the image of L under the homomorphism that collapses A to a singleton is wf. Hence, if L is wf, then L is nonnegative. Δ is an ω-continuous homomorphism from the language semiring generated by B to the tropical semiring Z ∪ {−∞}, min, + . Thus it is decidable in polynomial time if G is nonnegative using the Bellman-Ford algorithm [2] .

In particular, because of context-freeness, it follows that, if G is wf, then for

The words r X mentioned in the definition of bounded well-formedness can be computed in polynomial time using the Bellman-Ford algorithm similar to [13] ; more precisely, a straight-line program (SLP) (see e.g. [6] for more details on SLPs), i.e. a context-free grammar generating exactly one derivation tree and thus word, can be extracted from G for each r X .

Tree-to-Word Transducers. We define a linear tree-to-word transducer (LT B ) M = (Σ, B, Q, S, R) where Σ is a finite ranked input alphabet, B is the finite (unranked) output alphabet, Q is a finite set of states, the axiom S is of the form u 0 or u 0 q(x 1 )u 1 with u 0 , u 1 ∈ B * and R is a set of rules of the form

n ≤ m and σ an injective mapping from {1, . . . , n} to {1, . . . , m}. Since non-deterministic choices of linear transducers can be encoded into the input symbols, we may, w.l.o.g., consider deterministic transducers only. For simplicity, we moreover assume the transducers to be total. This restriction can be lifted by additionally taking a top-down deterministic tree automaton for the domain into account. The constructions introduced in Sect. 3 would then have to be applied w.r.t. such a domain tree automaton. As we consider total deterministic transducers there is exactly one rule for each pair q ∈ Q and f ∈ Σ.

A 2-copy tree-to-word transducer (2-TW) is a tuple N = (Σ, B, Q, S, R) that is defined in the same way as an LT B but the axiom S is of the form u 0 or

T Σ denotes the set of all trees/terms over Σ. We define the semantics q :

The semantics M of an LT B M with axiom u 0 is given by ρ(u 0 ); if the axiom is of the form u 0 q(x 1 )u 1 it is defined by ρ(u 0 q (t)u 1 ) for all t ∈ T Σ ; while the semantics N of a 2-TW N with axiom u 0 is again given by ρ(u 0 ) and for axiom

Note that the output language of an LT B is context-free and a corresponding context-free grammar for this language can directly read from the rules of the transducer.

Additionally, we may assume w.l.o.g. that all states q of an LT B are nonsingleton, i.e., L(q) contains at least two words. We call a 2-

Balanced and well-formed states are defined analogously. We use q to denote the inverse transduction of q which is obtained from a copy of the transitions reachable from q by involution of the right-hand side of each rule. As a consequence, q (t) = q (t) for all t ∈ T Σ , and thus, L(q ) = L(q) . We say that two states q, q are equivalent iff for all t ∈ T Σ , q (t) = q (t). Accordingly, two 2-TWs M , M are equivalent iff for all t ∈ T Σ , M (t) = M (t).

Let M denote a 2-TW. W.l.o.g., we assume that the axiom of M is of the form q 1 (x 1 )q 2 (x 1 ) for two states q 1 , q 2 . If this is not yet the case, an equivalent 2-TW with this property can be constructed in polynomial time. We reduce balancedness of M to decision problems for linear tree-to-word transducers alone. Proof. Assume first that M with axiom q 1 (x 1 )q 2 (x 1 ) is balanced, i.e., L(M ) = ε. Then for all w , w with w = w w ∈ L(M ), ρ(w ) = u ∈ A * and ρ(w ) = u . Thus, both L(q 1 ) and L(q 2 ) consist of well-formed words only. Assume for a contradiction that q 1 and q 2 are not equivalent. Then there is some t ∈ T Σ such that q 1 (t) ρ = q 2 (t). Let q 1 (t) = u ∈ A * and q 2 (t) = q 2 (t) = v with v ∈ A * and u = v. Then ρ( q 1 (t) q 2 (t)) = ρ(uv ) = ε as u = v, u, v ∈ A * . Since M is balanced, this is not possible. Now, assume that L(q 1 ) and L(q 2 ) are well-formed, i.e., for all t ∈ T Σ , q 1 (t) ∈ A * and q 2 (t) ∈ A * . Additionally assume that q 1 and q 2 are equivalent, i.e., for all t ∈ T Σ , q 1 (t) = q 2 (t) = q 2 (t) . Therefore for all t ∈ T Σ , q 2 (t) = q 1 (t) and hence, ρ( q 1 (t) q 2 (t)) = ρ( q 1 (t) q 1 (t) ) = ε Therefore, the 2-TW M must be balanced.

The output languages of states q 1 and q 2 are generated by means of context-free grammars of polynomial size. (2) , g (0) } (the superscript denotes the rank), output alphabet B = {a, a }, axiom q 3 (x 1 ) and rules

We obtain a CFG producing exactly the output language of M by nondeterministically guessing the input symbol, i.e. the state q i becomes the nonterminal W i . The axiom of this CFG is then W 3 , and as rules we obtain

Note that the rules of M and the associated CFG use a form of iterated squaring, i.e. W 3 → 2 W 4 3 , that allows to encode potentially exponentially large outputs within the rules (see also Example 4). In general, words thus have to be stored in compressed form as SLPs [6] .

Therefore, Theorem 2 of Sect. 4 implies that well-formedness of q 1 , q 2 can be decided in polynomial time. Accordingly, it remains to consider the equivalence problem for well-formed LT B s. Since the two transducers in question are wellformed, they are equivalent as LT B s iff they are equivalent when their outputs are considered over the free group F A . In the free group F A , we additionally have that a a ρ = ε-which does not hold in our rewriting system. If sets L(q 1 ), L(q 2 ) of outputs for q 1 and q 2 , however, are well-formed, it follows for all u ∈ L(q 1 ), v ∈ L(q 2 ) that ρ(uv ) = ρ(ρ(u)ρ(v )) cannot contain a a. Therefore, ρ(uv ) = ε iff uv is equivalent to ε over the free group F A . In [5, Theorem 2], we have proven that equivalence of LT B s where the output is interpreted over the free group, is decidable in polynomial time. Thus, we obtain our main theorem.

As described in the preceding sections, given a 2-TW we split it into the two underlying LT B s that process a copy of the input tree. We then check that each of these two LT B s are equivalent w.r.t. the free group. As sketched in Example 1 we obtain a context-free grammar for the output language of each of these LT B s. It then remains to check that both context-free grammars are well-formed. In order to prove that we can decide in polynomial time whether a context-free grammar is well-formed (short: wf), we proceed as follows:

First, we introduce in Definition 3 the maximal suffix extension of a language L ⊆ Σ * w.r.t. the lcs (denoted by lcsx(L)), i.e. the longest word u ∈ Σ ∞ s.t. lcs(uL) = u lcs(L). We then show that the relation L ≈ lcs L :⇔ lcs(L) = lcs(L )∧ lcsx(L) = lcsx(L ) is an equivalence relation on Σ * that respects both union and concatenation of languages (see Lemma 5) . It then follows that for every language L ⊆ Σ * there is some subset T lcs (L) ⊆ L of size at most 3 with L ≈ lcs T lcs (L).

We then use T lcs to compute a finite ≈ lcs -equivalent representation T ≤h X of the reduced language generated by each nonterminal X of the given contextfree grammar inductively for increasing derivation height h. In particular, we show that we only have to compute up to derivation height 4N + 1 (with N the number of nonterminals) in order to decide whether G is wf: In Lemma 7 we show that, if G is wf, then we have to have T ≤4N +1 X ≈ lcs T ≤4N X for all nonterminals X of G. The complementary result is then shown in Lemma 6, i.e. if G is not wf, then we either cannot compute up to T ≤4N +1 X as we discover some word that is not wf, or we have T ≤4N X ≈ lcs T ≤4N +1 X for at least one nonterminal X.

We first show that we can compute the longest common suffix of the union L ∪ L and the concatenation LL of two languages L, L ⊆ Σ * if we know both lcs(L) and lcs(L ), and in addition, the longest word lcsx(L) resp. lcsx(L ) by which we can extend lcs(L) resp. lcs(L ) when concatenating another language from left. In contrast to the computation of the lcp presented in [7] , we have to take the maximal extension lcsx explicitly into account. In this paragraph we do not consider the involution, thus let Σ denote an arbitrary alphabet. If lcs(L) is not contained in L, then lcs(L) has to be a strict suffix of every shortest word in L, and thus immediately lcsx(L) = ε. As in the case of the lcs, also lcsx(L) is already defined by two words in L:

We show that we can compute the lcs and the extension lcsx of the union resp. the concatenation of two languages solely from their lcs and lcsx. To this end, we define the lcs-summary of a language as: Definition 4. For L ⊆ Σ * set π lcs (L) := (lcs(L), lcsx(L)). The equivalence relation ≈ lcs on 2 Σ * is defined by: L ≈ lcs L iff π lcs (L) = π lcs (L ). As both the lcs and the lcsx are determined by already two words (cf. Lemmas 1 and 4), it follows that every L ⊆ Σ * is ≈ lcs -equivalent to some sublanguage T lcs (L) ⊆ L consisting of at most three words where the words xR, yR can be chosen arbitrarily up to the stated constraints (with R = lcs(L)):

Deciding Well-Formedness. For the following, we assume that G is a context-free grammar over B = A ∪ A with nonterminals X. Set N := |X|. We further assume that G is nonnegative, and that we have computed for every nonterminal X of G a word r X ∈ A * (represented as an SLP) s.t. |r X | = d X and r X ∈ Prf(ρ(L X )). 1 In order to decide whether G is wf we compute the languages ρ(r X L ≤h X ) modulo ≈ lcs for increasing derivation height h using fixed-point iteration. Assume inductively that (i) r X L ≤h X is wf and (ii) that we have computed T ≤h X := T lcs (ρ(r X L ≤h X )) ≈ lcs ρ(r X L ≤h X ) for all X ∈ X up to height h. Then we can compute T lcs (ρ(r X L ≤h+1 X )) for each nonterminal as follows:

Note that, if all constants r X r Y and all T ≤h X are wf, but G is not wf, then the computation has to fail while computing r X r Y T ≤h Y r Z ; see the following example.

Example 4. Consider the nonnegative context-free grammar G given by the rules (with the parameter n ∈ N fixed)

with axiom S. Except for B all nonterminals generate nonnegative languages. Note that the nonterminals W n to W 1 form an SLP that encodes the word b 2 n by means of iterated squaring which only becomes productive at height h = n + 1.

For h ≥ n + 3 we have:

Here the words r X used to cancel the longest prefix of closing brackets (after reduction) are

)/2 and n + 3 ≤ h ≤ h 0 ; in particular, the lcs of T ≤h S has already converged to c at h = n+3, only its maximal extension lcsx changes for n + 3 ≤ h ≤ h 0 . We discover the first counterexample a 2 n b that G is not wf while computing T ≤h0+1 V = T lcs (ρ(T ≤h0 U b )). As illustrated in Example 4, if G is not wf, then the minimal derivation height h 0 + 1 at which we discover a counterexample might be exponential in the size of the grammar. The following lemma states that up to this derivation height h 0 the representations T ≤h X cannot have converged (modulo ≈ lcs ).

The following Lemma 7 states the complementary result, i.e. if G is wf then the representations T ≤h X have converged at the latest for h = 4N modulo ≈ lcs . The basic idea underlying the proof of Lemma 7 is similar to [7] : we show that from every derivation tree of height at least 4N + 1 we can construct a derivation tree of height at most 4N such that both trees carry the same information w.r.t. the lcs (after reduction). In contrast to [7] we need not only to show that T ≤4N X has the same lcs as ρ(r X L ≤4N X ), but that T ≤4N X has converged modulo ≈ lcs if G is wf; to this end, we need to explicitly consider lcsx, and re-prove stronger versions of the results regarding the combinatorics on words which take the involution into account (see A.6 in the appendix of the extended version [4] ).

Let G be a context-free grammar with N nonterminals and L(G) be wf. For every nonterminal X let r X ∈ A * s.t. |r X | = d X and r X L X wf. Then ρ(r X L X ) ≈ lcs ρ(r X L ≤4N X ), and T ≤4N X ≈ lcs T ≤4N +1 X for every nonterminal X.

The following example sketches the main idea underlying the proof of Lemma 7.

Example 5. The central combinatorial observation 2 is that for any well-formed language L ⊆ B * of the form

we have that its longest common suffix after reduction lcs ρ (L) := lcs(ρ(L)) is determined by the reduced longest common suffix of αγβ and either (α, β)(μ i , ν i )γ = αμ i γν i β or (α, β)(μ i , ν i )(μ j , ν j )γ = αμ i μ j γν j ν i β for some i ∈ {1, 2} but arbitrary j ∈ {1, 2} in the latter case. 3 Assume now we are given a context-free grammar G with N variables. Further assume that L := L(G) is well-formed. W.l.o.g. G is in Chomsky normal form and reduced to the productive nonterminals reachable from the axiom of G. Let L ≤4N denote the sublanguage of words generated by G with a derivation tree of height at most 4N . Pick a shortest (before reduction) word κ 0 ∈ L := L(G). Then there is some κ 1 ∈ L with R := lcs ρ (L) = lcs ρ (κ 0 , κ 1 ); we will call any such word a witness (w.r.t. κ 0 ) in the following. If R ∈ L, then κ 0 ρ = R, and any word in L is a witness. In particular, there is a witness in L ≤4N . So assume R ∈ L. Then we may factorize (in a unique way) κ 0 = κ 0 aκ 0 and κ 1 = κ 1 bκ 1 such that ρ(κ 0 ) = R = ρ(κ 1 ) where a, b ∈ A with a = b. Then ρ(κ 0 ) = z 0 aR and ρ(κ 1 ) = z 1 bR. Further assume that κ 1 ∈ L ≤4N , otherwise we are done. Fix any derivation tree t of κ 1 , and fix within t the main path from the root of t to the last letter b of the suffix bκ 1 of ρ(κ 1 ) (the dotted path in Fig. 1 ). We may assume that any path starting at a node on this main path and then immediately turning left towards a letter within the prefix κ 1 consists of at most N nonterminals: if any nonterminal occurs twice the induced pumping tree can be pruned without changing the suffix bκ 1 ; as the resulting tree is still a valid derivation tree w.r.t. G, we obtain another witness w.r.t. κ 0 . Thus consider any path (including the main path) in t that leads from its root to a letter within the suffix bκ 1 . If every such path consists of at most 3N nonterminals, then every path in t consists of at most 4N nonterminals so that κ 1 ∈ L ≤4N follows. Hence, assume there is at least one such path consisting of 3N + 1 nonterminals. Then there is some nonterminal X occurring at least four times on this path. Fix four occurrences of X and factorize κ 1 accordingly In the proof of Lemma 7 we show that we may assume-as L is well-formedthat u, v, w, s 1 , s 2 , s 3 ∈ A * with only τ 1 , τ 2 , τ 3 ∈ B * . From this factorization we obtain the sublanguage L := (u, v)[(s 1 , τ 1 ) + (s 2 , τ 2 ) + (s 3 , τ 3 )] * w. Our goal is to show that (u, v)w or (u, v)(s i , τ i )w or (u, v)(s i , τ i )(s j , τ j )w (for i = j) is a witness w.r.t. κ 0 : note that each of these words result from pruning at least one pumping tree from t which inductively leads to a procedure to reduce t to a derivation tree of height at most 4N that still yields a witness for R = lcs ρ (L) w.r.t. κ 0 . Assume thus specifically that neither (u, v)w = uwv nor (u, v)(s 3 , τ 3 )w = us 3 wτ 3 v nor (u, v)(s i , τ i )(s 3 , τ 3 )w = us i s 3 wτ 3 τ i v for i ∈ {1, 2} is a witness w.r.t. κ 0 , i.e. each of these words end on aR after reduction. Apply now the result mentioned at the beginning of this example to the language L := (u, v)[(s 1 , τ 1 ) + (s 2 , τ 2 )] * (s 3 , τ 3 )w: by our assumptions κ 1 ∈ L is a witness w.r.t. us 3 wτ 3 v ∈ L so that both lcs ρ (L ) = lcs ρ (L) and also (u, v)(s 1 , τ 1 ) 2 (s 3 , τ 3 )w is a witness w.r.t. us 3 wτ 3 v as we may choose j = 1. Thus also lcs ρ (L) = lcs ρ (L ) for L := (u, v)[(s 1 , τ 1 ) + (s 3 , τ 3 )] * w as L ⊆ L and both (u, v)w ∈ L and (u, v)(s 1 , τ 1 )(s 1 , τ 1 )(s 3 , τ 3 )w ∈ L . Applying the same argument now to L , but choosing j = i it follows that (u, v)(s 1 , τ 1 )w or (u, v)(s 3 , τ 3 )(s 1 , τ 1 )w has to be a witness w.r.t. κ 0 .

The sketched argument can be adapted so that it also allows to conclude the maximal extension after reduction lcsx(ρ(L)) has to have converged at derivation height 4N the latest, if L is well-formed. For details, see the proof of Lemma 7 in the appendix of the extended version [4] .

As |T ≤h X | ≤ 3, a straight-forward induction also shows that every word in T ≤h X can be represented by an SLP that we can compute in time polynomial in G for h ≤ 4N + 1; together with the preceding Lemmas 7 and 6 we thus obtain the main result of this section: Theorem 2. Given a context-free grammar G over B we can decide in time polynomial in the size of G whether G is wf.

We have shown that well-formedness for context-free languages is decidable in polynomial time. This allowed us to decide in polynomial time whether or not a 2-TW is balanced. The presented techniques, however, are particularly tailored for 2-TWs. It is unclear how a generalization to transducers processing three or more copies of the input would look like. Thus, the question remains whether balancedness is decidable for general MSO definable transductions. It is also open whether even the single bracket case can be generalized beyond MSO definable transduction, e.g. to output languages of top-down tree-to-word transducers [12] .

Formal properties of XML grammars and languages

Derivation tree analysis for accelerated fixed-point computation

A characterization of parenthesis languages

On the balancedness of tree-to-word transducers

Equivalence of linear tree transducers with output in the free group

Algorithmics on SLP-compressed strings: a survey

Computing the longest common prefix of a context-free language in polynomial time

Balancedness of MSO transductions in polynomial time

XML validation for context-free grammars

Visibly pushdown transducers with well-nested outputs

Elements of Automata Theory

Equivalence of deterministic top-down tree-tostring transducers is decidable

Complexity results on balanced context-free languages

We also like to thank the anonymous reviewers for their detailed comments and valuable advice.