Mathieu Hoyrup

The dimension of ergodic random sequences

Keywords: Shannon-McMillan-Breiman theorem, Martin-Löf random sequence, effective Hausdorff dimension, compression rate, entropy

Let µ be a computable ergodic shift-invariant measure over {0, 1} N . Providing a constructive proof of Shannon-McMillan-Breiman theorem, V'yugin proved that if x ∈ {0, 1} N is Martin-L öf random w.r.t. µ then the strong effective dimension Dim(x) of x equals the entropy of µ. Whether its effective dimension dim(x) also equals the entropy was left as an problem question. In this paper we settle this problem, providing a positive answer. A key step in the proof consists in extending recent results on Birkhoff's ergodic theorem for Martin-L öf random sequences.

Introduction

The effective dimension and strong effective dimension of an infinite binary sequence x are defined as

dim(x) = lim inf n K(x↾ n ) n Dim(x) = lim sup n K(x↾ n ) n ,
where K(w) is the Kolmogorov complexity of w.

They can be characterized as effective versions of Hausdorff and packing dimensions respectively, or by divergence of s-gales (see [Lut00, May02, AHLM07] for the original results and [Lut05] for a survey).

Let p ∈ [0, 1] be a computable real number and µ p the Bernoulli measure over Cantor space given by µ p [w] = p |w| 1 (1-p) |w| 0 . It is well-known that if an infinite binary sequence x is Martin-L öf random w.r.t. µ p then dim(x) = Dim(x) = h(µ p ), where h(µ p ) is the entropy of µ p defined by h(µ p ) = -p log(p) -(1p) log(1p).

(1)

This result is not difficult to prove and reduces to the strong law of large numbers for Martin-L öf random sequences, as on the one hand1

K(x↾ n ) = -log µ p [x↾ n ] + O(1)
for µ p -random sequences by Levin-Schnorr theorem, and on the other hand

- 1 n log µ p [x↾ n ] = - |x↾ n | 1 n log(p) - |x↾ n | 0 n log(1 -p)
which converge to h(µ p ) for µ p -random sequences, by the Strong Law of Large Numbers for Martin-L öf random sequences. This result highlights the relationship between Shannon's information theory, Kolmogorov algorithmic information theory and effective randomness.

Ergodic theory provides a natural extension of information theory in which many results can be transferred, with more involved proofs, from the case of independent identically distributed random variables to the ergodic case, where independence is only required asymptotically, in the average (see Section 2 for a precise definition).

