Etienne Grandjean
email: etienne.grandjean@unicaen.fr

Frédéric Olive
email: frederic.olive@lif.univ-mrs.fr

A logical approach to locality in pictures languages

Keywords: Picture languages, locality and tiling, recognizability, linear time, cellular automata, logical characterizations, monadic second-order logic, existential second-order logic. 1998 ACM Subject Classification: F.1.1 Models of Computation, F.1.3 Complexity Measures and Classes, F.4.3 Formal Languages

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

Introduction: context and discussion

Locality is a useful and widespread concept common to many areas of science: physics, chemistry, mathematics, etc. In computer science, it is a unifying notion, connecting combinatorics, logic, formal language theory, computational models, and complexity theory. For example, the local and combinatorial notion of tiling allowed Hao Wang and al. to prove in 1962 the undecidability of the decision problem of some logics [START_REF] Kahr | Entscheidungsproblem reduced to the forall-exists-forall case[END_REF][START_REF] Wang | Dominoes and the aea case of the decision problem[END_REF][START_REF] Wang | Computation, Logic, Philosophy. A Collection of Essays[END_REF][START_REF] Börger | The Classical Decision Problem[END_REF]. Locality is also a reference notion in computational complexity (e.g., see [START_REF] Van Emde | Dominos are forever[END_REF][START_REF] Van Emde | The convenience of tilings. Complexity, Logic and Recursion Theory[END_REF]) and in formal language theory with the notion of regular or recognizable language that has been extended to tree or graph languages (see [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of Second-Order logic[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF]). Typically, as recalled by Borchert [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF], Mac Naughton and Papert established in their classical monograph [START_REF] Mcnaughton | Counter-free automata[END_REF] that a word language is regular "iff it consists of the words whose positions can be colored so that the coloring respects the letters and obeys a given finite set of neighborhood constraints".

There is a wealth of notions of locality in logic and finite model theory. For first-order logic, Libkin's book [START_REF] Libkin | Elements of Finite Model Theory[END_REF] (see Chapters 4 and 5) identifies Hanf locality [START_REF] Hanf | Model-theoretic methods in the study of elementary logic[END_REF] and Gaifman locality [START_REF] Gaifman | On local and nonlocal properties[END_REF] and describes a series of locality results for this logic [START_REF] Fagin | Monadic generalized spectra[END_REF][START_REF] Fagin | On monadic np vs. monadic co-np[END_REF][START_REF] Schwentick | On winning ehrenfeucht games and monadic np[END_REF][START_REF] Hella | Notions of locality and their logical characterizations over finite models[END_REF][START_REF] Schwentick | Local normal forms for first-order logic with applications to games and automata[END_REF][START_REF] Libkin | Logics capturing local properties[END_REF] and its order-invariant extension [START_REF] Grohe | Locality of order-invariant first-order formulas[END_REF] or counting extension [START_REF] Libkin | Logics with counting and local properties[END_REF].

As a striking result, Gaifman's Theorem states in 1982 [START_REF] Gaifman | On local and nonlocal properties[END_REF] that any first-order sentence is equivalent to a boolean combination of local sentences: roughly, a local sentence states the existence of k elements x 1 , . . . , x k , at distance 2d from each other (for some fixed d) such that for each x i , the restriction of the structure to the set of elements at distance d of x i has some fixed property ψ.

When applied to a class of structures of bounded degree, e.g. the class of cubic graphs, the local feature of first-order sentences can be even strengthened. As shown in [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF][START_REF] Lindell | A normal form for first-order logic over doubly-linked data structures[END_REF], such a sentence is essentially equivalent to a boolean combination of cardinality formulas with only one variable, i.e. of the form ∃ k x ψ(x), meaning "there exists k elements x that satisfy ψ(x)".

An even stronger notion of locality in logic is presented by Borchert in [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF]. There, a picture language is local if it is defined as the set of pictures that do not contain any pattern belonging to some fixed finite set. Borchert proves that a picture language is local iff it is definable by a first-order sentence with only one variable that is universally quantified, provided each picture is represented on its pixel domain with successor functions that encode the pixel adjacencies.

Computational models and computational complexity also involve several locality notions. Whereas it is questionable whether the Random Access Machine (RAM) or the pointer machine (e.g., see [START_REF] Schönhage | Storage modification machines[END_REF]) are local models, Turing machines and cellular automata are regarded as the prototypical models of local sequential and local parallel computation, respectively. Notice the role of the underlying structure for deciding what is local and what is nonlocal: while a configuration of a Turing machine or of a cellular automaton is essentially a word or a picture, that are local structures, a configuration of a RAM (resp. pointer machine) is a function from addresses to register contents (resp. from locations to locations). Clearly, such a function f allows to access in one step any location b from any other one a, even it they are arbitrarily far from each other, provided that f (a) = b: this contradicts the locality principle.

This paper 1 deals with locality in the context of words and pictures as underlying structures. For any dimension d ≥ 1, a d-picture language is a set of d-dimensional words (colored d-dimensional grids). We study descriptive complexity of nondeterministic classes of word/picture languages by syntactical fragments of existential second-order logic. First, notice the following results:

1. In a series of papers culminating in [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF], Giammarresi et al. proved that a 2-picture language is recognizable (i.e. is the projection of a local picture language) iff it is definable in existential monadic logic (EMSO). In short: REC 2 = EMSO. This is a picture language variant of the classical characterization of the regular/recognizable word language by (existential) monadic second-order logic, in short REG = REC 1 = EMSO = MSO [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF][START_REF] Elgot | Decision problem of finite automata design and related arithmetics[END_REF][START_REF] Trakhtenbrot | Finite automata and the logic of one-place predicates[END_REF][START_REF] Mcnaughton | Counter-free automata[END_REF].

2. In fact, the class REC 2 contains some NP-complete problems. More generally, one observes that for each dimension d ≥ 1, REC d can be defined as the class of d-picture languages recognized in constant time by nondeterministic d-dimensional cellular automata. That means, for each L ∈ REC d there is some constant integer c such that each computation stops at instant c and a picture belongs to L iff it has at least one computation that stops with each cell in an accepting state (see e.g. [START_REF] Sommerhalder | Parallel language recognition in constant time by cellular automata[END_REF]).

The present paper originates from two questions about word/picture languages:

• How can we generalize the proof of the above-mentioned theorem of Giammarresi et al. to any dimension? That is, can we establish the equality REC d = EMSO for d-picture languages of any dimension d ≥ 1?

• Can we obtain logical characterizations of time complexity classes of cellular automata ? This originates from a question J. Mazoyer asked the first author in 2001 (personal communication): exhibit a logical characterization of the linear time complexity class of nondeterministic cellular automata.

As Cris Moore has pointed to us (personal communication), it is significant that those picture language classes -recognizable languages and picture languages recognized by time bounded cellular automatawere invented independently in the physics literature (see [START_REF] Lindgren | Complexity of two-dimensional patterns[END_REF] for a survey). It is also well-known that those two kinds of picture languages are strongly related: it is a folklore result that the set of time-space diagrams of any time-bounded (nondeterministic) cellular automaton is a recognizable picture language.

A d-picture language is a set of d-pictures p : [1, n] d → Σ. There are two natural manners to represent such an object as a first-order structure, both presented in the literature:

• as a pixel structure (see e.g. [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF][START_REF] Giammarresi | Two-dimensional languages, volume 3-Beyond words of Handbook of Theoretical Computer Science[END_REF][START_REF] Matz | The monadic quantifier alternation hierarchy over grids and graphs[END_REF][START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF]): on the pixel domain [1, n] d where the sets p -1 (s), s ∈ Σ, are encoded by unary relations (Q s ) s∈Σ and the underlying d-dimensional grid is encoded by d successor functions (see Definition 2.2);

• as a coordinate structure (implicitly defined and used in [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF], Lemma 9.2(d)): on the coordinate domain [1, n] where the sets p -1 (s) are encoded by d-ary relations (R s ) s∈Σ . Moreover, one uses the natural linear order of the coordinate domain [1, n] and its associate successor function (see Definition 2.3).

Our main results

We establish two kinds of logical characterizations of d-picture languages, for all dimensions d ≥ 1:

1. On pixel structures: REC d = ESO(arity 1) = ESO(var 1) = ESO(∀ 1 , arity 1). That means a d-picture language is recognizable iff it is definable in monadic ESO (resp. in ESO with one first-order variable, or in monadic ESO with one universally quantified first-order variable).

2. On coordinate structures: NLIN d ca = ESO(var d + 1) = ESO(∀ d+1 , arity d + 1); that means a d-picture language is recognized by a nondeterministic d-dimensional cellular automaton in linear time (see e.g. [START_REF] Terrier | Language Recognition by Cellular Automata[END_REF][START_REF] Kutrib | Nondeterministic cellular automata and languages[END_REF]) iff it is definable in ESO with d +1 distinct first-order variables (resp. ESO with second-order variables of arity at most d + 1 and a prenex first-order part of prefix ∀ d+1 ).

Significance of our results

Results of above Items 1 and 2 proceed from normalizations of first-order and ESO logics that we prove over picture languages. Roughly speaking, they mean that the languages of the involved complexity/logical classes are "projections" of local languages, or -in logical terms -are definable by ESO sentences whose first-order part is a local formula.

More specifically, the normalization equality ESO(arity 1) = ESO(∀ 1 , arity 1) of Item 1 is a consequence of the fact that, on pixel structures (and, more generally, on structures that consist of bijective functions and unary relations), any first-order formula is equivalent to a boolean combination of cardinality formulas of the form: "there exists k distinct elements x such that ψ(x)", where ψ is a quantifier-free formula with only one variable. The normalization of the logic -reducing it to its "one first-order variable" fragment, explicitly expresses the local feature of MSO on pictures. The results and methods of Item 1 can be summed as follows: one exploits the homogeneous framework of logic for making simpler, more explicit -using only one first-order variable -and more uniform the proof and ideas of the main result of Giammarresi et al. [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF][START_REF] Giammarresi | Two-dimensional languages, volume 3-Beyond words of Handbook of Theoretical Computer Science[END_REF]; this allows us to generalize it to any dimension and, potentially, to other regular structures.

Intuitively, our characterization NLIN d ca = ESO(∀ d+1 , arity d + 1) of Item 2 naturally reflects a symmetry property of the time-space diagram of any computation of a nondeterministic d-dimensional cellular automaton: informally, the single first-order variable representing time cannot be distinguished from any of the d variables that represent the d-dimensional space. In other words, the d + 1 variables can be permuted without increasing the expressive (or computational) power of the formula. This is the sense of the inclusion ESO(∀ d+1 , arity d + 1) ⊆ NLIN d ca whose proof is far from trivial: roughly speaking, it needs to normalize any sentence of ESO(∀ d+1 , arity d + 1) by "sorting" its d + 1 first-order variables so that the sentence so "sorted" becomes local. As expected, this "sorted" ESO(∀ d+1 , arity d + 1) characterization of NLIN d ca for coordinate representation of pictures is the exact equivalent of the ESO(∀ 1 , arity 1) characterization of recognizable picture languages in pixel representation: the set of time-space diagrams of a (nondeterministic) cellular automaton is recognizable.

Notice that Borchert [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] has stated some results to be compared with our logical characterizations of recognizable languages and of linear time bounded complexity classes of multidimensional cellular automata. However, paradoxically, his paper never mentions cellular automata. To avoid technicalities in this introduction, we will describe and discuss the results of [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF], less general than ours, in Section 11.

Additional results

The last part of this paper consists of an attempt to answer two natural questions related to each other and concerning the frameworks/meaning of our main results and the possible extensions of these results:

• Question 1: Why two distinct frameworks? Why our logical characterizations of the class, on one hand, of recognizable pictures, i.e. EMSO on pixel encoding, and on the other hand, of the linear-time complexity class of nondeterministic d-dimensional cellular automata, i.e. ESO(var d) on coordinate encoding, do not involve the same logical framework with the same encoding?

• Question 2: Strict hierarchies: Which strict hierarchy results can we prove among the various definability classes we have studied?

Question 1: two frameworks. First, notice that for dimension one, i.e. for word languages, the pixel representation and the coordinate one trivially coincide. So the logical characterizations Intuitively, the logic ESO(var d) -or its equivalent restriction ESO(∀ d , arity d) -is not local when it is applied to the coordinate representations of d-pictures, for d ≥ 2. However, we will establish in Proposition 9.11 that such a locality can be obtained by "folding" the pictures: a d-picture language L is definable in ESO(var d) for coordinate representation iff the set of folded versions of pictures of L belongs to REC for coordinate representation of d-picture languages with d ≥ 2. This striking result contrasts with the equality ESO(var 1) = ESO(arity 1) for the pixel representation. To our knowledge, this is also the first result that shows that the arity is strictly more expressive than the number of first-order variables in ESO definability. We should mention that the proof of this separation result and of Theorem 10.6 involves in an essential manner the hypothesis that the arity of the ESO predicates equals the arity of the input predicates.

If the ESO arity is greater than the input arity then those separation problems remain open.

Structure of the paper

After Section 2 recalls succinctly some definitions -pictures, picture languages, the two encodings of pictures and logical notions -, Section 3 proves our first main result: logical characterizations of the class REC of recognizable picture languages.

The long proof of our second main result, the logical characterizations of NLIN d ca , is presented along Sections 4 to 8. A very long part of the proof consists in successively normalizing the logic ESO(var d) into more and more restrictive forms, the last one being ESO(∀ d , arity d, sorted ).

A recapitulation and a comparison of all the previous results is given in Section 9 with a formal proof that the same -pixel or coordinate -representation cannot be used for characterizing both classes REC and NLIN d ca ; however, we show how "folding" the pictures allows to relate in some manner the involved logics and both picture representations.

Finally, some hierarchy results are proved in Section 10 and Section 11 presents some additional results, open problems and final remarks.

Preliminaries

In the definitions below and all along the paper, we denote by Σ, Γ some finite alphabets and by d a positive integer. For any positive integer n, we set [n] := {1, . . . , n}. We are interested in sets of pictures of any fixed dimension d. Notice that 1-pictures on Σ are nothing but nonempty words on Σ.

Pictures as model theoretic structures

Along the paper, we will often describe d-languages as sets of models of logical formulas. To allow this point of view, we must settle on an encoding of d-pictures as model theoretic structures.

For logical aspects of this paper, we refer to the usual definitions and notations in logic and finite model theory (see [9] [45], or [START_REF] Grädel | Finite Model Theory and Its Applications[END_REF]). A signature (or vocabulary) σ is a finite set of relation and function symbols each of which has a fixed arity. A (finite) structure S of vocabulary σ, or σ-structure, consists of a finite domain D of cardinality n ≥ 1, and, for any symbol s ∈ σ, an interpretation of s over D, often denoted by s for simplicity. The tuple of the interpretations of the σ-symbols over D is called the interpretation of σ over D and, when no confusion results, it is also denoted σ. The cardinality of a structure is the cardinality of its domain. For any signature σ, we denote by struc(σ) the class of (finite) σ-structures. We write models(Φ) the set of σ-structures which satisfy some fixed formula Φ. We will often deal with tuples of objects. We denote them by bold letters.

There are two natural manners to represent a picture by some logical structure: on the domain of its pixels, or on the domain of its coordinates. This gives rise to the following definitions: Definition 2.2. The pixel structure, or pixel encoding, of a picture p :

[n] d → Σ is the structure pixel d (p) = ([n] d , (Q s ) s∈Σ , (succ i ) i∈[d] , (min i ) i∈[d] , (max i ) i∈[d] ).
where • succ j is the (cyclic) successor function according to the j th dimension of [n] d , mapping each (a 1 , . . . , a d ) ∈

[n] d on (a

( j) 1 , . . . , a ( j) d ) ∈ [n] d
, where we set : a ( j) i = a i for i j and, beside, a

( j) j = a j + 1 if a j < n; a ( j) j = 1 otherwise;
in other words, for a ∈ [n] d , succ j (a) is the d-tuple a ( j) obtained from a by "increasing" its j th component according to the cyclic successor on [n];

• the min i 's, max i 's and Q s 's are the following unary (monadic) relations:

min i = {a ∈ [n] d : a i = 1}; max i = {a ∈ [n] d : a i = n}; Q s = {a ∈ [n] d : p(a) = s}.
Definition 2.3. The coordinate structure, or coordinate encoding, of a picture p :

[n] d → Σ is the structure coord d (p) = [n], (Q s ) s∈Σ , <, succ, min, max (1)

where

• for s ∈ Σ, Q s is a d-ary relation symbol interpreted as the set of cells of p labelled by s; in other words:

Q s = {a ∈ [n] d : p(a) = s};
• <, min, max are predefined relation symbols of respective arities 2, 1, 1, that are interpreted, respectively, as the sets {(i, j) : 1 ≤ i < j ≤ n}, {1} and {n};

• succ is a unary function symbol interpreted as the cyclic successor (that is: succ(i) = i + 1 for i < n and succ(n) = 1).

For a d-language L, we set pixel

d (L) = {pixel d (p) : p ∈ L} and coord d (L) = {coord d (p) : p ∈ L}.
Remark 2.4. In the sequel, we often write, for some logical property P, that "P holds on pixel encodings", or "P holds on d-pixel encodings". Naturally, it means the property P holds for all structure of the form pixel(p) (or pixel d (p) in the latter case). The same formulations occur for "coordinate encodings" Remark 2.5. Several details are irrelevant in Definitions 2.2 and 2.3, i.e. our results still hold for several variants, in particular:

• In Definition 2.3, the fact that the linear order < and the equality = are allowed or not and the fact that min, max are represented by individual constants or unary relations;

• In both definitions, the fact that the successor function(s) is/are cyclic or not and is/are completed or not by predecessor(s) function(s).

At the opposite, it is essential that, in both definitions:

• The successor(s) is/are represented by function(s) and not by (binary) relation(s);

• The min, max are explicitly represented.

Logics under consideration

Let us now come to the logics involved in the paper. All formulas considered hereafter belong to relational Existential Second-Order logic. Given a signature σ, indifferently made of relational and functional symbols, a relational existential second-order formula of signature σ has the shape Φ ≡ ∃Rϕ(σ, R), where R = (R 1 , . . . , R k ) is a tuple of relational symbols and ϕ is a first-order formula of signature σ ∪ {R}. We denote by ESO σ the class thus defined. We will often omit to mention σ for considerations on these logics that do not depend on the signature. Hence, ESO stands for the class of all formulas belonging to ESO σ for some σ.

We will pay great attention to several variants of ESO. In particular, we will distinguish formulas of type Φ ≡ ∃Rϕ(σ, R) according to: the number of distinct first-order variables involved in ϕ, the arity of the second-order symbols R ∈ R, and the quantifier prefix of some prenex form of ϕ.

With the logic ESO σ (∀ d , arity ), we control these three parameters: it is made of formulas of which firstorder part is prenex with a universal quantifier prefix of length d, and where existentially quantified relation symbols are of arity at most . In other words, ESO σ (∀ d , arity ) collects formulas of shape ∃R∀xθ(σ, R, x) where θ is quantifier free, x is a d-tuple of first-order variables, and R is a tuple of relation symbols of arity at most . Relaxing some constraints of the above definition, we set:

ESO σ (∀ d ) = >0 ESO σ (∀ d , arity ) and ESO σ (arity ) = d>0 ESO σ (∀ d , arity ).
Finally, we write ESO σ (var d) for the class of formulas that involve at most d first-order variables, thus focusing on the sole number of distinct first-order variables (possibly quantified several times).

In the following sections, we'll prove that some logics have the same expressive power, as far as given sets of structures are concerned. When a normalization of a logic L into a logic L is thus relativized to a specific class S of structures, we write: L = L on S. The next definition details the meaning of this formulation.

Definition 2.6. Given a set of structures S and a formula Φ, the set of models of Φ that belong to S is denoted by models S (Φ). Two formulas Φ and Φ are S-equivalent if models S (Φ) = models S (Φ ). Given two logics L and L , we say that L ⊆ L on S if each Φ ∈ L is S-equivalent to some Φ ∈ L . Furthermore, we write L = L on S if both L ⊆ L and L ⊆ L hold on S.

In some very rare cases, we will consider the extension of ESO obtained by allowing quantification over functional symbols. The corresponding logic, ESOF, gathers all formulas of the form ∃R∃fϕ(σ, R, f), where R (resp. f) is a tuple of relational (resp. functional) symbols and ϕ is any first-order formula of signature σ ∪ {R, f}. The restrictions ESOF(var d) and ESOF(∀ d , arity ) of ESOF are defined as for ESO. The expressive power of these logics is quite high. A σ -NRAM is a nondeterministic Random Access Machine that takes σ-structures as inputs in the following way: for each s ∈ σ of arity and each -tuple t ∈ D , a special register [s, t] contains the value of s(t). Let NTIME σ (n d ) be the class of problems on σstructures decidable by a σ -NRAM in time O(n d ) where n is the size of the domain D of structures. The following was proved in [START_REF] Grandjean | Graph properties checkable in linear time in the number of vertices[END_REF]: Theorem 2.7 ( [START_REF] Grandjean | Graph properties checkable in linear time in the number of vertices[END_REF]). For all d > 0, NTIME(n d ) = ESOF(var d).

In the same paper, a normalization of ESOF(var d) was stated: Proposition 2.8 ( [START_REF] Grandjean | Graph properties checkable in linear time in the number of vertices[END_REF]). For all d > 0, ESOF(var d) = ESOF(∀ d , arity d).

Recognizable picture languages and their logical characterizations

In this section, we define the class of local (resp. recognizable) picture languages and establish the logical characterizations of the class of recognizable picture languages.

Local and recognizable picture languages

Our notion of local picture language or tilings language is based on some sets of allowed patterns (called tiles) of the bordered pictures. It is a simple generalization to any dimension of the notion of hv-local 2dimensional picture language of [START_REF] Latteux | Recognizable picture languages and domino tiling[END_REF] (see also [START_REF] Giammarresi | Two-dimensional languages, volume 3-Beyond words of Handbook of Theoretical Computer Science[END_REF][START_REF] Giammarresi | Recognizable picture languages[END_REF][START_REF] Giammarresi | Two-dimensional finite state recognizability[END_REF][START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF][START_REF] Giammarresi | Computing languages by (bounded) local sets[END_REF][START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF]). To define it formally, we need to mark the border of pictures. Here is our definition of local picture language or tilings language. Definition 3.2.

1. Given a d-picture p and an integer j

∈ [d], two cells a = (a i ) i∈[d] and b = (b i ) i∈[d]
of p are j-adjacent if they have the same coordinates, except the j th one for which |a jb j | = 1.

2.

A tile for a d-language L on Γ is a pair in (Γ ) 2 .

A picture p :

[n] d → Γ is j-tiled by a set of tiles ∆ ⊆ (Γ ) 2 if for any two j-adjacent points a, b ∈ dom(p ): (p (a), p (b)) ∈ ∆. 4. Given d sets of tiles ∆ 1 , . . . , ∆ d ⊆ (Γ ) 2 , a d-picture p is tiled by (∆ 1 ,. . . ,∆ d ) if p is j-tiled by ∆ j for each j ∈ [d].
5. We denote by L(∆ 1 ,. . . ,∆ d ) the set of d-pictures on Γ that are tiled by (∆ 1 ,. . . ,∆ d ).

6. A d-language L on Γ is local if there exist ∆ 1 , . . . , ∆ d ⊆ (Γ ) 2 such that L = L(∆ 1 ,. . . ,∆ d ). We then say that L is (∆ 1 , . . . , ∆ d )-local, or (∆ 1 , . . . , ∆ d )-tiled.
Remark 3.3. This notion of locality is more restrictive than that given by Giammarresi and al. [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF]. However, this does not affect the notion of recognizability as defined below, a robust notion that remains equivalent to that defined in [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF].

L = {π(p) : p ∈ L(∆ 1 , . . . , ∆ d )}.
We denote by REC d the class of recognizable d-languages.

Logical characterizations of recognizable picture languages

A characterization of recognizable languages of dimension 2 by a fragment of existential monadic second-order logic was proved by Giammarresi et al. [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF]. They established: Theorem 3.5 ([23]). For any 2-language L: L ∈ REC 2 ⇔ pixel 2 (L) ∈ ESO(arity 1).

In this section, we return to this result. We simplify its proof, refine the logic it involves, and generalize its scope to any dimension. Theorem 3.6. For any d > 0 and any d-language L, the following assertions are equivalent: Theorem 3.6 is a straightforward consequence of the forthcoming Propositions 3.9 and 3.14. The former states the equivalence of Items 1 and 2 above; the latter establishes the normalization ESO(arity 1) = ESO(∀ 1 , arity 1) on pixel structures.

In order to prove Proposition 3.9, it is convenient to first normalize the sentences of ESO(∀ 1 , arity 1). This is the role of the technical result below, which asserts that on pixel encodings, such a sentence can be rewritten in a very local form where the first-order part alludes only pairs of adjacent pixels of the bordered picture.

Lemma 3.7. On pixel structures, any sentence ϕ ∈ ESO(∀ 1 , arity 1) is equivalent to a sentence of the form:

∃U∀x i∈[d]          min i (x) → m i (x) ∧ max i (x) → M i (x) ∧ ¬max i (x) → Ψ i (x)          . ( 2
)
Here, U is a list of monadic relation variables and m i , M i , Ψ i are quantifier-free formulas such that

• atoms of m i and M i have all the form Q(x),

• atoms of Ψ i have all the form Q(x) or Q(succ i (x)),

where, in both cases, Q ∈ {(Q s ) s∈Σ , U}.

Proof. Let ϕ ∈ ESO(∀ 1 , arity 1) be a sentence on pixel structures. Suppression of equalities: Without loss of generality, assume that ϕ is in negative normal form2 ∃U∀xψ and that each equality in ψ is of the form succ

c i 1 i 1 . . . succ c i k i k (x) = x (3)
where the k indices i 1 , . . . , i k (k > 0) are pairwise distinct, and the exponents c i 1 , . . . , c i k are positive integers. Equation (3) holds in some pixel structure pixel d (p) of domain [n] d for some x (or, equivalently, for all x), iff the side n of p satisfies equalities n

= c i 1 = c i 2 = • • • = c i k .
So, we have to suppress any equality/inequality of the form n = c or n c, for c ≥ 1, in ϕ. First, notice that the inequality n c can be rewritten as

n > c ∨ j∈[c-1] n = j.
So, there remains to suppress such an equality/inequality n = c or n > c, for c ≥ 1. This can be done by introducing c + 1 new unary relation symbols denoted coord

= j 1 (x), for j ∈ [c + 1]. Intuitively, coord = j
1 (x) means: "the first coordinate of point x is j". Clearly, for any c > 0, the unary relations coord = j 1 are defined by induction on j ∈ [c + 1] with the formula ∀x δ c (x) where

δ c = (min 1 (x) ↔ coord =1 1 (x)) ∧ j∈[c] (¬max 1 (x) → (coord = j 1 (x) ↔ coord = j+1 1 (succ 1 (x)))).
Using those relations, it is rather easy to see that the two formulas ∀x (max 1 (x) → coord =c 1 (x)) and ∀x (coord

= j 1 (x) → coord = j+1 1 (succ 1 (x)))
express the assertions n = c and n > c, respectively. Hence, the first-order sentence ∀x ψ(x) is equivalent to the ESO(∀ 1 , arity 1)-sentence:

∃coord ∀x : δ(x) ∧ ψ (x)
where coord denotes the list of unary relation variables coord

= j
1 introduced in the required formulas δ c (x), the conjunction of which is denoted δ(x), and ψ (x) is the formula ψ(x) where each "sub-formula" n = c (resp. n > c) is replaced by the equivalent formula max 1 (x) → coord =c 1 (x) (resp. j∈[c] (coord

= j 1 (x) → coord = j+1 1 (succ 1 (x)))).
So, our sentence ϕ can be assumed to be in prenex conjunctive normal form ∃U∀xψ without equality, that means ψ is a conjunction of clauses with literals of the form Q(τ(x)) or ¬Q(τ(x)) where Q belongs to the set of relations

{(min i ) i∈[d] , (max i ) i∈[d] , (Q s ) s∈Σ , U} and τ is a (possibly empty) composition of function symbols succ i , i ∈ [d].
The idea is to introduce for each atom Q(τ(x)) that occurs in ψ a new unary relation variable denoted U Q,τ so that the atom U Q,τ (x) is equivalent to (can replace) the atom Q(τ(x)).

The U Q,τ 's are defined inductively by the conjunction of the following equivalences, denoted by basic and succ i -induct:

• basic: U Q,Id (x) ↔ Q(x), • succ i -induct: U Q,τsucc i (x) ↔ U Q,τ (succ i (x))
from which the equivalence claimed U Q,τ (x) ↔ Q(τ(x)) can be deduced.

Let δ(x) denote the conjunction of all the equivalences that define the U Q,τ 's and let ψ (x) denote the formula ψ(x) where each atom Q(τ(x)) is replaced by the atom U Q,τ (x). Clearly, the sentence ϕ = ∃U∀xψ(x) is equivalent to the sentence

ϕ = ∃U∃(U Q,τ ) s ∀x (ψ (x) ∧ δ(x)).
Now, put ϕ , that means ψ (x) ∧ δ(x), in conjunctive normal form. In order to organize and transform the clauses of ϕ , some terminology is required about clauses:

• a clause is x-pure (resp. i-cyclic) if it only contains atoms of the form Q(x) (resp. Q(x) or Q(succ i (x)))
where Q is a unary relation symbol which is neither any min j nor any max j ;

• an i-local clause is of the form ¬max i (x) → C(x) where C(x) is an i-cyclic clause;

• an i-min (resp. i-max) clause is of the form min i (x) → C(x) (resp. max i (x) → C(x)) where C(x) is an x-pure clause.

Using those definitions, we observe that

• the clauses of the conjunctive normal form of ψ (x) are x-pure;

• the succ i -induct clauses of δ(x) are i-cyclic;

• each basic implication of δ(x) of the form U Q,Id (x) → Q(x) or Q(x) → U Q,Id (x) is an x-pure clause except in case Q is min i or max i (i ∈ [d])
; clearly, in this case, the implication can be rephrased in one of the following four forms:

1. min i (x) → C(x), 2. max i (x) → C(x), 3. ¬min i (x) → C(x), 4. ¬max i (x) → C(x),
where C(x) is an x-pure clause (literal). Clauses 1 and 2 are i-min and i-max clauses, respectively. Clause 4 is i-local. Clause 3 can be replaced by the i-local clause ¬max i (x) → C(succ i (x)); this is justified by the equivalence (easily proved) of the universally quantified versions of those implications:

∀x(¬min i (x) → C(x)) ⇔ ∀x(¬max i (x) → C(succ i (x))).
So, we have shown how to rephrase the first-order part (that is ψ (x) ∧ δ(x)) of ϕ as a conjunction of x-pure clauses, i-cyclic clauses, i-local clauses, i-min clauses and i-max clauses. In fact, all those clauses are local with the exception of i-cyclic clauses. Recall that an i-cyclic clause C(x, succ i (x)) only contains atoms of the two forms Q(x) or Q(succ i (x))) where Q is a unary relation symbol which is neither any min j nor any max j . Its nonlocality is due to the following fact: if for a d-picture p we have a ∈ max i for any pixel a ∈ dom(p), then the pixel succ i (a) is not adjacent to a in p since we have succ i (a) ∈ min i by cyclicity of the function (permutation) succ i . In order to recover locality, let us first replace each i-cyclic clause C(x, succ i (x)) by the equivalent conjunction of the following two clauses:

1. the i-local clause ¬max i (x) → C(x, succ i (x)); 2. the "nonlocal" clause max i (x) → C(x, succ i (x)).

So, there remains to get rid of the "nonlocal" clause 2. The trick consists in making available in all the points of any succ i -cycle the value of each unary relation Q for the min i point of this cycle. This can be done by using a new unary relation symbol U Q min,i (x) defined inductively by the conjunction of the following min i and i-local clauses

min i (x) → (U Q min,i (x) ↔ Q(x)) ¬max i (x) → (U Q min,i (x) ↔ U Q min,i (succ i (x))).
Clearly, for each point a of any succ i -cycle γ, we have the constant value

U Q min,i (a) = Q(b)
where b is the unique point in γ ∩ min i . A new unary relation symbol U Q max,i can be defined similarly for max i . This justifies that each "nonlocal" clause max i (x) → C(x, succ i (x)) can be replaced by the x-pure clause C (x) obtained by substituting in the clause C(x,

succ i (x)) each atom Q(x) (resp. Q(succ i (x))) by U Q max,i (x) (resp. U Q min,i (x)).
Let us recapitulate what we have obtained. Our initial sentence ϕ = ∃U∀x ψ(x) of ESO(∀ 1 , arity 1) is logically equivalent to a sentence of the form ∃U ∀x Ψ(x) where

• U is the union of the set of ESO unary symbols of ϕ , that are U and the U Q,τ 's, and of the U Q min,i 's and U Q max,i 's we have just introduced; • Ψ(x) is a conjunction of x-pure clauses, i-min clauses, i-max clauses and i-local clauses. Now, it is easy to transform the conjunction of clauses Ψ(x) into the conjunction of formulas required:

i∈[d] [(min i (x) → Ψ min i (x)) ∧ (max i (x) → Ψ max i (x)) ∧ (¬max i (x) → Ψ i (x))].
More precisely, for each i ∈ [d],

• the conjunction of the i-min clauses (resp. the i-max clauses) and the x-pure clauses of Ψ(x) is trivially transformed into the required form min i (x) → Ψ min i (x) (resp. max i (x) → Ψ max i (x));

• the conjunction of the i-local clauses and the x-pure clauses of Ψ(x) is similarly transformed into the required form ¬max i (x) → Ψ i (x).

This completes the proof of Lemma 3.7.

Remark 3.8. The normal form of the formula obtained in Lemma 3.7 guarantees its local feature. In particular, notice that any successor symbol succ i can only apply to arguments assumed to be not in max i . That means we get the same normal form if the cyclic successor functions succ i , i ∈ [d], are replaced by successor functions for which succ i (a) = a (instead of a (i) ) if a ∈ max i .

Using the normal form so obtained for ESO(∀ 1 , arity 1) formulas on pixel structures, it is rather easy to prove the following equivalence. Proposition 3.9. For any d > 0 and any d-language L on Σ: L ∈ REC d ⇔ pixel d (L) ∈ ESO(∀ 1 , arity 1).

Proof.

⇒ A picture belongs to L if there exists a tiling of its domain whose projection coincides with the content of it cells. In the logic involved in the proposition, the "arity 1" corresponds to formulating the existence of the tiling, while the "∀ 1 " is the syntactic resource needed to express that the tiling behaves as expected. Let us detail these considerations. By Definition 3.2, there exist an alphabet Γ (which can be assumed disjoint from Σ), a surjective function π : Γ → Σ and d subsets ∆ 1 , . . . , ∆ d ⊆ (Γ ) 2 such that

L = {π • p : p ∈ L(∆ 1 , . . . , ∆ d )} (4)
The membership of a picture p : [n] d → Γ to L(∆ 1 , . . . , ∆ d ) is easily expressed on pixel d (p ) by a firstorder formula that asserts, for each dimension i ∈ [d], that, for any pixel x of p , the couple (x, succ i (x)) can be tiled with some element of ∆ i . Namely,

p ∈ L(∆ 1 , . . . , ∆ d ) iff pixel d (p ) | = ∀x ψ ∆ 1 ,...,∆ d (x)
, where:

ψ ∆ 1 ,...,∆ d (x) = i∈[d]                          min i (x) → ( ,s)∈∆ i Q s (x) ∧ ¬max i (x) → (s,s )∈∆ i Q s (x) ∧ Q s (succ i (x)) ∧ max i (x) → (s, )∈∆ i Q s (x)                          . Now, by (4)
Θ L = (∃Q s ) s∈Γ ∀x : ψ ∆ 1 ,...,∆ d (x) ∧ s∈Σ          Q s (x) → s ∈π -1 (s) Q s (x) ∧ s ∈Γ\π -1 (s) ¬Q s (x)          .
Here, denotes the exclusive disjunction. Notice that since Σ ∩ Γ = ∅, the tuples (Q s ) s∈Σ and (Q s ) s∈Γ are also disjoint. As Θ L clearly belongs to ESO(∀ 1 , arity 1), the proof is complete.

⇐ Consider L such that pixel d (L) ∈ ESO(∀ 1 , arity 1). Lemma 3.7 ensures that pixel d (L) is characterized by a sentence of the form:

∃U∀x i∈[d]          min i (x) → m i (x) ∧ max i (x) → M i (x) ∧ ¬max i (x) → Ψ i (x)          . ( 5
)
Here, U is a list of monadic relation variables and m i , M i , Ψ i are quantifier-free formulas such that atoms of m i and M i have all the form Q(x) and atoms of

Ψ i have all the form Q(x) or Q(succ i (x)), wih Q ∈ {(Q s ) s∈Σ , U}.
We have to prove that L is the projection of some local d-language L loc on some alphabet Γ, that is a (∆ 1 ,. . . , ∆ d )-tiled language for some ∆ 1 ,. . . , ∆ d ⊆ Γ 2 . Let U 1 , . . . , U k denote the list of (distinct) elements of the set {(Q s ) s∈Σ , U} of unary relation symbols of ϕ, so that the first ones U 1 , . . . , U m are the Q s 's (here, min i and max i symbols are excluded). The trick is to put each subformula m i (x), M i (x) and Ψ i (x) of ϕ into its complete disjunctive normal form with respect to U 1 , . . . , U k . Typically, each subformula Ψ i (x) whose atoms are of the form U j (x) or U j (succ i (x)), for some j ∈ [k], is transformed into the following "complete disjunctive normal form":

( , )∈∆ i          j∈[k] j U j (x) ∧ j∈[k] j U j (succ i (x))          . (6)
Here, the following conventions are adopted:

• = ( 1 , . . . , k ) ∈ {0, 1} k and similarly for ;

• for any atom α and any bit j ∈ {0, 1}, j α denotes the literal α if j = 1, and the literal ¬α otherwise.

For ∈ {0, 1} k , we denote by Θ (x) the "complete conjunction" j∈[k] j U j (x). Intuitively, Θ (x) is a complete description of x and the set

Γ = i∈[m] {0 i-1 10 m-i } × {0, 1} k-m
is the set of possible colors (remember that the Q s 's that are the U j 's for j ∈ [m] form a partition of the domain). The complete disjunctive normal form (6) of Ψ i (x) can be written into the suggestive form

( , )∈∆ i Θ (x) ∧ Θ (succ i (x)) .
If each subformula m i (x) and M i (x) of ϕ is similarly put into complete disjunctive normal form, that is ( , )∈∆ i Θ (x) and ( , )∈∆ i Θ (x), respectively (there is no ambiguity in our implicit definition of the sets ∆ i , since Γ), then the above sentence (5) equivalent to ϕ becomes the following equivalent sentence:

ϕ = ∃U∀x i∈[d]                          min i (x) → ( , )∈∆ i Θ (x) ∧ max i (x) → ( , )∈∆ i Θ (x) ∧ ¬max i (x) → ( , )∈∆ i ( Θ (x) ∧ Θ (succ i (x)) )                         
Finally, let L loc denote the d-language over Γ defined by the first-order sentence ϕ loc obtained by replacing each Θ by the new unary relation symbol Q in the first-order part of ϕ . In other words, pixel d (L loc ) is defined by the following first-order sentence:

ϕ loc = ∀x i∈[d]                          min i (x) → ( , )∈∆ i Q (x) ∧ max i (x) → ( , )∈∆ i Q (x) ∧ ¬max i (x) → ( , )∈∆ i ( Q (x) ∧ Q (succ i (x)) )                          Hence, L loc = L(∆ 1 , . . . , ∆ d ).
That is, L loc is indeed local and the corresponding sets of tiles are the ∆ i 's of the previous formula. It is now easy to see that our initial d-language L is the projection of the local language L loc by the projection π : Γ → Σ defined as follows: π( ) = s iff i = 1 for i ∈ [m] and U i is Q s . This completes the proof.

A normalization of ESO(arity 1) on pixel structures

Let us now come to the last step of the proof of Theorem 3.6. A key point of this step is a quantifier elimination result for first-order logic, proved independently in [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF] and in [START_REF] Lindell | A normal form for first-order logic over doubly-linked data structures[END_REF]. Its statement needs two new definitions.

Definition 3.10. A bijective structure is a finite structure of the form

S = (dom(S), f 1 , . . . , f d , f -1 1 , . . . , f -1 d , U 1 , . . . , U m ),
where each f i is a unary bijective function of inverse bijection f -1 i and the U i 's are unary relations.

Definition 3.11. A cardinality formula is a first-order formula of the form ∃ ≥k x ψ(x), where k ≥ 1 and ψ(x) is a quantifier-free formula with only one variable x. The quantifier ∃ ≥k x means "there exist at least k elements x such that".

Let us present without proof the following normalization of first-order logic on bijective structures which was proved in [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF][START_REF] Lindell | A normal form for first-order logic over doubly-linked data structures[END_REF] and extends a pioneering result by Seese [START_REF] Seese | Linear time computable problems and logical descriptions[END_REF][START_REF] Seese | Linear time computable problems and first-order descriptions[END_REF]. Proposition 3.12 ( [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF][START_REF] Lindell | A normal form for first-order logic over doubly-linked data structures[END_REF]). On bijective structures, each first-order sentence is equivalent to a boolean combination of cardinality formulas.

Clearly, a pixel structure expanded by the inverse functions of its successor functions, that is by the

predecessor functions pred i = succ -1 i , i ∈ [d]
, is a bijective structure. Therefore:

Corollary 3.13. On pixel structures, each first-order sentence is equivalent to a boolean combination of cardinality formulas.

Proof. By Proposition 3.12, each first-order sentence on pixel structures is equivalent to a boolean combination of cardinality formulas on pixel structures expanded by the predecessor functions. It is easy to see that any occurrence of a predecessor symbol pred i in a formula ∃ ≥k x ψ(x) can be eliminated: this can be done by replacing each occurrence of x in ψ(x) by succ i (x) (this is justified by the bijectivity of the successor function) and simplifying pred i (succ i (x)) = x (this is justified by the fact that all the predecessor and successor functions commute each other).

This allows to prove the following proposition.

Proposition 3.14. ESO(arity 1) ⊆ ESO(∀ 1 , arity 1) on d-pixel structures, for any dimension d > 0.

Proof. Let ∃U ϕ be an ESO(arity 1)-sentence. It is sufficient to prove that its first-order part ϕ can be transformed into an equivalent formula in ESO(∀ 1 , arity 1). By Corollary 3.13, ϕ is equivalent to a boolean combination of sentences of the form ψ ≥k = ∃ ≥k x ψ(x) (for k ≥ 1) where ψ(x) is a quantifier-free formula with the single variable x. Therefore, it is easily seen that proving the proposition amounts to show that each sentence of the form ψ ≥k or ¬ψ ≥k can be translated in ESO(∀ 1 , arity 1) on pixel structures. This is done as follows.

For a given sentence ∃ ≥k x ψ(x), we introduce k new unary relations U =0 , U =1 , . . . , U =k-1 and U ≥k , with the intended meaning:

A pixel a ∈ [n] d belongs to U = j (resp. U ≥k ) iff there are exactly j (resp. at least k) pixels b ∈ [n] d lexicographically smaller than or equal to a such that pixel d (p) | = ψ(b).
Then, we have to compel these relation symbols to fit their expected interpretations by means of a universal first-order formula with a single variable. First, we demand the relations to form a partition of the domain:

(1)

i< j<k ¬U =i (x) ∨ ¬U = j (x) ∧ i<k ¬U =i (x) ∨ ¬U ≥k (x) .
Then, we temporarily denote by ≤ lex the lexicographic order on [n] d inherited from the natural order on [n], and by succ lex , min lex , max lex its associated successor function and unary relations corresponding to extremal elements. Then the sets described above can be defined inductively by the conjunction of the following six formulas:

(2) (min lex (x) ∧ ¬ψ(x)) → U =0 (x) (3) (min lex (x) ∧ ψ(x)) → U =1 (x) (4) i<k (¬max lex (x) ∧ U =i (x) ∧ ¬ψ(succ lex (x)) → U =i (succ lex (x)) (5) i<k-1 (¬max lex (x) ∧ U =i (x) ∧ ψ(succ lex (x)) → U =i+1 (succ lex (x)) (6) (¬max lex (x) ∧ U =k-1 (x) ∧ ψ(succ lex (x)) → U ≥k (succ lex (x)) (7) (¬max lex (x) ∧ U ≥k (x) → U ≥k (succ lex (x))
Hence, under the hypothesis (1) ∧ . . . ∧ (7), the sentences ψ ≥k and ¬ψ ≥k are equivalent, respectively, to ∀x : max lex (x) → U ≥k (x) and ∀x : max lex (x) → ¬U ≥k (x).

To complete the proof, it remains to get rid of symbols succ lex , min lex and max lex that are not allowed in our language. It is done by referring to these symbols implicitly rather than explicitly. For instance, since succ lex (x) = succ i succ i+1 . . . succ d (x) for the smallest i ∈ [d] such that j>i max j (x), each formula ϕ involving succ lex (x) actually corresponds to the conjunction:

i∈[d]          (¬max i (x) ∧ i< j≤d max j (x)) → ϕ i          ,
where ϕ i is obtained from ϕ by the substitution succ lex (x) succ i . . . succ d (x). Similar arguments allow to get rid of min lex and max lex .

Remark 3.15. In this proof of ESO(arity 1) ⊆ ESO(∀ 1 , arity 1) on pixel structures pixel d (p), two crucial features of such a structure are involved:

• its bijective nature, which allows to rewrite first-order formulas as (boolean combinations of) cardinality formulas with a single first-order variable;

• the regularity of its predefined arithmetics (the functions succ i defined for each dimension), that endows pixel d (p) with a grid structure: it enables us to implicitly define a linear order of the whole domain dom(p) by means of first-order formulas with a single variable, which in turn allows to express cardinality formulas by "cumulative" arguments, via the sets U =i and U ≥k . Proposition 3.14 straightforwardly generalizes to the various structures that fulfill these two properties.

To conclude this section, let us mention that we can rather easily derive from Theorem 3.6 the following additional characterization of REC d : Corollary 3.16. For any d > 0 and any d-language L, L ∈ REC d ⇔ pixel d (L) ∈ ESO(var 1).

Linear time of cellular automata and its logical characterization

Beside the notion of recognizable picture language, the main concept studied in this paper is the classical notion of linear time complexity on nondeterministic cellular automata of any dimension (see for instance [START_REF] Kari | Basic Concepts of Cellular Automata[END_REF][START_REF] Terrier | Language Recognition by Cellular Automata[END_REF][START_REF] Kutrib | Nondeterministic cellular automata and languages[END_REF][START_REF] Delorme | Cellular automata: A parallel model[END_REF][START_REF] Sommerhalder | Parallel language recognition in constant time by cellular automata[END_REF][START_REF] Ozhigov | Computations on nondeterministic cellular automata[END_REF][START_REF] Lindgren | Complexity of two-dimensional patterns[END_REF][START_REF] Poupet | Cellular automata: Real-time equivalence between one-dimensional neighborhoods[END_REF]). We first present some general and informal considerations about cellular automata. In Subsection 4.2, we will give a precise definition of a specific model, the d-dimensional one-way cellular automaton. Then, in Subsection 4.3, we will state our main logical characterization theorem and will prove its first implication.

General considerations about cellular automata

Cellular automata are the simplest model of local and massively parallel computation. Basically, a cellular automaton is a regular array of identical cells called cellular array. Each cell is a copy of the same finite state automaton. At each step of a computation, the next state of each cell is produced by a local transition rule according to the current states of its neighbor cells. There are various definitions of cellular automata, depending essentially on the form of the cellular array, in particular on its dimension, on the chosen neighborhood, and on how the input is given to the cellular array.

In general, the cellular array is a finite line of cells (dimension d = 1), or is a finite rectangular grid of some fixed dimension d = 2, 3, or more. So, at each step of a computation, the states of the cellular array constitute a rectangular picture of dimension d over the state alphabet. It is natural to assume that the input of a d-dimensional cellular automaton is a d-picture on an alphabet Σ included in the state alphabet. Recall that all input d-pictures are assumed of the form p : [n] d → Σ. The integer n is called the side of the picture p and is the reference parameter for measuring complexity.

In the literature (e.g. [START_REF] Kari | Basic Concepts of Cellular Automata[END_REF][START_REF] Terrier | Language Recognition by Cellular Automata[END_REF][START_REF] Kutrib | Nondeterministic cellular automata and languages[END_REF][START_REF] Delorme | Cellular automata: A parallel model[END_REF][START_REF] Poupet | Cellular automata: Real-time equivalence between one-dimensional neighborhoods[END_REF][START_REF] Lindgren | Complexity of two-dimensional patterns[END_REF]), one essentially uses two different kinds of neighborhoods (each with two variants):

• a two-way neighborhood: the neighbors of a cell a = (a 1 , . . . , a d ) are the cells b = (b 1 , . . . , b d ) such that max i∈[d] |a i -b i | ≤ 1, this is the so-called Moore neighborhood (resp. Σ i∈[d] |a i -b i | ≤ 1, this is the von Neumann neighborhood);
• a one-way neighborhood3 : the neighbors of a cell a = (a 1 , . . . ,

a d ) are the cells b = (b 1 , . . . , b d ) such that b i ≥ a i , for each i ∈ [d], and max i∈[d] (b i -a i ) ≤ 1(resp. Σ i∈[d] (b i -a i ) ≤ 1).
A cellular automaton is called two-way or one-way according to its specified neighborhood. A d-dimensional cellular automaton runs within time T (n) if any of its computations stops within exactly T (n) -1 steps, for any input d-picture of side n. The most studied time bounded classes of picture languages are the following:

• the class of picture languages recognized by cellular automata in linear time, that means time O(n);

• the class of picture languages recognized by cellular automata in real time, that means the minimal time necessary for that the content of every cell of the input picture can be communicated to the reference cell 1 d = (1, . . . , 1): e.g., it is time n + 1 if the chosen neighborhood is one-way with the above-mentioned condition max i∈

[d] (b i -a i ) ≤ 1.
As the other computational models, cellular automata can be deterministic or nondeterministic. In this paper, we are interested in the nondeterministic case. While most relationships between the above complexity classes, linear/real time on one-way/two-way cellular automata, are open questions in the deterministic case (e.g., see [START_REF] Poupet | Cellular automata: Real-time equivalence between one-dimensional neighborhoods[END_REF] and the nice survey [START_REF] Terrier | Language Recognition by Cellular Automata[END_REF] that describes what is known in the deterministic case), the situation is much simpler and well-known in the nondeterministic case, as expressed by the following proposition given here without proof. So, the linear time complexity class of nondeterministic cellular automata is a very robust notion; in particular, as it is equal to the real time class, it is the minimal time complexity class that allows to synchronize, i.e. to communicate to a reference cell the content of each other cell.

Linear time of nondeterministic cellular automata of any dimension

For simplicity of notation, we only present formally the notion of one-way d-dimensional cellular automaton, instead of the more usual notion of two-way d-dimensional cellular automaton. There are some technicalities in our definition of the transition function of such an automaton. This is due to the need to distinguish the different possible positions of the pixels of a picture w.r.t. its border: the chosen one-way neighborhood of a cell x = (x 1 , . . . , x d ), that is the set of cells y = (y 1 , . . . , y d ) such that 0 ≤ y ix i ≤ 1 for each i ∈ [d], may be incomplete according to the position of the cell x w.r.t. the border of the picture. This is defined as follows.

Definition 4.3. (See Figure 1.) A pixel x = (x 1 , . . . , x d ) ∈ [n] d is in position a = (a 1 , . . . , a d ) ∈ {0, 1} d in a picture p : [n] d → Γ or in the domain [n] d if for all i ∈ [d] we have a i = 0 if x i = n and a i = 1 if x i < n.
We are going to define the transition function on a pixel x of a picture p according to some "neighborhood" denoted p a,x (it is a subpicture of p) whose domain, denoted by Dom a , depends on the position a of the pixel in the picture. We denote by neighb a (Γ) the set of all possible a-neighborhoods on an alphabet Γ, that is the set of functions ν : Dom a → Γ. Let us now define a computation.

(n) ∈ A T (n)-1 (p) of A on p such that p T (n) (1 d ) ∈ F. A d-language L on Σ is accepted, or recognized, by A in time T (n) if it
is the set of d-pictures p accepted by A in time T (n), i.e. such that there exists p ∈ A T (n)-1 (p) where n is the size of p and with p (1 d ) ∈ F.

If T (n) = cn + c , for some integers c, c , then L is said to be recognized in linear time and we write L ∈ NLIN d ca .

The time bound T (n) > n of the above definition is necessary and sufficient to allow the information of any pixel of p to be communicated to the pixel of minimal coordinates, 1 d . Remark 4.9. As stated in Proposition 4.2 above, the nondeterministic linear time class NLIN d ca is very robust, i.e. is not modified by many changes in the definition of the automaton or in its time bound. In particular, the constants c, c defining the bound T (n) = cn + c can be arbitrarily fixed, provided T (n) > n. For example, the class NLIN d ca does not change if we take the minimal time T (n) = n + 1, called real time.

A logical characterization of nondeterministic linear time for cellular automata

With Theorem 3.6, we have stated a logical characterization of REC, the class of recognizable picture languages. The four forthcoming sections (including the present one) are devoted to the second central issue of this paper: a logical characterization of NLIN ca , the linear time complexity class of nondeterministic cellular automata. To be precise, we will soon establish: By abuse of language, we will write "NLIN d ca = ESO(var d + 1) on d-coordinate structures" to mention the above equivalence.

There are many such logical characterizations of complexity classes, see e.g. [START_REF] Fagin | Generalized first-order spectra and polynomial-time recognizable sets[END_REF][START_REF] Grädel | Capturing complexity classes by fragments of second order logic[END_REF][START_REF] Lautemann | A logical characterisation of linear time on nondeterministic turing machines[END_REF], or the surveys [START_REF] Immerman | Descriptive complexity[END_REF][START_REF] Fagin | Finite-model theory-a personal perspective[END_REF]. In most cases, the right-to-left implication, i.e. the inclusion of the logically defined class in the complexity class, is easier than the converse one. This is due to the great flexibility of computational models, that allows to easily translate, in most cases, syntactic properties of the logic into bounds over computational resources. As a significant example, in the proof of Fagin's statement that ESO ⊆ NP [START_REF] Fagin | Generalized first-order spectra and polynomial-time recognizable sets[END_REF]:

• existential second-order quantifications relate to nondeterminism;

• universal first-order quantifications give rise to deterministic for loops;

• arities of relation symbols are interpreted in terms of the size of handled objects;

• in particular, arities of existentially quantified relation symbols determine the size of objects to be guessed, that is, somehow, the "amount" of nondeterminism involved in the computation.

Those correspondences hold even more tightly when computation resources are tighter : see for instance the proof of the inclusion SO(horn) ⊆ P by Grädel [START_REF] Grädel | Capturing complexity classes by fragments of second order logic[END_REF], or that of ESOF(var 1) ⊆ NLIN by the present authors [START_REF] Grandjean | First-order spectra with one variable[END_REF][START_REF] Grandjean | Graph properties checkable in linear time in the number of vertices[END_REF]. However, in either of those two cases some preliminary normalization result about the logic, actually SO(horn) ⊆ ESO(horn) and ESOF(var 1) ⊆ ESOF(∀ 1 , arity 1), respectively, appears as a crucial point of the proof; in either case, it is the condition to make logical formulas "handleable" for the computation model that has to evaluate them.

At the opposite of most cases, the right-to-left implication of Theorem 9.1, i.e. the inclusion ESO(var d + 1) ⊆ NLIN d ca , is far more difficult to demonstrate than the converse one: it is a very hard task to prove that an ESO(var d + 1)-sentence can be evaluated, over a d-coordinate structure taken as input, by a linear time cellular automaton. This is mainly due to the "local" behavior of cellular automata, which seems not adapted to the evaluation of an ESO(var d + 1)-formula over a d-picture. Indeed, such a formula possibly connects pixels of the picture that may be arbitrarily far away from each other; and dealing with pixels that do not belong to a same neighborhood is seemingly out of the ability of our computational device. As outlined above, the proof of the right-to-left implication of Theorem 9.1 compels us to normalize the logic under consideration, in such a way that the formulas to be evaluated are rewritten under a form that can be "handled" by a cellular automaton. This will be done in several steps. We will cope with these successive normalizations in the forthcoming sections. For now, let us establish the "easy part" of the theorem, with Proposition 4.10 below. ψ(x, t) is the conjunction ψ(x, t) = init(x, t) ∧ step(x, t) ∧ end(x, t) of three formulas whose intuitive meaning is the following.

• ∀x∀t init(x, t) describes the first configuration of A, i.e. at initial instant 1, that is the input picture p 1 = p;

• ∀x∀t step(x, t) describes the computation between the instants t and t + 1, for t ∈ [n -1], i.e. describes the (t + 1) th configuration p t+1 from the t th one p t , i.e. says p t+1 ∈ A(p t ) ;

• ∀x∀t end(x, t) expresses that the n th configuration p n leads to a (last) (n + 1) th configuration p n+1 ∈ A(p n ) which is accepting, i.e. with an accepting state in cell

1 d : p n+1 (1 d ) ∈ F.
Let us give explicitly these three formulas. The first one is straightforward:

init(x, t) ≡ min(t) →          s∈Σ R s (x, t) ↔ Q s (x) ∧ s∈Γ\Σ ¬R s (x, t)         
The second formula is

step(x, t) ≡ a∈{0,1} d ν∈neighb a (Γ)          ¬max(t) ∧ P a (x) ∧ b∈Dom a R ν(b) (x + b, t) → s∈δ a (ν) R s (x, succ(t))          Here,
denotes the exclusive disjunction. Furthermore:

• For x ∈ [n] d and a = (a 1 , . . . , a d ) ∈ {0, 1} d , the formula P a (x) claims that the pixel x is in position a.

Namely:

P a (x) ≡ i∈[d] (¬ i )max(x i ), where (¬ i ) is ¬ if a i = 1
, and nothing otherwise.

• For b = (b 1 , . . . , b d ) ∈ {0, 1} d ,
x + b abbreviates the tuple of terms (θ 1 , . . . , θ d ) where, for each i, the term θ i is x i if b i = 0, and succ(x i ) otherwise.

It is easy to verify that the formula ∀x step(x, t) means p t+1 ∈ A(p t ). Finally, here is the last formula :

end(x, t) ≡          max(t) ∧ i∈[d] min(x i )          →                min(t) → ν∈N 0 R ν(0 d ) (x, t) ∧ ¬min(t) → ν∈N 1 b∈{0,1} d R ν(b) (x + b, t)               
In this formula, the sets N 0 and N 1 are defined by:

N 0 = {ν ∈ neighb 0 d (Γ) : δ 0 d (ν) ∩ F ∅}; N 1 = {ν ∈ neighb 1 d (Γ) : δ 1 d (ν) ∩ F ∅}.
Let us explain the meaning of the formula end(x, t) which is rather technical due to the need to distinguish two cases according to the size n of the input picture: if n = 1 then the position of the reference pixel 1 d is 0 d ; otherwise, i.e. if n > 1, it is 1 d . Under the hypothesis max(t), the condition min(t) (resp. ¬min(t)) is equivalent to n = 1 (resp. n > 1). In either case, the disjunction ν∈N 0 (resp. Let us conclude this section with three remarks.

Remark 4.11. The proof of Proposition 4.10 is almost straightforward because, by Proposition 4.2, it is sufficient that our logic can define an accepting computation of a one-way cellular d-dimensional cellular automaton of real time n + 1, which is, up to 1, the side n of the input picture. In contrast, proving directly that an accepting computation of linear time O(n) of a (more natural) two-way d-dimensional cellular automaton can be defined in ESO(var d + 1) would be possible but much more technical. Therefore, similarly to normalizations of logically defined classes, the robustness property expressed by Proposition 4.2 can be regarded as a "normalization" of the linear time complexity class of nondeterministic cellular automata. Remark 4.12. One observes that the formula constructed in the proof of Proposition 4.10 belongs to the logic ESO(∀ d+1 , arity d + 1) that is seemingly more restricted than ESO(var d + 1). Actually, we will prove in the next section that these two logics coincide on coordinate d-structures.

Remark 4.13. The respective roles of time and space are seemingly dissymmetric in the sentence we have just constructed. However, the proof and the meaning of the converse implication coord d (L) ∈ ESO(var d + 1) ⇒ L ∈ NLIN d ca that will be presented in the next sections show that actually the d dimensions of space are -or can be made -symmetrical w.r.t. time.

A first normalization of ESO sentences with d variables on coordinate structures

From now on, we aim at establishing the converse of Proposition 4.10. It amounts to prove that for each ESO(var d)-formula, there exists a d-automaton able to evaluate this formula on any (d -1)-coordinate structure in linear time. As mentioned before Proposition 4.10, this result necessitates a preliminary normalization of the logic ESO(var d). Indeed, the main feature of a cellular automaton is its ability to perform parallel computations on the pixels of an input picture, as far as the data to be considered when dealing with a pixel are locally supplied, that is, can be collected in a neighborhood of the pixel. But it appears that the properties encoded by an ESO(var d)-formula Φ do not fulfill this last prerequisite. For instance, assume that Φ is the ESO(var 2)-formula ∀x, y : U(x, y) ↔ U(y, x). In order to evaluate Φ on a picture p, A has to check, for every couple (x, y), whether pixels of coordinates (x, y) and (y, x) have the same "color" with respect to U. That is, A has to check a property that relates pixels far from each other. And such a test seems to exceed the capacity of A.

It should now be clear that making this evaluation possible means preventing that the cellular automaton has to check constraints connecting arbitrarily distant pixels. With this purpose, we must initially normalize the logic ESO(var d + 1), so as to force its formulas "to speak locally", that is, to assert local properties, which bring into play only adjacent cells, or at least pixels at a constant distance, namely, pixels belonging to the neighborhood of a given pixel x.

We now go into this normalization task. The present section is dedicated to the proof of the following statement:

Proof.

The proof amounts to establishing that each ESO(var d)-formula is equivalent to an ESO(∀ d )formula on any coordinate structure. Clearly, we can assume without loss of generality that the initial ESO(var d)-formula is first-order. So let's consider a first-order formula ϕ written with at most d variables.

We first aim at writing ϕ under prenex form, without introducing new first-order variables. This entails introducing second-order variables existentially quantified. More precisely, the rewriting procedure is based on a depth-first traversal of the tree decomposition of ϕ. Each internal node of this tree corresponds to some subformula of ϕ of arity k -say θ(x 1 , . . . , x k ) -, and gives rise to a new relation symbol R θ of the same arity. This relation is forced to encode the set {x s.t. θ(x)} via a formula def θ (R θ ) defined as follows:

• If θ ≡ Qyθ (x, y) where Q is a quantifier, then def θ (R θ ) ≡ ∀x : R θ (x) ↔ Qyθ (x, y) • If θ ≡ θ (x) • θ"(x) for some connective •, then def θ (R θ ) ≡ ∀x : R θ (x) ↔ (θ (x) • θ"(x)).
If θ has no free variables, the relation symbol R θ is choosen with arity 1 and its definition is written either ∀x : R θ (x) ↔ Qyθ(y) or ∀x : R θ (x) ↔ (θ • θ"), according to the form of θ. Here, x is any variable of ϕ distinct from y. Each time a node θ(x) has been visited, the corresponding R θ and def θ are generated and ϕ is updated by the substitution θ(x) R θ (x). Then, the procedure is run recursively on the formula so obtained.

Let us illustrate this procedure by running it on the first-order formula with three variables:

ϕ ≡ ∃x ( ∀y∃z U(x, y, z) ∨ ∃y D(x, y) ) → ∀y ( D(y, y) ∨ ∃x U(x, y, x) ) .

We merely display the definition formulas generated by the procedure, along with the relation symbols R 1 , . . . , R 9 corresponding to the nine internal nodes of ϕ. The successive updates of ϕ are implicit.

def 1 (R 1 ) ≡ ∀x, y : R 1 (x, y) ↔ ∃z U(x, y, z)

def 2 (R 2 ) ≡ ∀x : R 2 (x) ↔ ∀y R 1 (x, y) def 3 (R 3 ) ≡ ∀x : R 3 (x) ↔ ∃y D(x, y) def 4 (R 4 ) ≡ ∀x : R 4 (x) ↔ (R 2 (x) ∨ R 3 (x)) def 5 (
↔ (R 5 (x) → R 8 (x))
Now, our initial formula can be rewritten:

ϕ ≡ ∃R 1 , . . . , R 9 :         1≤i≤9 def i (R i )         ∧ ∀x R 9 (x). (8)
Notice that for each i, either def i is prenex and universal, or it has the form ∀u : α(u) ↔ Qvβ(u, v). It is easily seen that this last form is equivalent to the conjunction:

∀uQv α(u) → β(u, v) ∧ ∀uQ * v β(u, v) → α(u) ,
where Q * is ∀ if Q is ∃ and vice versa. Therefore, following Equation [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF], ϕ can now be written as a conjunction of prenex formulas, each of which involves no more than three variables and has a quantifier prefix of the shape ∀x or ∀x∃y. In order to write this conjunction under prenex form without adding new firstorder variables, we have to "replace" existential quantifiers by universal ones. Afterward ϕ, as a conjunction of formulas of the type ∀x, y, z θ, could be written under the requisite shape. We show below how to deal with this specific formula. The general case is strictly similar.

To get rid of existential quantifiers occuring in (some of) the def i 's, we will invoke the arithmetical symbols of the signature of ϕ. Remember that the conjuncts that are not still universal all have the form ∀x∃yθ(x, y), where x and y are tuples of first-order variables of respective arities k and 1. The predefined arithmetics included in coordinate signatures allow to defining, for any such conjonct, a relation of arity k + 1 that witnesses the existence of some y fulfilling θ(x, y) for a given x. This idea is completed as follows: Let W be a new (k + 1)-ary relation symbol associated with ∃yθ(x, y). We want the assertion W(x, y) to signify that there exists z ≤ y such that θ(x, z) holds. This interpretation is achieved thanks to the following formula:

∀x∀y min(y) → (W(x, y) ↔ θ(x, y)) ∧ W(x, succ(y)) ↔ (θ(x, succ(y)) ∨ W(x, y))
We denote by W = witness(∃yθ) this last formula. When it is satisfied, the assertion ∀x∃yθ(x, y) is clearly equivalent to ∀x∀y : max(y) → W(x, y).

For instance, the above formula def 1 (R 1 ) gives rise to the non-universal formula def 1 1 (R 1 ) ≡ ∀x, y∃z : R 1 (x, y) → U(x, y, z). This shoud be managed as follows: A ternary relation symbol W 1 is introduced (i.e., existentially quantified) and compelled to fit its intended interpretation via the formula: W 1 = witness(δ 1 ), where δ 1 ≡ ∃z : R 1 (x, y) → U(x, y, z). Afterwards, the formula def 1 1 (R 1 ) is replaced by ∀x, y, z : max(z) → W 1 (x, y, z). When this task has been achieved for each non universal formula def i , the formula displayed in (8) becomes:

∃(R i ) i∈I ∃(W j ) j∈J :          j∈J W j = witness(δ j )          ∧        i∈I def i        ∧ ∀x R (x).
Here, I = {1, . . . , 9}, J = {1, 3, 5, 6} (the j ∈ J correspond to formulas def j that are non-universal), = 9, and δ j is the existential part of the (old) formula def j . Clearly, this formula can be written in ESO(∀ d ) for d = 3.

Arity vs number of first-order variables

We prove here a normalization of the logic ESO(∀ d ), similar to that of Proposition 2.8. This proof involves the following easy fact: Fact 5.3. Suppose we are given a family of functions ( f i : X i → Y) i∈I and a family of relations (R i ⊆ X i ) i∈I , indexed by the same finite set I. The following assertions are equivalent:

(i) ∀i, j ∈ I, ∀x ∈ X i , ∀y ∈ X j : f i (x) = f j (y) ⇒ R i (x) = R j (y) ; (ii) ∃R ⊆ Y such that ∀i ∈ I, ∀x ∈ Y: R i (x) = R( f i (x)). Proof. (ii) ⇒ (i) is clear. For the converse implication, we define R on each set f i X i = { f i (x), x ∈ X i } by: ∀x ∈ X i , R( f i (x)) = R i (x)
. Hyptothesis (i) guarantees the coherence of this definition. To complete it, we set R(x) = 0 for every x ∈ Y \ i∈I f i X i . The relation R thus defined clearly witnesses to condition (ii). Proof. Let Φ ∈ ESO(∀ d ). To fix ideas, let us assume that Φ has the very simple shape:

Φ ≡ ∃R∀x 1 , . . . , x d ϕ(x, R), ( 9
)
where R is a single k-ary relation symbol for some k > d, and ϕ is a quantifier free formula. The formula to be built must have the form:

Ψ ≡ ∃ρ∀x 1 , . . . , x d ψ(x, ρ),
where ρ is a tuple of d-ary relation symbols and ψ is quantifier free.

The substitution of d-ary symbols for R rests in the limitation of the number of first-order variables in Φ: each atomic formula involving R has the form R(t 1 , . . . , t k ) where the t i 's are terms built on x 1 , . . . , x d . Therefore, although R is k-ary, in each of its occurrences it behaves as a d-ary symbol, dealing with the sole variables x 1 , . . . , x d . Hence, the key is to create a d-ary symbol for each occurrence of R in Φ or, more precisely, for each k-tuple of terms (t 1 , . . . , t k ) involved in a R-atomic formula.

More formally, let us denote by T(Φ) the set of terms occuring in Φ, and by T R (Φ) the set of tuples of terms involved in a R-atomic subformula of Φ. That is, each element of T R (Φ) is a k-tuple

t(x) = (t 1 (x 1 , . . . , x d ), . . . , t k (x 1 , . . . , x d )) ∈ T(Φ) k
such that the formula R(t(x)) appears in Φ. For each t(x) ∈ T R (Φ), consider a new d-ary relation symbol R t(x) . Now, consider a σ-stucture S of domain [n], and denote by S , R some expansion of S to σ ∪ {R}. (That is, we denote by R both the relationnal symbol and its interpretation on [n].) Furthermore, fix the S -interpretation of each R t(x) , for t(x) ∈ T R (Φ), by

∀x ∈ [n] d : R t(x) (x) = R(t(x)), (10)
and denote by R the tuple (R t(x) ) t(x)∈T R (Φ) thus defined. Then clearly:

S , R | = ∀xϕ(x, R) ⇔ S , R | = ∀x φ(x, R, σ), ( 11
)
where φ is obtained from ϕ by substituing the formula R t(x) (x) for each occurrence of the formula R(t(x)).

Before continuing with this proof, let's illustrate the previous definitions with a simple example.

Example. Consider the ESO(∀ 2 )-formula: ∃R∀x, yϕ(x, y, R), where

ϕ ≡ R(x, y, x) ∧ ¬R(y, x, y). ( 12
)
According to the notations used so far, we have:

d = 2, k = 3, T(Φ) = {x, y} and T R (Φ) = {(x, y, x), (y, x, y)}.
The binary relation symbols associated to the tuples of terms in T R (Φ) are denoted R (x,y,x) and R (y,x,y) . The formula φ obtained from ϕ, following [START_REF] Fagin | Generalized first-order spectra and polynomial-time recognizable sets[END_REF], is written:

φ ≡ R (x,y,x) (x, y) ∧ ¬R (y,x,y) (x, y).
If, for any interpretation of R on [n], we fix the interpretations of R (x,y,x) and R (y,x,y) as in [START_REF] Elgot | Decision problem of finite automata design and related arithmetics[END_REF]:

∀a, b < n : R (x,y,x) (a, b) = R(a, b, a) and R (y,x,y) (a, b) = R(b, a, b), then it is easily seen that S , R | = ∀x, y ϕ(x, y, R, σ) iff S , R | = ∀x, y φ(x, y, R (x,y,x) , R (y,x,y) , σ).
Let's come back to the proof of Proposition 5.4. Equations ( 10) and ( 11) yield:

S | = ∃R∀x ϕ(x, R) ⇒ S | = ∃R∀x φ(x, R, σ), ( 13
)
where R is a tuple of d-ary relation symbols indexed by T R (Φ), say (R t ) t∈T R (Φ) . Unfortunately, the converse implication does not hold in general. For instance, one can check, with the formula ϕ displayed in [START_REF] Fagin | Monadic generalized spectra[END_REF], that the formula ∃R (x,y,x) ∃R (y,x,y) ∀x∀y φ has a model, while ∃R∀x∀y ϕ doesn't have. To get the right-toleft implication in [START_REF] Fagin | A spectrum hierarchy[END_REF], we have to strengthen the hypothesis with some assertion that compels the tuple (R t ) t∈T R (Φ) to be, in some sense, the d-ary representation of some k-ary relation. All in all, we confront the following question: Given a σ-structure S , a set T ⊂ T(Φ) k and a family (R t ) t∈T of d-ary relations over the domain [n] of S , what are the conditions on (R t ) t∈T that ensure

∃R ⊆ [n] k such that ∀t ∈ T, ∀a ∈ [n] d : R t (a) = R(t(a)) (14)
Each k-tuple t ∈ T defines a function from [n] d to [n] k , via the process of interpretation of terms. (For instance, the triple of terms t = (succ 3 x, x, succ 2 y) maps each couple (a, b) 3 , where + is the addition modulo n.) Therefore, if in the statement of Fact 5.3 we set:

∈ [n] 2 onto the triple (a + 3, a, b + 2) ∈ [n]
X i = [n] d for each i, Y = [n] k and ( f i ) i∈I = (t) t∈T ,
we get the equivalence of ( 14) with the following assertion:

∀t, t ∈ T, ∀a, a ∈ [n] d : t(a) = t (a ) ⇒ R t (a) = R t (a ),
which is translated into the logical formula:

t,t ∈T ∀x, x : t(x) = t (x ) → R t (x) ↔ R t (x ) , (15)
where x, x are d-tuples of first-order variables.

In order to express condition [START_REF] Fagin | Comparing the power of monadic NP games[END_REF] in the required formalism, it remains to reduce the number of quantifiers (remember our logic allows only d universal first-order quantifiers). Since the conjunction and the universal quantification commute, we just have to tackle the case of a single conjunct ∀x, x :

t(x) = t (x ) → R t (x) ↔ R t (x ) . ( 16
)
To process, we invoke the specificity of coordinate encodings, which has not been mentioned so far in our reasoning. Since succ is the only function symbol in the signature of coordinate structures, all the terms under consideration have the form succ i (u) for some i ∈ N and some first-order variable u. Hence, the equality t(x) = t (x ) is a conjunction i≤k θ i of k atomic formulas of the type succ a (x) = succ b (y), with x ∈ x, y ∈ x and a, b ≥ 0. Thus the formula displayed in ( 16) can be written as:

∀x, x : i≤k θ i → R t (x) ↔ R t (x ) . ( 17
)
Since the successor function is cyclic, the assertion succ a (x) = succ b (y) is equivalent to x = succ b-a (y) if a ≤ b, and to y = succ a-b (x) if a ≥ b. Using this fact, we can eliminate some variables from formula [START_REF]STACS 2001, 18th Annual Symposium on Theoretical Aspects of Computer Science[END_REF].

For instance, assume that θ 1 ≡ succ a (x) = succ b (y) with x ∈ x, y ∈ x and a ≤ b. Then, ( 17) is equivalent to ∀x, x ψ, where ψ is the formula obtained from ( 17) by suppressing θ 1 from the conjunction i≤k θ i (which therefore becomes 2≤i≤k θ i ) and by replacing, in the resulting formula, each occurence of x by the term succ b-a (y). Notice that the formula thus obtained has the same form as [START_REF]STACS 2001, 18th Annual Symposium on Theoretical Aspects of Computer Science[END_REF]. Hence, we can iteratively repeat this procedure until there is no more equality of type succ a (x) = succ b (y) in the conjunction θ i (but it may remain some equalities of the form succ a (x) = succ b (x), with x ∈ x ∪ x ).

Example. In order to illustrate this procedure, assume the arity of R t and R t (and hence, that of x and x ) is 2, and consider the two triples of terms t = (succ 5 x, y, succ 2 y) and t = (succ 2 y, succ 3 y, succ 5 x). Suppose we are given the following formula:

Φ ≡ ∀x, y, x , y : t(x, y) = t (x , y ) → R t (x, y) ↔ R t (x , y )
in which we want to eliminate as much first-order variables as possible. We first write Φ as: ∀x, y, x , y :

         succ 5 x = succ 2 y ∧ succ 6 y = succ 2 x ∧ succ 2 x = succ 5 y          → R t (x, y) ↔ R t (x , y ) .
Starting the substitution described above, we suppress the first equality in the conjunction and replace each occurence of y by succ 5-2 x = succ 3 x. Thus we get the equivalent formula: ∀x, y, x , y :

succ 6 y = succ 2 x ∧ succ 2 x = succ 8 x → R t (x, y) ↔ R t (x , succ 3 x) ,
An iteration of the process provides the formula: ∀x, y, x , y : succ 2 x = succ 8 x → R t (x, y) ↔ R t (succ 4 y, succ 3 x) , which can be more simply writen: ∀x, y, x , y : x = succ 6 x → R t (x, y) ↔ R t (succ 4 y, succ 3 x) .

Afterward, we can obviously get rid of the quantifications over variables that do not appear any more in the matrix of the formula. This finally gives the following formula, equivalent to Φ on coordinate structures: ∀x, y : x = succ 6 x → R t (x, y) ↔ R t (succ 4 y, succ 3 x) .

Here, the number of first-order variables agrees with the arity of R t and R t .

To conclude, it remains to make the following three remarks:

(1) In the previous example, the number of first-order variables after the elimination procedure equals the arity of R t . This is not a coincidence: In all cases, the procedure provides us with a universal fist-order formula whose number of variable is at most d, the arity of R t and R t . This is because the procedure reduces to a single variable each set of variables in x ∪ x that are connected by equalities of the form succ a x = succ b y, via the initial conjunction i≤k θ i . For instance, if this conjunction initially contains the equalities succ 2 x = succ 3 x , succ 4 x = succ 2 y and succ 3 y = succ 5 y , then the four variables x, y, x , y will reduce to one during the procedure. More precisely: let us consider the bipartite graph G build on the set of variables x ∪ x , by linking two variables u ∈ x, v ∈ x when there is an equality succ a u = succ b v in the conjunction i≤k θ i . It is easily seen that the elimination procedure reduces to one variable all variables lying on a same connected component of G. Hence, the number of variables left by the procedure is bounded by the number of connected components of G. Since each connected component contains at least one variable of x (for G is bipartite between x and x ), this number of connected components is itself bounded by the cardinality of x, which is d.

(2) Using the strategy described above, each conjunct of ( 15) can be rewritten with only d universal first-order variables. These rewriting results in a new first-order formula Rep k d , equivalent to Condition (15) (which ensures that the relations R t , t ∈ T R (Φ), constitute a "d-ary representation of a k-ary relation") and has a universal prefix ∀x 1 , . . . , x d of length d. Clearly, the ESO(∀ d , arity k)-formula initially considered in (9), Φ ≡ ∃R∀x 1 , . . . , x d ϕ(x, R), is equivalent on picture encodings to the following ESO(∀ d , arity d)-formula:

∃(R t ) t∈T R (Φ) : Rep k d (R t ) t∈T R (Φ) ∧ ∀x φ x, (R t ) t∈T R (Φ)
, where φ is obtained from ϕ by replacing each R(t(x)) by R t (x).

(3) Finally, we let the reader to verify that this procedure can be extended to any number of relation symbols existentially quantified in Φ.

Theorem 5.1 immediately proceeds from Propositions 5.2 and 5.4 above. We will remember that: Over coordinate structures, each ESO(var d)-formula can be written:

Φ ≡ ∃R∀x ±                min(succ i (x)), max(succ i (x)), succ i (x) = succ j (y), Q a (succ i 1 (x j 1 ), . . . , succ i p (x j p ), R(succ i 1 (x j 1 ), . . . , succ i p (x j p )               
where Q a ∈ σ, R ∈ R and x, y and the x i 's are all components of x.

(

) 18
Remark 5.5. Notice that Theorem 5.1 and, more generally, the results of this sections hold with exactly the same proof whatever the arity of the input relation symbols (Q s ) s∈Σ is. This won't be the case in some of the forthcoming normalization results, which will heavily depend on the arity of the input structure.

6. "Sorting" the logic: some motivations and a preliminary example

Motivations

When introducing Section 5 (see p. 24), we mentioned a particular source of "non-locality" in the logic ESO(var d), due to possible occurences in a given ESO(var d)-formula ϕ, of both subformulas R(x, y) and R(y, x), for some relation symbol R. Indeed, evaluating such a ϕ brings about comparing the contents of the two non-adjacent pixels of respective coordinates (x, y) and (y, x). For a cellular automaton, this situation appears as a major obstacle for achieving the evaluation of ϕ. Of course, this non-local feature persists in ESO(∀ d , arity d)-formulas. That's why we now engage in a normalization of ESO(∀ d , arity d) into an equivalent logic in which such failure to locality is prevented.

Let us detail our goal. We deal with ESO(∀ d , arity d)-formulas conceived to "talk" about (d -1)-pictures. Such formulas involve two kinds of relation symbols: the "guessed" ones (those that are existentially quantified) of arity d, and the "input" ones (which are part of the signature), of arity d -1. In both cases, we demand that an atomic subformula R(t 1 , . . . , t k ), where k is either d or d -1 according to the arity of R and where the t i 's are terms build on the first-order variables x 1 , . . . , x d , fulfill the sorting condition: for each 1 ≤ i ≤ k, the term t i is formed with the variable x i . That is, the variables x 1 , . . . , x d always occur in the same order in atomic subformulas.

There is a less important cause of non-locality of ESO(∀ d , arity d)-formulas, owing to terms that involve iteration of the successor function. For instance, a cellular automaton that attempt to evaluate a formula containing the subformulas R(x, y) and R(x, succ 3 (y)), has to check the pixels of coordinate (x, y) and (x, succ 3 (y)), which are not adjacent. Actually, this apparent difficulty could be circumvent, since the cellular automaton could carry on this check in constant time. But we choose to include this last characteristic in the objectives of our normalization, because it can be achieved with minor cost, and because it will lighten the proof of Proposition 9.2, which is -we must keep that in mind -the aim of this whole normalization process.

The reader should be now in a position to get the motivation of the technical Definition 6.2 below, which formalizes the requirements that an ESO(∀ d , arity d)-formula must fulfill to pretend to "locality". Before coming to that definition, let us introduce a notation that describes pixel which differs from a given d-pixel x by one unity in one dimension: Definition 6.1. Let n, d > 0 and x = (x 1 , . . . , x d ) ∈ [n] d . For any i ∈ {1, . . . , d}, x (i) denotes the tuple obtained from x by replacing its i th component by its own successor. That is:

x (i) = (x 1 , . . . , x i-1 , succ(x i ), x i+1 , . . . , x d ).
We now define a sorted version of ESO(∀ d , arity d). It has very strict requirements on tuples of first-order variables involved in the atoms of the formulas: they must represent pixels that differ by at most one in at most one dimension. That is:

• their components are in the same order;

• there is at most one occurrence of succ in each atom.

These requirements (and a little more) are formalized below. Definition 6.2. Let k, d be two integers such that d ≥ k ≥ 1. A sentence over coordinate structures for kpictures is in ESO(∀ d , arity d, sorted ) if it is of the form ∃R∀xψ(x) where 1. R is a list of relation symbols of arity d; 2. ψ is a quantifier-free formula whose list of first-order variables is x = (x 1 , . . . , x d );

3. each atom of ψ is of one of the following forms:

(i) Q s (x 1 , . . . , x k ), for s ∈ Σ, (ii) R(x) or R(x (i) ) where R ∈ R and i ∈ [d], (iii) min(x i ) or max(x i ), for i ∈ [d].
(Remember that beside arithmetic symbols, the tuple of k-ary relations (Q s ) s∈Σ constitutes the core of the signature in the coordinate representation of a k-picture -see Definition 2.3.)

In the two following sections, we prove the normalization ESO(∀ d , arity d) = ESO(∀ d , arity d, sorted ) for (d -1)-pictures (i.e. for k = d -1). In Proposition 7.7, we'll deal with conditions (3ii) and (3iii) of Definition 6.2. At this point, we'll get a normalization of ESO(∀ d , arity d) into the so-called "half-sorted logic", denoted by ESO(∀ d , arity d, half-sorted ). It will remain to manage with the input relation symbols. This will be done in Section 8, where we tackle Condition (3i).

To facilitate the presentation of the forthcomming results, let's first introduce some notations about tuples and permutations. (ii) We say that x is increasing, and we write x↑, when (iv) If α ∈ S(d) and x is a d-tuple, we denote by x α the d-tuple whose i th component is the α th i component of x. That is: if x = (x 1 , . . . , x d ), then x α = (x α 1 , . . . , x α d ). It is less ambiguous to define x α by the assertion: for any i ∈ {1, . . . , d},

[x] 1 ≤ • • • ≤ [x] d .
[x α ] i = [x] α(i) .
Thus, if β also belongs to S(d), we get

[(x α ) β ] i = [x α ] β(i) = [x] αβ(i)
. Whence the identity:

(x α ) β = x αβ .
In particular, (x α ) α -1 = x. In coherence with Definition 6.1, the arrangement of x (i) according to the permutation α is denoted by (x (i) ) α .

Example. Take x = (5, 3, 7, 2) in [START_REF] Ebbinghaus | Finite Model Theory[END_REF] 4 and α = 4213, β = 1432 in S(4). Then x α = (2, 3, 5, 7) is increasing while x β = (5, 2, 7, 3) is not. Besides, x (3) = (5, 3, 8, 2) while (x α ) (3) = (2, 3, 6, 7) and (x (3) ) α = (2, 3, 5, 8) = (x α ) (4) .

The two upcoming sections are devoted to the normalization ESO(var d) = ESO(∀ d , arity d, sorted ) on coordinate structures of dimension d -1. This result is stated in Theorem 8.7. Because of the previous steps of normalization (Propositions 5.2 and 5.4), it amounts to proving that ESO(∀ d , arity d) = ESO(∀ d , arity d, sorted ) on (d -1)-coordinate structures. Remember this essentially means that R-atoms of an ESO(∀ d , arity d)formula can be compelled to fit the form R(x 1 , . . . , x k ) if R is in the signature, or R(x) (resp. R(x (i) )) if R is existentially quantified (see Definition 6.2). It will appear that the technics involved in this normalizations of R-atoms are quite different, depending on whether R is part of the input or not. Hence, we'll prove this result in two steps, matching the two above mentionned cases:

In Section 7, we state a weaker form of the inclusion ESO(∀ d , arity d) ⊆ ESO(∀ d , arity d, sorted ). There, we relax one of the constraints on the target logic. Namely, we replace constraint (3i) of Definition 6.2 by the more liberal requisit that each Q s -atom has the form Q s (x ι 1 , . . . , x ι k ), where ι is an injection from [k] into [d]. This gives rise to the definition of the so-called half-sorted logic: on coordinate pictures of dimension d -1. We chose in both case to introduce the proofs with a simple example illustrating some important features.

An example

Let's now illustrate the first step of the normalization. We want to prove that each formula Φ in ESO(∀ d , arity d) can be written in ESO(∀ d , arity d, half-sorted ) on coordinate structures. Assume d = 2 and Φ is a formula in ESO(∀ 2 , arity 2) that has the simple form Φ = ∃R∀x∀yψ(x, y), where R is a binary relation symbol and ψ is a quantifier-free formula in which the R-atoms have the following forms:

(1) R(x, y);

(2) R(succ(x), y);

(3) R(x, succ(y)); (4) R(y, x). R(x, y) R(succ(x), y) R(x, succ(y)) R(y, x) (We don't evoke the form of others atoms since we focus here on the treatment of the guessed relation R.)

ψ < (x, y) R 1 (x, y) R 1 (succ(x), y) R 1 (x, succ(y)) R 2 (x, y) ψ = (x, y) R 1 (x, y) R 2 (x, succ(y)) R 1 (x, succ(y)) R 1 (x, y) ψ > (x, y) R 2 (y, x) R 2 (y, succ(x)) R 2 (succ(y), x) R 1 (y, x)
For given x and y, the pixels (x, y), (succ(x), y) and (x, succ(y)) are adjacent, while (y, x) is arbitrarily far from the former, since it is symmetric of (x, y) with respect to the diagonal x = y. Hence we have to eliminate subformulas ot type [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]. The intuitive idea is to "fold" the picture along this diagonal. Then R is represented by two "half relations" R 1 and R 2 , that are superposed in the half square x ≤ y above the diagonal.

Thus, R 1 and R 2 are binary relations whose intuitive meaning is the following: for points (x, y) such that x ≤ y, one has R 1 (x, y) = R(x, y) and R 2 (x, y) = R(y, x). By this transformation, both informations R(x, y) and R(y, x), dealing with symmetric pixels (x, y) and (y, x), are accessible by checking the validity of the assertions R 1 (x, y) and R 2 (x, y) on the sole pixel (x, y), where x ≤ y. The case y ≤ x is similar. This solves the problem of neighborhood.

Formaly, the sentence Φ = ∃R∀x∀yψ(x, y) is normalized as follows. Let coherent(x, y) denote the formula x = y → (R 1 (x, y) ↔ R 2 (x, y)) whose universal closure ensures the coherence of R 1 and R 2 on the common part of R they both represent, that is the diagonal x = y. Using R 1 and R 2 , it is not difficult to construct a formula

ψ (x, y) = coherent(x, y) ∧           x < y → ψ < (x, y) ∧ x = y → ψ = (x, y) ∧ x > y → ψ > (x, y)          
such that the sentence Φ = ∃R 1 , R 2 ∀x, y ψ (x, y), which belongs to ESO(∀ 2 , arity 2), is equivalent to Φ. Let us describe and justify its precise form and meaning.

The formulas ψ < (x, y), ψ = (x, y) and ψ > (x, y) are obtained from formula ψ(x, y) by substitution of R 1 -or R 2 -atoms for R-atoms, according to the cases described in Table 1. It is easy to check that each replacement is correct according to its case. For instance, it is justified to replace each atom of the form R(x, succ(y)) in ψ by R 2 (succ(y), x) when x > y (in order to obtain the formula ψ > (x, y)), because when x > y we get succ(y) ≤ x and hence the equivalence R(x, succ(y)) = R 2 (succ(y), x) holds, by definition of R 2 .

Notice that the variables x, y always occur in this order in each R 1 -or R 2 -atom of the formulas ψ < and ψ = (see Table 1). At the opposite, they always occur in the reverse order y, x in the formula ψ > (x, y). This is not a problem because, by symmetry, the roles of x and y can be exchanged and the universal closure ∀x, y : x > y → ψ > (x, y) is trivially equivalent to ∀x, y : y > x → ψ > (y, x). So, the above sentence Φ -and hence, the original sentence Φ -is equivalent to the sentence denoted Φ" obtained by replacing in Φ the subformula x > y → ψ > (x, y) by y > x → ψ > (y, x). By construction, relation symbols R 1 and R 2 only occur in Φ within atoms of the three required "sorted" forms: R i (x, y), R i (succ(x), y) or R i (x, succ(y)).

Finally, notice that the resulting sentence involves equalities and inequalities although it shoud not be the case, according to Definition 6.4. We will see how to fix this point in the next section, when dealing with the general case.

Sorting guessed relations

For the general case, the steps of the proof are similar to those presented above, but the notations and details of the proof are more involved. Let us succinctly describe the ESO relations of arity d to be introduced in the main normalization step, and corresponding to the relations R 1 and R 2 defined in Subsection 6. Then, we introduce a partition of the domain [n] d into subdomains, similar to the partition of [n] 2 into the three subsets of equation x < y, x = y, x > y, described in Subsection 6.2. According to the case (i.e., to the subdomain of the partition), this allows to replace each R-atom in Φ by an atom of the sorted form R α (x) or R α (x (i) ), where x = (x 1 , . . . , x d ) and 1 ≤ i ≤ d (remember x (i) is the tuple x where x i is replaced by succ(x i ) -see Definition 6.1). Finally, the equalities are eliminated in order to obtain a sentence that fully fit the syntactical restrictions of ESO(∀ d , arity d, half-sorted ). Proof. The proof of (a) is quite immediate and we just illustrate it with an example. Assume that Φ involves the P-atom P(succ 2 x 1 , x 2 , succ x 1 , succ 3 x 2 ) for some relation symbol P. Then clearly Φ is equivalent, on picture-structures, to:

∃R∃A∀x : φ(x, R, A) ∧ (x 1 = succ x 3 ∧ x 4 = succ 3 x 2 ) → (A(x 2 , x 3 ) ↔ P(x 1 , x 2 , x 3 , x 4 ))
where φ is obtained from ϕ by substituting the formula A(x 2 , succ(x 1 )) for each occurrence of the atom P(succ 2 x 1 , x 2 , succ x 1 , succ 3 x 2 ).

In order to prove (b), assume for simplicity that R reduces to a single relational symbol R of arity p < d. The idea is to replace R by a d-ary relation symbol R with dp dummy arguments. Clearly, Φ is equivalent to the formula:

∃R ∀x : φ ∧ p<i≤d R (x 1 , . . . , x i , . . . , x d ) ↔ R (x 1 , . . . , succ(x i ), . . . , x d ).
Here, φ is obtained from ϕ by replacing each atomic subformula R(t 1 , . . . , t p ) by R (t 1 , . . . , t p , x i 1 , . . . , x i d-p ), where x i 1 , . . . , x i d-p is the complete list of distinct variables among x that do not occur in t 1 , . . . , t p . (Remember that I(k, d) is the set of injections from {1, . . . , k} into {1, . . . , d} -see Definition 6.3(iii).) Fact 7.3. On coordinate structures, any formula Φ = ∃R∀xϕ(x, R) ∈ ESO(∀ d , arity d) can be written in such a way that each R-atom of ϕ, with R ∈ R, has one of the two forms: R(x (i) ) or R(x α ), where α ∈ S(d).

Proof. We prove the result for d = 3. The general case is similar. Let be the maximal value of an i ∈ N such that succ i (x) occurs in Φ, for any x ∈ x. For each R ∈ R, we introduce new d-ary relation symbols R i, j,k for every i, j, k ≤ . We want to force the following interpretations of the R i, j,k 's:

R i, j,k (u 1 , u 2 , u 3 ) = R(succ i u 1 , succ j u 2 , succ k u 3 ).
This is done inductively, with the formulas:

• ∀x : R 0,0,0 (x 1 , x 2 , x 3 ) ↔ R(x 1 , x 2 , x 3 ) • ∀x : i< j,k≤ (R i+1, j,k (x 1 , x 2 , x 3 ) ↔ R i, j,k (succ(x 1 ), x 2 , x 3 )) • ∀x : j< i,k≤ (R i, j+1,k (x 1 , x 2 , x 3 ) ↔ R i, j,k (x 1 , succ(x 2 ), x 3 )) • ∀x : k< i, j≤ (R i, j,k+1 (x 1 , x 2 , x 3 ) ↔ R i, j,k (x 1 , x 2 , succ(x 3 )))
Factorizing the quantifications and using notations of Definition 6.3, the conjunction of these formulas can be written:

∀x                                R 0,0,0 (x) ↔ R(x)∧ i< j,k≤ (R i+1, j,k (x) ↔ R i, j,k (x (1) ))∧ j< i,k≤ (R i, j+1,k (x) ↔ R i, j,k (x (2) ))∧ k< i, j≤ (R i, j,k+1 (x) ↔ R i, j,k (x (3) ))                               
Let us denotes by decomp(R, (R i, j,k ) i, j,k≤ ) this last formula. It clearly fulfills the condition of the statement. Now, consider the formula

∃R∃((R i, j,k ) i, j,k≤ )) R∈R : R∈R decomp(R, (R i, j,k ) i, j,k≤ ) ∧ ∀x φ, ( 19
)
where φ is obtained from ϕ by the substitutions: R(succ i x, succ j y, succ k z) R i, j,k (x, y, z).

Then, the formula ( 19) is equivalent to Φ and also fits the requirements of Fact 7.3. It is the rewriting of Φ announced.

Notice that in the so-obtained formula, one can assume that each equality has the form x = succ i y: it suffices to replace each general equality succ i (x) = succ j (y) by succ i-j (x) = y or x = succ j-i (y) according to the sign of ij. Thus, Fact 7.1, Remark 7.2 and Fact 7.3 finally result in: On coordinate structures of dimension k ≤ d, any formula Φ ∈ ESO(∀ d , arity d) can be written:

Φ ≡ ∃R∀x ±          min(succ i (x)), max(succ i (x)), x = succ i (y), Q s (x ι ), R(x α ), R(x (i) )          (20)
where s ∈ Σ, R ∈ R, x, y ∈ x, ι ∈ I(k, d), α ∈ S(d) and i ∈ {1, . . . , d}.

Toward a last refinement, we can use the trick of the proof of Fact 7.3 to further simplify atomic formulas involving the predicate symbols =, min and max. In order to deal with =, for instance, we existentially quantify over new binary relation symbols S 1 , . . . , S , where is the maximal integer such that an equality of the form x = succ (y) occurs in the formula. We force these symbols to fit the interpretation: S i (x, y) iff x = succ i (y), with the formula:

S 0 (x, y) ↔ x = y ∧ 0<i≤ S i (x, y) ↔ S i-1 (x, succ(y))
in which the sole equality has the form x = y. Hence, substituing S i (x, y) for each subformula x = succ i (y) of Φ, we ensure that all equalities in Φ have the form x = y for some x, y ∈ x. At this step, one can replace the binary symbols S 1 , . . . , S by d-ary relation symbols, as in the proof of Fact 7.1(b), without introducing new equalities. The same process can be carry on to simplify min-and max-atoms. Finally, Equation ( 20) can be more precisely formulated: On coordinate structures of dimension k ≤ d, any formula Φ ∈ ESO(∀ d , arity d) can be written:

Φ ≡ ∃R∀x ± min(x), max(x), x = y, Q s (x ι ), R(x α ), R(x (i) )
where s ∈ Σ, R ∈ R, x, y ∈ x, ι ∈ I(k, d), α ∈ S(d) and i ∈ {1, . . . , d}.

(Notice that despite the appearances, terms involving the function symbol succ have not vanished: they are hidden in the notation R(x (i) ).) It remains to prove that we can get rid of the atomic formulas R(x α ), where α id. This part is rather technical, so we provide some preliminary explanations before stating the logical framework which allows the normalization. In order to get rid of each literal of the form R(x α ), we will divide the set R ⊆ Actually, α∈S(d) [α] is not really a partition, since the [α]'s can overlap. Hence, Definition 7.4 induces some connexions between the relations R α : if some x is both in [α] and in [β], or equivalently, if

[n] d in d! relations R α ⊆ [n] d ,
x α = x β , then x ∈ R ∩ [α] iff x ∈ R ∩ [β]
and hence, by Definition 7.4: R α (x α ) = R β (x β ). We will keep in mind :

∀α, β ∈ S(d), ∀x ∈ [n] d : x α = x β ⇒ R α (x α ) = R β (x β ). (22)
The following lemma states that condition [START_REF] Giammarresi | Two-dimensional languages, volume 3-Beyond words of Handbook of Theoretical Computer Science[END_REF] ensures that the R α 's issue from a single relation R, according to Definition 7.4. Besides, a new formulation of the condition is given in Item 3 of the lemma, that will better fit our syntactical restrictions. Lemma 7.5. Let (R α ) α∈S(d) be a family of d-ary relations on [n] such that R α ⊆ [id] for each α. The following are equivalent:

1. ∃R ⊆ [n] d such that for each α ∈ S(d): R α = {x ∈ [id] s.t. R(x α -1 )} ; 2. ∀α, β ∈ S(d), ∀x ∈ [n] d : x α = x β ⇒ R α (x α ) = R β (x β ) ; 3. ∀α ∈ S(d), ∀τ ∈ T (d), ∀x ∈ [n] d : x = x τ ⇒ R α (x) = R ατ (x).
(Remember that T (d) denotes the set of transpositions of {1, . . . , d} -see Definition 6.3(iii).)

Proof. 1 ⇒ 2: See Equation (22). 2 ⇒ 1: For (R α ) α∈S(d) fulfilling 2, consider the relation R ⊆ [n] d defined by: R(x) iff R α (x α ) for some α such that x α ↑ . (23)
This definition is well formed, since for any α, β ∈ S(d) and any x ∈ [n] d such that both x α ↑ and x β ↑ hold, we have

x α = x β and thus, by 2, R α (x α ) = R β (x β ). Now, let α ∈ S(d). For any x ∈ [id] we have (x α -1 ) α ↑ (since (x α -1 ) α = x) and hence, by (23), R α (x) = R α ((x α -1 ) α ) = R(x α -1 ). Besides, R α (x) = 0 for any x [id], since R α ⊆ [id]. Thus R α is obtained from R as required in 1. 2 ⇒ 3: Let α ∈ S(d), τ ∈ T (d) and x ∈ [n] d such that x = x τ . Set y = x α -1 .
Then, y α = x = x τ = (y α ) τ = y ατ . Therefore we get by 2: R α (y α ) = R ατ (y ατ ), and hence: R α (x) = R ατ (x).

3 ⇒ 2: Let α, β ∈ S(d) and x ∈ [n] d such that x α = x β . For y = x α , the equality x α = x β can be written y = y α -1 β . It means that the permutation α -1 β exchanges integers that index equal components of y. It is easily seen that this property can be required for each transposition occuring in a decomposition of α -1 β on T (d). That is, there exist some transpositions τ 1 , . . . ,

τ k ∈ T (d) such that α -1 β = τ 1 . . . τ k and y = y τ 1 = y τ 1 τ 2 = • • • = y τ 1 ...τ k .
Then, applying 3 to these successive tuples, we get: R α (y

) = R ατ 1 (y τ 1 ) = R ατ 1 τ 2 (y τ 1 τ 2 ) = • • • = R ατ 1 ...τ k (y τ 1 ...τ k ). Hence R α (y) = R β (y α -1 β ), that is R α (x α ) = R β (x β ), as required.
Lemma 7.6. Let R and (R α ) α∈S(d) be defined as in Definition 7.4. Let α, β ∈ S(d) and i ∈ {1, . . . , d}. For any x ∈ [α]: (i) ) is equivalent to:

1. R(x β ) = R β -1 α (x α ).

R(x

x i = x α d ∧ R ατ j,d ((x α ) (d) ) ∨ i≤k<d x i = x α k x α k+1 ∧ R ατ j,k ((x α ) (k) ) ,
where j = α -1 (i). (Here, τ u,v denotes the transposition swapping u and v.)

Proof. 1. Since x ∈ [α], and hence x α ∈ [id], Definition 7.4 yields:

R β -1 α (x α ) = R((x α ) (β -1 α) -1 ) = R((x α ) α -1 β ) = R(x αα -1 β ) = R(x β ). 2. From x (i) = (x 1 , . . . , succ(x i ), . . . , x d ) we get: (x (i) ) α = (x α 1 , . . . , x α j-1 , succ(x i ), x α j+1 , . . . , x α d ), where j = α -1 (i). Since x α 1 ≤ • • • ≤ x α d ,
the above tuple (x (i) ) α is almost increasingly ordered. More precisely, there exists k ∈ {1, . . . , d} such that:

x α 1 ≤ • • • ≤ x α j-1 ≤ x i = x α j+1 = • • • = x α k ≤ x α k+1 ≤ • • • ≤ x α d ,
where j = α -1 (i). Clearly, the largest such k is characterized by: (k = d) or (x i = x α k < x α k+1 ). Or equivalently, by:

(x i = x α d ) or (x i = x α k x α k+1 ). ( 24
)
If we denote by τ j,k the transposition over {1, . . . , d} which permutes j and k, the definition of k yields that the tuple

(x (i) ) ατ j,k = (x α 1 , . . . , x α j-1 , x α k , x α j+1 , . . . , x α k-1 , succ(x i ) , x α k+1 , . . . , x α d ) is increasing. Hence, R(x (i) ) = R ατ j,k ((x (i) ) ατ j,k
). Besides, since x α k = x i , the tuple (x (i) ) ατ j,k above can also be written:

(x (i) ) ατ j,k = (x α 1 , . . . , x α j-1 , x i , x α j+1 , . . . , x α k-1 , succ(x α k ) , x α k+1 , . . . , x α d ).
That is: (x (i) ) ατ j,k = (x α ) (k) . Therefore: R(x

(i) ) = R ατ j,k ((x α ) (k)
). We can finally state: there exists a sole k ∈ {i, . . . , d} defined by [START_REF] Giammarresi | Computing languages by (bounded) local sets[END_REF], and for this k we have: R(x

(i) ) = R ατ j,k ((x α ) (k)
). Reminding that j = α -1 (i), the conclusion immediatly proceeds.

Φ ≡ ∃R∀x α∈S(d) (x ∈ [α] → ϕ) .
Furthermore, all R-atoms of ϕ can be assumed of the form R(x α ) or R(x (i) ), thanks to Fact 7.3. To get rid of the literals R(x α ), we substitute to R a tuple of relations (R α ) α∈S(d) that encode R on the sets [α]. We proved in Lemma 7.5 that this substitution is legal as soon as R α ⊆ [id] and R α (x) = R ατ (x) for all α ∈ S(d), τ ∈ T (d) and every x ∈ [n] d such that x τ = x. Then, Lemma 7.6 gives the translation of R-atomic formulas into formulas expressed in term of the R α 's. All in all, we get the equivalence of the initial formula Φ to the following:

∃(R α ) α∈S(d)                          ∀x α∈S(d) (R α (x) → x ∈ [id])∧ ∀x α∈S(d) τ∈T (d) (x τ = x → (R α (x) ↔ R ατ (x)))∧ ∀x α∈S(d) x ∈ [α] → ϕ α (x, (R γ ) γ∈S(d) )                          (25)
where each ϕ α is obtained from ϕ by the substitutions:

• R(x β ) R β -1 α (x α ) • R(x (i) )              x i = x α d ∧ R ατ α -1 (i),d ((x α ) (d) ) ∨ i≤k<d x i = x α k x α k+1 ∧ R ατ α -1 (i),k ((x α ) (k) )             
The first two conjuncts of [START_REF] Grädel | Capturing complexity classes by fragments of second order logic[END_REF] ensure that the family (R α ) α∈S(d) encodes a relation R (see Lemma 7.5); the third interprets assertions of the form R(x β ) and R(x (i) ) according to the modalities described in Lemma 7.6. Because of permutability of the conjunction and the universal quantifier, this third conjunct can be rewritten:

α∈S(d) ∀x : x ∈ [α] → ϕ α (x, (R γ ) γ∈S(d) ) (26)
For a fixed conjunct in [START_REF] Grädel | Finite Model Theory and Its Applications[END_REF], i.e. for a fixed α, all atomic subformulas of ϕ α built on the R γ 's have the form R γ (x α ) or R γ ((x α ) (i) ) for some γ ∈ S(d) and some i ∈ {1, . . . , d}. Hence, the substitution of variables x/x α allows to write such a conjunct as: ∀x : x ∈ [id] → φα where φα ≡ ϕ α (x/x α ) only involves (R γ )-subformulas of the form R γ (x) or R γ (x (k) ) for some γ ∈ S(d) and k ∈ {1, . . . , d}. Finally, the initial formula Φ is proved equivalent to the following formula Ψ, whose all R-atoms agrees with the sorted property (Condition (3b) of Definition 6.2):

Ψ ≡ ∃(R α ) α∈S(d)                          ∀x α∈S(d) R α (x) → x ∈ [id] ∧ ∀x α∈S(d) τ∈T (d) x τ = x → (R α (x) ↔ R ατ (x)) ∧ ∀x α∈S(d) x ∈ [id] → φα (x, (R γ ) γ∈S(d) )                          (27)
The proof is not yet completed: one could refer to Definition 6.4 (3) to verify that neither the relation = nor the relation < can be involved in an ESO(∀ d , arity d, half-sorted )-formula. However, these two predicates still appear in formula [START_REF] Grandjean | First-order spectra with one variable[END_REF] (the inequalities are hidden in the expression "x ∈ [id]" that abbreviates the formula x 1 ≤ • • • ≤ x d ), and it remains to get rid of them. To this end, we introduce two new binary relation symbols E and P < that will be forced to coincide with = and < by use of inductive constraints written with the successor function. But the assignment of maintaining the sorted property precludes us from writing formulas that we would be naturally minded to invoke when formalizing these constraints. For instance, the formulas E(x 1 , x 1 ) and E(x 1 , x 2 ) ↔ E(succ(x 1 ), succ(x 2 ) contain non sorted atoms and hence don't fit our syntactical restrictions. Therefore, we introduce two additionnal binary relation symbols, S and P > , intended to simulate, respectively, the successor function and the strict linear order opposite to <. It appears that we can stipulate the interpretations of E and S by a simultaneous inductive scheme expressed in sorted fashion thanks to the formula below:

Θ 1 (E, S ) ≡ ∀x 1 , x 2                min(x 1 ) → min(x 2 ) ↔ E(x 1 , x 2 ) ∧ min(x 2 ) → min(x 1 ) ↔ E(x 1 , x 2 ) ∧ ¬max(x 2 ) → E(x 1 , x 2 ) ↔ S (x 1 , succ(x 2 ) ∧ S (x 1 , x 2 ) ↔ E(succ(x 1 ), x 2 )                .
In a similar way, P < and P > are compelled to fit their intended meaning via the following formula, in which we assume the interpretation of E has been previously fixed (by Θ 1 ):

Θ 2 (E, P < , P > ) ≡ ∀x 1 , x 2                (E(x 1 , x 2 ) ∨ P < (x 1 , x 2 )) → (¬max(x 2 ) → P < (x 1 , succ(x 2 ))) ∧ (E(x 1 , x 2 ) ∨ P > (x 1 , x 2 )) → (¬max(x 1 ) → P > (succ(x 1 ), x 2 )) ∧ P < (x 1 , x 2 ) → (¬P > (x 1 , x 2 ) ∧ ¬E(x 1 , x 2 )) ∧ P > (x 1 , x 2 ) → ¬E(x 1 , x 2 )                .
Clearly, the formula Ψ displayed in [START_REF] Grandjean | First-order spectra with one variable[END_REF] can be rewritten in ∃E, S , P < , P > : Ψ ∧ Θ 1 ∧ Θ 2 , where Ψ is obtained from Ψ by the substitutions:

x i = x j E(x i , x j ), x i < x j P < (x i , x j ) and x j < x i P > (x i , x j )
for any i < j. The resulting formula respects the sorting property. At last, notice that one can subtitute d-ary relation symbols for E, S , P < and P > without spoiling the sorted property, as we did it in the proof of Fact 7.1(b).

All in all, the results obtained in Section 7 can be recapitulated as follows:

On (d -1)-coordinate pictures, each ESO(∀ d , arity d)-formula can be written under the form:

Φ ≡ ∃R∀x ± min(x), max(x), Q s (x ι ), R(x), R(x (i) ) .
Here, R is d-ary and belongs to R, s ∈ Σ and

Q s has arity d -1, x ∈ x, ι ∈ I(d -1, d), i ∈ [d]. (28)

Sorting input relations

We now embark on the last step of our "localization" of ESO(var d)-formulas. Thanks to the results proved so far, it suffices to prove the inclusion, to be stated in Proposition With definitions 6.4 and 6.2 in mind, our purpose can be very simply defined: given a formula Φ of the form described in Equation [START_REF] Grandjean | Graph properties checkable in linear time in the number of vertices[END_REF], we want to replace by a sorted atom each atom of the form Q(x ι ), where Q ∈ (Q s ) s∈Σ and ι ∈ I(d -1, d), ι id. In the vein of Section 7, we aim at defining a tuple of relations (Q ι ) ι∈I(d-1,d) , in such a way that Q ι (x) = Q(x ι ) for each x. Clearly, such relations will allow to write Φ under the desired form, by substituing each subformula Q(x ι ) with Q ι (x). Of course, the definition of the Q ι 's must be logically formulated in our syntactical restrictions, that is, without involving any x α such that α id. Furthermore, the way we carried out this strategy in Section 7 is no more avalaible. Indeed, there we sorted atoms R(x α ) build on some existentially quantified d-ary relations R by suppressing R in favour of some new existentially quantified relations R α , α ∈ S(d). (See proof of Proposition 7.7.) Of course, we can't operate like this with the relation Q, which is part of the input.

To give a hint of the method used in the present section, let's start with an example.

An easy case

Consider the case where d = 2. We deal with two first-order variables x and y and we only accept atoms of the form Q(x), R(x, y), R(succ(x), y) and R(x, succ(y)) for any input unary relation Q and any guessed binary relation R. How can we tackle occurences of some atom Q(y) in the formula ? A natural idea is to define a new binary relation Q 2 in such a way that Q 2 (x, y) = Q(y) holds for any x, y. (We denote it Q 2 to refer both to Q and to the projection of (x, y) on its second component.) Hence, we set:

Q 2 = {(x, y) : Q(y)}.
Thus, any atom Q(y) could be replaced by the sorted atom Q 2 (x, y). But the logical definition of Q 2 with our syntactical constraints compels to introduce an additional binary relation T that will be used as a buffer to transport the information Q(y) into the expression Q 2 (x, y). Informally, we can set

T = {(x, y) : Q(x + y)}.
Clearly, T is inductively defined from Q by the assertions T (x, 0) = Q(x) and T (x + 1, y) = T (x, y + 1). Besides, Q 2 is defined from T by Q 2 (0, y) = T (0, y) and Q 2 (x, y) = Q 2 (x + 1, y). All these assertions can be rephrazed in our logical framework, with the following formulas:

∀x, y min(y) → (T (x, y) ↔ Q(x)) ∧ (¬max(x) ∧ ¬max(y)) → T (succ(x), y) ↔ T (x, succ(y)) ; ∀x, y min(x) → (Q 2 (x, y) ↔ T (x, y)) ∧ Q 2 (x, y) ↔ Q 2 (succ(x), y) .
It just remains to insert this defining formulas in the initial formula Φ to be normalized, and to replace each occurrence of Q(y) by Q 2 (x, y). Of course, such a construction has to be carried on for each input unary relation Q.

General case: the sliding puzzle

When the dimension d exceeds 2, the construction is more intricate. For a given input relation Q, there are now numerous sources of corruption of the sorted property. For instance, if d = 4 then Q has arity 3 and we may enconter many kinds of non sorted Q-atoms in the formula to be normalized: Q(x 2 , x 3 , x 1 ), Q(x 1 , x 4 , x 2 ), Q(x 2 , x 3 , x 4 ), etc. Dealing with these different atoms necessitate to introduce two new series of predicates, (Q α ) α∈S(d) and (T α ) α∈S(d) , whose definitions are interconnected. In particular, the definition of the T α 's must be done step-by-step, according to an inductive process by which a new relation T β is built from a yet-defined relation T α , where α and β differ by exactly one transposition (i.e., β = ατ for some τ ∈ T (d)). The key point of the proof will be to organize a traversal of the set of permutations which allows this recursive procedure of definition. In particular, it will be necessary that two consecutive transpositions labeling this traversal share a common position -that is, they should be written (i j) and ( jk) for some i, j, k ∈ [d] -, in the same way a move from one position to another in a sliding puzzle always involves the place left vacant by the previous move.

Given i, j ∈ {1, . . . , d} and α ∈ S(d), we denote by (i j) the transposition that exchanges i and j, 4 and by α(i j) the composition of α and (i j). It is well-known that each permutation α can be written as a product of transpositions,

α = (u 1 v 1 )(u 2 v 2 ) . . . (u p v p ). (29)
Besides, for any transposition (uv) and any r not in {u, v}, it holds (uv) = (ru)(uv)(vr). This yields two consequences of interest for the decomposition (29):

• First, we can assume that u 1 = d (or equivalently, v 1 = d), since if d {u 1 , v 1 }, then we can write α = (du 1 )(u 1 v 1 )(v 1 d)(u 2 v 2 ) . . . (u p v p ).

• Moreover, (29) can be further refined, by demanding that v i = u i+1 for each i. For if some sequence (ab)(cd) with b {c, d} occurs in [START_REF] Grandjean | Descriptive complexity of picture languages[END_REF], it can be replaced by (ab)(bc)(cd)(db), and a left-to-right iteration of such rewritings along the factorization yields the desired property.

Finally, does mean suppressing useless sequences as (ab)(ba), each α ∈ S(d) can be written

α = (du 1 )(u 1 u 2 )(u 2 u 3 ) . . . (u k-2 u k-1 )(u k-1 u k ), (30)
where for each i, the terms u i , u i+1 and u i+2 are pairwise distinct elements of {1, . . . , d}. We call alternated factorization of α such a decomposition.

A permutation α admits several alternated factorizations, and we want to single out one of them for each α, in order to allow an inductive reasoning built on this particular decomposition. There is no canonical way to perform this task. In the following lemma, we roughly describe one arbitrary choice. It refers to the Cayley graph G d of the symmetric group S(d) with respect to the set of generators T (d). Recall that G d is the graph of domain S(d) whose edges are all pairs of permutations (α, α(i j)), for i j in {1, . . . , d}. In Fig 2, we display the steps of the construction of T 4 from T 2 . Letters (a), . . . , (d) in the figure refer to the above items. The correction of the method on this example is clear. We leave it to the reader to verify that it generalises to any d.

This lemma allows us to choose, for each α ∈ S(d), one specified alternated factorization of α: it is the decomposition (di 1 )(i 1 i 2 ) . . . (i k-1 i k ) corresponding to the unique path from id to α in T d . We denote by id.di 1 .i 1 i 2 . . . . .i k-1 i k this particular factorization. And when this path until α can be continued in T d to some permutation α(i k i k+1 ), we denote by α.i k i k+1 this last permutation. For instance, in the example displayed in Fig 2, we can write 2143 = 4123.13 and 3124 = 4123.14 while 4321 = 4123(24) cannot be written 4123. [START_REF] Giammarresi | Computing languages by (bounded) local sets[END_REF]. Notice furthermore that the integers i k and i k+1 are ordered in the notation α.i k i k+1 (unlike in the notation α(i k i k+1 )): we place in first position the integer i k involved in the last transposition leading to α (with i k = d if α = id). All in all, the reader is invited to keep in mind the numerous presuppositions attached to the notation α.uv: the statement β = α.uv means: (a)

(b)
(a) (b) (c) (d)
Figure 2: Construction of T 4 from T 2 . The result is an oriented tree rooted at id, spanning S(4), whose all pathes from id are alternated.

• β = α(uv) ;

• (α, β) is an edge of T d ;

• either α = id and u = d, or α = γ.tu for some γ ∈ S(d) and some t u in {1, . . . , d}.

Let us now come to a straightforward remark connecting d-tuples to alternated factorizations. First, remember that for x = (x 1 , . . . , x d ), i ∈ {1, . . . , d} and α, β ∈ S(d),

• we denoted by [x] i the i th component of x ;

• we defined x α as the d-tuple (x α 1 , . . . , x α d ) ;

• we noticed that (x α ) β = x αβ .

(See Definition 6.3.) Fact 8.2. For any x ∈ [n] d , α ∈ S(d), and i, j ∈ {1, . . . , d}: All in all, our normalization process can be summarized as follows:

(a) x α.i j = (x α ) (i j) . (b) [x α.i j ] j = [x] d .
On (d -1)-coordinate structures, each ESO(var d)-formula can be written under the form:

Φ ≡ ∃R∀x ± min(x i ), max(x i ), Q(x -), R(x), R(x (i) )
Here, R (resp. Q) is a list of relation symbols of arity d (resp. d -1), x = (x 1 , . . . ,

x d ), i ∈ [d], Q ∈ (Q s ) s∈Σ , R ∈ R. (32)
Remark 8.8.

1. The proof of Proposition 8.6 crucially involves the possibility to use one of the d dimensions that is left unoccupied by the (d -1)-ary input relation symbols. This free dimension acts as a buffer that enabled us to play the above mentioned sliding puzzle. Therefore, the result is a fortiori valid when the input relations have arity less than d -1. In other terms, the statement of Proposition 8.6, and hence that of Theorem 8.7 , actually holds on coordinate structures of dimension k < d.

2. Besides, one can assume that the successor function occuring in formulas displayed in [START_REF] Hanf | Model-theoretic methods in the study of elementary logic[END_REF] only applies to arguments that are not maximal, or alternatively, that succ(n) = n, which means that the interpretation of the successor function symbol is the noncyclic successor instead of the cyclic one. Proof. Let Φ be the formula characterizing coord d (L). From Theorem 8.7 (see also Equation ( 32)), we can assume that Φ has the form:

Φ ≡ ∃R∀x∀t ± min(x i ), max(x i ), min(t), max(t), Q(x), R(x, t), R(x (i) , t), R(x, succ(t)) . for i ∈ [d], Q ∈ (Q s ) s∈Σ and R ∈ R.
Moreover, according to Remark 8.8 we can assume without loss of generality that the succ symbol is interpreted as the noncyclic successor function.

The key point is that sentence Φ can be checked in O(n) steps (for an input picture of domain [n] d ) by a local and parallel nondeterministic process. More precisely, it is easy to construct a d-automaton which uses the following informal but intuitive algorithm to check whether coord d (p) | = Φ, for any input picture p : [n] d → Σ:

For t = 1, 2, . . . , n, sequentially, For all a ∈ [n] d , in parallel,

• Guess (nondeterministically) the truth values of the atoms R(a, t);

• Check (deterministically) whether the values of the R(a, t)'s are compatible 5with each other, with the values of the input atoms Q(a) and of the atoms min(a i ) and max(a i ), with the "previous" values of atoms R(a, t -1) (provided t > 1);

• If some answer is "no" then Reject;

Accept.

The process is correct because at each moment the cellular automaton at cell a ∈ [n] d has only to consider the fixed number of information bits that the point a = (a 1 , . . . , a d ) and its d neighbor points a (i) = (a 1 , . . . , a i-1 , succ(a i ), a i+1 , . . . , a d ) hold. Each of the n iterations of the first loop ("For t = 1, 2, . . . , n") is performed in constant time, hence the total time is O(n).

Then, we have stated characterizations of NLIN d ca for coordinate encoding of pictures (Theorem 9.1 and Theorem 8.7):

L ∈ NLIN d ca ⇔ coord d (L) ∈ ESO(∀ d+1 , arity d + 1, sorted ) ⇔ coord d (L) ∈ ESO(∀ d+1 , arity d + 1) ⇔ coord d (L) ∈ ESO(var d + 1). ( 34
)
One could legitimately ask whether a same encoding of pictures would permit characterizations of both REC d and NLIN d ca . We now answer this question in its two aspects. • The strict inclusion NLIN d ca NTIME d ca (n d ) is a particular case of the nondeterministic time hierarchy theorem [START_REF] Cook | A hierarchy for nondeterministic time complexity[END_REF][START_REF] Seiferas | Separating nondeterministic time complexity classes[END_REF] adapted to nondeterministic d-dimensional cellular automata, see [START_REF] Iwamoto | A time hierarchy theorem for nondeterministic cellular automata[END_REF] that has proved it for d = 1: we are convinced it can be generalized to any d > 1.

•

Coordinate representation does not fit recognizable picture languages

One can easily translate the logical characterization of REC d in ESO(∀ 1 , arity 1) for the pixel representation, into a characterization in ESO(∀ d , arity d, sorted ) for the coordinate representation. This is due to the following fact: Proof. To justify this equivalence, let us define a notion of sorted ESO(∀ 1 , arity 1)-formula, even if it is much less relevant that the corresponding definition for d ≥ 2: An ESO(∀ 1 , arity 1)-formula Φ belongs to ESO(∀ 1 , arity 1, sorted ) if it can be written Φ ≡ ∃U∀x ϕ, where ϕ is a quantifier free formula of the form:

ϕ ≡ ± Q(x), U(x), U(succ i (x)), min i (x), max i (x) (35)
Here, U is a list of unary relation symbols, U ∈ U, Q belongs to the sequence (Q s ) s∈Σ of input unary relations, x is the unique first-order variable and i ∈ That means the following implications hold,

coord d (L) ∈ ESO(var d -1) ⇒ L ∈ REC d ⇒ coord d (L) ∈ ESO(var d),
but neither of their converses does.

Proof.

L ∈ REC

d ⇒ coord d (L) ∈ ESO(var d).
This implication is a weakening of the equivalence stated in Fact 9.4. However, Lemma 9.6 implies that the converse implication is false. It completes the proof.

For pictures languages of dimension d ≥ 2 and coordinate encoding, the definability class ESO(∀ d , arity d), although logically robust, does not coincide with some complexity class. However, the additional expressivity power due to the ability to freely permute the coordinates (i.e. the arguments of relation symbols) in a sentence of this logic intuitively corresponds to the ability to add in the neighborhood of any pixel a = (a 1 , . . . , a d ) ∈ [n] d all its permuted pixels a α = (a α(1) , . . . , a α(d) ), for each permutation α of [d]. This remark will be made precise using the notion of folded picture.

Formula ϕ 2 ensures that for each R ∈ Rel(ϕ), its associated relations R α 's agree on their common parts as mentioned in Section 7. Moreover, ϕ 3 expresses that the relations Q σ , σ ∈ Σ d , are what they should be for the folded picture p fold , as explained here below. By [START_REF] Kari | Basic Concepts of Cellular Automata[END_REF] applied to the relation Q σ(α),α -1 (a) associated with Q σ(α) , we have:

Q σ(α),α -1 = {a ∈ [n] d : a↑ and a α ∈ Q σ(α) }.
Hence, by Lemma 9.10, In view of equivalence [START_REF] Kutrib | Nondeterministic cellular automata and languages[END_REF], there only remains to justify the following implication:

Q σ(α),α -1 = {a ∈ [n] d : a↑ and a ∈ Q σ }. This corresponds to equivalence Q σ (x) ↔ ( α∈S(d) Q σ(α),α -1 (x) of
coord d (p ) | = Φ fold ⇒ ∃p(p = p fold ).
It is clear that the "subformula" ∀x : ϕ 0 (x) ∧ ϕ 1 (x) ∧ ϕ 2 (x) ∧ ϕ 3 (x) of Φ fold implies that the underlying picture is of the form p fold as required. This concludes the proof of implication 1 ⇒ 2. Let's now prove the converse one.

2 ⇒ 1 Assume that the folded language L fold of a d-language L on Σ is recognizable. By Fact 9.4 the set of coordinate structures coord d (L fold ) is defined in ESO(∀ d , arity d), i.e., by a sentence Φ of the form Φ = ∃R∀x ϕ(x), where R is a set of d-ary relation variables and ϕ is a quantifier-free formula with the list of first-order variables x = (x 1 , . . . , x d ). The intuitive idea of the construction of the following sentence, denoted Φ unfold , also in ESO(∀ d , arity d), that defines the set of coordinate structures coord d (L), is to view each picture p ∈ L as the projection of a picture that is the superposition of p and of its folded picture p fold :

Φ unfold = ∃(Q σ ) σ∈Σ 0 d ∃R∀x ϕ unfold (x)
where

ϕ unfold (x) = ϕ(x) ∧                (x↑) → σ∈Σ d Q σ (x) ↔ α∈S(d) Q σ(α) (x α ) ∧ ¬(x ↑) → Q 0 (x) ∧ σ∈Σ d ¬Q σ (x) .               
In order to justify the correctness of sentence Φ unfold , that means, for each d-picture p on Σ,

p ∈ L ⇔ coord d (p) | = Φ unfold ,
it is sufficient to prove the following equivalence:

coord d (p fold ) | = Φ ⇔ coord d (p) | = Φ unfold . ( 39
)
The implication ⇐ of (39) is obvious since ϕ is a conjunct of ϕ unfold . The converse implication ⇒ is a straigtforward consequence of the definitions and, for conjunct 9.2.3, of Lemma 9.10. Proposition 9.11 is proved.

3. Elsewhere: p mix (a) = 0 otherwise, i.e., if not a↑. . Therefore, by the pigeonhole principle, for n sufficiently large, there will be two different pictures p 1 and p 2 in L n whose corresponding pictures p 1 and p 2 in L n such that p 1 = π • p 1 and p 2 = π • p 2 have the same border stripe. By definition of a local language, that implies that the mixed picture

p mix = [p 2 /p 1 ]
also belongs to L n and therefore its projection

p mix = π • p mix = [π • p 2 /π • p 1 ] = [p 2 /p 1 ]
belongs to L n , i.e., is in L = (sym d ) fold as p 1 an p 2 are. Now, notice that by clause 1 (resp. clause 2) of the definition of the picture p mix = [p 2 /p 1 ], the restriction of p mix to the subdomain Rep n (resp. T n ) is the restriction of p 1 to Rep n (resp. the restriction of p 2 to T n ). This implies p mix = p 1 (resp. p mix = p 2 ) because this restriction is a one-one mapping as item 1 (resp. item 2) of Lemma 10.4 asserts. This is a contradiction since pictures p 1 and p 2 are different each other. This proves L = (sym d ) fold REC d and hence Lemma 10.5.

We now have all the tools to prove the following strict hierarchy theorem. Proof. Note that all the equalities and inclusions mentioned in the theorem either have been already proved or are trivial. There remains to justify the strictness of two of these inclusions.

: ψ 0 (x 1 , x 2 ) ∧ ψ 1 (x 1 , x 2 )
, where:

ψ 0 ≡ {min(x 1 ) ∨ max(x 2 ))} → R sym (x 1 , x 2 ) ↔ (min(x 1 ) ∨ max(x 2 )) and ψ 1 ≡ {¬max(x 1 ) ∧ ¬max(x 2 )} → R sym (succ(x 1 ), x 2 ) ↔ R sym (x 1 , succ(x 2 )) ,
defines the binary relation R sym (x 1 , x 2 ) to be x 1 + x 2 = n+1 on any coordinate structure of domain [n]. Hence, by Definition 10.1 and its footnote, one easily sees that the set of structures coord d (sym d ) is defined by the following sentence ϕ sym in ESO(∀ d+1 , arity d):

∃R sym ∀x 0 . . . ∀x d                ψ 0 (x 1 , x 2 ) ∧ ψ 1 (x 1 , x 2 ) ∧ α∈S(d) (Q 1 (x) ↔ Q 1 (x α )) ∧ R sym (x 1 , x 0 ) → (Q 1 (x) ↔ Q 1 (x 1→0 )) .               
Here, as usual, x = (x 1 , . . . , x d ), x α = (x α(1) , . . . , x α(d) ), and x 1→0 is the d-tuple x where x 1 is replaced by x 0 . This achieves the proof of Theorem 10.

Conclusion: final remarks, additional results and open problems

Locality in logic

As recalled in the introduction of this paper there are several notions of locality in logic. The locality of general first-order definability expressed by the normal form of Gaifman's Theorem [START_REF] Gaifman | On local and nonlocal properties[END_REF] is weaker than the locality of first-order logic definability with only one variable (universally quantified) over picture languages (with adjacency represented by successor functions), a notion that Borchert [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] has shown to be equivalent to tilability. Note that this strong locality is obtained in accordance with the locality of the underlying grid structure.

In this paper, we have used exclusively this stronger notion. We have established natural EMSO or ESO characterizations of two nondeterministic classes of picture languages: recognizable picture languages and linear time class of nondeterministic cellular automata.

Of course, those complexity/logical notions are nonlocal: concerning the most restrictive one, recognizable picture properties, surprising, Reinhardt [START_REF] Reinhardt | On some recognizable picture-languages[END_REF][START_REF] Reinhardt | The #a = #b pictures are recognizable[END_REF] has proved that several global properties including connectivity are recognizable and there are also NP-complete problems among recognizable ones.

However, the intuitive idea that both are classes of "projections" of local languages is made explicit by their characterization by ESO logics with normal forms whose first-order part is local: that means with only one first-order variable for pixel encoding, or -for coordinate encoding of d-pictures -with d + 1 "sorted" first-order variables, one of which intuitively represents the time.

Extensions and limits of our results

It is interesting to notice that several of our results can be extended: 11.3. Other related results of the literature Borchert [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] has stated some results to be compared with our logical characterizations of recognizable languages and of linear time bounded complexity classes of multidimensional cellular automata although, paradoxically, his paper never mentions cellular automata. More precisely, Giammarresi [START_REF] Giammarresi | Computing languages by (bounded) local sets[END_REF] and/or Borchert [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] have studied a class of word languages (resp. 2-picture languages called graph languages) that Borchert has called COL d or d-dimensionally colorable language, for any fixed integer d ≥ 1 (resp. COL d G , for any fixed integer d ≥ 2). Among other equivalent characterizations, [START_REF] Giammarresi | Computing languages by (bounded) local sets[END_REF] and/or [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] defined COL d (resp. COL d G ) as the class of word (resp. 2-picture) languages L for which there exists a recognizable d-picture language L such that L is the set of frontiers (resp. square frontiers) of the pictures of L : a word w (resp. 2-picture f ) is the frontier (resp. square frontier) of a d-picture p : [n] d → Σ if w is the word (resp. f is the d-picture) written on the first "edge" (resp. first "face") of the d-dimensional colored "cube" p, that means w = w 1 w 2 . . . w n with w i = p(i, 1, . . . , 1), for each i ≤ n ( f is f : [n] 2 → Σ with f (i, j) = p(i, j, 1, . . . , 1), for all (i, j ∈ [n] 2 ). Indeed, from these definitions the following fact is easily deduced:

•
Fact 11.1.

• COL 1 is the class of regular word languages and COL 2 G is the class of recognizable 2picture languages, respectively: COL 1 = REC 1 = REG and COL 2 G = REC 2 .

• For any d > 1 (resp. d > 2), a word language (resp. 2-picture language) L belongs to COL d (resp. COL d G ) iff there exists a nondeterministic (d -1)-dimensional cellular automaton that recognizes L in linear time.

Then Borchert [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] states logical characterizations (Lemma 5.2 and Corollary 9.2(d) in [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF]) that can be rephrased as follows:

1. On words, COL 1 = REC 1 = REG = ESO(∀ 1 , arity 1).

2. For d > 1, a word language belongs to COL d , i.e. is recognized by some nondeterministic (d -1)dimensional cellular automaton in linear time, iff it is definable in ESO(∀ d , arity d).

3. For d > 2, a 2-picture language belongs to COL d G , i.e. is recognized by some nondeterministic (d -1)dimensional cellular automaton in linear time, iff it is definable in ESO(∀ d , arity d) for coordinate representation.

However, the sketchy proofs of results 2 and 3 given by [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF] have some drawbacks. The implications "definability" → "complexity", i.e. the inclusions ESO(∀ d , arity d) ⊆ COL d for word languages, and ESO(∀ d , arity d) ⊆ COL d G for 2-picture languages, are not correctly justified in [START_REF] Borchert | Formal language characterizations of P, NP, and PSPACE[END_REF]. As we have seen in our proofs of Proposition 8.6, Theorem 8.7, and Proposition 9.2, one should beforehand normalize each sentence by "sorting" its first-order variables.

Some remarks about the dimensions of pictures

For sake of simplicity and uniformity, we have chosen in this paper to restrict the presentation of results to "square" pictures, i.e. pictures of prototype p : [n] d → Σ. This may appear as a too strong requirement. In this section, we explain how our results about logical classes and their relationships with complexity classes REC d and NLIN d ca can be extended to the "most general" picture languages, i.e. to sets of d-pictures of prototype p : • The "perimeter" of a c-balanced d-picture p of length n is Θ(n) and its size (called area, or volume, etc., according to its dimension d) is |p| = Θ(n d ).

• So, linear time means time linear in the perimeter of the d-picture p or, equivalently, in |p| 1/d .

We can easily extend all our results about square d-languages to well-balanced d-languages. In order to reduce the well-balanced case to the "square" case we need some new definitions. The following result is easy to prove.

Lemma 11.7. Let L be a well-balanced d-picture language. Then L ∈ NLIN d ca ⇔ L = ∈ NLIN d ca .

Remark 11.8. Notice that the nontrivial (right-to-left) implication of the previous lemma means that the dautomaton A 1 that recognizes L = in linear time can be simulated by some d-automaton A 2 that recognizes L in the same time (up to a constant factor) but with less space: the computation area consists of the cells of p instead of the cells of its squared version p = . This is possible with the following trick: the fact that the i th dimension n of p = is replaced by n i ≥ n/c allows to "fold" the picture c times along its i th dimension. All in all, each cell of p simulates (at most) c d cells of p = . This is performed by taking for the set of states of A 2 the set Γ c d where Γ is the set of states of A 1 .

Now, let us compare any well-balanced d-picture language L and its squared language L = from a logical point of view. The domain of the coordinate representation of a d-picture p :

[n 1 ] × • • • × [n d ] is naturally [n]
where n is the length of p, i.e. n = max(n 1 , . . . , n d ). So, we define the coordinate representation of p as

coord d (p) = coord d (p = ).
So, as a trivial consequence, coord d (L) = coord d (L = ). This justifies that the results of Sections 4-10 also hold in the extended case of well-balanced d-picture languages.

More hierarchies

It is also natural to address the question of the strictness or collapsing of the following "hierarchies" about second-order logic (SO) over picture languages :

1. Is there a strict hierarchy of SO or MSO according to the second-order quantifier alternation? It is well-known that the answer is negative for MSO on word languages and tree languages: on these classes of languages, MSO = EMSO holds. That is, the hierarchy collapses at it first level: see e.g. Chapter 7 of Libkin's book [START_REF] Libkin | Elements of Finite Model Theory[END_REF].

At the opposite, Matz, Schweikardt and Thomas [START_REF] Matz | The monadic quantifier alternation hierarchy over graphs is infinite[END_REF][START_REF] Schweikardt | The monadic quantifier alternation hierarchy over grids and pictures[END_REF][START_REF] Matz | The monadic quantifier alternation hierarchy over grids and graphs[END_REF][START_REF] Matz | Expressive power of monadic logics on words, trees, pictures, and graphs[END_REF] have answered Question 1 positively for MSO over 2-dimensional picture languages: the quantifier alternation is strict at each level for MSO on 2-picture languages in pixel representation (and, as a consequence, is also strict over the class of finite graphs).

Their proof is essentially based on the fact that, for any positive integer k, there is a function f k : N → N (defined as a fixed height tower of exponentials) such that the set of rectangular grids of format n × f k (n) (i.e, of width n and length f k (n)) can be defined by some Σ k MSO sentence but cannot be defined by some Σ k-1 MSO sentence.

So, the hierarchy result essentially rests on the (more than exponential) imbalance between the two dimensions of the rectangular grid.

In view of this result a natural question arises: Is the MSO-alternation hierarchy strict for square picture languages (or equivalently, well-balanced picture languages)? The only thing we know is that the class EMSO = REC d is not closed under complement: notice non-Mirror d ∈ EMSO but we have proved Mirror d EMSO.

Question 2: Hierarchies for number of second-order quantifiers

The answer is totally known and uniform for picture languages of any dimension. In all cases, the hierarchy collapses at its first level. More precisely, Thomas [START_REF] Thomas | Classifying regular events in symbolic logic[END_REF] has established that every EMSO sentence over words is equivalent to a sentence whose monadic quantifier prefix consists of a single existential quantifier. Matz [START_REF] Matz | One quantifier will do in existential monadic second-order logic over pictures[END_REF] has proved the same result over 2-pictures in the pixel representation. (This strongly contrasts with a result by Otto [START_REF] Otto | A note on the number of monadic quantifiers in monadic Σ 1 1[END_REF] who proves a strict hierarchy at each level for the number of monadic quantifiers in EMSO over graphs.)

The proof of Matz can be extended (with the same arguments and slight adaptations) to any dimension d, for both pixel and coordinate representations. In other words, in both representations, all the logical classes -essentially ESO(arity d) and ESO(∀ k , arity d) -we have studied over picture languages of any dimension are not modified by the requirement there should be only one ESO relation symbol. The main difference is that this latter result involves the existential second-order logic with functions (ESOF) instead of or in addition to relations and holds in all kinds of structures without restriction: pictures, structures of any arity and any type, etc. It is also interesting and maybe surprising to notice that, in those results, the time degree d of a RAM computation plays the same role as the dimension d + 1 of the time-space diagram of a linear time bounded computation for a d-dimensional cellular automaton.

Both results attest of the robustness of the time complexity classes NTIME ram (n d ) and NLIN d ca . They stress the significance of the RAM's as a sequential model, and of the cellular automata as a parallel model. Also, note that such machine-independent characterizations of complexity classes for linear time or other time bounds defined up to a constant factor are rather rare in the literature: as other examples in finite model theory we only know the logical characterization of linear time of nondeterministic Turing machines by Lautemann et al. [START_REF] Lautemann | A logical characterisation of linear time on nondeterministic turing machines[END_REF] and the algebraic characterization of linear time of deterministic RAM's by Grandjean and Schwentick [START_REF] Grandjean | Machine-independent characterizations and complete problems for deterministic linear time[END_REF].

REC 1 =-

 1 REG = ESO(arity 1) = ESO(var 1) = ESO(∀ 1 , arity 1) and NLIN 1 ca = ESO(var 2) = ESO(∀ 2 , arity 2) are established in a unique framework for words. Let us now justify our distinct frameworks for any larger dimension d > 1. Coordinate representation does not fit REC d : The class of recognizable d-picture languages cannot be naturally characterized in logic with coordinate representation because of the following strict inclusions established in Section 9.2: ESO(var d -1) REC d ESO(var d).

-Question 2 :Theorem 10 . 6 .

 2106 d . Pixel representation does not fit NLIN d ca : We will prove in Section 9.2 the following sequence of strict inclusions for pixel representation of d-pictures and d > 1: ESO(var 1) NLIN d ca ESO(var 2) This justifies that no logic of the form ESO(var k) -or, equivalently, ESO(∀ k , arity k)) -, for any k, can characterize the class NLIN d ca for pixel representation. Strict hierarchies. Our final result (see Section 10) is a strict hierarchy result for d-languages represented by coordinate structures. It shows some subtile relationships between the number of first-order variables and the arity of the ESO relation symbols. For each integer d ≥ 2 and for d-languages represented by coordinate structures, the following (strict) inclusions hold: REC d ESO(var d) = ESO(∀ d , arity d) ESO(∀ d+1 , arity d) ⊆ NLIN d ca = ESO(var d + 1) = ESO(∀ d+1 , arity d + 1) Theorem 10.6 straightforwardly yields the following separation result: ESO(var d) ESO(arity d)

Definition 2 . 1 .

 21 A d-dimensional picture or d-picture on Σ is a function p : [n] d → Σ where n is a positive integer. The set dom(p)= [n] d is called the domain of picture p and its elements are called points, pixels or cells of the picture. A set of d-pictures on Σ is called a d-dimensional picture language, or d-language, on Σ.

Definition 3 . 1 .

 31 By Γ we denote the alphabet Γ ∪ { } where is a special symbol not in Γ. Let p be any dpicture of domain [n] d on Γ. The bordered d-picture of p, denoted by p , is the function p : [0, n + 1] d → Γ defined by p (a) = p(a) if a ∈ dom(p) ; p (a) = otherwise.Here, "otherwise" means that a is on the border of p , that is, some component a i of a is 0 or n + 1.

1. L ∈ REC d ; 2 .

 2 pixel d (L) ∈ ESO(∀ 1 , arity 1); 3. pixel d (L) ∈ ESO(arity 1).

Remark 4 . 1 .

 41 By definition, the space used by a d-dimensional cellular automaton is exactly the space (set of cells) occupied by its input d-picture.

Proposition 4 . 2 (

 42 folklore). For any dimension d and every d-picture language L, the following conditions are equivalent: 1. L is recognized in linear time by a nondeterministic d-dimensional two-way cellular automaton; 2. L is recognized in linear time by a nondeterministic d-dimensional one-way cellular automaton; 3. L is recognized in real time by a nondeterministic d-dimensional two-way cellular automaton (with either above Moore or von Neumann neighborhoods); 4. L is recognized in real time by a nondeterministic d-dimensional one-way cellular automaton (with either above neighborhoods).

Definition 4 . 4 .

 44 For each a = (a 1 , . . . , a d ) ∈ {0, 1} d , let us define the a-domain as Dom a = [0, a 1 ] × • • • × [0, a d ]. The a-neighborhood of some pixel x ∈ [n] d in position a in a picture p : [n] d → Γ is the function p a,x : Dom a → Γ defined as p a,x (b) = p(x + b), where x + b denotes the sum of the vectors x and b.

Figure 1 :

 1 Figure1: pixels x, y, z and t are, respectively, in position (1, 1), (0, 1), (1, 0), and (0, 0). Whence their associated neighborhoods, which appear as colored pixels on the figure.

  Such neighborhoods are used to describe the "transition function" of the cellular automata that we now define: Definition 4.5. A one-way nondeterministic d-dimensional cellular automaton (d-automaton, for short) over an alphabet Σ is a tuple A = (Σ, Γ, δ, F), where• the finite alphabet Γ called the set of states of A includes the input alphabet Σ and the set F of accepting states: Σ, F ⊆ Γ;• δ is the (nondeterministic) transition function of A: it is a family of a-transition functions δ = (δ a ) a∈{0,1} d of the form δ a : neighb a (Γ) → P(Γ).

Definition 4 . 6 .

 46 Let A = (Σ, Γ, δ, F) be a d-automaton and p, p : [n] d → Γ be two d-pictures on Γ. We say that p is a successor of p for A, denoted by p ∈ A(p), if, for each position a ∈ {0, 1} d and each point x of position a in [n] d , p (x) ∈ δ a (p a,x ). The set of j th -successors of p for A, denoted by A j (p), is defined inductively:A 0 (p) = {p} and, for j ≥ 0, A j+1 (p) = p ∈A j (p) A(p ).Definition 4.7. A computation of a d-automaton A = (Σ, Γ, δ, F) on an input d-picture p : [n] d → Σ is a sequence p 1 , p 2 , p 3 , . . . of d-pictures such that p 1 = p and p i+1 ∈ A(p i ) for each i. The picture p i , i ≥ 1, is called the i th configuration of the computation. A computation is accepting if it is finite -it has the form p 1 , p 2 , . . . , p k for some k -and the cell of minimal coordinates, 1 d = (1, . . . , 1), of its last configuration is in an accepting state: p k (1 d ) ∈ F. Definition 4.8. Let A = (Σ, Γ, δ, F) be a d-automaton and let T : N → N be a function such that T (n) > n. A d-picture p on Σ is accepted by A in time T (n) if A admits an accepting computation of length T (n) on p. That means there exists a computation p = p 1 , p 2 , . . . , p T

Theorem 9 . 1 .

 91 For any d > 0 and any d-language L, L ∈ NLIN d ca ⇔ coord d (L) ∈ ESO(var d + 1).

Proposition 4 . 10 .

 410 For any d > 0 and any d-language L, L ∈ NLIN d ca ⇒ coord d (L) ∈ ESO(var d + 1). Proof. Let L ∈ NLIN d ca . By Proposition 4.2, we can assume without loss of generality that L is recognized by a d-automaton A = (Σ, Γ, δ, F) in real time, i.e. in time n+1. The ESO(var d +1)-sentence to be constructed is of the form ∃(R s ) s∈Γ ∀x∀t ψ(x, t), where ψ(x, t) is a quantifier-free formula such that: -ψ uses a list of exactly d + 1 first-order variables x = (x 1 , . . . , x d ) and t. Intuitively, the d first ones represent the coordinates of any point in dom(p) = [n] d and the last one represents any of the first n instants t ∈ [n] of the computation (the last instant n + 1 is not explicitly represented); -ψ uses, for each state s ∈ Γ, a relation symbol R s of arity d + 1. Intuitively, R s (a 1 , . . . , a d , t) holds, for any a = (a 1 , . . . , a d ) ∈ [n] d and any t ∈ [n], iff the state of cell a at instant t is s.

  ν∈N 1 ) expresses there exists p n+1 ∈ A(p n ) such that p n+1 (1 d ) ∈ F. Therefore, we have proved that, for any d-picture p on Σ, the structure coord d (p) satisfies the ESO(var d + 1)-sentence ∃(R s ) s∈Γ ∀x∀t ψ(x, t) if and only if A has an accepting computation p = p 1 , p 2 , . . . , p n+1 of length n + 1 on p, i.e. A accepts p in time n + 1, or, by definition, p ∈ L. Hence, L ∈ ESO(var d + 1), as required.

Theorem 5 . 1 .

 51 For any d > 0, ESO(var d) = ESO(∀ d , arity d) on coordinate structures.This theorem will result from the forthcoming Proposition 5.2 and Proposition 5.4. The former states that each formula of ESO(var d) can be written in such a way that its first-order part is prenex, universal, with no more than d universal quantifiers. With the latter, we rewrite each formula of ESO(∀ d ) in such a way that the arity of each guessed relation symbol of the formula is at most d. 5.1. Skolemization Proposition 5.2. For any d > 0, ESO(var d) ⊆ ESO(∀ d ) on coordinate structures of any dimension.

Proposition 5 . 4 .

 54 For any d > 1, ESO(∀ d ) ⊆ ESO(∀ d , arity d) on coordinate structures.

Definition 6 . 3 .

 63 Let n, d > 0 and x ∈ [n] d . (i) We denote by [x] i the i th component of x. E.g. (5, 7, 2) 2 = 7.

(

  iii) S(d) stands for the set of permutations of {1, . . . , d}. Given pairwise distinct α 1 , . . . , α d in {1, . . . , d}, we denote by α 1 . . . α d the permutation α ∈ S(d) that maps each i on α i . Conversely, for α ∈ S(d) we set α i := α(i). By T (d) we denote the set of transpositions of {1, . . . , d}. Finally, for k ≤ d we write I(k, d) for the set of injections from {1, . . . , k} into {1, . . . , d}.

( v )

 v For α ∈ S(d) and n > 0, we set [α] = {x ∈ [n] d s.t. x α ↑}. Clearly, [n] d = α∈S(d) [α]. Beside, denoting by id the identity on {1, . . . , d}, we get x ∈ [id] iff x↑ and therefore x ∈ [α] iff x α ∈ [id].

Definition 6 . 4 .

 64 Let k, d be two integers such that d ≥ k ≥ 1. A sentence over coordinate structures for kpictures is in ESO(∀ d , arity d, half-sorted ) if it is of the form ∃R∀xψ(x) where 1. R is a list of relation symbols of arity d; 2. ψ is a quantifier-free formula whose list of first-order variables is x = (x 1 , . . . , x d ); 3. each atom of ψ is of one of the following forms: (a) Q s (x ι ), where s ∈ Σ and ι is an injection from [k] into [d], (b) R(x) or R(x (i) ) where R ∈ R and i ∈ [d], (c) min(x i ) or max(x i ), for i ∈ [d]. Proposition 7.7 state the equality ESO(∀ d , arity d) = ESO(∀ d , arity d, half-sorted ) on coordinate pictures while Proposition 8.6 completes the process of normalization by stating the equality ESO(∀ d , arity d, half-sorted ) = ESO(∀ d , arity d, sorted )

2 .

 2 Here again, each ESO relation symbol R of the original sentence Φ in ESO(∀ d , arity d) is replaced byor, intuitively, "divided into"d! new ESO relation symbols R α of the same arity d. Here, α ranges over permutations of the set of indices [d]. The intended meaning of each relation R α is the following: for each tuple (a 1 , . . . , a d ) ∈ [n] d such that a 1 ≤ a 2 . . . ≤ a d , we have R α (a 1 , . . . , a d ) = R(a α(1) , . . . , a α(d) ).

Fact 7 . 1 .

 71 On coordinate structures, any formula Φ = ∃R∀xϕ(x, R) ∈ ESO(∀ d , arity d) can be written in such a way that:(a) Each atomic subformula P(t 1 , . . . , t p ) of ϕ, where P is either an input or a guessed relation symbol, fulfills Var(t i ) ∩ Var(t j ) = ∅ for every 1 ≤ i < j ≤ p.(b) Each guessed relation symbol R ∈ R has arity d exactly.

Remark 7 . 2 .

 72 Considering this proof, we can sharpen the statement of Fact 7.1 by adding the following requirement: if the Q s 's have arity k ≤ d, (c) Each Q s -atom of Φ, for s ∈ Σ, has the form Q s (x ι 1 , . . . , x ι d-1 ) where ι ∈ I(k, d).

  each corresponding to a given permutation α of {1, . . . , d}. Definition 7.4. For R ⊆ [n] d and for each α ∈ S(d), we define a d-ary relation R α on [n] by: R α = {x ∈ [id] s.t. R(x α -1 )}. Alternatively, R α can be defined by: R α = {x α : x ∈ R ∩ [α]}. (Refer to Definition 6.3(v) for the meaning of notations [α] and [id].) Thus, Definition 7.4 associates with each R ⊆ [n] d a family (R α ) α∈S(d) of relations, each of which is entirely contained in the set [id]. This family is intended to represent R through its d! fragments according to the partition [n] d = α∈S(d) [α]. Namely, each R α encodes the fragment R ∩ [α] over [id].

Proposition 7 . 7 .

 77 For d > 1, ESO(∀ d , arity d) ⊆ ESO(∀ d , arity d, half-sorted ) on coordinate structures of dimension d -1. Proof. To simplify, assume we want to translate in ESO(∀ d , arity d, half-sorted ) some ESO(∀ d , arity d)formula of the very simple shape: Φ ≡ ∃R∀xϕ(x, R), where R is a (single) d-ary relation symbol, x is a d-tuple of first-order variables, and ϕ is a quantifier-free formula. Since the sets [α], α ∈ S(d), cover the domain [n], we obtain an equivalent rewriting of Φ with the following artificial relativization:

8 . 6 :

 86 on coordinate structures of dimension d -1, ESO(∀ d , arity d, half-sorted ) ⊆ ESO(∀ d , arity d, sorted ).

Lemma 8 . 1 .

 81 There exists an oriented tree T d covering G d that is rooted at id and such that each T d -path starting at id, say idα 1 . . . α p , corresponds to an alternated factorization of α p .Proof. Trees T d for d ≥ 2 are defined inductively. For d = 2, there is a unique such tree: (12) → (21) = (12)(21). So, assume we are given T d-1 and carry on the construction of T d as follows: (a) First, view each permutation α = α 1 . . . α d-1 ∈ S(d -1) as a permutation of {2, . . . , d} by renaming α i as α i + 1. That is, replace α = α 1 . . . α d-1 by α + = (α 1 + 1) . . . (α d-1 + 1). (b) Then, replace each such α + by β = β 1 . . . β d ∈ S(d) defined by: β 1 = 1 and β i = [α + ] i-1 = α i-1 + 1 for i > 1. Thus, T d-1 now covers the set of permutations β ∈ S(d) that fulfill [β] 1 = 1. (c) For each node β thus obtained, create a new node labelled by the composition of β with the transposition (1d) -that is by the permutation β(1d) -and create an edge β → β(1d). (d) Finally, link each such node β(1d) to d -2 new nodes β(1d)(di), for i = 2, . . . , d -1.

Proposition 8 . 6 .Theorem 8 . 7 .

 8687 Proof. (a) From α.i j = α(i j) and x αβ = (x α ) β (see Definition 6.3(iv)). (b) By induction on α:if α = id, then necessarily i = d and [x id.d j ] j = [x] d clearly holds. Otherwise, [x α.i j ] j = [(x α ) i j ] j = [x α ] i = [x] d ,by induction hypothesis. For any d > 1, ESO(∀ d , arity d, half-sorted ) ⊆ ESO(∀ d , arity d, sorted ) on coordinate structures of dimension d -1. Theorem 5.1, Proposition 7.7 and Proposition 8.6 can now be collected in the following result: For any d > 1, ESO(var d) = ESO(∀ d , arity d, sorted ) on coordinate structures of dimension d -1.

9 .Proposition 9 . 2 .

 992 Recapitulation of the results: power/limits of coordinate/pixel encodings 9.1. Characterization of NLIN ca After all the previous normalizations of logics over the coordinate encoding of pictures, we are now in a position to prove the expected characterization of NLIN ca . Theorem 9.1. For any d > 0 and any d-language L, L ∈ NLIN d ca ⇔ coord d (L) ∈ ESO(var d + 1). This theorem will straightforwardly proceed from Proposition 4.10, Theorem 8.7, and from Proposition 9.2 below: For any d > 0 and any d-language L, coord d (L) ∈ ESO(var d + 1) ⇒ L ∈ NLIN d ca .

9. 2 .

 2 Why do we need two encodings of pictures ? In Section 3, we have established natural characterizations of REC d for pixel encoding of pictures. The corresponding statements (Theorem 3.6 and Corollary 3.16) can be summed up as follows: for any d > 0 and any d-language L, L ∈ REC d ⇔ pixel d (L) ∈ ESO(∀ 1 , arity 1) ⇔ pixel d (L) ∈ ESO(arity 1) ⇔ pixel d (L) ∈ ESO(var 1).

9. 2 . 1 .

 21 Pixel representation does not fit NLIN d ca One can prove the following sequence of inclusions for pixel representation of d-picture languages with d > 1: ESO(var 1) = REC d NLIN d ca NTIME d ca (n d ) ⊆ ESO(var 2), where NTIME d ca (n d ) denotes the class of d-picture languages recognized by nondeterministic d-dimensional cellular automata in time O(n d ). Let us justify the (strict) inclusions that have not been proved beforehand in this paper.

  The implication L ∈ NTIME d ca (n d ) ⇒ pixel d (L) ∈ ESO(var 2) can be proved almost exactly as the particular implication L ∈ NLIN 1 ca ⇒ pixel d (L) ∈ ESO(var 2) among the recapitulated equivalences (34) above for word languages (adapt the proof of Proposition 4.10): consider the fact that a d-picture of side n contains n d pixels and use the implicit lexicographic successor function of the set of pixels induced by the d successor functions, exactly as we did in Section 3.3. Hence, the strict inclusions ESO(var 1) NLIN d ca ESO(var 2) so established justify that no logic of the form ESO(var k) -or, equivalently, ESO(∀ k , arity k)) -, for any k, can characterize the class NLIN d ca for pixel representation.

Fact 9 . 3 .

 93 pixel d (L) ∈ ESO(∀ 1 , arity 1) ⇔ coord d (L) ∈ ESO(∀ d , arity d, sorted ).

Proposition 9 . 7 .

 97 [d]. Because of the proximity of pixel encoding and coordinate encoding of a d-picture p : [n] d → Σ, it is easy to associate with each Φ ≡ ∃U∀x ϕ of the form displayed in (35), an ESO(∀ d , arity d, sorted )-formula Ψ on coordinate signature, in such a way that pixel d (p) | = Φ ⇔ coord d (p) | = Ψ. It suffices to set Ψ = ∃R∀xψ(x) where: • R is a list of d-ary relation symbols (R U ) U∈U , one-one associated with the unary relation variables U ∈ U ; • ψ(x) uses the list of d first-order variables x = (x 1 , . . . , x d ) and is obtained from ϕ(x) by the substitutions: For each integer d ≥ 2 and for d-languages represented by their coordinate structures, the following strict inclusions hold: ESO(var d -1) REC d ESO(var d).

1 .

 1 coord d (L) ∈ ESO(var (d -1)) ⇒ L ∈ REC d . This implication is a direct consequence of the equivalence L ∈ REC d ⇔ coord d (L) ∈ ESO(∀ d , arity d, sorted ) stated in Fact 9.4 and of the following equalities/inclusions, that hold on coordinate pictures of dimension d: ESO(var (d -1)) = ESO(∀ d-1 , arity (d -1)) ⊆ ESO(∀ d , arity d, sorted ). The equality has been proved in Theorem 5.1 ; the inclusion can be proved exactly as the inclusion stated in Proposition 8.6, that is: ESO(∀ d , arity d, half-sorted ) ⊆ ESO(∀ d , arity d, sorted ). Furthermore, the converse implication L ∈ REC d ⇒ coord d (L) ∈ ESO(var (d -1)) does not hold. To see this, consider the set L 1 of d-pictures p on Σ = {0, 1} whose pixels all contain symbol 1. Trivially, L 1 ∈ REC d . However, coord d (L 1 ) ESO(var (d -1)). Let us justify this last assertion. Intuitively, each sentence in ESO(var (d -1)) = ESO(∀ d-1 , arity (d -1)) can only express constraints about O(n d-1 ) pixels. More precisely, for any sentence ϕ ∈ ESO(∀ d-1 , arity (d -1)) over the d-coordinate Σ-signature, let the integer k be the maximal composition depth of the successor function in ϕ. Any atom of ϕ that involves an input relation symbol Q s , s ∈ Σ, is of the form Q s (τ 1 (x i 1 ), . . . , τ d (x i d )), for d terms τ j (x i j ), i j ∈ [d -1]. By the pigeonhole principle, at least two of those terms involve the same variable x i , i.e., there are two distinct indices 1 ≤ j < j ≤ d, such that i j = i j . For any d-picture p : [n] d → Σ, let D k (n) denote the set of pixels a = (a 1 , . . . , a d ) ∈ [n] d for which there are two coordinates a j , a j , 1 ≤ j < j ≤ d, at distance at most k: |a ja j | ≤ k. Of course, |D k (n)| = O(n d-1 ). It is easy to convince oneself that the sentence ϕ cannot control any pixel of p outside the O(n d-1 ) pixels of D k (n). That means that if two pictures p, p : [n] d → Σ coincide on those pixels, i.e. if p(a) = p (a) for every a ∈ D k (n), then coord d (p) | = ϕ ⇔ coord d (p ) | = ϕ. Clearly, such a sentence cannot define coord d (L 1 ).

ϕ 3 .

 3 Finally, Equivalence (38) is justified similarly as one shows that ESO(∀ d , arity d) = ESO(∀ d , arity d, half-sorted ), in Proposition 7.7. In order to prove the implication (36) and hence implication 1 ⇒ 2, it is sufficient to justify the following equivalence, for every d-picture p on Σ 0 d : coord d (p ) | = Φ fold ⇔ ∃p (p = p fold and coord d (p) | = Φ).

For a positive

  integer n, let L n = {p ∈ L : dom(p) = [n] d }. Notice that the number of pictures in L n is greater than 2 cn d , for some constant c, by item 3 of Lemma 10.4. Let L n be the set of pictures in L (on Γ) whose projections by π are in L n . The restriction of a picture p : [n] d → Γ to the "border set" 10 B n = {a ∈ [n] d : a↑ and (a d = (n + 1)/2 or a d = (n + 1)/2 + 1)} is called the border stripe of p . Let S n be the set of border stripes of pictures of L n . Clearly, |B n | ≤ 2n d-1 and then, |S n | ≤ |Γ| 2n d-1 . For n sufficiently large, we have 2 cn d > |Γ| 2n d-1

Theorem 10 . 6 .

 106 For each integer d ≥ 2 and for d-languages represented by coordinate structures, the following (strict) inclusions hold: REC d ESO(var d) = ESO(∀ d , arity d) ESO(∀ d+1 , arity d) ⊆ NLIN d ca = ESO(var d + 1) = ESO(∀ d+1 , arity d + 1)

6 .

 6 The above strict inclusion ESO(var d) ESO(∀ d+1 , arity d) trivially yields the following result. Corollary 10.7. For each integer d ≥ 2 and for d-languages represented by coordinate structures, we have the strict inclusion: ESO(var d) ESO(arity d). Remark 10.8. Corollary 10.7 surprisingly contrasts with the equality ESO(var 1) = ESO(arity 1) for dlanguages represented by pixels structures, see Theorem 3.6 and Corollary 3.16.

••

  Our logical normalization ESO(var k) = ESO(∀ k , arity k) holds for sets of structures of any arity d provided they are equipped with a successor function (explicitly given or implicitly defined), in particular the sets coord d (L) or pixel d (L), for a picture language L of any dimension d. Our main characterization result of d-picture languages with coordinate encoding coord d (L) ∈ ESO(var d + 1) ⇔ L ∈ NLIN d ca also holds (with the same proofs) for all dimensions k > d; that means, for any d-picture language L and all k > d, the set of coordinate structures coord d (L) is definable in ESO(var k) iff L is recognized in time O(n) by some nondeterministic cellular automaton of dimension k -1, i.e. of set of cells [n] k-1 . The previous result is essentially due to the normalization result ESO(∀ k , arity k) = ESO(∀ k , arity k, sorted ) that holds for all structures of arity d equipped with a successor function, provided k > d, and is false for k ≤ d, as we have shown for k = d.

[n 1 ]

 1 × • • • × [n d ] → Σ. "Most general" means as much general as they make sense in the logical or complexity theoretical framework involved. 11.4.1. REC d and logical characterizations in pixel encodings. All our characterizations of REC d for pixel encodings (see Section 3) hold for pictures of general prototype p : [n 1 ] × • • • × [n d ] → Σ, without any restriction, i.e. for all n i ≥ 1, i ∈ [d]. Moreover, our proofs also hold without change, except, of course, the references to integer n which should be replaced by integer n i according to the involved dimension i ∈ [d]. 11.4.2. NLIN d ca and logical characterizations in coordinate encodings. The definition of linear time complexity of d-automata is not clear for input pictures whose domain has the general form [n 1 ] × • • • × [n d ] without restriction. However, linear time, i.e. time O(n), makes sense when the n i are of the same order Θ(n), i.e. the pictures are "well-balanced". This justifies the following definition. Definition 11.2. A d-picture language L is well-balanced if there is some constant positive integer c such that the domain [n 1 ] × • • • × [n d ] of each picture p ∈ L fulfills the condition: for i ∈ [d], n ≤ c n i , where n = max(n 1 , . . . , n d ) is called the length of p; we say that the picture p (resp. the picture language L) is c-balanced. It is straightforward to adapt our notion of linear time to well-balanced picture languages. Definition 11.3. A c-balanced d-picture language L belongs to NLIN d ca if there exist a d-automaton A and a linear function T (n) = c 1 n + c 2 such that L is the set of c-balanced d-pictures p accepted by A in time T (n), where n is the length of p. Remark 11.4. These notions are justified by the following points:

Definition 11 . 5 .Remark 11 . 6 .

 115116 With each d-picture p of length n, one associates its squared d-picture, denoted by p = , of domain [n] d obtained by putting the new special symbol in each additional cell. Formally, p = (a) = p(a) if a ∈ dom(p); otherwise. With any d-picture language L one associates its squared d-picture language, L = = {p = : p ∈ L}. Let c be a constant. If p is a c-balanced d-picture, then the size of its squared picture p = is |p = | = Θ(|p|)

2 .

 2 Is there a strict hierarchy of the classes ESO(arity d) and ESO(∀ k , arity d) according to the number of ESO relation symbols? 11.5.1. Question 1: Hierarchies for second-order quantifier alternation

11. 6 .

 6 Logical characterizations of complexity classes for linear time or time bounds defined up to a constant factor Notice that Theorem 9.1 that characterizes the linear time complexity class of nondeterministic cellular automata is very similar to the following result about time complexity O(n d ), for any d ≥ 1, of nondeterministic RAMs, by the present authors [28]: NTIME ram (n d ) = ESOF(var d) = ESOF(∀ d , arity d).

  Because of the last item of Definition 3.2, one can also write: L is recognizable if there exist a surjective function π : Γ → Σ and d sets ∆ 1 , . . . , ∆ d ⊆ (Γ ) 2 such that

Definition 3.4. A d-language L on Σ is recognizable if it is the projection (i.e. homomorphic image) of a local d-language over an alphabet Γ. It means there exist a surjective function π : Γ → Σ and a local d-language L loc on Γ such that L = {π(p) : p ∈ L loc }.

where of course π(p) means π • p.

  , a picture p : [n] d → Σ belongs to L iff it results from a π-renaming of a picture p ∈ L(∆ 1 , . . . , ∆ d ). It means there exists a Γ-labeling of p (that is, a tuple (Q s ) s∈Γ of subsets of [n] d ) corresponding to a picture of L(∆ 1 , . . . , ∆ d ) (i.e. fulfilling ∀x ψ ∆ 1 ,...,∆ d (x, (Q s ) s∈Γ )) and from which the actual Σ-labeling of p (that is, the subsets (Q s ) s∈Σ ) is obtained via π. More precisely:

p ∈ L iff pixel d (p) | = Θ L , where:

Table 1 :

 1 Replacement of R-atoms by R 1 -or R 2 -atoms

  Proposition 9.7 states that the inclusion REC d ESO(var d) is strict. Also, the inclusion ESO(∀ d , arity d) ESO(∀ d+1 , arity d) is strict with the d-language sym d as a counterexample: Lemma 10.5 states that coord d (sym d ) ESO(∀ d , arity d), for all d ≥ 2; so, it only remains to prove coord d (sym d ) ∈ ESO(∀ d+1 , arity d). First, one can easily check that the first-order sentence ∀x 1 ∀x 2

A preliminary and much shorter version of this paper has appeared as a conference paper[START_REF] Grandjean | Descriptive complexity of picture languages[END_REF].

That means the scope of each negation is an atomic formula.

It is called one-way because each information can only be communicated along each coordinate in one direction, here the decreasing direction. At the opposite, each information can be communicated in both decreasing and increasing directions in the two-way case.

rather than τ i, j , as in the previous section.

That means: verify that the constraints of ψ(a, t) and ψ(a, t -1) (when t > 1) are satisfied together.

For Q s , it is also denoted Q s,α .

B n consists of two rows of pixels, the first one satisfying a d = (n + 1)/2 and a↑ in Rep n and the second one satisfying a d = (n + 1)/2 + 1 and a↑ in T n .

Acknowledgments

We warmly thank Gaétan Richard for a number of stimulating discussions and for having obtained in collaboration with us several results of this paper, in particular Proposition 4.10 and Proposition 5.2. The first author is grateful to Véronique Terrier for her suggestions, specially about the implicit links between cellular automata and recognizable picture languages, and for the many references to the literature she gave us. We also thank Oliver Matz for several interesting discussions and informations about recognizable picture languages and Nicolas Bacquey for having pointed us a mistake in a previous proof of Proposition 4.10.

Given a d-tuple x = (x 1 , . . . , x d ) of first-order variables, we denote by x -the (d -1)-tuple obtained from x by erasing its last component. That is, (x 1 , . . . , x d-1 , x d ) -:= (x 1 , . . . , x d-1 ).

In particular, for α ∈ S(d), we denote by x - α the (d -1)-tuple (x α 1 , . . . , x α d-1 ). Each (d -1)-tuple build upon the d variables x 1 , . . . , x d can clearly be written x - α for some α ∈ S(d). Therefore, the occurence of a non-sorted atom in Φ has the form Q(x - α ) for some Q ∈ (Q s ) s∈Σ and some α ∈ S(d), and the purpose of this section amounts to rewrite each such occurence Q(x - α ) as Q (x) for some well chosen relation Q .

Definition 8.3. Given a (d -1)-ary relation Q and two family of d-ary relations, (T α ) α∈S(d) and (Q α ) α∈S(d) , we say that (T α , Q α ) α∈S(d) is a d-simulation of Q if the following axioms hold, for any α ∈ S(d) and any i, j ≤ d such that α.i j is defined, and for any d-tuple x of variables:

(A 2 ) T α.i j (x) = T α.i j (x (i j) ).

(A 6 ) Q α.i j (x) doesn't depend on [x] j .

Lemma 8. [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]. Let (T α , Q α ) α∈S(d) be a d-simulation of some (d -1)-ary predicate Q. For any x ∈ [n] d and α ∈ S(d):

Proof. Let us first prove that for any x ∈ [n] d and α ∈ S(d):

We proceed by induction on α. If α = id, [START_REF] Grohe | Locality of order-invariant first-order formulas[END_REF] follows from (A 1 ). Given a non-identique permutation α.i j, we have: T α.i j (x α.i j ) = T α.i j ((x α ) (i j) ) by Fact 8.2-(a).

= T α.i j (x α ) by (A 2 ).

But [x

Therefore we can resume the above sequence of equalities with:

This completes the proof of [START_REF] Grohe | Locality of order-invariant first-order formulas[END_REF] Let us now prove the equality Q α (x α ) = Q(x -). If α = id, the result comes from (A 4 ). For a non-identique permutation α.i j, we have to prove Q α.i j (x α.i j ) = Q(x -) for any tuple x ∈ [n] d . First notice that we can restrict without loss of generality to the case where [x] d = 0. Indeed, we can otherwise consider the tuple y obtained from x by setting [x] d to 0. (That is, y only differs from x by its d th component, which is null.) Clearly, y -= x -. Besides, the j th component of x α.i j is [x] d , from Fact 8.2-(b). Similarly, the j th component of y α.i j is [y] d . Hence, the tuples x α.i j and y α.i j coincide on each component of rank distinct from j. Therefore Q α.i j (x α.i j ) = Q α.i j (y α.i j ) by (A 6 ) and we get:

The proof is complete.

.

Proof. Clearly, the formula (F i ) is a mere transcription of the axiom (A i ) for each i 2. We have to prove that (F 2 ) implies (A 2 ). Formula (F 2 ) yields that T α.i j (x) has the same value on tuples of the form

for any c ≤ min{n -1x, y}, where x + c (resp. yc) is the component of rank i (resp. j) of x. (That is:

In other words, the value of T α.i j (x) depends on [x] i + [x] j rather than on the precise values of these two components. As a consequence, for any u ∈

and any x, y ∈ [n]:

This is Axiom (A 2 ).

It remains to prove that such relations (T α ) α∈S(d) and (Q α ) α∈S(d) exist for every Q. To see this, assume we are given a (d -1)-ary relation Q and define the Q α 's and the T α 's as follows:

We leave it to the reader to check that the sequence (T α , Q α ) α∈S(d) satisfies the formulas (F 1 ), . . . , (F 6 ) (and hence, is a d-simulation of Q).

-

This definition clearly gives rise to a formula Ψ that belongs to ESO(∀ d , arity d, sorted ). Furthermore, it immediatly yields the expected equivalence

To conclude the proof, it remains to verify that each ESO(∀ 1 , arity 1)-formula can be written in ESO(∀ 1 , arity 1, sorted ), on pixel structures. We leave it to the reader.

Mixing Fact 9.3 with the first equivalence in [START_REF] Hella | Notions of locality and their logical characterizations over finite models[END_REF], we immediatly get:

But requiring the sentence to be sorted seems rather artificial. In the characterization of NLIN ca (Theorem 9.1), we admitted this constraint as a necessary step of the proof, but it was crucial, in our point of view, that Theorem 8.7 provides us with a mean to circumvent it. What about the present case ? Can the sorted constraint be dropped in Fact 9.4 ? The forthcoming Proposition 9.7 will show that it cannot. In order to prove it, we first state a simple lemma about the so-called Mirror d language.

Definition 9.5. For d ≥ 2, we denote by Mirror d the set of pictures p :

(Remember that ( 12) is the transposition that swaps 1 an 2. Therefore, a [START_REF] Fagin | Monadic generalized spectra[END_REF] is the tuple a in which the two first components have been interchanged -see Definition 6.3(iv). E.g., [START_REF] Cook | A hierarchy for nondeterministic time complexity[END_REF][START_REF] Börger | The Classical Decision Problem[END_REF][START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF][START_REF] Courcelle | Graph structure and monadic second-order logic, a language theoretic approach[END_REF] [START_REF] Fagin | Monadic generalized spectra[END_REF] ) .

The statement "Mirror d REC d " can be proved by a reasoning very similar to that of Theorem 2.6 in Giammarresi et al. [START_REF] Giammarresi | Monadic second-order logic over rectangular pictures and recognizability by tiling systems[END_REF]. For sake of completeness, and because we will prove another adaptation of that result in Lemma 10.5, we now recall and adapt the proof explicitly. It essentially amounts to a counting argument. Let us sketch it: Assume that the language Mirror d is recognizable. Hence, it is the projection of a local language and can be written Mirror d = π(Loc) = {π(p) : p ∈ Loc}, for some local language Loc = L(∆ 1 , . . . , ∆ d ) over an alphabet Γ, and some surjection π : Γ → Σ (see Definition 3.4). To get a contradiction, the trick is to mix two distinct pictures p and q of Mirror d into another picture [p/q] whose "top part", i.e. the half-picture over the diagonal, is the top part of p, and whose "down part" (half-picture under the diagonal) is the down part of q. By definition, [p/q] does not belong to Mirror d . However, a locality and counting argument yields that it should belong to this language, a contradiction. In order to detail this argument, we introduce some preliminary notations.

Given n, d > 0, we define the three following subsets of [n] d : 5. For a picture language L, we set diag(L) = {diag(p) : p ∈ L}.

6. Given two d-pictures p, q : [n] d → Σ, we denote by [p/q] the picture defined as follows:

q(a) otherwise.

In other words, [p/q] is the picture that coincides with p on its top part and with q on its down part.

7. Given a d-language L we denote

Let's now come back to the Mirror language. We have assumed that Mirror d is the projection of a local language over Γ:

for sufficiently large n, we have for some

By the pigeonhole principle, this last inequality guarantees the existence of two pictures π(p), π(q) ∈ Mirror d n = π(Loc n ) (i.e. p, q ∈ Loc), such that:

Items (i) and (ii) clearly force [π(p)/π(q)] Mirror d . In the same time, we deduce from (ii) that [p/q] is tiled by (∆ 1 , . . . , ∆ d ), as p and q are. This is because for every j ∈ [d], any pair of j-adjacent points a, b ∈ [n] d :

• either are both in top([n] d ), where [p/q] coincides with p,

• or are both in down([n] d ), where [p/q] coincides with q,

• or are both in diag([n] d ), where [p/q] coincides both with p and q.

In all cases, the pattern [p/q](a), [p/q](b) is either p(a), p(b) or q(a), q(b) , hence belonging to (Remember that a is increasing, denoted by a↑, if

Notice that p → p fold is a one-one mapping from the set of d-pictures on Σ to the set of d-pictures on Σ 0 d that fulfill condition 2: p fold (a) = 0 if not a↑. All the information about p is contained in the part of p fold that consists of increasing pixels. For example, for d = 2, if a 1 ≤ a 2 , then the "folded point" p fold (a 1 , a 2 ) contains both p(a 1 , a 2 ) and p(a 2 , a 1 ), and p fold (a 2 , a 1 ) = 0. In other terms, all the information on p is gathered over the diagonal a 1 = a 2 , i.e. on the pixels (a 1 , a 2 ) of p fold such that a 1 ≤ a 2 . Definition 9.9. For any d-language L on Σ, its folded language is the d-language on Σ 0 d :

We now establish a simple correspondence between the coordinate encodings of p fold and p.

Lemma 9.10. For any d-picture p on Σ, any increasing point a ∈ dom(p), and every σ ∈ Σ d ,

Proof. Definitions 9.8 and 9.9 yield the following equivalences: for any d-picture p on Σ, any increasing point a ∈ dom(p), and any σ ∈ Σ d ,

Beside, for each α ∈ S(d), p fold (a

). This leads to the claimed equivalence.

The following proposition states the precise relationships between the logic ESO(∀ d , arity d) and the recognizable d-languages. Proposition 9.11. For any d ≥ 1 and any d-language L, the following assertions are equivalent:

Proof. 1 ⇒ 2 By Fact 9.4, one has to prove the implication

The proof is similar to that of the statement of Proposition 7.7:

The two proofs involve the same tools and similar formulas. Therefore, we essentially justify here the additional points. Let L be a d-language on Σ whose set of coordinate structures coord d (L) is defined by an ESO(∀ d , arity d) sentence Φ, that is Φ = ∃R∀x ϕ(x), where R is a set of relation variables of arity d and ϕ(x) is a quantifier-free formula whose list of first-order variables is x = (x 1 , . . . , x d ). The main idea is the following. Instead of associating families of d! relation symbols (R α ) α∈S(d) with the sole guessed relation symbols R ∈ R, we do the same for input relation symbols (also of arity d) Q s , s ∈ Σ. Thus, denoting Rel(ϕ) = {R, (Q s ) s∈Σ }, we associate with each (R, α) ∈ Rel(ϕ) × S(d) a d-ary relation symbol R α 6 , according to Definition 7.4. That is, we set:

Let's denote by ϕ fold (x) the conjunction of the following quantifier-free formulas:

where φα is obtained from ϕ by substituting R-atoms, for R ∈ Rel(ϕ), with some "sorted" R γ -atoms R γ (x) or R γ (x ( j) ), j ∈ [d], see Lemma 7.6. Let us now define the ESO(∀ d , arity d, sorted )-sentence

We claim that for every d-picture p on Σ, the following equivalence holds:

In this purpose, let us comment upon the above conjuncts ϕ 0 -ϕ 3 . Formulas ϕ 0 -ϕ 2 correspond to those displayed in Equation ( 25) of Proposition 7.7. Clearly, ϕ 0 and ϕ 1 express that in the folded picture p fold , all the informations are gathered in the "folded part" (the increasing pixels) while the other pixels contain 0.

Hierarchy results

We are now ready to prove some strict hierarchy results between the classes REC d , NLIN d ca and our logical classes.

For that purpose we will use the notion of "folded" language with Proposition ?? and the following "symmetric" language as a counterexample. where a sym(i) denotes the tuple a whose i th component a i is replaced by its "symmetric value" n + 1a i 7 .

In other words, the values p(a) are defined up to all possible permutations of coordinates and up to all possible symmetries a → a sym(i) .

There is another equivalent definition of language sym d that uses an equivalence relation on pixels. Proof. Assertion 1 is a straightforward consequence of Definitions 10.1 and 10.2. Assertion 2 easily follows from the following observation: for all integer u ∈ [n], exactly one of the following conditions holds: For simplicity (abuse) of notation, in case a↑, i.e., when p(a) is a constant mapping, the constant value p(a)(α) ∈ {0, 1} for all α ∈ S(d) is also denoted by p(a). So, L will be regarded as a d-language on alphabet Σ = {0, 1} (instead of alphabet Σ 0 d ) defined by clauses 1 and 2 above. In other words, the expression "p(a) is a constant mapping from S(d) to {0, 1}" is replaced in clause 1 by "p(a) ∈ {0, 1}". We have to prove that L is not recognizable. Our proof by contradiction is very similar to the proof of the same result for the d-language Mirror d (see Lemma 9.6).

Assume that L is recognizable, that is, L is the projection of some local d-language L on Γ by some function π : Γ → {0, 1}. Let us introduce the following notation: for two pictures, 8 For example, for d = 2, Rep n is the set of ordered pairs of integers (a 1 , a 2 ) such that 1 ≤ a 1 ≤ a 2 ≤ (n + 1)/2 and its cardinality is at least 1/2(n/2) 2 = 1/8 n 2 .

9 The fact that p(a) should be a constant function is a straightforward consequence of item 1 in the above Definition 10.1 of sym d .