First, the strong law of large numbers extends to Birkhoff's ergodic theorem. Second, the coincidence between local information and entropy extends through the Shannon-McMillan-Breiman theorem. Whether Martin-L öf randomness fits with these theorems has been an open problem for a while. The first results were proved by V'yugin [V'y98], based on non-classical, constructive proofs of the theorems. He proved, in particular: Theorem 1.1 (Effective Birkhoff ergodic theorem I). Let µ be a computable shift-invariant ergodic measure over {0, 1} N and f ∈ L 1 (µ) be computable. For every Martin-Löf µ-random sequence x,

lim n→∞ 1 n n-1 k=0 f • T k (x) = f dµ.
The entropy of an ergodic measure is defined as

h(µ) = lim n→∞ - 1 n |w|=n µ[w] log µ[w]. (2)
Observe that (1) and (2) are consistent as they give the same quantity when µ is a Bernoulli measure.

Theorem 1.2 (Effective Shannon-McMillan-Breiman theorem I). Let µ be a computable shiftinvariant ergodic measure over {0, 1} N . For every Martin-Löf µ-random sequence x,

lim sup n→∞ K(x↾ n ) n = lim sup n→∞ - 1 n log µ[x↾ n ] = h(µ).
The question whether lim inf K↾ n n coincides with h(µ) for every Martin-L öf µ-random was left open by V'yugin. An alternative proof of Theorem 1.2 approximating ergodic measures by Markovian measures was later developed by Nakamura [Nak05], but also left the question open. In this paper we provide a positive answer to this question.

A classical proof of the Shannon-McMillan-Breiman theorem uses Birkhoff's ergodic theorem, applied to some particular functions. The problem in making it effective is that these functions are not computable in general. Recent works have been achieved to push the effective ergodic theorem to the largest possible class of functions. Here we extend it enough to get the full effective Shannon-McMillan-Breiman theorem.

In Section 2 we recall basic notions of computability, randomness and ergodic theory. In Section 3 we develop effective versions of Birkhoff's ergodic theorem. In Section 4 we present our main result.

Background and notations

We work on the Cantor space {0, 1} N of infinite binary sequences. A finite word w ∈ {0, 1} * determines the cylinder [w] ⊆ {0, 1} N of infinite sequences starting with w. If x ∈ {0, 1} N and n ∈ N, x↾ n is the prefix of x of length n, and is also denoted x 0 x 1 . . . x n-1 . The cylinders form a base of the product topology.

Effective topology. An open set

U ⊆ {0, 1} N is effective if it is a recursively enumerable union of cylinders. A closed set is effective it its complement is an effective open set. A function f : {0, 1} N → R is computable if
there is a Turing machine that on oracle x and input n computes a rational number q such that |qf (x)| < 2 -n . Equivalently, f is computable if for every rational numbers a < b, f -1 (a, b) is effectively open, uniformly in a, b. A function f : {0, 1} N → [0, +∞] is lower (resp. upper) semi-computable if there is a Turing machine that on oracle x and input n computes a rational number q n such that f (x) = sup n q n (resp. f (x) = inf n q n ). Equivalently, f is lower (resp. upper) semicomputable if for every rational number a, f -1 (a, +∞] (resp. f -1 [0, a)) is effectively open, uniformly in a.

Kolmogorov complexity and Martin-L öf randomness.

For w ∈ {0, 1} * , K(w) is the prefix version of Kolmogorov complexity, defined by Levin and Chaitin independently. It is defined as the length of a shortest input of a universal Turing machine with prefix-free domain computing w on that input.

A probability measure µ over {0, 1} N is determined by its value on cylinders µ

[w], for w ∈ {0, 1} * . µ is computable if µ[w] is a computable real number, uniformly in w. Given a computable probability measure µ, a sequence x ∈ {0, 1} N is Martin-L öf µ-random, denoted x ∈ ML µ , if there is c such that for all n, K(x↾ n ) ≥ -log µ[x↾ n ] -c.
Martin-L öf's original definition [ML66] was expressed in terms of tests rather than complexity, but the one given here, due to Levin and Chaitin [Cha75] independentely, was proved to be equivalent by Levin [Lev73] and Schnorr [START_REF] Schnorr | Process complexity and effective random tests[END_REF].

The function

t µ (x) = sup n {-log µ[x↾ n ] -K(x↾ n )}
is lower semi-computable and 2 tµ dµ ≤ 1. Moreover, it was proved in [Gác80] that 2 tµ is maximal in the sense that for every integrable lower semi-computable function f : {0, 1} N → [0, +∞], there exists c f such that f ≤ c f 2 t µ . We call such an f a µ-test. It tests Martin-L öf randomness in the sense that x ∈ ML µ iff f (x) < ∞ for each µ-test f iff t µ (x) < ∞. More can be found on this subject in [Nie09, DH10].

Ergodic theory. We recall some basic notions of ergodic theory, more details can be found in [Smo71, Pet83]. We denote by T : {0, 1} N → {0, 1} N the shift map defined by

T (x 0 x 1 . . .) = x 1 x 2 . . .. A measure µ over {0, 1} N is shift-invariant if for all Borel sets A, µ(T -1 A) = µ(A), equivalently if µ[0w] + µ[1w] = µ[w] for all w ∈ {0, 1} * . µ is ergodic if for all Borel sets A such that T -1 A = A up to a null sets, µ(A) = 0 or 1. Equivalently, µ is ergodic if for all u, v ∈ {0, 1} * , lim n→∞ 1 n n-1 k=0 µ([u] ∩ T -k [v]) = µ[u] • µ[v].

Effective ergodic theorems

The following theorem, taken from [BDMS10], extends a result of Kučera from the uniform measure to any ergodic shift-invariant measure: Theorem 3.1 (Effective Poincaré recurrence theorem). Let µ be a computable ergodic shiftinvariant measure and C ⊆ {0, 1} N an effective closed set such that µ(C) > 0. Every Martin-Löf µ-random sequence has a tail in C, i.e. for every x ∈ ML µ there exists k such that T k (x) ∈ C.

In [BDH + 10] and [START_REF] Johanna | Martin-L öf random points satisfy Birkhoff's ergodic theorem for effectively closed sets[END_REF] independently this result was used to prove that not only the orbit of x eventually falls into C, but it does so with frequency µ(C). Theorem 3.2 (Effective Birkhoff ergodic theorem II). Let µ be a computable ergodic shiftinvariant measure and C ⊆ {0, 1} N an effective closed set such that µ(C) > 0. For every Martin-Löf µ-random sequence x,

lim n→∞ 1 n |{k < n : T k (x) ∈ C}| = µ(C).
We first generalize the result from sets to functions:

Theorem 3.3 (Effective Birkhoff ergodic theorem III). Let µ be a computable ergodic shiftinvariant measure. Assume f : {0, 1} N → [0, +∞] is:

• either lower semi-computable,

• or upper semi-computable and bounded by a µ-test.

For each x ∈ ML µ ,

lim n→∞ n-1 k=0 f • T k (x) = f dµ.
Proof. Let us introduce the notation

A f n (x) = 1 n (f (x) + . . . + f • T n-1 (x)
). If f is lower semi-computable, then there is a sequence of uniformly computable nonnegative functions f n ր f . Applying Theorem 1.1 to

f n and x ∈ ML µ gives lim inf k A f k (x) ≥ lim inf k A fn k (x) = f n dµ. By the monotone convergence theorem, f n dµ ր f dµ, so lim inf k A f k (x) ≥ f dµ. If f dµ = ∞ we are done.
Otherwise, let q > f dµ be a rational number. The set C K := {x : ∀k ≥ K, A f k (x) ≤ q} is effectively closed and by the classical ergodic theorem, there exists K such that µ(C K ) > 0. Theorem 3.1 tells us that if x ∈ ML µ then there is n such that

T n (x) ∈ C K . As a result, lim sup A f k (x) = lim sup A f k (T n (x)) ≤ q.
As this is true of every q > f dµ, we get the result. Now, if f is upper semi-computable and f ≤ t where t is a µ-test, then for x ∈ ML µ , applying the preceding result to t and tf ,

A f n (x) = A t n (x) -(A t-f n (x)) → t dµ -(t -f ) dµ = f dµ.
We then extend this result further:

Corollary 3.1 (Effective Birkhoff ergodic theorem IV). Let f : {0, 1} N → [0, +∞] be ∆ 0 2 on ML µ , i.e. there is a sequence f n of uniformly computable functions such that f (x) = lim n f n (x) for each x ∈ ML µ . Assume that f is dominated by a µ-test. For every x ∈ ML µ ,

lim n→∞ n-1 k=0 f • T k (x) = f dµ.
Proof. Let g N = inf n≥N f n and h N = min(t, sup n≥N f n ). On ML µ , g N ր f and h N ց f . By the monotone and dominated convergence theorem, the convergences hold in L 1 (µ). Applying Theorem 3.2 to g N and h N gives the result. More precisely, for every x ∈ ML µ and every N,

lim inf n A f n (x) ≥ lim inf n A g N n (x) = g N dµ lim sup n A f n (x) ≤ lim sup n A h N n (x) = h N dµ, so f dµ = sup N g N dµ ≤ lim inf n A f n (x) ≤ lim sup n A f n (x) ≤ inf N h N dµ = f dµ.

The effective Shannon-McMillan-Breiman theorem

We now present our main result.

Theorem 4.1 (Effective Shannon-McMillan-Breiman theorem II). Let µ be a computable shiftinvariant probability measure. For each x ∈ ML µ ,

lim n→∞ K(x↾ n ) n = lim n→∞ - 1 n log µ[x↾ n ] = h(µ).
A proof of the classical result, stating the result for a.e. x, can be found in [Smo71, Pet83]. It makes use of martingale convergence theorems and ergodic theorems. The main difficulty in adapting the proof is to make sure that the effective versions of the ergodic theorem can be applied. The rest of this section is devoted to the proof of Theorem 4.1.

An easy calculation shows that

-log µ[x↾ n ] = n-1 k=0 f n-1-k • T k (x) (3)
where

f k (x) := -log µ[x 0 |x 1 . . . x k ] = -log µ[x 0 . . . x k ] µ[x 1 . . . x k ] for k ≥ 1, f 0 (x) := -log µ[x 0 ].
Lemma 4.1. f k (x) converge for each x ∈ ML µ .

Proof. Define the computable martingale

d(ǫ) = 2 d(x 0 ) = 1 µ[x 0 ] d(x 0 . . . x k ) = µ[x 1 . . . x k ] µ[x 0 . . . x k ] for k ≥ 1.
By the effective Doob's convergence theorem (see Theorem 7.1.3 on page 270 in [DH10]), for each x ∈ ML µ , d(x 0 . . . x k ) converges, and so does f k (x) = log d(x 0 . . . x k ).

Let f (x) be the limit. We write

- 1 n log µ[x↾ n ] = 1 n n-1 k=0 (f n-1-k • T k (x) -f • T k (x)) + 1 n n-1 k=0 f • T k (x)
and prove that the first term tends to 0 while the second term converges to f dµ = h(µ).

We will use the following lemma (Corollary 2.2 on page 261 in [START_REF] Petersen | Ergodic Theory[END_REF], Lemma 4.26 on page 26 in [Smo71]).

Lemma 4.2. f

* := sup k f k ∈ L 1 .
As f k → f a.e. and the convergence is dominated by f

* ∈ L 1 , f k → f in L 1 . Proposition 4.1. For each x ∈ ML µ , lim n 1 n n-1 k=0 f • T k (x) = f dµ = h µ (P ). (4)
Proof. That f dµ = h(µ) is a classical result and follows from h(µ) = lim k f k dµ and the L 1 -convergence of f k to f . f * is lower semi-computable and by Lemma 4.2 it is a µ-test. By construction, f is ∆ 0 2 on ML µ and it is dominated by f * so it satisfies the conditions of Corollary 3.1, from which the result follows directly.

Proposition 4.2. For each x ∈ ML µ ,

lim n→∞ 1 n n-1 k=0 f n-1-k • T k (x) -f • T k (x) = 0. (5) Proof. Let g N = sup k≥N |f k -f | and gN = sup k,j≥N |f k -f j |. For x ∈ ML µ , |f k (x) -f (
1 n n-1 k=0 f n-1-k • T k -f • T k ≤ 1 n n-1 k=0 |f n-1-k • T k -f • T k | = 1 n n-1-N k=0 |f n-1-k • T k -f • T k | + 1 n n-1 k=n-N |f n-1-k • T k -f • T k | ≤ 1 n n-1-N k=0 g N • T k + 1 n n-1 k=n-N (f * + f ) • T k ≤ 1 n n-1-N k=0 gN • T k + 1 n n-1 k=0 (f * + f ) • T k - 1 n n-N -1 k=0 (f * + f ) • T k .
Fix N and let n → ∞. As gN ∈ L 1 is lower semi-computable, the first term converges to gN dµ by the Effective Ergodic Theorem 3.3. As f * + f is ∆ 0 2 on ML µ and is dominated by the µ-test 2f * , the second and the third terms converge to (f * + f ) dµ by Corollary 3.1 so their limits cancel each other.

As gN dµ → 0, we have proved equality (5).

Putting equalities (3), (4) and (5) together gives, for x ∈ ML µ ,

  x)| = lim j |f k (x)f j (x)| = lim sup j |f k (x)f j (x)| ≤ sup j≥N |f k (x)f j (x)|, so g N (x) ≤ gN (x). As f k → f a.e., gN → 0 a.e. As gN ≤ 2f * ∈ L 1 , gN → 0 in L 1 by the dominated convergence theorem. On ML µ ,

  1-k • T k (x) = h(µ).

K is the prefix version of Kolmogorov complexity


Ralf Winkler
email: winkler@zas.gwz-berlin.de

Susanne Fuchs

Pascal Perrier

Mark Tiede

Speaker-specific biomechanical models: From acoustic variability via articulatory variability to the variability of motor commands in selected tongue muscles

In this work we have constructed biomechanical tongue models derived from MRI data in order to investigate the effects of differing locations of vocal tract bending on variability in motor command space and overall articulatory variability for vowel targets. Acoustic models predict negligible effects of the bend of the vocal tract if its length is held constant. However, the location of this bend crucially determines the relation between vertical and horizontal dimensions of the tract and thus the relative freedom of tongue movement within these dimensions. We predict that articulatory variability will be greater along those dimensions with more degrees of freedom as determined by vocal tract configuration imposed by bend location, and present simulation results that in general support this position.

Theoretical background

Although native speakers of a given language may use the same phonemic inventory, speakers vary from one to another with respect to their acoustics, articulation, and probably also their respective motor commands. However, the latter is more speculative. The variability among speakers may be driven by anatomical, emotional, social and communicative factors. In a previous study [START_REF] Brunner | On the relationship between palate shape and articulatory behavior[END_REF] we have focused on palatal morphology in constraining individual speech motor control. Here we concentrate on individual differences in the location of the vocal tract bend and its impact on speaker specific variability at three levels: acoustics, articulation and motor commands. Such an investigation is not possible using human subjects for two reasons: first, one cannot control or disentangle the different factors described above; second, so far it is impossible to observe motor commands for human tongue movements. Instead, we build speaker-specific biomechanical tongue models on the basis of human imaging data that allow us to link motor commands, articulation and acoustics. To our knowledge, such an investigation has not been carried out before. Unlike speakerspecific geometrical models which offer only superficial interpretations of underlying control, biomechanical tongue models have the advantage of controlling muscular length and forces as the results of the combined influences of central commands and feedback signals, and therefore they provide insights into the underlying muscle activations and dynamics which drive the tongue's movement.

Modeling

In this section the necessary steps to construct speaker-specific models are presented. After a short description of the labeling procedure, the steps towards building speakerspecific biomechanical models, running simulations and estimating the acoustics are presented.

Labeling human imaging data

Speaker-specific models were constructed based on Magnetic Resonance Imaging (MRI) data of two speakers (Figure 1, top row). Imaging data were originally collected for 10 isolated vowels to study inter-speaker acoustic and articulatory variability [START_REF] Apostol | Étude et simulation des caractéristiques individuelles des locuteurs par modélisation du processus de production de la parole[END_REF]. Details regarding the image acquisition procedure as well as the image resolution are specified in [START_REF] Apostol | Étude et simulation des caractéristiques individuelles des locuteurs par modélisation du processus de production de la parole[END_REF].

Within each image slice the airway was segmented from the surrounding tissues manually by using the itk-SNAP software [START_REF] Yushkevich | User-guided 3D active contour segmentation of anatomical structures: Significantly improved efficiency and reliability[END_REF]. The biomechanical tongue model is implemented with standard teeth and standard lips. For that reason segmentation of the air channel terminates at the incisors. The lip region was ignored during segmentation because the front tube used during area function calculation was kept invariant. Furthermore, the epiglottis and the uvula were consistently excluded because the tongue contour is handled separately in the articulatory model and the uvula is not part of the model.

Speaker-specific biomechanical tongue models

The speaker-specific models are based on the well established 2D biomechanical tongue model of [START_REF] Perrier | Influences of tongue biomechanics on speech movements during the production of velar stop consonants: A modeling study[END_REF], which consists of a deformable Finite Element Mesh (FEM) embedded in rigid vocal tract walls in the mid-sagittal plane (Figure 1, 2 nd row). The geometry of the mesh has been specifically designed to facilitate anatomical implementation of the muscles within the tongue. The model is controlled according to the λ-model [START_REF] Feldman | Once More on the Equilibrium-Point Hypothesis (Lambda-Model) for Motor Control[END_REF], which generates muscle force as a function of the difference between a centrally specified threshold length λ and the actual muscle length. Details regarding the assumptions underlying the design of the speaker-specific models are given in Winkler et al. (submitted). Anatomical landmarks necessary for constructing speaker-specific models include the following: the mid-sagittal tongue contour at rest position, the mid-sagittal palate contour, the velar contour, the posterior pharyngeal wall, the lower and upper limits of the tongue insertions on the mental spine (P1 and P2), and the styloid process (P3).

These mid-sagittal landmarks were extracted from labeled imaging data for each of the two subjects with the tongue in rest position.

The three anatomical landmarks (P1, P2 and P3) were measured from a high-definition mid-sagittal view of the speaker's MRI data. P1 and P2 were determined on the basis of grey level changes in the mental spine region. It is not possible to determine the exact location of the styloid process in the mid-sagittal plane directly. As an approximation in the mid-sagittal plane, P3 was placed on the internal contour of the sphenoid bone at 1/3 of its length.

Based on these anatomical landmarks the original generic biomechanical model was adapted to a speaker-specific anatomy (for details of the matching procedure see Winkler et al. (submitted)). The matching procedure fully determines the geometry of the new mesh and consequently the muscle arrangement within the new speakerspecific tongue model. It preserves the original topology of the mesh while accounting for the speaker-specific morphology.

In order to simulate tongue movements with the two speaker-specific biomechanical tongue models, motor commands and their activation duration have to be specified for successive targets. In order to compare speaker-specific biomechanical tongue models with each other, not absolute but relative motor command values were chosen. The motor commands were defined relative to their rest position (Δλ = λ target -λ rest ).

Acoustic modeling

In order to determine acoustics from articulation, the 2D distance function resulting from the biomechanical tongue model has to be converted to its corresponding area function. There are basically two different methods. On the one hand, in absence of the 3D airway contours a set of physiologically realistic α-values from the literature (for instance in [START_REF] Perrier | Vocal tract area function estimation from midsagittal dimensions with CT scans and a vocal tract cast: Modeling the transition with two sets of coefficients[END_REF]) can be applied to estimate the areas from distance values. On the other hand, the coefficients can be determined speaker-specifically if 3D data are available.

In our approach this is accomplished by determining the distance function based on a pre-defined grid [START_REF] Perrier | Influences of tongue biomechanics on speech movements during the production of velar stop consonants: A modeling study[END_REF], and subsequent reconstruction of the area function proceeds according to the speaker-specific coefficients for an adapted version of the α-β-model [START_REF] Perrier | Vocal tract area function estimation from midsagittal dimensions with CT scans and a vocal tract cast: Modeling the transition with two sets of coefficients[END_REF]) associated with the respective grid lines.

Estimating acoustics (i.e. formants) from area functions does not involve any speakerspecific adaptation. In our experiments formants are computed by coupling an acoustic analog of the vocal tract with the reconstructed area functions.

Experimentation

Acoustic models of speech production assume that the length of the vocal tract, and the length and location of the constriction defining the resonance cavities are crucial parameters for the description of the spectral properties of vowels. The location of the vocal tract bend seems to play a negligible role with respect to the acoustics, assuming the length of the tract is kept constant [START_REF] Sondhi | Resonances of a bent vocal tract[END_REF]. However, the location of the bend within the vocal tract affects the relative vertical and horizontal dimensions of the tract and we suppose that it is likely to influence the degrees of freedom of articulatory motion in the respective directions. The two speakers we selected to build speakerspecific models show two different locations of vocal tract bending. Speaker CS has a relatively long vertical dimension in comparison to the horizontal dimension whereas speaker AV shows about equal proportions between the two. In other words, for CS the location of the vocal tract bend is more anterior than for AV (assuming the same vocal tract length). These relations may also be representative for differences between males (CS with a long pharynx) and females (AV with a shorter pharynx).

Method

We assume that for vowel production, the goals of speech production are primarily auditory [START_REF] Perrier | Control and representations in speech[END_REF]. Based on this assumption, in the region of maximal overlap of the formant spaces of model AV and CS three formant ellipses were defined in the F1/F2 plane for the three corner vowels. Prior to the definition of the formant ellipses, the area functions were manipulated to match the acoustic vowel space of the two speakers. In a first step the length of the epilaryngeal tube of speaker CS was shortened to match that of speaker AV. Secondly, the original area values in the laryngeal region were fixed to a physiologically realistic value of 0.4 cm 2 . In the region of the epiglottis the area values were decreased by 50% for both speakers to avoid an artificially large cavity resulting from the excised epiglottis in the tongue model. Finally, the area functions were re-scaled to a vocal tract length of 17 cm, since we wanted to disentangle the impact of vocal tract length and the location of vocal tract bending. For each acoustic vowel target 36 simulations per speaker were randomly selected whose respective first two formant values were equally distributed over the corresponding ellipse area.

Assuming the same acoustic target regions of the corner vowels for both models, we now look at the articulatory correspondences in the two models and their respective motor commands. Of particular interest is the amount of variability at the articulatory and motor command levels.

Results

Articulatory results

In order to obtain the articulatory results for the simulations of each model which correspond to the acoustic dispersion ellipses, we selected three nodes along the surface of the Finite Elemente Mesh for /i, a/ and two for /u/. These nodes are located at the constriction location of the relevant vowel, i.e. node locations differ among the vowels.

For each node the standard deviation in the vertical (y) and horizontal (x) direction was calculated. We then compared the standard deviation of the two models by subtracting the respective x-or y-standard deviations of CS from AV. If the difference in standard deviation is close to zero, both models behave in a similar fashion. Negative values correspond to a larger standard deviation for CS than AV and positive values to a larger standard deviation for AV than CS. We expect that the CS model shows generally more variability in the vertical direction, since it has a longer pharynx than the AV-model. For AV we expect that more variability is allowed in the horizontal direction, since it has a relatively long horizontal dimension in comparison to the CS-model.

Figure 2 displays the results, which are split by vowel. The red triangles show the results in the vertical direction and the black dots the results in horizontal direction. Given the same acoustic output for CS and AV, the articulatory variation differs. Model CS allows more variability (negative values for the difference in standard deviation) in the vertical direction for /a/ and /i/, but not for /u/. Findings for /u/ may differ from the other vowels since the constriction location is placed along the bending of the vocal tract and may be affected by it. Model AV allows more variability (positive values for the difference in standard deviation) in the horizontal direction for /u/ only. In /a/ the two models are quite similar (close to zero) and in /i/ the CS-model can vary more freely than the AV-model. This result goes against our original hypothesis. However, /i/ is to a large extent constrained by the shape of the palate which varies between the two models.

Plot of Means

Vowels

To summarize, the articulatory results provide evidence that the location of the vocal tract bending affects the articulatory variability for back and low vowels. Speakers with long vertical vocal tract dimensions have larger degrees of freedom to move vertically than speakers with shorter vertical vocal tract dimensions. Similarly, speakers with long horizontal dimensions have the possibility to move more freely in this direction than speakers with shorter horizontal dimensions. The variability of front vowels may be more constrained by the shape and steepness of the palate than by vocal tract bending.

Results for the motor commands

In this section we will concentrate on the variability in lambda values (=motor commands) for /a/ and /u/ only. In principle, 6 different muscles can be activated, but only a few of them are necessary to realize the constriction of the relevant vowel.

To produce the velar constriction of /u/, a combined activation of the Styloglossus and Genioglossus Posterior are necessary. Both muscles are responsible for pulling the tongue up and back. We found slightly more variation in both muscles in the CS-model.

For /a/ a constriction is formed in the pharyngeal region. This constriction is produced by a combination of Hyoglossus (moving the tongue down and back) and Styloglossus (up and back) activation. Results from our simulations show much more variation for model CS in both muscles than in model AV.

Summary and conclusion

We have constructed speaker-specific biomechanical tongue models with the aim of investigating the effect of the location of vocal tract bending on articulatory variability and the variability in motor command space. Assuming the length of the vocal tract is kept constant, acoustic models predict only negligible effects of the bend of the vocal tract. However, the bending location within the vocal tract may be crucial for the relation between vertical and horizontal dimensions in the vocal tract and the respective degrees of freedom the tongue has within these dimensions.

Based on similar acoustic targets for the corner vowels we ran simulations using the speaker-specific models and analyzed the corresponding variability at the articulatory and motor command level.

Evidence for our assumptions was found for back and low vowels. The high front vowels may be more sensitive to palate shape than the location of the bend in the vocal tract. Further investigations are planned which will allow us to disentangle effects due to different vocal tract shapes and biomechanics.

Figure 1 :

 1 Figure 1: 1 st row: Mid-sagittal MRI data (left AV, right CS), 2 nd row: biomechanical tongue models with FE mesh for both speakers, 3 rd row: articulatory simulations, 4 th row: corresponding vowel spaces

Figure 2 :

 2 Figure 2: Differences in variability (standard deviation) of the articulatory data in vertical (y) and horizontal (x) direction between model AV and CS; if this difference is negative then variability CS >variabillity AV ; for positive values variability CS <variability AV . Data are split by vowel.

* Supported by a grant from the German Research Council to the SPRECHart project.


Rudolph Sock
email: sock@unistra.fr

Fabrice Hirsch

Yves Laprie

Pascal Perrier

Béatrice Vaxelaire

Gilbert Brock

Fayssal Bouarourou

Camille Fauth

Véronique Ferbach-Hecker

Liang Ma

Béatricevaxelaire

Véroniqueferbach-Hecker

Julie Busset

Jean Sturm

An X-ray database, tools and procedures for the study of speech production

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

Introduction

Today, Electro Magnetic Articulometers (EMA), optical motion capture systems, ultrasounds and dynamic MRI are the favoured experimental setups used to study speech kinematics. EMA and optical systems have the strong advantage in that they perform at sample frequencies which are way above the Nyquist frequency of vocal tract movements. They also have the crucial possibility to inform on actual flesh-point movements. However, optical systems are obviously not adapted to visualisation of non-visible movements that occur inside the vocal tract. Similarly, EMA systems provide information limited to the region extending from the lips to the rear part of the hard palate. To get information on the remaining part of the vocal tract, ultrasounds and MRI techniques are more appropriate, in spite of the fact that they offer a global description without any information on flesh points. However, ultrasound data are also spatially limited by the shadow projected by the hyoid bone onto the lower part of the pharynx, and most current systems provide data at the limited sampling rate of 30Hz. In addition, calibration issues are still under debate regarding such systems. MRI techniques provide very accurate views of vocal tract geometry. Nevertheless, even if constant improvements suggest that such techniques will be the best in a near future, 2D dynamic MRI cannot, to day, provide images at a rate higher that 20 Hz. In addition, the latter technique calls for an expensive experimental setup, which will not necessarily be available to every speech laboratory. In this context, endeavouring for the dissemination of cine-radiographic data recorded in the past, at a time when no regulations limited their use, and of tools allowing their analyses and their application in the context of speech motor control studies, and of articulatory modelling approaches, represents an interesting contribution to problems related to the speech sciences in general. Cineradiographic systems provide 2D images of the whole vocal tract, from the glottis to the lips at 50 or 60Hz rates.

The Phonetics Institute of Strasbourg (IPS), whose research activities, in part, are conducted within a larger laboratory, LiLPa (Linguistique, Langues et Parole), has been the centre of excellence in France, and one of the main centres in the world, for cineradiographic data acquisition. This is mainly due to the expertise of Georges Straka, Pela Simon [START_REF] Simon | Les consonnes françaises. Mouvements et positions articulatoires à la lumière de la radiocinématographie[END_REF] and André Bothorel [START_REF] Bothorel | quatre sujets : vues latérales du conduit vocal, vues frontales de l'orifice labial, données acoustiques[END_REF]. In this context, the current project, coordinated by the IPS in Strasbourg, the Gipsa-Lab in Grenoble and the LORIA in Nancy, aims to share some of the best X-ray movies on speech production that were made at the IPS, as from the end of the fifties. The project concerns 20 movies of high quality, dealing with linguistic issues in languages spoken in Europe, in Africa, in Asia and in Latin America. The following will be made available to the scientific community: 1) a set of multilingual and multimedia data, unique in the world, on speech production containing cine-radiographic images of the vocal tract, acoustic signals, tracings and contours of the vocal tract, all synchronised and accessible within a processing platform; 2) adapted tools and software that allow extracting articulatory information from these data, in relation with prior phonological labelling.

Tools and procedures developed

Despite their intrinsic interest, X-ray films cannot be used directly. We therefore developed software intended to extract, store and process contours of speech articulators. This software called "X-articulators" comprises tools to, firstly, delineate contours and, secondly, to exploit them.

Delineating articulator contours

Drawing contours by hand is a tedious task and several works have been dedicated to the automatic tracking of articulator contours [START_REF] Thimm | Extraction of articulators in x-ray image sequences[END_REF][START_REF] Laprie | Towards automatic extraction of tongue contours in x-ray images[END_REF][START_REF] Jallon | A semi-automatic method for extracting vocal-tract movements from x-ray films[END_REF]. We developed software, called "Xarticulators"', enabling several tracking tools to be used according to the nature of articulators.

Rigid structures, like the mandible, can be tracked robustly by correlating a reference image, with images to process. In this particular case, the photometric energy of the mandible is sufficiently stronger than that of the tongue to neglect its influence all the more since the region to be correlated can be chosen so as to minimize the effect of the tongue. This simple tracking turned out to be very efficient to tract the mandible, the upper part of the skull in order to compensate for head movements, and even the hyoid bone provided that it does not move too high and intersect other high photometric organs. Tracking provides the displacement parameters, i.e. rotation and translation.

Structure deforming along time, and giving rise to one contour only, i.e. the lips, the larynx and the epiglottis, have been tracked via the algorithm proposed by [START_REF] Jallon | A semi-automatic method for extracting vocal-tract movements from x-ray films[END_REF]. Contours have been drawn by hand for a series of key images (approximately 10% of the total number of images to process) and approximated by Bspline curves, with a constant number of control points.

The general idea is to choose a rectangular region in the image including the object to be tracked. Then, images are cut to keep only this region in order to remove the influence of other organs. Non key images are indexed by calculating the distance of their DCT coefficients (Discrete Cosine Transform) to those of the key images. For each image, the three closest key images are kept with their distance to the image analyzed. Finally, the new contour given by the control points of the spline is the weighted average of the contours of the three closest key images. If the visual evaluation of tracking shows that some images are not tracked correctly, because they are too far from key images, then they are added as key images. The tongue contour is much more difficult to track automatically since there are one or two contours depending on tongue shape. The contour to consider is that of the midsagittal plane (see [START_REF] Vaxelaire | Apports des techniques radiologiques et de la radiocinématographie à l'étude de la production de la parole[END_REF] for a discussion). In many images, the tongue presents a marked groove located at the mid-sagittal plane, which gives the relevant contour. The two upper edges of the tongue may give rise to a second image contour (or exceptionally two if the tongue is not symmetric at all) (see Fig. 1). In practice, this explains the existence of two contours in X-ray images. Since we also recorded MRI images for one speaker of the database it was possible to check contours chosen to represent the tongue even if the tongue was partially hidden. Another difficulty is the presence of teeth in the oral cavity which hide the tongue contour. Human experts often use a completion strategy consisting in drawing a convex contour in the mouth probably because this shape is much more natural. However, ultrasound images, and MR images as well, show that the tongue contour is concave not only for retroflex tongue shapes but also for many other less extreme tongue shapes.

Although there are some automatic or semi-automatic tracking algorithms, the difficulties presented above led us to draw tongue contours by hand in order to guarantee their relevance. However, the graphical interface of X-articulators offers many tools to make this work easier. In particular, it is well known that the perception of movement by eyes makes the detection of contours easier. We thus added tools to play a small number of contiguous images, preceding or following the current image, when drawing a contour.

Processing of articulator contours

Contours alone are not very useful and therefore X-articulators provide several tools to make the exploitation of contours easier.

Firstly, it is possible to add landmarks on contours in order to identify a given anatomical point (tongue apex, higher incisor…) used to anchor a coordinate system (e.g. that of the articulatory model). Landmarks can also be used to link two objects. For instance the specific region of the mandible used to track this structure has been chosen to minimize interactions with the tongue and aluminium filters. Its shape thus does not correspond to that of the mandible. A more realistic contour of the mandible can be attached to this region and its movement is copied from the region used for tracking. Secondly, since it is important to relate contours to phonemes uttered, it is possible to import a file of phonetic annotations. Synchronization of the annotation is carried out via visual events which produce an acoustic event simultaneously.

Thirdly, X-articulators provides tools to construct articulatory models from the articulator contours via Principal Component Analysis (PCA). The main articulator is the mandible, whose movement is approximated by two linear components controlling the rotation and the shift. The first component roughly corresponds to jaw aperture. The deformation modes of the tongue are then determined by PCA after the mandible movement has been subtracted from the tongue contours. Then, lip deformations are approximated by two factors (roughly aperture and protrusion), and the lower part of the pharynx (including the larynx and the epiglottis) is represented by two factors. The entire model is described in [START_REF] Laprie | Proceeding of International Seminar on Speech Production[END_REF].

Semi-automatic articulatory measurement

A semi-automatic procedure to measure displacements of articulators of the vocal tract from radiographic tracings has been defined, implemented and validated. For such an analysis, it is important to extract a limited number of points which inform, in a relevant manner, on anterior-posterior and vertical positions of articulators, and from which, in the absence of flesh-point information, and by calculating velocities and accelerations, would adequately reflect the kinematic behaviour of vocal tract articulators. In this aim, we have proposed to describe the tongue contour from, on one hand, the three most elevated intersection points of the superior contour of the tongue, using 4 horizontal lines, parallel to the average direction from the hard palate, and spaced every 0.5 cm (the highest line going through the superior incisive), and, on the other hand, the 3 most posterior intersection points of the lingual contour using 4 lines parallel to the average direction from the posterior pharyngeal wall (the most retreated being that which approaches the pharyngeal wall). This method is currently being tested in the kinematic analysis of the effects of juncture in one of the French movies.

The database and accessing the database

The database on the site currently comprises 4 X-ray-movies, chosen from the archives of the IPS; they have been digitized and synchronized with the audio. Access to the database is at present restricted, as it is in an assessment phase, carried out by laboratories that have expertise in the study of speech production, based on X-ray data.

Consulting and distribution of data to a larger public could only be done after refinement of the ergonomics of the database and clarification of some legal issues related to distribution of processed medical data.

Procedures to access the data, via internet, have also been defined. A restricted sub-set can be visualized directly at the website of the project.

Searching in the database

Several searching methods are available (Figure 3): 1. Search by corpus: the user types the name of the researcher for whom the movie was made, and in response all sentences of the entire corpus will be listed; 2. Search by sequence: the user types a string of sounds, and the database in return gives all sentences which comprise this string of sounds, side-by-side; 3. Search by phoneme: the user selects a sound or sounds he or she wants to examine.

The base proposes all sentences in which the sound or the sounds requested figure.

In case of several sounds, the base will present all sentences in which these sounds appear, be they side-by-side or not. 4. Search by language: the user selects the language he or she wants to study. The base proposes all sentences in the selected language. 5. A cross-research, using all these different criteria is also possible.

Sheets and selecting a sheet

A sheet is available and searchable for each sentence in the database (Figure 4). It furnishes information on the speaker, the language and the different phonemes which appear in the sentence. Some images that allow the user to verify the quality of the images of the movie are visible. When tracings of the vocal tract are available, they are also available in the sheet. Finally, note that the movie could be played.

The user may select a sheet or several sheets, and place them in his or her basket, so as to be able to retrieve later and more easily movies of interest. Informations on the speaker, the language and different phonemes which appear in the selected sentence are given. The movie can be played to evaluate its quality; tracings of the vocal tract area are proposed here.

Ordering a movie

Movies on the site are of poor quality. To obtain them in a better resolution, an e-mail message should be sent to sock@unistra.fr. The movies would then be sent by internet or on a DVD (in a DV, .avi or .mov format).

Conclusion

The IPS X-ray data correspond to 20 movies of high quality. Some of these movies are associated with digitised hand-drawn tracings. Others are currently being processed with the help of the software X-articulators.

By the time of the ISSP conference, 10 movies, together with available associated data would be sent, on request, to researchers preoccupied with speech production and perception studies.

Figure 1 :

 1 Figure 1: Tongue (from Lundberg and Stone (1999) with the three contours (in yellow) that can appear on an X-ray image.

Figure 2 :

 2 Figure 2: Examples of contours on X-ray images. The two yellow lines in the right image correspond to the tongue contours visible in the pharyngeal cavity.

Figure 3 .

 3 Figure 3. The database form. Searches can be made by corpus, sequence, phoneme and language.

Figure 4 .

 4 Figure 4. Example of a sheet. Informations on the speaker, the language and different phonemes which appear in the selected sentence are given. The movie can be played to evaluate its quality; tracings of the vocal tract area are proposed here.

DOCVACIM : DOnnées Cinéradiographiques Valorisées pour l'étude de la Coarticulation, de l'Inversion et l'évaluation de Modèles physiques. An Agence Nationale de la Recherche (ANR n° ANR-07-CORP-018) Project,

-2011


Marco Kuhlmann

Joachim Niehren

Logics and Automata for Totally Ordered Trees

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

A totally ordered tree is a tree equipped with an additional total order on its nodes. It provides a formal model for data that comes with both a hierarchical and a sequential structure. Depending on the application, the two structural aspects may be more or less dependent on each other: the total order may be obtained by a traversal of the tree, defined by a logic formula from tree relations, or completely independent.

The research reported in this paper is motivated by an application of totally ordered trees in computational linguistics, where they are used as formal models for dependency structures. A dependency structure is a representation of the syntactic structure of a natural-language sentence in terms of wordto-word dependencies, such as the dependency between a verb and its direct object. Such dependencies impose a tree-shaped hierarchical structure onto the words, while word order imposes a sequential structure. An example for a dependency structure is given in Fig. 1. Dependency-based representations have a long history in descriptive linguistics. Recently, they have received a lot of interest for many computational tasks, such as information extraction [START_REF] Culotta | Dependency tree kernels for relation extraction[END_REF], Figure 1: A dependency structure machine translation [START_REF] Quirk | Dependency treelet translation: Syntactically informed phrasal SMT[END_REF], and, most prominently, data-driven parsing [START_REF] Nivre | The CoNLL 2007 shared task on dependency parsing[END_REF].

In this paper, we study monadic second-order logic (MSO) as a description language for totally ordered terms (tots). Dependency structures can be understood as special cases of tots, where the sibling order is induced by the total order. Monadic second-order logic is generally useful in order to express properties of graphs or trees [START_REF] Thatcher | Generalized finite automata with an application to a decision problem of second-order logic[END_REF][START_REF] Courcelle | Handbook of graph grammars and computing by graph transformations[END_REF][START_REF] Gottlob | Monadic queries over tree-structured data[END_REF][START_REF] Courcelle | Graph Grammars and Logic[END_REF].

Here we are particularly interested in lifting Doner, Thatcher, and Wright's theorem on the equivalent expressiveness of MSO and tree automata for finite trees to tots [START_REF] Thatcher | Generalized finite automata with an application to a decision problem of second-order logic[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF]. This theorem has first been proved for ground terms, and got extended to various kinds of trees and graphs of bounded tree width [START_REF] Rabin | Decidability of Second-Order Theories and Automata on Infinite Trees[END_REF][START_REF] Gottlob | Monadic datalog and the expressive power of languages for web information extraction[END_REF][START_REF] Courcelle | Graph Grammars and Logic[END_REF].

The new problem that we are faced with, is to deal with the addition of a total order to a finite term structure. The easy cases of this problem are those where the total order is MSO-definable from the term structure: MSO for ground terms is decidable, and thus MSO for ground terms with MSO-defined total orders is decidable as well. In the first part of the paper, we prove that MSO for general tots is not decidable. We show this by a reduction of the MSO satisfiability problem for grids; this problem is well-known to be undecidable (while first-order logic of grids can encoded into Presburger arithmetics). In the second part of the paper, we restrict the classes of models of MSO formulas to sets of tots with bounded gap-degree [START_REF] Plátek | On relaxability of word order by D-Grammars[END_REF]. This means that the descendant sets of nodes are segmented into a bounded number of intervals in the total order. Our main contribution is the result that MSO satisfiablity of sets of tots with bounded gap-degree is decidable. In order to establish this, we introduce an algebraization for these sets. This leads us to a notion of tree automaton for gap-bounded sets of tots, which we show to have the same expressiveness as MSO.

Related work. Our algebraic perspective on automata goes back to the work of Mezei and Wright from the 1960s [START_REF] Mezei | Algebraic automata and context-free sets[END_REF]. It was generalized by Courcelle [START_REF] Courcelle | Recognizable sets of unrooted trees[END_REF], and applied to many kinds of trees, including unranked sibling-ordered trees as they appear in the context of XML [START_REF] Carme | Querying unranked trees with stepwise tree automata[END_REF]. Courcelle has proposed two different algebraizations for graphs [START_REF] Courcelle | Graph Grammars and Logic[END_REF] for which MSO can be reduced to finite automata. Graphs of bounded tree or clique width belong to these algebras, so that MSO satisfiability is decidable for them.

Dependency structures can be used to quantify the generative capacity of many grammar formalisms for natural language [START_REF] Kuhlmann | Dependency Structures and Lexicalized Grammars[END_REF]: they are more informative than strings, but less formalism-specific than parse trees. The formal properties of dependency structures and sets of such structures have been studied only recently [START_REF] Kuhlmann | Dependency Structures and Lexicalized Grammars[END_REF]. Automata for these structures define a notion of regularity. For regular sets of dependency structures, there is a direct relation between the gap-degree measure and string-generative capacity. In particular, regular sets of dependency structures with gap-degree 0 correspond exactly to the context-free languages, and regular sets of structures with gap-degree at most 1 and an additional property called well-nestedness give the string languages generated by Lexicalized Tree Adjoining Grammars (TAGs). More generally, every string language obtained from a regular set of dependency structures with bounded gap-degree is semilinear and can be recognized in polynomial time. Without gap restrictions, parsing quickly becomes NP-hard [START_REF] Koller | Generation as dependency parsing[END_REF]. Recent work has shown that most dependency structures required for the analysis of natural language have a small gap-degree [START_REF] Kuhlmann | Mildly non-projective dependency structures[END_REF]. However, not all natural languages can be described by sets of dependency structures with bounded gap-degree; counterexamples have been given for Czech [START_REF] Holan | Two useful measures of word order complexity[END_REF]. 2 Totally Ordered Terms

We start by introducing totally ordered terms, and MSO for their description. We make use of the following auxiliary notions and notations:

nod (σ(t 1 , . . . , t m )) = {ε} ∪ { iπ ∈ N * | i ∈ [m], π ∈ nod (t i ) } .
A linearization of a finite set A is a word in A * in which each element of A occurs exactly once. We note that the set of linearizations of A is isomorphic to the set of total orders on A in an obvious way.

Definition 1. A totally ordered term (tot) over Σ is a pair τ = t, w where t ∈ T Σ is a term, and w is a linearization of nod(t).

The set of all tots over Σ is denoted by TOT Σ . Three examples for tots are visualized in Fig. 2; each of them provides a different linearization for the same term a(b(c), d(e)). Solid edges depict the term structure, dotted lines project nodes to their position in the linearization. In Fig. 2a, the nodes of a(b(c), d(e)) are ordered by the preorder traversal of the underlying term structure. The two examples in Fig. 2b and 2c are derived by swapping c with e and d, e, respectively.

In the following, we often identify a term t ∈ T Σ with a relational structure nod (t) ; ( : σ) σ∈Σ : for each m-ary symbol σ ∈ Σ, this structure provides a labelling relation : σ with arity m + 1. Given a node π ∈ nod (t), labelling π : σ(π1, . . . , πn) holds if and only if π is labelled by σ in t. A tot τ = (t, w) can be viewed as a relational structure that extends the structure corresponding to t by the total order that is represented by the linearization w.

Monadic second-order logic (MSO) for tots is defined as usual. Let Vars be a set that contains infinitely many node variables x, y, z ∈ Vars, and infinitely many set variables X, Y, Z ∈ Vars. The formulas of MSO for tots are the following, where σ ∈ Σ is a function symbol of arity m:

φ, φ ′ ::= x : σ(x 1 , . . . , x m ) | x y | x ∈ X | φ ∧ φ ′ | ¬φ | ∃ x. φ | ∃ X. φ
These formulas are interpreted in the usual Tarskian style in the relational structures corresponding to tots. Given a tot τ = (t, w) and a variable assignment α : Vars → nod (t), we write τ, α |= φ if and only if the formula φ evaluates to true in τ under the assignment α, and τ |= φ if τ, α |= φ holds for any assignment α.

MSO formulas with n free node variables over the signature Σ define n-ary relations for all tots over Σ. Most basically, we can define node equality (=), equality-or-precedence ( ), and the child relation ⊳:

x ⊳ y = def σ∈Σ 1≤i≤m=ar(σ) ∃ x 1 , . . . , x m . y = x i ∧ x : σ(x 1 , . . . , x m )) .
The dominance relation ⊳ * of a term is the reflexive, transitive closure of ⊳, and thus definable in MSO. 3 This is in contrast to first-order logic, where the dominance relation is usually added to the relational structure. Let C ⊆ TOT Σ be a set of tots over Σ. The MSO-satisfiability problem of C is the problem to decide whether ∃ τ ∈ C. τ |= φ, where φ is some closed MSO formula.

Undecidability of MSO Satisfiability

We now present our first technical result, which is valid for all signatures Σ with at least one binary function symbol and one constant.

Theorem 1. MSO satisfiability for the class of all tots over Σ is undecidable.

For the proof, we make use of a simple tool to obtain undecidability results for graph-like structures. Let m, n ∈ N. The grid of dimensions m × n is the structure

G m,n = [m] × [n] ; nextEast, nextSouth , where nextEast = { i, j , i ′ , j ′ | i ′ = i + 1, j ′ = j } and nextSouth = { i, j , i ′ , j ′ | i ′ = i, j ′ = j + 1 } .
We can view a grid as an (m × n)-matrix in which we can navigate along columns (using the relation nextEast) and rows (using nextSouth). The square grid of size m is the grid of dimensions m × m. The following result is standard:

Fact [START_REF] Courcelle | Graph Grammars and Logic[END_REF]. The MSO satisfiability problem of every class of graphs that contains infinitely many square grids is undecidable.

To make use of this result to prove Theorem 1, we show how to encode grids as tots (Proposition 1), and that every closed MSO formula interpreted on grids can be translated into a closed MSO formula interpreted on tots that has the same models modulo encoding (Proposition 2).

Without loss of generality, we use the signature Σ = {cons, •, nil} with ar(cons) = 2, ar(•) = 1, and ar(nil) = 0, and employ the following naming scheme for nodes: for 0 ≤ i and 1 ≤ j, The encoding of the general grid G m,n is the tot G m,n = t m,n , w m,n , where

π i,j = if i = 0 then 1 j-1 else 1 j-1 21 i-1 . cons cons cons nil • • • • • • • • • nil nil nil π0,1 π0,2 π0,3 π0,4 π1,1 π1,2 π1,3 π2,1 π2,2 π2,3 π3,1 π3,2 π3,3 π4,1 π4,2 π4,3
t m,n = if n = 1 then cons(nil, • m (nil)) else cons(t m,n-1 , • m (nil)) w m,n = π 0,1 • • • π 0,n • π 0,n+1 • π 1,1 • • • π 1,n • • • π m+1,1 • • • π m+1,n
For illustration, Fig. 3 shows the tot that encodes the square grid G 3,3 . We will use the nodes that are labelled with the constructor • (i.e., the nodes of the form π i,j , i ∈ [m], j ∈ [n]) as representatives for the entries of the grid proper.

The following MSO-defined sets are of general interest for the axiomatization of grid encodings. We use definitions by formulas with free set variables that may be parametrized by a free node variable x, so that the corresponding sets are parametrized by the node value of x.

FirstChild (x) = { y | x : •(y) } ∪ { y | ∃ z. x : cons(y, z) } SecondChild (x) = { y | ∃ z. x : cons(z, y) } , Root = { x | Father (x) = ∅ } Father (x) = { y | x ∈ FirstChild (y) } ∪ { y | x ∈ SecondChild (y) } Succ(x) = { y | x ≺ y, ¬∃ z. x z y } , Cons = { x | x : cons(_, _) } , Grid = { x | x : •(_) } , Nil = { x | x : nil } .
We note that, since is a total order, Succ is an injective partial function. The cons-labelled nodes provide the backbone of the tot; they 'glue' the lines of the grid together. The north of the grid is its first line; the south is its last line.

Backbone = (Root ∪ FirstChild (Backbone)) -Nil LastBackbone = { x ∈ Backbone | FirstChild (x) ⊆ Nil } North = (SecondChild (Root) ∪ FirstChild (North)) ∩ Grid South = (SecondChild (LastBackbone) ∪ FirstChild (South)) ∩ Grid
Recursive definitions are interpreted with respect to least fixed points, which is expressible in MSO, as is the reflexive-transitive closure of a relational image S(x), denoted by S(x) * . We next define sets of nodes by MSO formulas that permit us to navigate through the grid:

NextEast(x) = { y ∈ Grid ∩ FirstChild (x) | x ∈ Grid } NextSouth(x) = { y ∈ Grid ∩ Succ(x) | x ∈ Grid -South }
The anchor of a node x is the (uniquely determined) closest node on the backbone that dominates x. Via the anchors, we can navigate along the rows in a grid.

Anchor (x) = { y ∈ Backbone | x ∈ FirstChild * (SecondChild (y)) } NextRow (x) = { y ∈ Grid | FirstChild (Anchor (x)) = Anchor (y) } PreviousRow (x) = { y ∈ Grid | FirstChild (Anchor (y)) = Anchor (x) }
We can now axiomatize the class of grid encodings in MSO:

(A1) The backbone consists of the nodes labelled with cons. Backbone = Cons (A2) For every node in the grid that does not lie in the south, taking the next step in the total order takes us to the next row.

∀ x ∈ Grid -South. ∃ y ∈ NextRow (x). Succ(x) = {y} (A3)
Dually, every node in the grid that does not lie in the north can be reached from a node in the previous row. Succ(FirstChild (LastBackbone)) = SecondChild (Root) (A7) The total order propagates along the rows of the grid.

∀ x ∈ Grid -North. ∃ y ∈ PreviousRow (x). Succ(y) = {x} (
∀ x, y. Succ(Father (x)) = Father (y) =⇒ Succ(x) = {y} (A8) When being in the south, the next step with the total order leads to the first element of the next column eastwards.

∀ x ∈ North. Succ(NextSouth * (x) ∩ South) = FirstChild (x)
Proposition 1. Every encoded grid satisfies the axioms A1-A8. Conversely, every tot that satisfies these axioms is a grid encoding.

Proof. To verify that encoded grids satisfy the axioms A1-A8 is straightforward; here we show the converse. Let τ = (t, w) be a tot such that τ |= A1 ∧ • • • ∧ A8. We show that there exists a grid G m,n such that τ = G m,n . Axiom A 1 asserts that Backbone = Cons, which implies that t has the following form, where t i = • mi (nil) for some m i ≥ 0: t = cons(t 1 , cons(t 2 , . . . cons(t n , nil) . . .)).

We have to show that all terms t i have the same length in order to prove that t = t m,n . This property is less obvious since it depends on the total order among the nodes. For n = 0, it follows that t = nil, and there is nothing to show, so we can assume n ≥ 1. The form of t implies that Backbone = { π 0,j | j ∈ [n] },

North = { π i,1 | i ∈ [m 1 ] } , and South = { π i,n | i ∈ [m n ] } . Lemma 1. m 1 = • • • = m n
We first show that |t 1 | ≤ |t j | for all j ∈ [n] by induction on n. The case n = 1 is trivial. For the case n > 1, it suffices to show that |t n-1 | ≤ |t n |. This follows from Axiom A2, which asserts that for each node π in t n-1 , there exists a node π ′ in t n such that Succ(π) = {π ′ }, and from the observation that Succ is total for all nodes of t 1 by Axiom A4, functional and injective. Dually, using Axiom A3, we can show that

|t j | ≤ |t 1 | for all j ∈ [n]. Consequently, |t 1 | = • • • = |t n |.
It remains to show that w is indeed the total order that is imposed on the encoded grid. The following series of Lemmas together with Axiom A4 establishes that the total order on t is uniquely determined by the axioms. Since the order in the grid translation satisfies these axioms, it must be equal to this order.

Lemma 2. ∀ j ∈ [n]. Succ(π 0,j ) = {π 0,j+1 } and Succ(π 0,n+1 ) = {π 1,1 }
Since for each j ∈ [n], the node π 0,j is a cons node, the first half of the claim is stated in Axiom A5. The successor of π 0,n+1 follows from Axiom A6 in combination with the observation that SecondChild (Root) = {π 1,1 }; this is so since Root ⊆ Cons by Axiom A6, and n ≥ 1.

Lemma 3. ∀ i ∈ [m]. ∀ j ∈ [n -1]. Succ(π i,j ) = {π i,j+1 }
We show that Succ(Father (π i,j )) = Father (π i,j+1 ), and from this deduce the claim by Axiom A7. The proof proceeds by induction on i. In the case that i = 1, using the definition of Father and Lemma 2, we see that Succ(Father (π 1,j )) = Succ(π 0,j ) = {π 0,j+1 } = Father (π 1,j+1 ) .

For i > 1, we may assume that Succ(π i-1,j ) = {π i-1,j+1 }. Thus,

Succ(Father (π i,j )) = Succ(π i-1,j ) = {π i-1,j+1 } = Father (π i,j+1 ) . Lemma 4. ∀ i ∈ [m]. Succ(π i,n ) = {π i+1,1 }
We start by proving the following auxiliary claim by induction on j:

∀ j ∈ [n]. ∀ i ∈ [m]. NextSouth * (π i,j ) ∩ South = {π i,n }
For j = n, this is obvious, given that π i,n ∈ South. For j < n, we may assume that NextSouth * (π i,j+1 ) ∩ South = {π i,n }. Moreover, π i,j ∈ Grid -South, which, by definition of NextSouth, implies that NextSouth(π i,j ) = Succ(π i,j ). Thus, Instantiating Axiom A8 with π i,1 ∈ North, we see that

NextSouth * (π i,j ) ∩ South = NextSouth * (NextSouth(π i,j )) ∩ South = NextSouth * (Succ(π i,j ))∩South Lemma 3 = NextSouth * (π i+1,j )∩South = {π i,n } . nextEast(x, y) 0 = y ∈ NextEast(x) ∀ x. ψ 0 = ∀ x ∈ Grid . ψ 0 nextSouth(x, y) 0 = y ∈ NextSouth(x) ∀ X. ψ 0 = ∀ X ⊆ Grid . ψ 0 x ∈ X 0 = x ∈ X ∩ Grid ψ ∧ ψ ′ 0 = ψ 0 ∧ ψ ′ 0 ¬ψ 0 = ¬ ψ 0
Succ(NextSouth * (π i,1 ) ∩ South) = FirstChild (π i,1 ) = {π i+1,1 } .
Since NextSouth * (π i,1 )∩South = {π i,n } by the auxiliary claim above, this implies that Succ(π i,n ) = {π i+1,1 }.

Together with Axiom A4, the preceding Lemmas establish that Succ(π) is uniquely determined for all π = π m,n . This ends the proof of Proposition 1. .

Proposition 1 states that we can define the encodings of grids using MSO for tots. We now show how to express MSO formulas for grids using MSO formulas for tots. The translation of a closed MSO formula ψ for grids is as follows:

ψ = def ∃Grid ∃NextSouth∃NextEast∃ . . . . (Defs ∧ A1 ∧ • • • ∧ A8 ∧ ψ 0 )
where ψ 0 is given in Fig. 4, and Defs contains the above definitions for all occuring set variables, all of which are existentially quantified in the outermost quantifier prefix.

Proposition 2. For every closed formula ψ from the set of all MSO formulas over grids and every grid G, ψ |= G implies that ψ |= G .

Proving this proposition from Proposition 1 is routine, since it is largely independent of the particularities of the encoding. Note however that the proposition does not hold for formulas with free variables. For these, quantification would need to be restricted to nodes in Grid , and exclude nodes in Cons ∪ Nil .

Bounded Gap-Degree

Given the undecidability of the MSO satisfiability problem for the class of unrestricted tots, we are interested in restricted classes for which decidability can be obtained. A family of such classes that is relevant for applications in computational linguistics is obtained from the gap-degree measure [START_REF] Plátek | On relaxability of word order by D-Grammars[END_REF][START_REF] Kuhlmann | Dependency Structures and Lexicalized Grammars[END_REF]. Let τ be a tot, and let π, π 1 , π 2 be nodes of τ . The set of descendants of π, denoted by desc(π), is the set of all nodes π ′ ∈ nod (t) such that π ⊳ * π ′ . The interval with endpoints π 1 and π 2 , denoted by [π 1 , π 2 ], is the set of all nodes π ′ ∈ nod (τ ) such that π 1 π ′ π 2 . Note that for terms ordered by a pre-order traversal, each descendant set forms an interval. In the general case, though, a descendant set desc(π) may be partitioned into a sequence of (maximal) intervals, which we call the segments of π. We define MSO formulas y 1 ≡ x y 2 stating that y 1 and y 2 belong to the same segment of x:

y 1 ≡ x y 2 = def ∀ z. (y 1 z y 2 ∨ y 2 z y 1 ) → x ⊳ * z
This formula defines an equivalence relation ≡ π on the descendant set desc(π) with the property that each equivalence class forms a (maximal) interval. We call such a relation a segmentation. Definition 2. Let τ be a tot, and let π be a node of τ . The gap-degree of π, deg(π), is defined as the index of the relation ≡ π , minus one. The gap-degree of τ , deg(τ ), is the maximum among the gap-degrees of its nodes. A set L of tots is gap-bounded, if there is a constant g L such that deg(τ ) ≤ g L , for every τ ∈ L.

The tot in Fig. 2a has gap-degree 0, while those in Figs. 2b and2c have gapdegree 1. In Figs. 2b andFigs. 2c, the node b has two segments ({b} and {c}); in Fig. 2a, it has only one ({b, c}).

Lemma 5. The gap-degree of the tot G n,n is n + 1.

This Lemma shows that our undecidability proof fails when we restrict the models of our MSO formulas to classes of tots that are gap-bounded. Even better, this restriction implies decidability: Theorem 2. The MSO satisfiability problem of every gap-bounded class of tots is decidable.

The remainder of this paper is concerned with the proof of this result. To do so, we establish a link between MSO for gap-bounded classes of tots on the one hand, and an algebraic notion of automata on the other.

Segmented Tots and Subtots

We develop a notion of 'substructure' for tots that will serve as intermediate results when constructing tots algebraically. They may be little more general than tots, in that their linearisations may be segmented, so we call them segmented tots.

For illustration, let us reconsider the tot in Fig. 2c. Its first subterm is b(c). The linearization of the nodes of this subterm is segmented into two parts, while leaving a gap between the b-node and the c node, into which external nodes may be plugged, such as the nodes of d(e) when reconstructing the original tot.

A k-segmented linearization over a finite set A is a k-tuple w 1 , . . . , w k of nonempty words over A such that w 1 • • • w k forms a linearization. Every k-segmented linearization w defines a total ordering on A, which satisfies a 1 a 2 if a 1 occurs left of a 2 in w. In addition, it defines an equivalence relation ≡ on A, such that a 1 ≡ a 2 if they occur in the same segment of w. The segments of w are the equivalence classes of ≡, so that the index of ≡ is k. The equivalence classes form intervals with respect to the total ordering, i.e.:

a 1 ≡ a 2 ⇒ ∀ a. (a 1 a a 2 ∨ a 2 a a 1 ) → a 1 ≡ a ≡ a 2
Conversely, every pair of total ordering on A and an equivalence relation ≡ on A of index k that satisfy the above condition define an k-segmented linearization on A. Definition 3. A k-segmented tot over a signature Σ is a pair t, w where t is a term over Σ and w a k-segmented linearization of nod(t).

The relational structure corresponding to a segmented tot (t, w) is the structure nod (t) ; , ≡, ( : σ) σ∈Σ ; it provides the total ordering and the equivalence relation ≡ defined by w and the labeling predicates. The MSO of segmented tots is the MSO with symbols for all these relations and interpreted over these relational structures.

Substructures of segmented tots can now be defined by extending the notion of subterms. Let τ = t, w be a segmented tot and node π ∈ nod (t). The set desc(π) is segmented by the relation ≡ π , which is defined by an MSO formula with three free variables:

y 1 ≡ x y 2 = def y 1 ≡ y 2 ∧ ∀ z. (y 1 z y 2 ∨ y 2 z y 1 ) → x ⊳ * z .
This means that segments of desc(π) are either separated by nodes of τ external to desc(π) or by the segmentation of τ .

Let t| π the subterm of t at node π, i.e., t| ε = t and σ(t 1 , . . . , t m )| iπ = t i | π , where i ∈ [m] = ar(σ). Recall that nod (t| π ) = { π ′ | ππ ′ ∈ nod (t) }. The subtot of τ at π is given by the subterm t |π and the segmented linearization of its nodes induced by ≡ π and . The of gap-degree of a segmented tot τ is one less then the maximal number of segments of its subtots τ |π .

Segmented Words

We introduce segmented words and define operators for them that will be useful for the algebraization of tots. Let A be a set and k a natural numbers.

A k-segmented word over A is a k-tuple of non-empty words over A. The positions of a k-segmented

word ψ = a 1 1 • • • a n1 1 , . . . , a 1 k • • • a n k k are pairs of natural numbers: pos(ψ) = { i, j | i ∈ [k], j ∈ [n i ] }.
The set of positions is totally ordered by the lexicographic order, i.e. i ′ , j ′ < i, j iff i ′ < i or i ′ = i ∧ j ′ < j. It is partitioned into k classes by the equivalence i ′ , j ′ ≡ i, j iff i ′ = i. For every a ∈ A, the relation Q a ⊆ pos(ψ) contains all positions i, j where a occurs, i.e., a j i = a. We now define operators for k-segmented words, where we assume k ∈ [l] for a fixed natural number l. Let W (k) be the set of k-segmented words over A. We define a multi-sorted algebra S with domains W (1), . . . , W (l); the functions We define automata for the algebra of segmented tots T ′ as automata for the multi-sorted term algebra T ∆ . Since well-sorted terms over ∆ are recognizable, we can use standard tree automata that recognized languages of well-sorted terms.

We call a set of segmented tots L ⊆ T ′ with bounded gap-degree recognizable, if and only if the corresponding set of term encodings { t ∈ T ∆ | t T ′ ∈ L } is recognizable by a tree automaton. Standard results on tree automata [START_REF] Comon | Tree automata techniques and applications[END_REF] show that recognizable set of segmented tots are closed under union, intersection, complementation and projection. Note also, that the set of all tots (i.e., segmented tots without gaps) is recognizable Theorem 4. A gap-bounded set of segmented tots is MSO-definable if and only if it is recognizable. The transformations from formulas to automata and back are effective.

Proof. The transformation of automata for T ∆ into MSO for segmented tots needs to express the rules of the automata. This works as usual, except that one has to express the operators σ, ψ T ′ in the MSO of segmented tots. This is straightforward.

The transformation of MSO formulas to automata works as for Thatcher and Wright's theorem [START_REF] Thatcher | Generalized finite automata with an application to a decision problem of second-order logic[END_REF]: Boolean connectives and monadic second-order quantifiers are mapped to the closure operators for union, complementation and projection. What remains to show is that we can construct automata that check the atomic predicates x y and x ≡ y. The fundamental insight in this construction is that it suffices to remember, by means of the state information that the tree automaton provides, for each node π, in which segments of the subtot τ | π the nodes α(x), α(y) occur (if any). Based on this information, the question whether α(x) ≺ α(y) can be decided by looking at the label σ, ψ at π: if α(x) occurs in the j x th segment of the i x th substructure of τ | π , and α(y) occurs in the j y th segment of the i y th substructure, then α(x) ≺ α(y) iff the j x th occurrence of the symbol i x precedes the j y th occurrence of the symbol i y ; if α(x) or α(y) does not occur in some substructure, but equals π, then the relevant occurrence is the (single) occurrence of the symbol 0 in ψ. A similar argument holds for the case α(x) ≡ α(y). As long as the number of gaps (and hence, the number of segments) in a tot is bounded, the required state set is of bounded size.

One perhaps surprising consequence of this Theorem is that total orders of MSO-defined sets of tots with bounded gap-degree are always definable by MSO over terms without the order. Given a term t ∈ T Σ , variables x 1 , x 2 and nodes π, π ′ ∈ nod (t), let t * [x → π, y → π ′ ] ∈ T Σ×2 {x,y} be the tree obtained from t by annotating all its nodes by the set of variables that are mapped to it. Similarly, we define τ * [x → π, y → π ′ ] ∈ TOT Σ×2 {x,y} to be the tot term(τ ) * [x → π, y → π ′ ], seg(τ ) in which the variable assignment is annotated. Final remark. We have shown that the MSO satisfiability problem for tots with bounded gap-degree is decidable, while the general case is undecidable. A question that we need to leave unanswered for now is whether the first-order satisfiability problem of general tots is decidable in contrast to the case of MSO.

  swapping c and d, e

Figure 2 :

 2 Figure 2: Three total orders for the tree a(b(c), d(e))

Figure 3 :

 3 Figure 3: The encoding of the square grid G3,3. The solid lines represent the term structure; the dashed lines visualize the relation nextSouth.

  A4) The root node occupies the first position in the total order. ¬∃ x. Succ(x) = Root (A5) Every step to the first child of a cons node is a step in the total order. ∀ x ∈ Cons. Succ(x) = FirstChild (x) (A6) The nil node terminating the backbone immediately precedes the northwestern corner of the grid.

Figure 4 :

 4 Figure 4: Encoding MSO of grids into MSO of tots: the compositional part.

Corollary 1 .

 1 Let φ be a closed MSO formula for tots in TOT Σ with bounded gap degree. Then the following term language { term(τ) ∈ T Σ | τ |= φ } is regular as well as { term(τ ) * [x → α(x), y → α(y)] ∈ T Σ×2 {x,y} | τ |= φ }. Proof. The set L 1 = { τ ∈ TOT Σ | τ |= φ } is an MSO defined set of tots over Σ. Let A 1 be an tree automaton over ∆ that recognizes { s ∈ T ∆ | s T ∈ L 1 } according to Theorem 4. The projection A 1 to Σ recognizes { term(τ ) ∈ T Σ | τ ∈ L 1 }as required, where the rules of the projected automaton B 1 are as follows:σ, ψ (p 1 , . . . , p m ) → p ∈ Rules(A 1 ) σ( p 1 , ψ 1 , . . . , p m , ψ m ) → p, ψ ∈ Rules(B 1 )For the second statement, letL 2 = { τ * [x → α(x), y → α(y)] ∈ TOT Σ×2 {x,y} | τ, α |= φ ∧ x y } and automaton A 2 recognize { s ∈ T ∆×2 {x,y} | s T ∈ L 2 }according to Theorem 4. The projection A 2 to Σ × 2 {x,y} recognizes the second term language of the corollary { term(τ ) * [x → α(x), y → α(y)] ∈ T Σ×2 {x,y} | τ, α |= φ ∧ x y) }, where the projection automaton B 2 has the following rules: σ, ψ , V (p 1 , . . . , p m ) → p ∈ Rules(A 2 ) σ, V ( p 1 , ψ 1 , . . . , p n , ψ m ) → p, ψ ∈ Rules(B 2 )

  The set of positive natural numbers is denoted by N. Given some n ∈ N, we write [n] for the set {1, . . . , n}. A signature Σ is a non-empty, finite set of function symbols σ, each equipped with a fixed, non-negative arity, denoted by ar(σ). The set of (ground) terms over Σ is the smallest set T Σ such that if σ is a symbol of arity m and for each i ∈ [m], t i ∈ T Σ , then σ(t 1 , . . . t m ) ∈ T Σ . The set of nodes of a term t ∈ T Σ is a set of addresses in N * : the root node of t is addressed by the empty word ε, and the ith child of the node π is addressed by the extended address πi:

To see this, note that x dominates all elements of the set Y , where Y is the least set satisfying the equation Y = {x} ∪ { z | ∃ y. y ∈ Y → y ⊳ z }.

of this algebra are defined by segmented words. Each function first shuffles the segments of its arguments into a new segmented word, and then fuses adjacent segments to arrive at a segmented word with at most l segments. To make this formal, we need three auxiliary notions: The multiplicity of a letter a ∈ A in a segmented word ψ over A is the number of positions i, j ∈ pos(ψ) such that i, j ∈ Q a . A multiset over a finite set B is a function µ :

} defines an operator ψ S of type:

To give a definition of this function, let the occurrence number occ(i, j) ∈ N of a position i, j ∈ pos(ψ) with i, j ∈ Q a be the number of positions i ′ , j ′ ∈ pos(ψ)

where

The number of functions of S is infinite as long as we do not bound the maximal arity m ∈ N. Furthermore, S does not contain any constant, so it is useless standalone.

Algebra of Segmented Tots

For the algebraization of tots, we fix a signature Σ of function symbols and a gap bound l ∈ N. For all k ∈ N let T (k) ⊆ TOT Σ be the set of tots over Σ with k segments. We define a multi-sorted algebra T with domains T (1), . . . , T (l).

For every tot τ = t, w in T (k), let term(τ ) = t and seg(τ ) = w. The algebra T provides operations of type σ, ψ T :

. Specifically, we define the value σ, ψ T (τ 1 , . . . , τ n ) = τ as follows:

where pfx i is the function that takes a sequence of nodes and prefixes every node in this sequence by the address i. This algebra has a finite number of functions, whose maximal arity is bounded by the maximal arity in Σ. The constants of this algebra are of the form σ, 1 , where σ is a constant in Σ.

This means that every k-segmented tot can be constructed from the operators of the algebra T if k ∈ [l]. For instance, the tot in Fig. 2b is equal to: a, 0121 T ( b, 0, 1 T ( c, 0 T ), d, 10 T ( e, 0 T )) .

The substructure at b, i.e., the first child of the root, has gap-degree 1. This is reflected by the segmented word 0, 1 whose comma matches the gap.

Proof. Let τ = (t, w), where t = σ(t 1 , . . . , t n ) for some σ ∈ Σ, and t 1 , . . . , t n ∈ T Σ . For all i ∈ [k], let k i be the number of segments of τ | i , so that

The segmented linearization w of τ must be of the following form, where

This holds, since each segment of seg(τ ) must be a concatenation of words of S j i s due to convexity, and since the segments of the same substructure must appear in their original order. Let

The decomposition of segmented tots does not need to be unique; for example, a, 011 T ( a, 0, 1 T ( b, 0 T )) = a, 01 T ( a, 01 T ( b, 0 T )) .

Both expressions describe the same tot with term a(a(b)) and the node order ε 1 11. In the first expression, the subtot of the first child is artificially split into two subsequent segments, which are then fused without insertion of nodes into the gap. On the right, this artificial split is avoided. It is not difficult to see that every segmented tot can be constructed in a unique manner, when disallowing immediate repetitions in constructors ψ, i.e. segments in N * iiN * , for every i ∈ N. Let T ′ be the restriction of T to operators (σ, ψ) without immediate repetitions in ψ.