Étienne Grandjean
email: etienne.grandjean@unicaen.fr

Théo Grente
email: theo.grente@unicaen.fr

Descriptive complexity for minimal time of cellular automata

Descriptive complexity may be useful to design programs in a natural declarative way. This is important for parallel computation models such as cellular automata, because designing parallel programs is considered difficult. Our paper establishes logical characterizations of the three classical complexity classes that model minimal time, called real-time, of one-dimensional cellular automata according to their canonical variants. Our logics are natural restrictions of the existential second-order Horn logic. They correspond to the three ways of deciding a language on a square grid circuit of side n according to the three canonical placements of an input word of length n on the grid. Our key tool is a normalization method that transforms a formula into an equivalent formula that literally mimics a grid circuit.

Introduction 1.Descriptive complexity and programming

There are two criteria of interest of a complexity class: it contains a number of "natural" problems that are complete in the class; it has machine-independent "natural" characterizations, usually in logic, i.e., in so-called descriptive complexity. The most famous example is Fagin's Theorem [START_REF] Fagin | Generalized first-order spectra and polynomial-time recognizable sets[END_REF], [START_REF] Libkin | Elements of Finite Model Theory[END_REF], which characterizes NP as the class of problems definable in existential second-order logic (ESO). Similarly, Immerman-Vardi's Theorem [START_REF] Libkin | Elements of Finite Model Theory[END_REF], [START_REF] Immerman | Descriptive complexity[END_REF] and Grädel's Theorem [START_REF] Grädel | Capturing complexity classes by fragments of secondorder logic[END_REF], [START_REF] Grädel | Finite Model Theory and Its Applications[END_REF] characterize the class P by first-order logic plus least fixedpoint, and second-order logic restricted to Horn formulas, respectively.

Another interest of descriptive complexity is that it allows to automatically derive from a logical description of a problem a program that solves it. This is particularly interesting for the design of parallel programs that is considered a difficult task. Typically, a number of algorithmic problems (product of integers, product of matrices, sorting, etc.) are computable in linear time on cellular automata (CA), a local and massively parallel model. For each such problem, the literature presents an "ad hoc" parallel and local algorithmic strategy and gives the program of the final CA in an informal way [START_REF] Fischer | Generation of primes by one-dimensional real-time iterative array[END_REF], [START_REF] Delorme | Signals on cellular automata[END_REF]. However, the problems in concern can be defined inductively in a natural way. For instance, the product of two integers in binary notation is simply defined by the classical Horner's method and one may hope to directly derive a parallel program from such an inductive process.

Descriptive complexity and linear time on cellular automata

The present paper is in some sense the sequel of a recent paper [START_REF] Bacquey | Definability by Horn Formulas and Linear Time on Cellular Automata[END_REF] (see also [START_REF] Grandjean | A logical approach to locality in pictures languages[END_REF]). First, [START_REF] Bacquey | Definability by Horn Formulas and Linear Time on Cellular Automata[END_REF] observes that the inductive processes defining the problems in concern (product of integers, product of matrices, sorting, etc.) are "local" and are naturally formalized by Horn formulas, that is by conjunctions of first-order Horn clauses. Therefore, the computation is nothing else than the classical resolution method on Horn clauses, as in Prolog and Datalog [START_REF] Libkin | Elements of Finite Model Theory[END_REF], [START_REF] Grädel | Finite Model Theory and Its Applications[END_REF], [START_REF] Abiteboul | Foundations of Databases[END_REF]. Moreover, on every concrete problem defined by a Horn formula with d + 1 first-order variables, this inductive computation by Horn rules can be geometrically modeled as the displacement of a d-dimensional hyperplan along some fixed line in a space of dimension d + 1. To capture these inductive behaviors, [START_REF] Bacquey | Definability by Horn Formulas and Linear Time on Cellular Automata[END_REF] defines a logic denoted monot-ESO-HORN d (∀ d+1 , arity d+1 ) obtained from the logic ESO-HORN tailored by Grädel [START_REF] Grädel | Finite Model Theory and Its Applications[END_REF] to characterize P, by restricting both the number of first-order variables and the arity of secondorder predicate symbols. Besides, it includes an additional restriction -the "monotonicity condition" -that reflects the geometrical consideration above-mentioned. [START_REF] Bacquey | Definability by Horn Formulas and Linear Time on Cellular Automata[END_REF] proves that this logic exactly characterizes the linear time complexity class of cellular automata: more precisely, for each integer d ≥ 1, a set L of d-dimensional pictures can be decided in linear time on a d-dimensional CA -written L ∈ DLIN d CA -if and only if it can be expressed in monot-ESO-HORN d (∀ d+1 , arity d+1 ). For short:

DLIN d CA = monot-ESO-HORN d (∀ d+1 , arity d+1 ). To summarize, expressing a concrete problem in this logicwhich seems an easy task in practice and also is a necessary and sufficient condition according to the above equalityguarantees that this problem can be solved in linear time on a CA; moreover, the Horn formula that defines the problem can be automatically translated into a program of CA that computes it in linear time.

Logics for minimal time of cellular automata?

At this point, two natural questions arise: 1) Besides linear time, a robust and very expressive complexity class, what are the other significant and robust complexity classes of CA? 2) Can we exhibit characterizations of those complexity classes in some naturally (syntactically) defined logics so that any definition of a problem in such a logic can be automatically translated into a program of the complexity in concern?

Besides linear time, the main complexity notion wellstudied for a long time in the literature of CA is real-time, i.e., minimal time [START_REF] Cole | Real-time computation by n-dimensional iterative arrays of finite-state machine[END_REF], [START_REF] Smith | Real-time language recognition by one-dimensional cellular automata[END_REF], [START_REF] Dyer | One-way bounded cellular automata[END_REF]. A cellular automaton is said to run in real-time if it stops, i.e., gives the answer yes or no, at the minimal instant when the elapsed time is sufficient for the output cell (the cell that gives the answer) to have received each letter of the input. Real-time complexity appears as a sensitive/fragile notion and one generally thinks it is so for CA of dimension 2 or more [START_REF] Terrier | Two-dimensional cellular automata recognizer[END_REF], [START_REF] Grandjean | Differences between 2d neighborhoods according to real time computation[END_REF]. However, maybe surprisingly, one knows that real-time complexity is a robust notion for one-dimensional CA in the following sense: according to the many natural variants of the definition of a one-dimensional CA, which essentially rest on the choice of the neighborhood of the CA and the parallel or sequential presentation of its input word, exactly three real-time classes of one-dimensional CA 1 have been proved to be distinct [START_REF] Cole | Real-time computation by n-dimensional iterative arrays of finite-state machine[END_REF], [START_REF] Choffrut | On real-time cellular automata and trellis automata[END_REF], [START_REF] Ibarra | On one-way cellular arrays[END_REF], [START_REF] Poupet | Cellular automata: Real-time equivalence between onedimensional neighborhoods[END_REF]:

1) RealTime CA = RealTime OIA ; 2) Trellis = RealTime OCA ; 3) RealTime IA .
The final and decisive step to establish this classification is a nice dichotomy of [START_REF] Poupet | Cellular automata: Real-time equivalence between onedimensional neighborhoods[END_REF] on admissible neighborhoods 2 of CA, which can be rephrased as follows: for each neighborhood N admissible with respect to the first cell as output cell, the real-time complexity class of one-dimensional CA with parallel input mode and neighborhood N ,

• either is equal to the real-time class for the neighborhood {-1, 0, 1}, i.e., RealTime CA (class 1 above),

• or is equal to the real-time class for the neighborhood {-1, 0}, i.e., Trellis (class 2 above).

Further, it is surprising to notice that • the mutual relations between those three real-time classes are wholly elucidated: classes Trellis and RealTime IA are mutually incomparable for inclusion whereas we have the strict inclusion Trellis ∪ RealTime IA RealTime CA [START_REF] Cole | Real-time computation by n-dimensional iterative arrays of finite-state machine[END_REF], [START_REF] Čulík | Systolic trellis automata. I[END_REF], [START_REF] Terrier | Language not recognizable in real time by one-way cellular automata[END_REF],

• while it is unknown whether the trivial inclusion RealTime CA ⊆ DLIN 1 CA is strict; worse, even whether the inclusion RealTime CA ⊆ LinSpace is strict is an open problem!

Logics and grid circuits for real-time classes

Each of the three real-time classes 1-3 is robust, i.e, is not modified for many variants of CA (change of neighborhoods, etc.) and has two or three quite different equivalent definitions. For example, RealTime CA is equal to the linear time class of one-way CA with parallel input mode. Similarly, [START_REF] Okhotin | On the equivalence of linear conjunctive grammars and trellis automata[END_REF] has proved the surprising result that Trellis is the class of languages generated by linear conjunctive grammars (see also [START_REF]Conjunctive and boolean grammars: The true general case of the context-free grammars[END_REF]) and [START_REF] Terrier | Characterization of real time iterative array by alternating device[END_REF] has established that a language L is in RealTime IA if and only if its reverse language L R is recognized in real time by an alternating automaton with one counter.

Logics have two nice and complementary properties: they are flexible, hence expressive; they have normal forms, hence can be tailored for efficient programming. The main idea that led us to conceive the different logics for realtime classes can be summarized by the following simple question: what are the different ways to decide a language on a square grid circuit? For any integer n ≥ 1, let C n be the grid circuit n × n where the state q ∈ Q (for finite Q) of any site (i, j), 1 ≤ i, j ≤ n, is determined by the states of its 1. By default, a CA has a two-way communication and a parallel input mode. Any CA (resp. one-way CA or OCA) with sequential input mode is also called an iterative array or IA (resp. OIA).

2. The neighborhood of a CA is the finite set of integers N such that the state of any cell x at any non-initial instant t is determined by the states of the cells x + d, for d ∈ N , at instant t -1. A neighborhood is admissible with respect to a fixed output cell (in general the first or the last cell) if it allows to communicate each bit of the input to the output cell. "predecessors" (i -1, j), if it exists (i > 1), and (i, j -1), if it exists (j > 1), so that the output cell is the site (n, n). Up to symmetries, there are three canonical ways 3 to arrange an input word w = w 1 . . . w n of length n on the grid C n , see Figure 1: 1) GRID 1 : place the input on any side (or, equivalently, on both sides) that does (do) not contain the output cell; 2) GRID 2 : place the input on the diagonal opposite to the output cell; 3) GRID 3 : place the input on the diagonal that contains the output cell. A simple (reversible) deformation transforms a grid circuit of GRID i , i = 1, 2, 3, into a time-space diagram of a CA of the real-time class i in concern (recall: 1: RealTime CA ; 2: Trellis; 3: RealTime IA ), and conversely. More precisely, to characterize the three real-time classes, we define three sub-logics of the Horn logic that characterizes linear time of one-dimensional CA (DLIN 1 CA = monot-ESO-HORN 1 (∀ 2 , arity 2 )), called respectively pred-ESO-HORN, incl-ESO-HORN and pred-dio-ESO-HORN (defined in the next section), and we prove the following equalities:

1

) pred-ESO-HORN = GRID 1 = RealTime CA 2) incl-ESO-HORN = GRID 2 = Trellis 3) pred-dio-ESO-HORN = GRID 3 = RealTime IA
To establish the double nature of our three logics and deduce the previous equalities 1-3, we present each logic in two forms:

• we define it the largest possible, showing the extent of its expressiveness;

• we prove for it the most restricted normal form. In each case, a formula in normal form can be translated literally into a grid program, which is essentially a CA of the real-time complexity class in concern.

Structure of the paper: In preliminaries, we recall the classical definitions of one-dimensional cellular automata and of their real-time classes and define our three logics with an example of a problem naturally expressed in such a logic. Section 3 establishes how each of our logics can be normalized. Using these normal forms we show in Section 4 that our three logics exactly characterize the three real-time complexity classes and also -for inclusive logic -the class of linear conjunctive languages of Okhotin [START_REF] Okhotin | On the equivalence of linear conjunctive grammars and trellis automata[END_REF]. Section 5 gives conclusive remarks.

Preliminaries

Cellular automata and real-time complexity

A cellular automaton in one dimension is a tape of cells (each cell is a finite automaton) indexed by Z. Each cell takes a value from a finite set of states and the cells evolve synchronously along a discrete time scale. The evolution of the cell c is done according to a transition function which takes as input the state of the cell itself and the states of its neighbors at the previous time step and outputs a new state for the cell.

Definition 1 (cellular automaton). A cellular automaton is defined by a 5-tuple

(Q, Σ, Q accept , N , δ) where Q is a finite set of states, Σ ⊂ Q is the input alphabet, Q accept ⊂ Q is the set of accepting states, the neighborhood N is a finite ordered subset of Z and δ is the transition function from Q |N | to Q.
c, t = δ( c + v, t -1 : v ∈ N ).
Definition 2 (real time language acceptance). Cellular automata can act as language acceptors. In this case cellular automata work on a finite set of cells indexed by [1, n] where n is the size of the input word w = w 1 . . . w n , one of this cells is also chosen as the output cell (usually one of the border cells). A word w is said to be accepted by an automaton in real-time if its output cell enters an accepting state immediately after getting all the information from w.

The language accepted by a cellular automaton A in realtime (denoted by L(A)) is the set of all its accepted words in real-time.

Convention (permanent state, quiescent state).

All the cells of index outside [1, n] are in the permanent state ♯. Without information from the input a cell of index [1, n] is in the quiescent state λ.

The real-time computation power of a CA only depends on its communication scheme. That is fully determined by the following three specifications: the way the input is fed to the automaton, the way the cells communicate (depending on the neighborhood) and the output cell. The input is usually fed to the automaton in a parallel way: the i th bit of the input is given to the i th cell at the start of the computation. The input can also be fed in a sequential way: the i th bit of the input is given to the first cell at time i for which we add a specific transition function δ input . Usually the output cell is the first cell for two-way communications and the last one for one-way communication.

CA have their input fed in a parallel way and the cells communicate in two-way mode (N = {-1, 0, 1}). One-way cellular automata (OCA) and iterative arrays (IA) are two natural variants of CA. OCA are narrowed on the way the cells communicate: the information is only transmitted from left to right (N = {-1, 0}). The input mode of IA is no more parallel but sequential. Definition 3 (RealTime CA ). The class RealTime CA is the set of languages accepted by real-time CA with a parallel input, the neighborhood N = {-1, 0, 1} and the first cell as the output cell.

The class RealTime CA is equivalent to RealTime OIA , the set of languages accepted by one-way IA with sequential input running in real-time with neighborhood N = {-1, 0} and the last cell as the output cell.

Definition 4 (Trellis). The class Trellis is the set of languages accepted by trellis automata or equivalently by OCA running in real-time with a parallel input, the neighborhood N = {-1, 0} and the last cell as the output cell. The space-time diagrams of these real-time classes are depicted in Figure 2.

Our logics

The "local" nature of our logics requires that the underlying structure encoding an input word w = w 1 . . . w n on its index interval [1, n] = {1, . . . , n} only uses the successor and predecessor functions and the monadic predicates min and max as its only arithmetic functions/predicates: Definition 6 (structure encoding a word). Each nonempty word w = w 1 . . . w n ∈ Σ n on a fixed finite alphabet Σ is represented by the first-order structure

w := ([1, n]; (Q s ) s∈Σ , min, max, suc, pred)
of domain [1, n], monadic predicates Q s , s ∈ Σ, min and max such that Q s (i) ⇐⇒ w i = s, min(i) ⇐⇒ i = 1, and max(i) ⇐⇒ i = n, and unary functions suc and pred such that suc(i) = i + 1 for i < n and suc(n) = n, pred(i) = i -1 for i > 1 and pred(1) = 1. Let S Σ denote the signature {(Q s ) s∈Σ , min, max, suc, pred} of structure w . The monadic predicates Q s , s ∈ Σ, min, and max of S Σ are called input predicates.

Let x + k and xk abbreviate the terms suc k (x) and pred k (x), for a fixed integer k ≥ 0.

Let us now define two of our logics: Definition 7 (predecessor logics). A predecessor Horn formula (resp. predecessor Horn formula with diagonal inputoutput) is a formula of the form Φ = ∃R∀x∀yψ(x, y) where ψ is a conjunction of Horn clauses on the variables x, y, -of signature S Σ ∪ R (resp. S Σ ∪ R ∪ {=}) where R is a set of binary predicates called computation predicates, -of the form δ 1 ∧ . . . ∧ δ r → δ 0 where the conclusion δ 0 is either a computation atom R(x, y) with R ∈ R, or ⊥ (False) and each hypothesis δ i is either an input literal/conjunction of one of the forms:

• Q s (x -a), Q s (y -a) (resp. Q s (x -a) ∧ x = y), for s ∈ Σ and an integer a ≥ 0, • U (x -a), ¬U (x -a), U (y -a)
or ¬U (ya), for U ∈ {min, max} and an integer a ≥ 0, or a computation atom of the form S(xa, yb) or S(yb, xa), for S ∈ R and some integers a, b ≥ 0.

Let pred-ESO-HORN (resp. pred-dio-ESO-HORN) denote the class of predecessor Horn formulas (resp. predecessor Horn formulas with diagonal input-output) and, by abuse of notation, the class of languages they define.

The formulas of the "predecessor" logics defined above use the predecessor function but not the successor function: both logics inductively define problems in increasing both coordinates x and y. The inductive principle of our last logic is seemingly different: it lies on inclusions of intervals [x, y].

Definition 8 (inclusion logic

). An inclusion Horn formula is a formula of the form Φ = ∃R∀x∀yψ(x, y) where ψ is a conjunction of Horn clauses of signature S Σ ∪R∪{=, ≤, <} where R is a set of binary predicates called computation predicates, of the form x ≤ y ∧ δ 1 ∧ . . . ∧ δ r → δ 0 where the conclusion δ 0 is either a computation atom R(x, y) with R ∈ R, or the atom ⊥ (False), and each hypothesis δ i is 1) either an input literal of the form 4 U (x + a), ¬U (x + a), U (y + a) or ¬U (y + a), for U ∈ {(Q s ) s∈Σ , min, max} and an integer a ∈ Z, 2) or the (in)equality x = y or x < y 5 , 3) or a conjunction of the form

S(x + a, y -b) ∧ x + a ≤ y -b
for a computation atom S(x+a, y -b), with S ∈ R and some integers a, b ≥ 0.

Let incl-ESO-HORN denote the class of inclusion Horn formulas and, also, the class of languages they define. Note that the "inclusion" meaning of logic incl-ESO-HORN is given by hypotheses x ≤ y and x + a ≤ yb. It means that the inductive computation of each value R(x, y), for x ≤ y and R ∈ R, only use values of the form S(x + a, yb), for S ∈ R and an included interval

[x + a, y -b] ⊆ [x, y].
Notation: We will freely use the intuitive abbreviations x > a, x = a, for a constant integer a ≥ 1, and x ≤ na, x < na, x = na, for a constant integer a ≥ 0, and similarly for y. For example, x > 3 is written in place of ¬min(x-2) and y ≤ n-2 is written in place of ¬max(y+1). Technical remarks about our logics: Without loss of generality, we can suppose that each clause having a hypothesis atom of the form S(xa, yb) or S(yb, xa), for a, b ≥ 0, has also the hypotheses x > a (if a > 0) and y > b (if b > 0). The same for each hypothesis atom of the form Q s (xa) or Q s (yb), for a, b > 0. Similarly, we assume that each clause with a hypothesis of the form Q s (x + a) (resp. Q s (y + a)), with a > 0, also contains the hypothesis x ≤ na (resp. y ≤ na). Similarly, for each atom S(x + a, yb), for a, b ≥ 0.

Comparing the input presentation in our logics: The presentation of the input is more restrictive in Definition 7 of predecessor logics than in that of inclusion logic (Definition 8) because we have forbidden the use of the successor function for uniformity/aesthetics. However, allowing the same largest set of input literals (¬)U (x + a), (¬)U (y + a), 4. Without loss of generality, assume that there is no negation over a predicate Qs.

5. Then, the hypothesis x ≤ y is redundant.

for U ∈ {(Q s ) s∈Σ , min, max} and a ∈ Z, does not modify the expressive power of predecessor logics: steps 5 and 6 of the normalization of inclusive logic in Section 3 can be easily adapted to predecessor logics.

Using our logics for programming: an example

We now give an example of a natural problem expressed in one of our logics. The language notBordered is the set of all words w ∈ Σ + with no proper prefix equal to a proper suffix:

notBordered = {w | ∀w ′ such that w = w ′ u = vw ′ , w ′ = ǫ or w ′ = w}.
This language can be defined by Φ notBordered := ∃Border∀x∀yψ of pred-ESO-HORN where ψ is the conjunction of the following clauses where Border(x, y) means w 1 . . . w x = w y-x+1 . . . w y (see Figure 3): So, as a consequence of this paper, notBordered belongs to RealTime CA . In fact, more is known [START_REF] Terrier | Language not recognizable in real time by one-way cellular automata[END_REF]:

1) min(x)∧¬min(y)∧Q s (x)∧Q s (y) → Border(x, y) 2) ¬min(x)∧¬min(y)∧Border(x-1, y-1)∧Q s (x)∧ Q s (y) → Border(x, y), for all s ∈ Σ; 3) max(y) ∧ Border(x, y) → ⊥. If Border(x, y) is true when y is maximal, then w 1 . . . w x = w n-x+1 . . .
⊥ Q s (x) ∧ Q s (y) Border(x, y) ⊥ the "false"
notBordered ∈ RealTime CA \ (TREILLIS ∪ RealTime IA ).

Normalizing our logics

The most difficult and main parts of the proofs of our descriptive complexity results, i.e., equalities 1-3 of Subsection 1.4, are the following normalization lemmas. They are key ingredients because our normalized formulas can be literally simulated by grids and finally by CA of the corresponding real-time classes.

Lemma 1 (normalization of predecessor logics). Each formula

Φ ∈ pred-ESO-HORN (resp. Φ ∈ pred-dio-ESO-HORN) is equivalent to a formula Φ ′ ∈ pred-ESO-HORN (resp. Φ ′ ∈ pred-dio-ESO-HORN) normalized as follows: each clause of Φ ′ is of one of the following forms: • input clause of the form, for s ∈ Σ and R ∈ R: min(x) ∧ min(y) ∧ Q s (y) → R(x, y), or min(x) ∧ ¬min(y) ∧ Q s (y) → R(x, y) (resp. x = y ∧ min(x) ∧ Q s (x) → R(x, y), or x = y ∧ ¬min(x) ∧ Q s (x) → R(x, y)). • the contradiction clause, for a fixed R ⊥ ∈ R: max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥; • computation clause of the form δ 1 ∧ . . . ∧ δ r → R(x, y), for R ∈ R, where each hypothesis δ i is a conjunction of the form S(x -1, y) ∧ ¬min(x) or S(x, y -1) ∧ ¬min(y), for S ∈ R.
Let normal-pred-ESO-HORN (resp. normal-pred-dio-ESO-HORN) denote the class of formulas (languages) so defined.

Lemma 2 (normalization of inclusion logic). Each formula Φ ∈ incl-ESO-HORN is equivalent to a formula Φ ′ ∈ incl-ESO-HORN normalized as follows: each clause of Φ ′ is of one of the following forms: y), where R ∈ R and where each hypothesis δ i is a computation atom of either form S(x + 1, y) or S(x, y -1), for S ∈ R.

• input clause of the form x = y ∧ Q s (x) → R(x, y), for s ∈ Σ and R ∈ R; • the contradiction clause, for a fixed R ⊥ ∈ R, min(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥; • computation clause of the form 6 x < y ∧ δ 1 ∧ . . . ∧ δ r → R(x,
Let normal-incl-ESO-HORN denote the class of formulas (resp. languages) so defined.

Proof of the normalization lemmas 1 and 2

The normalization processes of our three logics are quite similar each other; further, some steps are exactly the same. Therefore, we choose to present here below the successive normalization steps for one logic: pred-ESO-HORN. Afterwards, we will succinctly describe how those steps should be adapted for the two other logics.

Proof of Lemma 1: Normalization of predecessor Horn formulas. Let a formula Φ ∈ pred-ESO-HORN. For simplicity of notation, we first assume that the only computation atoms of Φ are of the form R(x-a, y -b), a, b ≥ 0 (no atom of the form R(yb, xa)). We will show at the end of the proof how to manage the general case. Φ will be transformed into an equivalent normalized form Φ ′ by a sequence of 10 steps: 1) Processing the contradiction clauses; 2) Processing the input; 3) Restriction of computation atoms to R(x -1, y), R(x, y -1), and R(x, y); 4) Elimination of atoms x > a, x = a, y > a, y = a; 5) Processing of min and max; 6) Defining equality and inequalities; 7) Folding of the domain; 8) Deleting max in the initialization clauses; 9) From initialization clauses to input clauses; 10) Elimination of atoms R(x, y) as hypotheses.

In each of these 10 steps, we will introduce new (binary) computation predicates, to be added to the set R of existentially quantified predicates, and new clauses to define them.

1) Processing the contradiction clauses: Without loss of generality, one can assume there is the only contradiction clause max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥. Indeed, each contradiction clause ℓ 1 ∧ . . . ∧ ℓ k → ⊥ can be equivalently replaced by the conjunction of computation clauses

ℓ 1 ∧ . . . ∧ ℓ k → R ⊥ (x, y) with the clause R ⊥ (x, y) → ⊥
where R ⊥ is a new computation predicate (intuitively, always false). However, in place of the previous clause, we "delay" the contradiction, by propagating predicate R ⊥ 6. Note that the hypothesis x < y is equivalent to the expected inequality

x + 1 ≤ y or x ≤ y -1.
till point (n, n), thanks to the conjunction of the "transport" clauses R ⊥ (x -1, y) ∧ ¬min(x) → R ⊥ (x, y) and R ⊥ (x, y -1) ∧ ¬min(y) → R ⊥ (x, y) and of the unique contradiction clause max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥ required by the normal form.

2) Processing the input: The idea is to make available the letters of the input word only on the sides x = 1 and y = 1 of the square {(x, y) ∈ [1, n] 2 }, this by carrying out their transport thanks to new "transport" predicates W x s and W y s , for s ∈ Σ, inductively defined by the following clauses:

• initialization clauses Q s (x) ∧ min(y) → W x s (x, y) and Q s (y) ∧ min(x) → W y s (x, y); • transport clauses W x s (x, y -1) ∧ ¬min(y) → W x s (x, y) and W y s (x -1, y) ∧ ¬min(x) → W y s (x, y). By transitivity, these clauses imply clauses Q s (x) → W x s (x, y) and Q s (y) → W y s (x, y).
In other words, the minimal model of the conjunction of those clauses that expands structure w satisfies equivalences ∀x∀y (W x s (x, y)

⇐⇒ Q s (x)) and ∀x∀y (W y s (x, y) ⇐⇒ Q s (y)).
This justifies the replacement of the input atoms of form Q s (xa) and Q s (y -b) by the respective atoms W x s (xa, y) and W y s (x, yb) in all the clauses, except in the initialization clauses.

3) Restriction of computation atoms to R(x -1, y), R(x, y -1), R(x, y): The idea is to introduce new "shift" predicates R x-a , R y-b and R x-a,y-b , for fixed integers a, b > 0 and R ∈ R: typically, we define the predicate R x-a,y-b that intuitively satisfies the equivalence R x-a,y-b (x, y) ⇐⇒ R(x -a, y -b). Let us suggest the method by an example. Assume we have initially the Horn clause

x > 3 ∧ y > 2 ∧ R(x -2, y -1) ∧ S(x -3, y -2) → T (x, y).
This clause is replaced by the clause

x > 3 ∧ y > 2 ∧ R x-2 (x, y -1) ∧ S x-2,y-2 (x -1, y)) → T (x, y),
for which the predicates R x-1 and R x-2 are defined by the clauses

x > 1 ∧ R(x -1, y) → R x-1 (x, y) and x > 2 ∧ R x-1 (x -1, y) → R x-2 (x, y) which imply x > 2 ∧ R(x -2, y) → R x-2 (x, y) and then x > 2 ∧ y > 1 ∧ R(x -2, y -1) → R x-2 (x, y -1)
, and the predicates S x-1 , S x-2 , S x-2,y-1 and S x-2,y-2 defined by the respective clauses:

x > 1 ∧ S(x -1, y) → S x-1 (x, y), x > 2 ∧ S x-1 (x -1, y) → S x-2 (x, y), x > 2 ∧ y > 1 ∧ S x-2 (x, y -1) → S x-2,y-1 (x, y), and x > 2 ∧ y > 2 ∧ S x-2,y-1 (x, y -1) → S x-2,y-2 (x, y), which imply together the clause x > 2 ∧ y > 2 ∧ S(x -2, y -2) → S x-2,y-2 (x, y) and then also x > 3 ∧ y > 2 ∧ S(x -3, y -2) → S x-2,y-2 (x -1, y).
Remark 1. Atoms on min and x are of the forms min(x-a) or ¬min(xa) for a ≥ 0, or, equivalently, x = a + 1 or x > a + 1. Besides, for each integer a ≥ 1, the atom max(xa) is false. Therefore, one may consider that the only literals on x involving min or max are of the form min(x), ¬min(x), max(x), ¬max(x), x = a, x > a, for an integer a > 1, and similarly, for y. 4) Elimination of atoms x > a, x = a, y > a, y = a: By recurrence on integer a ≥ 1, let us define the binary predicates R x>a (and, similarly,

R x=a , R y>a , R y=a ) whose intuitive meaning is x > a (resp. x = a, y > a, y = a). The predicate R x>1 is defined by the clause ¬min(x) → R x>1 (x, y). For a > 1, let us define R x>a from R x>a-1 by the clause R x>a-1 (x -1, y) ∧ ¬min(x) → R x>a (x, y). By recurrence on integer a ≥ 1, these clauses imply x > a → R x>a (x, y).
This justifies the replacement of the atoms x > a and x = a, for a > 1, by R x>a (x, y) and R x=a (x, y), respectively, and similarly for y in place of x.

After step 4, the only literals involving min or max are (¬)min(x), (¬)max(x), (¬)min(y), (¬)max(y).

5) Processing of min and max:

To each literal η(x) of the form min(x), ¬min(x), max(x) or ¬max(x), associate the new binary predicate R η(x) defined by the conjunction of the initialization clause η(x) ∧ min(y) → R η(x) (x, y) and of the transport clause R η(x) (x, y -1) ∧ ¬min(y) → R η(x) (x, y). Do similarly for the literals η(y) ∈ {(¬)min(y), (¬)max(y)}. This justifies we replace each such literal η(x) (resp. η(y)) by the "equivalent" atom R η(x) (x, y) (resp. R η(y) (x, y)) in all the clauses, except in the above initialization clauses and in the contradiction clause or in case η(x) (resp. η(y)) is ¬min(x) (resp. ¬min(y)) and is joined to a hypothesis of the form R(x -1, y) (resp. R(x, y -1)).

Recapitulation: After step 5 each clause is of one of the following forms:

1) an initialization clause of one of the two forms:

• initialization for x = 1: min(x) ∧ η(y) → R(x, y) with η(y) ∈ {(Q s (y)) s∈Σ , (¬)min(y), (¬)max(y)}; • initialization for y = 1: min(y) ∧ η(x) → R(x, y) with η(x) ∈ {(Q s (x)) s∈Σ , (¬)min(x), (¬)max(x)}; 2) "the" contradiction clause max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥;
3) a computation clause of the form δ 1 (x, y) ∧ . . . ∧ δ r (x, y) → R(x, y), where each hypothesis δ i is of one of the three forms R(x, y), R(x -1, y) ∧ ¬min(x), R(x, y -1) ∧ ¬min(y).

In fact, without loss of generality, we can assume that each computation clause is of one of the following forms:

a) S(x -1, y) ∧ ¬min(x) → R(x, y); b) S(x, y -1) ∧ ¬min(y) → R(x, y); c) S(x, y) ∧ T (x, y) → R(x, y).
Justification of the assumption: "Decompose" each computation clause into clauses of forms (a,b,c) by introducing new intermediate predicates. For example, the computation clause y) is "equivalent" to the conjunction of the following clauses using new predicates R 5 , R 6 , R 7 :

R 1 (x -1, y) ∧ ¬min(x) ∧ R 2 (x, y -1) ∧ ¬min(y) ∧ R 3 (x, y) → R 4 (x,
R 1 (x -1, y) ∧ ¬min(x) → R 5 (x, y); R 2 (x, y -1) ∧ ¬min(y) → R 6 (x, y); R 5 (x, y) ∧ R 6 (x, y) → R 7 (x, y); R 7 (x, y) ∧ R 3 (x, y) → R 4 (x, y).
We now plan to fold the square domain {(x, y) ∈ [1, n] 2 } along the diagonal x = y on the over-diagonal triangle

T n = {(x, y) ∈ [1, n] 2 | x ≤ y}.
This requires to first define equality and inequalities.

6) Defining equality and inequalities:

Let us jointly define the predicates R = and R pred of intuitive meaning R = (x, y) ⇐⇒ x = y and R pred (x, y) ⇐⇒ x -1 = y by the following clauses:

min(x) ∧ min(y) → R = (x, y); ¬min(x) ∧ R = (x -1, y) → R pred (x, y); ¬min(y) ∧ R pred (x, y -1) → R = (x, y).
Then define the predicate R < such that R < (x, y) ⇐⇒ x < y with the two clauses ¬min(y

) ∧ R = (x, y -1) → R < (x, y) and ¬min(y) ∧ R < (x, y -1) → R < (x, y). Define similarly the predicate R ≤ such that R ≤ (x, y) ⇐⇒ x ≤ y with the two clauses min(x) ∧ min(y) → R ≤ (x, y) and ¬min(x) ∧ R < (x -1, y) → R ≤ (x, y).
For easy reading, we will freely write x = y, x < y and x ≤ y in place of the atoms R = (x, y), R < (x, y) and R ≤ (x, y), respectively. 7) Folding of the domain: Let us fold the square domain

{(x, y) ∈ [1, n] 2 } along the diagonal x = y on the over- diagonal triangle T n = {(x, y) ∈ [1, n] 2 |
x ≤ y} so that each point (y, x) such that x ≤ y is sent to its symmetrical point (x, y) ∈ T n . For that purpose, let us associate to each predicate R ∈ R a new (inverse) predicate R inv whose intuitive meaning is the following: for each x ≤ y, we have R inv (x, y) ⇐⇒ R(y, x). So, each clause C will be replaced by two clauses: the first one is the restriction of C to the triangle T n ; the second one is the folding on T n of the restriction of C to the under-diagonal triangle using predicates R inv . Finally, we will express that each R ∈ R coincides with its inverse R inv on the fold x = y.

Folding the initialization clauses: Each initialization clause of the form min(x) ∧ η(y) → R(x, y) (with η(y) ∈ {Q s (y)|s ∈ Σ} ∪ {(¬)min(y), (¬)max(y)}) applies to the line x = 1 which is included in the triangle T n and consequently it should be unchanged in the folding; in contrast, each initialization clause of the form

min(y) ∧ η(x) → R(x, y) (with η(x) ∈ {Q s (x)|s ∈ Σ} ∪ {(¬)min(x), (¬)max(x)}) is replaced by its folded version min(x) ∧ η(y) → R inv (x, y).
Folding the computation clauses: Let us describe how to fold the clauses (a) or (b) (folding clauses (c) is easy):

• Folding of clauses (a): A clause of the form S(x -1, y) ∧ ¬min(x) → R(x, y) is equivalent to the conjunction of clauses i) x ≤ y ∧ S(x -1, y) ∧ ¬min(x) → R(x, y) and ii) x > y ∧ S(x -1, y) ∧ ¬min(x) → R(x, y). Notice that clause (i) applies to the triangle T n since x ≤ y implies x -1 < y: therefore, clause (i) should be left unchanged. Clause (ii) is equivalent (by exchanging variables x and y) to the clause y > x ∧ S(y -1, x) ∧ ¬min(y) → R(y, x) whose folded (equivalent) form on T n is x < y ∧ S inv (x, y -1) ∧ ¬min(y) → R inv (x, y) since x < y implies x ≤ y -1.

• Folding of clauses (b): Similarly, a clause of the form S(x, y -1) ∧ ¬min(y) → R(x, y) is equivalent to the conjunction of clauses x < y ∧S(x, y -1)∧¬min(y) → R(x, y)

and x ≤ y ∧ S inv (x -1, y) ∧ ¬min(x) → R inv (x, y).
Folding the contradiction clause: Clearly, it is harmless to confuse the (contradiction) predicate R ⊥ and its inverse (R ⊥ ) inv ; consequently, the contradiction clause itself max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥ is its own folded version.

The diagonal fold: Finally, for each R ∈ R, the following two clauses mean that R coincides with its inverse R inv on the diagonal:

x = y ∧ R(x, y) → R inv (x, y); x = y ∧ R inv (x, y) → R(x, y).
Recapitulation: By a careful examination of the set of clauses obtained after steps 1-7, we can check that each of them is of one of the following forms:

1) an initialization clause of the form: min(x) ∧ η(y) → R(x, y) with η(y) ∈ {Q s (y)|s ∈ Σ} ∪ {(¬)min(y), (¬)max(y)}; 2) "the" contradiction clause max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥; 3) a computation clause of one of the following forms:

(a

) x ≤ y ∧ S(x -1, y) ∧ ¬min(x) → R(x, y); (b) x < y ∧ S(x, y -1) ∧ ¬min(y) → R(x, y); (c) x ≤ y ∧ S(x, y) ∧ T (x, y) → R(x, y); (d) x = y ∧ S(x, y) → R(x, y).

8) Deleting max in the initialization clauses:

The idea is to consider in parallel for each point (x, y) the case where the hypothesis max(y) holds and the contrary case where the negation ¬max(y) holds. For that purpose, we duplicate each computation predicate R in two new predicates denoted R y ←max and R y ←¬max . Intuitively, the atom R y ←max (x, y) (resp. R y ←¬max (x, y)) expresses the implication max(y) → R(x, y) (resp. ¬max(y) → R(x, y)).

Transforming the initialization clauses: According to the desired semantics of R y ←max and R y ←¬max , each initialization clause of the form min(x) ∧ max(y) → R(x, y) (resp. min(x) ∧ ¬max(y) → R(x, y)) should be rewritten as min(x) → R y ←max (x, y) (resp. min(x) → R y ←¬max (x, y)). Similarly, each initialization clause of the form min(x) ∧ η(y) → R(x, y), for η(y) ∈ {Q s (y)|s ∈ Σ} ∪ {(¬)min(y)} should be replaced by the conjunction of the following two clauses: min(x)∧η(y) → R y ←max (x, y) and min(x)∧η(y) → R y ←¬max (x, y).

Transforming the computation clauses: We describe it for each above form (a-d).

• Each clause (a) x ≤ y ∧ S(x -1, y) ∧ ¬min(x) → R(x, y) is replaced by the "equivalent" conjunction of the follow-

ing two clauses x ≤ y ∧ S y ←max (x -1, y) ∧ ¬min(x) → R y ←max (x, y) and x ≤ y ∧ S y ←¬max (x -1, y) ∧ ¬min(x) → R y ←¬max (x, y). • Each clause (b) x < y ∧ S(x, y -1) ∧ ¬min(y) → R(x, y)
is "equivalent" to x < y ∧ S y ←¬max (x, y -1) ∧ ¬min(y) → R(x, y) since the hypothesis ¬max(y-1) always holds. Consequently, clause (b) should be replaced by the "equivalent" conjunction of the following two clauses:

x < y ∧ S y ←¬max (x, y -1) ∧ ¬min(y) → R y ←max (x, y) and x < y ∧ S y ←¬max (x, y -1) ∧ ¬min(y) → R y ←¬max (x, y). • Each clause (c) x ≤ y ∧ S(x, y) ∧ T (x, y) → R(x, y) is replaced by the "equivalent" conjunction of the following two clauses: x ≤ y ∧ S y ←max (x, y) ∧ T y ←max (x, y) → R y ←max (x, y) and x ≤ y ∧ S y ←¬max (x, y) ∧ T y ←¬max (x, y) → R y ←¬max (x, y). • Make a similar substitution for each above clause (d).

Processing the contradiction clause: Obviously, the contradiction clause max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥ is equivalent to the formula max(x) ∧ max(y) ∧ (max(y) → R ⊥ (x, y)) → ⊥ and should be rewritten as max(x) ∧ max(y) ∧ (R ⊥ ) y ←max (x, y) → ⊥, which is of the required form if the predicate (R ⊥ ) y ←max is renamed R ⊥ . 9) From initialization clauses to input clauses: The initialization clauses are now of the form min(x) → R(x, y) or min(x) ∧ η(y) → R(x, y), for η(y) ∈ {Q s (y)|s ∈ Σ} ∪ {(¬)min(y)}. By a separation in cases, it is easy to transform each of these clauses into an equivalent conjunction of input clauses of the required (normalized) forms:

min(x) ∧ min(y) ∧ Q s (y) → R(x, y); min(x) ∧ ¬min(y) ∧ Q s (y) → R(x, y).
After step 9, the formula obtained is of the claimed normal form, except that some computation clauses may have atoms R(x, y) as hypotheses. Our last step is to eliminate such hypotheses. 10) Elimination of atoms R(x, y) as hypotheses: The first idea is to group together in each computation clause the hypothesis atoms of the form R(x, y) and the conclusion of the clause. Accordingly, the formula can be rewritten in the form

Φ := ∃R∀x∀y[ i C i (x, y) ∧ i∈[1,k] (α i (x, y) → θ i (x, y))]
where the C i 's are the input clauses and the contradiction clause, and each computation clause is written in the form α i (x, y) → θ i (x, y) where α i (x, y) is a conjunction of formulas of the only forms R(x -1, y) ∧ ¬min(x), R(x, y-1)∧¬min(y), but not R(x, y), and θ i (x, y) is a Horn clause whose all the atoms are of the form R(x, y). The second idea is to "solve" the Horn clauses θ i (containing only atoms of the form R(x, y)) according to the input clauses and all the possible conjunctions of hypotheses α i that may be true. Notice the two following facts: the hypotheses of the input clauses are input literals and the conjuncts of the α i 's are of the only forms R(x -1, y) ∧ ¬min(x), R(x, y -1) ∧ ¬min(y). So, we can prove by induction on the sum x + y that the obtained formula Φ ′ which is a conjunction of clauses (whose hypotheses do include no atom of the form R(x, y) anymore) is equivalent to the above formula Φ. For a detailed proof, see the appendix.

General case: Steps 1-7 are easy to adapt in the general case where the initial formula may contain hypotheses of the form R(yb, xa). The new points are the following: step 3 restricts the computation atoms to four forms: R(x, y), R(y, x), R(x -1, y) and R(x, y -1); step 7 (folding the domain) is adapted so that it eliminates the atoms of the form R(y, x) by using the following equivalence for x ≤ y, R(y, x) ⇐⇒ R inv (x, y). See the details in the appendix. This achieves the proof of the normalization result pred-ESO-HORN = normal-pred-ESO-HORN.

Adaptation of steps 1-10 for normalization of predecessor Horn formulas with diagonal input-output: Step 1 is not modified. In step 2, the initialization clauses are now x = y ∧Q s (x) → W x s (x, y) and x = y ∧Q s (y) → W y s (x, y) whereas the transport clauses are not modified. Steps 3 to 5 and the recapitulation after step 5 are not modified either, except that now each initialization clause is of one of the three forms: 1) x = y ∧ Q s (x) → R(x, y); 2) min(x) ∧ η(y) → R(x, y), with η(y) ∈ {(¬)min(y), (¬)max(y)}; 3) min(y) ∧ η(x) → R(x, y), with η(x) ∈ {(¬)min(x), (¬)max(x)}.

Steps 6 and 7 (folding of the domain) and the recapitulation after step 7 are not modified either, except that now each initialization clause has one of the only forms 1 and 2 above.

Step 8 (deleting max in the initialization clauses) can be easily adapted according to those initialization clauses whose forms after step 8 are now restricted to 1) x = y∧Q s (x) → R(x, y); 2) min(x)∧min(y) → R(x, y); 3) min(x) ∧ ¬min(y) → R(x, y). Clause 2 can be replaced by the equivalent clause 2') x = y ∧ min(x) → R(x, y).

Step 9 (from initialization clauses to input clauses) is modified as follows. Define the predicates R min(x) , R min(y) and R ¬min(y) by the initialization clauses 4) x = y ∧ min(x) → R min(x) (x, y) and 5) x = y ∧ min(x) → R min(y) (x, y), and the computation clauses ¬min(y) ∧ R min(x) (x, y -1) → R min(x) (x, y), ¬min(y) ∧ R min(y) (x, y -1) → R ¬min(y) (x, y), and ¬min(y) ∧ R ¬min(y) (x, y -1) → R ¬min(y) (x, y). This allows to replace the initialization clause 3 by the computation clause R min(x) (x, y) ∧ R ¬min(y) (x, y) → R(x, y). After those transformations all the initialization clauses are of the form x = y ∧ Q s (x) → R(x, y) (clause 1 above) or x = y ∧ min(x) → R(x, y) (clauses 2', 4 and 5 above). By a separation in cases, it is easy to transform each of these clauses into an equivalent conjunction of input clauses of the required (normalized) forms:

x = y ∧ min(x) ∧ Q s (x) → R(x, y), or x = y ∧ ¬min(x) ∧ Q s (x) → R(x, y).
Step 10 (Elimination of atoms R(x, y) as hypotheses) and the end of the proof are the same as those for pred-ESO-HORN. This achieves the proof of the equality preddio-ESO-HORN = normal-pred-dio-ESO-HORN. Lemma 1 is proved.

Proof of Lemma 2: Normalization of inclusion Horn formulas. It divides into seven steps.

1) Processing the contradiction clauses:

Here again, we delay the contradiction and propagate the predicate R ⊥ till the point (1, n) by the conjunction of the computation clauses x < y ∧ R ⊥ (x + 1, y) → R ⊥ (x, y) and x < y ∧ R ⊥ (x, y -1) → R ⊥ (x, y) and of the unique contradiction clause min(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥.

2) Processing the input: We make available the letters of the input word on the only diagonal x = y by introducing new predicates W x+a s and W y+a s , for a ∈ Z, whose intuitive meaning is:

W x+a s (x, y) ⇐⇒ Q s (x + a) ∧ 1 ≤ x + a ≤ n (resp. W y+a s (x, y) ⇐⇒ Q s (y + a) ∧ 1 ≤ y + a ≤ n).
They are inductively defined by the following clauses:

• Initialization clauses (on the diagonal):

x = y ∧ Q s (x) → W x s (x, y); (x = y) ∧ Q s (x) → W y s (x, y); x = y ∧ Q s (x -a) ∧ x > a → W x-a s (x, y), and x = y ∧ Q s (x -a) ∧ x > a → W y-a s (x, y), for a > 0; x = y ∧ Q s (y + a) ∧ y ≤ n -a → W x+a s (x, y), and x = y ∧ Q s (y + a) ∧ y ≤ n -a → W y+a s (x, y), for a > 0. • Transport clauses, for a ∈ Z: x < y ∧ W x+a s (x, y -1) → W x+a s (x, y), and x < y ∧ W y+a s (x + 1, y) → W y+a s (x, y).
This allows to replace each input atom Q s (x + a) (resp. Q s (y + a)), a ∈ Z, by the computation atom W x+a s (x, y) (resp. W y+a s (x, y)), in all the clauses, except in the initialization clauses.

Note that after step 2 the atoms on input predicates Q s occur (see the initialization clauses above) always jointly with x = y and in the only three forms Q s (x), Q s (xa) (jointly with x > a), or Q(y + a) (jointly with y ≤ na), for a > 0.

3) Processing the min/max literals: One may consider that the only literals on x involving min or max are of the forms x = a, x > a, for an integer a ≥ 1, or x = n-a, x < n-a, for a ≥ 0, and similarly for y.

As we have done for the Q s , we want to make available the information about min and max, i.e., about extrema, on the only diagonal x = y. We introduce for that new computation predicates defined inductively: R x=a , R x>a , for a ≥ 1, and R x=n-a , R x<n-a , for a ≥ 0, and similarly for y, with obvious intuitive meaning: for instance, R y>a (x, y) ⇐⇒ y > a. For example, define the predicate R x=a (resp. R y=a ) by the two clauses x = y ∧ x = a → R x=a (x, y) and x < y∧R x=a (x, y-1) → R x=a (x, y) (resp. x = y ∧ x = a → R y=a (x, y) and x < y ∧ R y=a (x + 1, y) → R y=a (x, y)). As another example, define R x<n-a by the clauses x = y ∧ y < na → R x<n-a (x, y) and x < y ∧ R x<n-a (x, y -1) → R x<n-a (x, y).

This allows to replace the "extremum" atoms x = a, x > a, x = na, x < na by the respective computation atoms R x=a (x, y), R x>a (x, y), R x=n-a (x, y), R x<n-a (x, y), in all the clauses, except in the initialization clauses and in the contradiction clause. And similarly for y.

The important fact is that after step 3, the predicate min (resp. max) only occurs in the form x = a or x > a (resp. in the form y = na or y < na) and always occurs jointly with x = y, i.e., is only used on the diagonal. 4) Restriction of computation atoms to R(x + 1, y), R(x, y -1), and R(x, y): This is a variant of the similar step in the normalization of predecessor logics (step 3). We introduce now new "shift" predicates R x+a , R y-b and R x+a,y-b , for fixed integers a, b > 0 and R ∈ R, with easy interpretation and definitions. In particular, the intuitive interpretation of the predicate R x+a,y-b is: R x+a,y-b (x, y) ⇐⇒ x + a ≤ yb ∧ R(x + a, yb). As an example, the "normalized" clause x < y ∧ S x+2,y-2 (x + 1, y) → S x+3,y-2 (x, y) defines the predicate S x+3,y-2 from the predicate S x+2,y-2 .

Recapitulation: After step 4, one may consider that each clause is of one of the following forms (1-3):

1) an initialization clause x = y ∧ δ → R(x, y),
where δ is

• either an input atom Q s (x),
• or an equality x = a, for a fixed a ≥ 1, or y = nb, for a fixed b ≥ 0,

• or a conjunction Q s (x -a) ∧ x > a, or Q s (y + b) ∧ y ≤ n -b, for a, b ≥ 1;
2) a computation clause of one of the forms (a,b,c):

a) x < y ∧ S(x + 1, y) → R(x, y); b) x < y ∧ S(x, y -1) → R(x, y); c) x y ∧ S(x, y) ∧ T (x, y) → R(x, y), where ∈ {<, =}; 3) "the" contradiction clause min(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥, which can be rephrased x = 1 ∧ y = n ∧ R ⊥ (x, y) → ⊥.
Justification for initialization clauses: By separation in cases, one easily obtains the above three forms of initialization clauses.

Justification for computation clauses: Here again, "decompose" each computation clause in clauses of above forms (a,b,c) by introducing new intermediate predicates. For example, the computation clause y) is "equivalent" to the conjunction of the following clauses using new predicates R 4 , R 5 :

x < y ∧ R 1 (x + 1, y) ∧ R 2 (x, y -1) → R 3 (x,
x < y ∧ R 1 (x + 1, y) → R 4 (x, y); x < y ∧ R 2 (x, y -1) → R 5 (x, y); x < y ∧ R 4 (x, y) ∧ R 5 (x, y) → R 3 (x, y).
Steps 5 and 6 that follow lie on a generalization of the method used in step 8 of the normalization of predecessor logics above (eliminating max in the initialization clauses). Roughly expressed, for any computation predicate R ∈ R and a hypothesis η, we introduce a new predicate R η ← whose intuitive meaning is: R η ← (x, y) ⇐⇒ (η → R(x, y)). Transforming the initialization clauses: For each clause (c) x y ∧ S(x, y) ∧ T (x, y) → R(x, y), where ∈ {<, =}, add clauses that cumulate the hypotheses provided they are compatible. More precisely, for all a ∈ [1, A] and b ∈ [0, B] and any two compatible (possibly empty) subsets η, θ of the set of two hypotheses {x = a, y = n -b}, we have the clause

5) Elimination of equalities

Each initial- ization clause x = y ∧ x = a → R(x, y) (resp. x = y ∧ y = n -b → R(x, y)) is transformed into the clause x = y → R x=a ← (x, y) (resp. x = y → R y=n-b ← (x, y
x y ∧ S η ← (x, y) ∧ T θ ← (x, y) → R η∪θ ← (x, y). For example, x y ∧ S x=a ← (x, y) ∧ T y=n-b ← (x, y) → R x=a,y=n-b ← (x, y) and x y ∧ S y=n-b ← (x, y) ∧ T x=a,y=n-b ← (x, y) → R x=a,y=n-b ← (x, y).

Processing the contradiction clause: The contradiction clause is equivalent to

x = 1 ∧ y = n ∧ (x = 1 ∧ y = n → R ⊥ (x, y)) → ⊥.
Consequently, it should be replaced by the

clause x = 1∧y = n∧(R ⊥ ) x=1,y=n ← (x, y) → ⊥, which is the contradiction clause required if the predicate (R ⊥ ) x=1,y=n ← is renamed R ⊥ . 6) Elimination of atoms Q s (x -a), Q s (y + b) (a, b > 0):
This step is quite similar to previous step 5: it is described in the appendix.

Recapitulation: After step 6, all the initialization clauses are of the form x = y ∧ Q s (x) → R(x, y) as required 7 .

7) Elimination of atoms R(x, y) as hypotheses: This step is exactly similar to the corresponding step 10 of normalizing predecessor logics. This completes the proof of the equality incl-ESO-HORN = normal-incl-ESO-HORN, i.e., Lemma 2.

Equivalence between our logics and CA complexity classes

The communication scheme of real-time classes finds a natural expression in our normalized logics. The input clauses, the only clauses using unary predicates Q s , express the way the input is fed to the automaton. The computation clauses with a computation atom R(x, y), R ∈ R, as their conclusion simulate the computation of the CA. Deducing or not deducing the "false" by contradiction clauses means rejection or acceptance. Each of our normalized logics can be described graphically on a grid, indexed by [1, n] 2 (see Figure 1).

Encoding automata states by predicates

The set R of predicates that will be used in formulas expressing the computation of an automaton A, with Q the set of its states, is R = {R q | q ∈ Q}. The intuitive meaning of this predicates is the following: R q (c, t) is true ⇐⇒ the cell c is in the state q at time t.

7. Note that an initialization clause of the form x = y → R(x, y) can be rewritten s∈Σ (x = y ∧ Qs(x) → R(x, y)) (separation in cases).

Encoding predicates by automata states

Let Φ be a formula defining a language L, in one of our logics, of the form Φ = ∃R∀x∀yψ(x, y) with R = (R 1 , . . . , R m ) and R 1 = R ⊥ . The set of states that will be used by an automaton A accepting L is Q = {♯, λ}∪{0, 1} m with ♯ the permanent state and λ the quiescent state. We denote by (q) i (i ∈ [1, m]), the i th bit of a state q ∈ {0, 1} m . Intuitively, (q) i refers to the predicate R i . Since the predicate R 1 = R ⊥ represents the "false", the set of accepting states is the set of states q ∈ {0, 1} m with the first bit (q) 1 equal to 0, that is

Q accept = {0} × {0, 1} m-1 .

Logical characterization of RealTime CA

In this section, we will show that the languages accepted in real-time by two-way CA with input fed in a parallel way and output read on the first cell are exactly the languages defined by a formula of pred-ESO-HORN.

Theorem 1. RealTime CA = pred-ESO-HORN

The proof will use the following inclusion scheme:

pred-ESO-HORN = normal-pred-ESO-HORN ⊆ RealTime OIA = RealTime CA ⊆ pred-ESO-HORN
The equality pred-ESO-HORN = normal-pred-ESO-HORN has already been proved in Section 3 and the other equality RealTime OIA = RealTime CA is folklore in automata theory. Two inclusions are left to be proved.

Lemma 3. RealTime CA ⊆ pred-ESO-HORN

Proof. We will show that for each automaton A ∈ RealTime CA we can build a formula Φ ∈ pred-ESO-HORN such that: w ∈ L(A) ⇐⇒ w satisfies the formula Φ.

First of all, one can be easily convinced that the computation power of a CA A ∈ RealTime CA with neighborhood N A = {-1, 0, 1} is equal to the computation power of a OCA A ′ with neighborhood N A ′ = {-2, -1, 0} running within the same computation time n where n is the size of the input (see Figure 4). This transformation can be seen on the space-time diagram of A with the variable change: c → c + t -1, where c is the index of the cell and t the time step of the computation. This geometrical transformation does not change the computation power so that:

L(A) = L(A ′ ). w 1 w 2 w 3 w 4 w 5 A w 1 w 2 w 3 w 4 w 5 A ′ Figure 4. Neighborhood's change: from {-1, 0, 1} to {-2, -1, 0} Input: The parallel input of A ′ is expressed by the conjunction ψ input = s∈Σ (min(t) ∧ Q s (c) → R s (c, t))
for Σ the input alphabet: each cell c is in the state w c ∈ Σ at the start of the computation. Computation: The state evolution of a cell of A ′ is given by the transition function:

c, t = δ A ′ ( c -2, t -1 , c -1, t -1 , c, t -1 ).
A transition rule δ A ′ (q 2 , q 1 , q 0 ) = q for q 2 = ♯ is expressed by the computation clause:

c > t ∧ ¬min(t) ∧ R q2 (c -2, t -1) ∧ R q1 (c -1, t -1) ∧ R q0 (c, t -1) → R q (c, t).
The specific case where q 2 is the permanent state ♯ (δ A ′ (♯, q 1 , q 0 ) = q) is handled by the clause: c = t∧¬min(t)∧R q1 (c-1, t-1)∧R q0 (c, t-1) → R q (c, t).

We denote ψ compute the conjunction of the above two sets of clauses. Remark: By construction of ψ input and ψ compute , we have the following equivalence for ψ ′ := ψ input ∧ ψ compute . The computation atom R q (c, t) is true in the minimal model ( w , R) of ∀c∀tψ ′ (c, t) ⇐⇒ the cell c is in the state q at time t.

Output: The contradiction clauses express the output on the last cell:

ψ output := q∈Q\Qaccept (max(c) ∧ max(t) ∧ R q (c, t) → ⊥)
The formula ψ expressing the computation of A ′ is the conjunction ψ := ψ ′ ∧ ψ output .

For each word w = w 1 . . . w n ∈ Σ + we have the following equivalences:

The cell 1 of A is in an accepting state q at time n ⇐⇒ The cell n of A ′ is in an accepting state q at time n ⇐⇒ The conjunction q∈Q\Qaccept R q (n, n) is false in the minimal model ( w , R) of ∀c∀tψ ′ (c, t) ⇐⇒ w satisfies the formula ∃R∀c∀tψ(c, t).

This proves L(A) ∈ pred-ESO-HORN.

Lemma 4. normal-pred-ESO-HORN ⊆ RealTime OIA Proof. We will show that for every language L ⊆ Σ + defined by a formula Φ ∈ normal-pred-ESO-HORN, a oneway iterative array A ∈ RealTime OIA can be constructed such that L = L(A).

Let Φ ∈ normal-pred-ESO-HORN be a formula of the form Φ = ∃R∀x∀yψ(x, y) where R = (R 1 , . . . , R m ) with R 1 = R ⊥ and ψ is a conjunction of Horn clauses of the three following forms:

• input clause of either form:

min(x) ∧ min(y) ∧ Q s (y) → R(x, y) or min(x) ∧ ¬min(y) ∧ Q s (y) → R(x, y), • the contradiction clause max(x) ∧ max(y) ∧ R ⊥ (x, y) → ⊥;
• computation clause of one of the following forms for some sets

H, H ′ [1, m] and i ∈ [1, m]: -¬min(x) ∧ h∈H R h (x -1, y) ∧ ¬min(y) ∧ h∈H ′ R h (x, y -1) → R i (x, y); -¬min(x) ∧ h∈H R h (x -1, y) → R i (x, y); -¬min(y) ∧ h∈H R h (x, y -1) → R i (x, y).
We will denote ψ ′ the formula ψ without the contradiction clause.

We first translate the formula Φ into a dependency graph of type GRID 1 (see Figure 1, with input exclusively on the left side). It will then be turned into a real-time OIA A. The transition function is composed by an input transition function δ input only applied on the first cell and the general transition function δ applied on the other cells c.

For all i ∈ [1, m] ; s ∈ Σ ; q, l, r ∈ Q \ {♯, λ}:
Input transition function:

δ input : Σ × Q → Q. The bit (δ input (s, ♯)) i is 1 if and only if there is an input clause min(x) ∧ min(y) ∧ Q s (y) → R i (x, y) in ψ. (δ input (s, q)) i is 1 if and only if there exists in ψ an input clause min(x) ∧ ¬min(y) ∧ Q s (y) → R i (x, y) or a computation clause ¬min(y) ∧ h∈H R h (x, y -1) → R i (x, y) with (q) h = 1, for all h ∈ H.
Transition function:

δ : Q × Q → Q applied on all cells c ∈ [2, n]. The bit (δ(l, r)) i is 1 if and only if there exists in ψ a computation clause h∈H R h (x -1, y) ∧ ¬min(x) ∧ h∈H ′ R h (x, y -1) ∧ ¬min(y) → R i (x, y) such that (l) h = 1 for all h ∈ H and (r) h = 1 for all h ∈ H ′ . The bit (δ(l, λ)) i is 1 if and only if there is in ψ a com- putation clause ¬min(x) ∧ h∈H R h (x -1, y) → R i (x, y) such that (l) h = 1, for all h ∈ H.
Let A = (Q, Σ, Q accept , N , δ input , δ) be the OIA defined above after making the change of variables of Figure 5: c = x; t = x + y -1. By construction of A, we have the following equivalences concluding the proof.

∀w ∈ Σ n : 1) ∀(a, b) ∈ [1, n] 2 , ∀i ∈ [1, m], the atom R i (a, b)
is true in the minimal model ( w , R) of ∀x∀y ψ ′ (x, y) ⇐⇒ The cell c = a is at time t = a + b -1 in a state q with (q) i = 1. 2) A accepts w in real-time ⇐⇒ w satisfies Φ.

Logical characterization of RealTime IA

In this section, we will show that the languages accepted in real-time by IA are exactly the languages defined by formulas of pred-dio-ESO-HORN.

Theorem 2. RealTime

IA = pred-dio-ESO-HORN.
The proof of Theorem 2 is close to the one of Theorem 1 and is obtained by the following inclusion scheme:

pred-dio-ESO-HORN = normal-pred-dio-ESO-HORN ⊆ RealTime IA ⊆ pred-dio-ESO-HORN.
The equality pred-dio-ESO-HORN = normal-pred-dio-ESO-HORN has been already proved in Section 3. We will now prove the two remaining inclusions.

Lemma 5. RealTime IA ⊆ pred-dio-ESO-HORN.
Proof. Let A be an automaton in RealTime IA , we apply the transformation c → c + t -1 on its time-space diagram.

This transformation gives us a new automaton A ′ with the neighborhood N ′ = {-2, -1, 0} and the input still fed sequentially but in the following way: the i th bit of the input is given to the cell i at time i. Since the input presentation is the only change between the computation of an automaton in RealTime IA and an automaton in RealTime CA , the computation clauses and the contradiction clauses will stay the same. Input: The diagonal input of A ′ is expressed by the conjunction of the input clauses:

ψ input := s∈Σ (t = c ∧ Q s (c) → R s (c, t)) for Σ ⊂ Q. Computation:
The conjunction ψ compute is defined from the transition rules of A ′ as in the previous section. Let ψ ′ be the conjunction ψ input ∧ ψ compute . Output: The output reading is done on the same cell as in the previous section.

ψ output := q∈Q\Qaccept (max(c) ∧ max(t) ∧ R q (c, t) → ⊥)
The formula ψ of pred-dio-ESO-HORN expressing the computation of A ′ is:

ψ := ψ ′ ∧ ψ output .
For each word w = w 1 . . . w n ∈ Σ + we have the following equivalences:

The cell 1 of A is in an accepting state q at time n ⇐⇒ The cell n of A ′ is in an accepting state q at time n ⇐⇒ The conjunction q∈Q\Qaccept R q (n, n) is false in the minimal model ( w , R) of ∀c∀tψ ′ (c, t) ⇐⇒ w satisfies the formula ∃R∀c∀tψ(c, t). This proves L(A) ∈ pred-dio-ESO-HORN. Lemma 6. normal-pred-dio-ESO-HORN ⊆ RealTime IA Proof sketch. Since the proof is similar to that of Lemma 4, we will here just give an hint on how to associate to each site (x, y) ∈ [1, n] 2 such that x ≤ y a site (c, t) of the space-time diagram of an iterative array A running in real-time (see Figure 6). The sites (x, y) ∈ [1, n] 2 such that x ≥ y are similarly handled. First, we apply to the set of sites (x, y) of the dependency graph of Φ variable change c ′ = y -x+1; t ′ = x+y -1. This variable change turns respectively the dependencies (x -1, y) → (x, y) and (x, y -1) → (x, y) into

(c ′ + 1, t ′ -1) → (c ′ , t ′ ) and (c ′ -1, t ′ -1) → (c ′ , t ′ )
expressing the two-way communication of an iterative array A ′ . The sites (c ′ , t ′ ) of the space-time diagram of A ′ takes their values in [1, n] × [1, 2n -1] and the i th bit of the input is fed on the site (1, 2i -1) (see Figure 6). In order to obtain the space-time diagram of an IA A running in real time, each site (c, t) = (⌈c ′ /2⌉ , ⌈t ′ /2⌉) of this diagram will record the set of sites {(c ′ -1, t ′ -1), (c ′ , t ′ ), (c ′ + 1, t ′ -1)} of the spacetime diagram of A ′ , with c ′ and t ′ odd and greater than 1 (see Figure 6).

Logical characterization of Trellis and linear conjunctive grammars

Conjunctive grammars, introduced by Okhotin [START_REF] Okhotin | On the equivalence of linear conjunctive grammars and trellis automata[END_REF], are an extension of context-free grammars. This class of formal It has been shown in [START_REF] Okhotin | On the equivalence of linear conjunctive grammars and trellis automata[END_REF] that languages obtained by the linear restriction of conjunctive grammars are the same as the ones recognized by trellis automata. The class of languages generated by linear conjunctive grammars is denoted LinConj.

Each rule of a linear conjunctive grammar G = (Σ, N, P, S) in normal form is a rule of the form:

A → sB 1 & . . . &sB ℓ &C 1 t& . . . &C p t or A → s with ℓ + p ≥ 1, A, B i , C j ∈ N and s, t ∈ Σ;
As a context-free language, a conjunctive language has an algebraic representation by least solution of a system of language equations with concatenation, union and intersection. For example, the rule A → sB 1 & . . . &sB ℓ &C 1 t& . . . &C p t gives us the language equation:

L(A) = sL(B 1 ) ∩ • • • ∩ sL(B ℓ ) ∩ L(C 1 )t ∩ • • • ∩ L(C p )t
where L(A) is the set of all words having the syntactic property A.

Our inclusive logic characterizes the class of (complements of) linear conjunctive languages: Theorem 3. For any L ∈ Σ + we have:

L ∈ incl-ESO-HORN ⇐⇒ (Σ + \ L) ∈ LinConj .
The theorem is proved in two steps.

Lemma 7. L ∈ incl-ESO-HORN ⇒ (Σ + \ L) ∈ LinConj
Proof. Let us show that for each language L ∈ incl-ESO-HORN defined by a formula Φ ∈ normal-incl-ESO-HORN, Φ = ∃R∀x∀yψ(x, y), we can build a grammar G Φ = (Σ, N, P, S) such that:

w ∈ L ⇐⇒ w / ∈ L(G Φ )
The grammar G Φ is defined as follows. The set of non-terminal symbols of G Φ is N = R and S = R ⊥ is the start symbol. The rules of G Φ are the following: To each input clause x = y ∧ Q s (x) → R(x, y) of Φ we associate the rule R → s.

To each computation clause of Φ x < y ∧ S 1 (x + 1, y) ∧ . . . ∧ S ℓ (x + 1, y) ∧ T 1 (x, y -1) ∧ . . . ∧ T p (x, y -1) → R(x, y) we associate the rules R → sS 1 & . . . &sS ℓ &T 1 t& . . . &T p t, for all s, t ∈ Σ.

Let ψ ′ be the conjunction ψ without the contradiction clause. By an easy induction, the following equivalence can be proved, for all R ∈ R, all words w = w 1 . . . w n ∈ Σ + , and all intervals

[a, b] ⊆ [1, n]: w a . . . w b ∈ L(R) ⇐⇒ ∀x∀yψ ′ ∧ i∈[a,b] Q wi (i) → R(a, b) is a tautology. Taking R = R ⊥ and [a, b] = [1, n] we obtain: w ∈ L(G Φ ) ⇐⇒ w Φ as claimed. Lemma 8. (Σ + \ L) ∈ LinConj ⇒ L ∈ incl-ESO-HORN
Proof. Let L be a language, subset of Σ + , such that (Σ + \ L) ∈ LinConj. We associate to the linear grammar G = (Σ, N, P, S) defining (Σ + \L) with N = {A 1 , . . . , A k } in normal form, as presented above, the formula Φ G := ∃R∀x∀yψ(x, y) with R = {A 1 , . . . , A k } and ψ the conjunction of the following Horn clauses:

the computation clause x < y ∧ Q s (x) ∧ ℓ i=1 B i (x + 1, y) ∧ p i=1 C i (x, y -1) ∧ Q t (y) → A(x, y) for each rule A → sB 1 & . . . &sB ℓ &C 1 t& . . . &C p t; the clause x = y ∧ Q s (x) → A(x,
y) for each rule A → s ; and the contradiction clause min(x)∧max(y)∧S(x, y) → ⊥.

The proof of the equivalence w ∈ L(G) ⇐⇒ w |= Φ G is the same as for the previous Lemma 7.

Logical characterization of Trellis

Clearly, the final state (result) q of a trellis automaton A = (Q, Σ, Q accept , δ) acting on a word w x . . . w y of length greater than 1 (x < y) is completely determined by the final state q l of A acting on the prefix w x . . . w y-1 and the final state q r of A acting on the suffix w x+1 . . . w y : q = δ(q l , q r ). This functional dependence ((x, y -1), (x + 1, y)) → (x, y) is exactly expressed by the computation clauses of the normalized inclusive logic. This suggests the following equality.

Theorem 4. incl-ESO-HORN = Trellis

The theorem is proved in two steps.

Lemma 9. Trellis ⊆ incl-ESO-HORN

Proof. Let A be a trellis automaton that accepts a language L ⊆ Σ + and let be a word w = w 1 . . . w n ∈ Σ + . Let us introduce the set of binary predicates R = {R q | q ∈ Q} with intuitive meaning: R q (x, y) is true ⇐⇒ the final state of A acting on the subword w x . . . w y is q. The following clauses describe the computation of A.

Input clauses:

ψ input := s∈Σ (x = y ∧ Q s (x) → R s (x, y)), for s ∈ Σ.

Computation clauses:

ψ compute := (q l ,qr )∈Q 2 (x < y ∧ R q l (x, y -1)∧ R qr (x + 1, y) → R q (x, y)) where q = δ(q l , q r ).

Contradiction clauses:

ψ output := q∈Q\Qaccept (min(x) ∧ max(y) ∧ R q (x, y) → ⊥) Let ψ ′ := ψ input ∧ ψ compute and ψ := ψ ′ ∧ ψ output .
For each word w = w 1 . . . w n ∈ Σ + we have the following equivalences:

A accepts w in time n ⇐⇒ The conjunction q∈Q\Qaccept R q (1, n) is false in the minimal model ( w , R) of ∀x∀yψ ′ (x, y) ⇐⇒ w satisfies the formula ∃R∀x∀yψ(x, y).
This proves L(A) ∈ incl-ESO-HORN.

Lemma 10. incl-ESO-HORN ⊆ Trellis

Proof sketch. Let Φ be a formula of normal-incl-ESO-HORN, we establish a natural bijection between the sites (x, y) of the domain of the formula and the sites (c, t) of the space-time diagram of a OCA running in real-time (see Figure 7). The transition function of this automaton is then deduced from the computation clauses of Φ as in sections 4.1 and 4.2.

Concluding remarks

It was known that the three complexity classes studied in this paper are the only distinct and natural complexity classes for minimal time, so-called real-time, of one-dimensional cellular automata. In various articles from the 1960s to 2000s, it has been established that each of those classes is robust, in particular with respect to the chosen neighborhood [START_REF] Poupet | Cellular automata: Real-time equivalence between onedimensional neighborhoods[END_REF], and has several equivalent characterizations in other frameworks: e.g, Trellis is the class of linear conjunctive languages [START_REF] Okhotin | On the equivalence of linear conjunctive grammars and trellis automata[END_REF].

In this paper, we have presented a unified view of these three real-time classes as part of descriptive complexity. We hope to have convinced the reader that the logics we have defined are useful tools to express problems in a natural way and to deduce automatically from any formula in such a logic an equivalent cellular automaton running in realtime. This is exemplified by languages notBordered and Palindrome, which can be succinctly defined in pred-ESO-HORN and incl-ESO-HORN, respectively, and hence, belong to RealTime CA and Trellis, respectively. Conversely, the problem Prime := {w ∈ Σ * | |w| is a prime integer} belongs to RealTime CA (and to RealTime IA ) by Fischer's algorithm [START_REF] Fischer | Generation of primes by one-dimensional real-time iterative array[END_REF], [START_REF] Delorme | Signals on cellular automata[END_REF]; therefore, it belongs to pred-ESO-HORN.

Further, we believe that the normalized versions of our three logics, identified to square grid circuits -a natural concept -offer a fresh view of the real-time complexity classes and an additional argument for their robustness. In addition, we are thinking about broadening our logics by allowing a limited use of negation on computation atoms like in Stratified Datalog [START_REF] Abiteboul | Foundations of Databases[END_REF], for easier programming inside these logics and without changing their real-time complexity.

Note that the notion of tautology used in the definition of K J is purely "propositional" because all the atoms involved are of the form R i (x, y), i.e., refer to the same pair of variables (x, y). Also, note that the function J → K J is monotonous:

for J ′ ⊆ J, we have K J ′ ⊆ K J because i∈J ′ θ i (x, y) → R h (x, y) implies i∈J θ i (x, y) → R h (x, y).
Clearly, it is enough to prove the following claim: Claim 1. The formula Φ is equivalent to the normalized formula

Φ ′ := ∃R∀x∀y [ i C i (x, y) ∧ J⊆[1,k] h∈KJ ( i∈J α i (x, y) → R h (x, y)) ].

Proof of the implication

Φ ⇒ Φ ′ : It is enough to prove the implication [ i∈[1,k] (α i (x, y) → θ i (x, y))] → [ i∈J α i (x, y) → h∈KJ R h (x, y)]
for all set J ⊆ [1, k]. The implication to be proved can be equivalently written:

[ i∈J α i (x, y)∧ i∈[1,k] (α i (x, y) → θ i (x, y))] → h∈KJ R h (x, y).
This implication is a straightforward consequence of the two following facts: The sub-formula between brackets above implies the conjunction i∈J θ i (x, y). As the implication i∈J θ i (x, y) → h∈KJ R h (x, y) is a tautology (by definition of K J ), the implication to be proved is a tautology too.

The converse implication Φ ′ ⇒ Φ is more difficult to prove. It uses a folklore property of propositional Horn formulas easy to be proved: Lemma 11 (Horn property: folklore). Let F be a strict Horn formula of propositional calculus, that is a conjunction of clauses of the form p 1 ∧ . . . ∧ p k → p 0 where k ≥ 0 and the p i 's are propositional variables. Let F ′ be the conjunction of propositional variables q such that the implication F → q is a tautology. F has the same minimal model 8 as F ′ .

Proof of the implication Φ ′ ⇒ Φ: Let w be a model of Φ ′ and let ( w , R) be the minimal model of the Horn formula

ϕ ′ := ∀x∀y [ i C i (x, y) ∧ J⊆[1,k] h∈KJ ( i∈J α i (x, y) → R h (x, y)) ].
It is enough to show that ( w , R) also satisfies the formula

ϕ := ∀x∀y [ i C i (x, y) ∧ i∈[1,k] (α i (x, y) → θ i (x, y)) ].
As each α i is a conjunction of formulas of the form R(x -1, y) ∧ ¬min(x), or R(x, y -1) ∧ ¬min(y), we make an induction on the domain

{(a, b) ∈ [1, n] 2 | a + b ≤ t}, for t ∈ [1, 2n].
More precisely, we are going to prove, by recurrence on the integer t ∈ [1, 2n], that the minimal model ( w , R) of ϕ ′ satisfies the "relativized" formula ϕ t of the formula ϕ defined by

ϕ t := ∀x∀y [ x + y ≤ t → [ i C i (x, y) ∧ i∈[1,k] (α i (x, y) → θ i (x, y)) ] ]
As the hypothesis x+y ≤ 2n holds for all x, y in the domain [1, n], ϕ 2n is equivalent to ϕ on the structure ( w , R).

Basis case: For

t = 1 the set {(a, b) ∈ [1, n] 2 |
a+b ≤ t} is empty so that the "relativized" formula ϕ 1 is trivially true in the minimal model ( w , R) of ϕ ′ . and then ( w , R) |= ϕ t .

Recurrence step: Suppose

( w , R) |= ϕ t-1 , for an integer t ∈ [2, 2n]. It is enough to show that, for each couple (a, b) ∈ [1, n] 2 such that a + b = t,
This concludes the inductive proof that ( w , R) |= ϕ t , for all t ∈ [1, 2n], and then w |= Φ. This proves the converse implication Φ ′ ⇒ Φ. Claim 1 is demonstrated. General case of Lemma 1: Steps 1-6 are easy to adapt in the general case where the initial formula may contain hypotheses of the form R(yb, xa). The new points are the following: Step 3 restricts the computation atoms to four forms: R(x, y), R(y, x), R(x -1, y) and R(x, y -1); the key point is the adaptation of step 7 (folding the domain) so that it eliminates the atoms of the form R(y, x). Without loss of generality, assume that each computation clause is of one of the following forms:

(a) S(x -1, y) ∧ ¬min(x) → R(x, y); (b) S(x, y -1) ∧ ¬min(y) → R(x, y); (c) S(x, y) ∧ T (x, y) → R(x, y); (d) S(y, x) → R(x, y). Here again, this is obtained by "decomposing" each computation clause into an "equivalent" conjunction of clauses using new intermediate predicates. For instance, the computation clause R 1 (x -1, y) ∧ ¬min(x) ∧ R 2 (x, y -1) ∧ ¬min(y) ∧ R 3 (y, x) → R 4 (x, y) is "equivalent" to the conjunction of the following clauses using the new predicates R 5 , R 6 , R 7 , R 8 : R 1 (x -1, y) ∧ ¬min(x) → R 5 (x, y); R 2 (x, y -1) ∧ ¬min(y) → R 6 (x, y); R 5 (x, y) ∧ R 6 (x, y) → R 7 (x, y); R 3 (y, x) → R 8 (x, y); R 7 (x, y) ∧ R 8 (x, y) → R 4 (x, y).

The folding of clauses (a-c) is not modified. Let us describe how to fold the (new) clauses (d): S(y, x) → R(x, y). Obviously, such a clause is equivalent to the conjunction of the two clauses (i) x ≤ y ∧ S(y, x) → R(x, y) and (ii) y ≤ x∧S(y, x) → R(x, y). The equivalent "folded" form of clause (i) is x ≤ y ∧ S inv (x, y) → R(x, y). The clause (ii) is equivalent to the clause x ≤ y ∧ S(x, y) → R(y, x) the equivalent "folded" form of which is x ≤ y ∧ S(x, y) → R inv (x, y). Finally, steps 8-10 are not modified.

Step 6 of Lemma 2: Elimination of atoms Q s (xa), Q s (y + b), for a, b > 0: This step is quite similar to step 5. For each R ∈ R, we introduce new predicates: R x-a1,...,x-a l ,y+b1,...,y+bm ←s1,...,s l ,t1,...,tm with l, m ≥ 0, the s i , t j ∈ Σ, 0 ≤ a 1 < a 2 . . . < a l ≤ A and 0 ≤ b 1 < b 2 . . . < b m ≤ B, where A (resp. B) is the maximal a in atoms Q s (x-a) (resp. maximal b in atoms Q s (y + b)). Their intuitive meaning is as follows: R x-a1,...,x-a l ,y+b1,...,y+bm ←s1,...,s l ,t1,...,tm x < y ∧ S x-a1,...,x-a l ,y+b1,...,y+bm ←s1,...,s l ,t1,...,tm (x + 1, y) → R

x-(a1-1),...,x-(a l -1),y+b1,...,y+bm ←s1,...,s l ,t1,...,tm (x, y).

Similarly, to each clause (b) x < y ∧ S(x, y -1) → R(x, y) add the clauses x < y ∧ S x-a1,...,x-a l ,y+b1,...,y+bm ←s1,...,s l ,t1,...,tm (x, y -1) → R

x-a1,...,x-a l ,y+(b1-1),...,y+(bm-1) ←s1,...,s l ,t1,...,tm (x, y). Moreover, add for a 1 = 0 and each s 1 ∈ Σ, the following "verification" clauses, which intuitively delete the hypothesis Q s1 (x) after verifying that it is satisfied because of the equivalence W x s1 (x, y) ⇐⇒ Q s1 (x): x < y ∧ S x,x-a2,...,x-a l ,y+b1,...,y+bm ←s1,s2,...,s l ,t1,...,tm (x, y) ∧ W x s1 (x, y) → R x-a2,...,x-a l ,y+b1,...,y+bm ←s2,...,s l ,t1,...,tm (x, y). Similarly, add for b 1 = 0 and each t 1 ∈ Σ, the "verification" clauses (justified by W y t1 (x, y) ⇐⇒ Q t1 (y)) : x < y ∧ S x-a1,...,x-a l ,y,y+b2,...,y+bm ←s1,...,s l ,t1,t2,...,tm (x, y) ∧ W y t1 (x, y) → R x-a1,...,x-a l ,y+b2,...,y+bm ←s1,...,s l ,t2...,tm (x, y).

For each clause (c) x y ∧ S(x, y) ∧ T (x, y) → R(x, y), where ∈ {<, =}, add similar clauses that cumulate hypotheses provided they are compatible: for example, the clause x y ∧ S x-1,x-3,y+2 s1,s2,t1 (x, y) ∧ T x-1,y+2,y+4 s1,t1,t2 (x, y) → R x-1,x-3,y+2,y+4 s1,s2,t1,t2 (x, y).

3 Figure 1 .

 31 Figure 1. The three ways to arrange the input on the grid

w 1 w 2 w 3 w 4 w 5 w 1 w 2 w 3 w 4 w 5 RealTime OCA w 1 w 2 w 3 w 4 w 5 Figure 2 .

 5552 Figure 2. The space-time diagram of the three natural real-time classes

  w n and therefore w / ∈ notBordered.

Figure 3 .

 3 Figure 3. Computation of ΦnotBordered on the word abbaabb

  x = a (a ≥ 1) and y = nb (b ≥ 0), except in the contradiction clause: Let A (resp. B) be the maximum of the integers a (resp. b) that occur in the equalities x = a (resp. y = nb) of the clauses. For each R ∈ R, we introduce the new predicates R x=a ← , R y=n-b ← and R x=a,y=n-b ← , for all a ∈ [1, A] and b ∈ [0, B], whose intuitive meaning has been announced. For example, we should have R x=a,y=n-b ← (x, y) ⇐⇒ (x = a ∧ y = nb → R(x, y)).

1 ←

 1 )). Transforming the computation clauses: To each clause (a) x < y ∧ S(x + 1, y) → R(x, y) add the clauses x < y ∧ S x=a,y=n-b ← (x + 1, y) → R x=a-1,y=n-b ← (x, y), for all a ∈ [2, A] and b ∈ [0, B] (justification: the hypothesis x + 1 = a is equivalent to x = a -1). Similarly, for each clause (b) x < y ∧ S(x, y -1) → R(x, y) add the clauses x < y ∧ S x=a,y=n-b ← (x, y -1) → R x=a,y=n-(b-1) ← (x, y), for all a ∈ [1, A] and b ∈ [1, B]. Also add for clauses (a,b) the similar (simplified) clauses with only one (instead of two) equality hypothesis. For example, for clause (a) we add the clauses x < y ∧ S x=a ← (x + 1, y) → R x=a-(x, y), for all a ∈ [2, A], and x < y ∧ S y=n-b ← (x + 1, y) → R y=n-b ← (x, y), for all b ∈ [0, B].

5 →Figure 5 .

 55 Figure 5. Variable change

5 → 5 (AFigure 6 .

 556 Figure 6. Variable change and grouping

w 1 w 2 w 3 w 4 w 5 RealTime OCA w 1 w 2 w 3 w 4 w 5 TrellisFigure 7 .

 557 Figure 7. The bijection between incl-ESO-HORN and Trellis

  we have ( w , R) |= i∈[1,k] (α i (a, b) → θ i (a, b)). Let J a,b be the set of indices i ∈ [1, k] such that the couple (a, b) satisfies α i : J a,b := {i ∈ [1, k] | ( w , R) |= α i (a, b)}. Recall that each α i (a, b) is a (possibly empty) conjunction of atoms R(a ′ , b ′ ) with (a ′ , b ′ ) = (a -1, b) or (a ′ , b ′ ) = (a, b -1), therefore such that a ′ + b ′ = t -1. Let any set J ⊆ [1, k].Let us examine the two possible cases:1) J ⊆ J a,b : then the conjunction i∈J α i (a, b) holds in ( w , R); hence, in ( w , R), the conjunction h∈KJ ( i∈J α i (a, b) → R h (a, b)) is equivalent to h∈KJ R h (a, b);2) J \ J a,b = ∅: then the conjunction i∈J α i (a, b) is false in ( w , R); hence, the conjunction h∈KJ ( i∈J α i (a, b) → R h (a, b)) holds in ( w , R).

8 .

 8 For example, forF := p 1 ∧ p 3 ∧ (p 1 ∧ p 3 → p 5 ) ∧ (p 1 ∧ p 2 → p 4 ),we have F ′ := p 1 ∧p 3 ∧p 5 which has the same minimal model I as F ; this model is given by I(p 1 ) = I(p 3 ) = I(p 5 ) = 1 and I(p 2 ) = I(p 4 ) = 0.

From ( 1 )

 1 and (2), we deduce that in ( w , R) the conjunction J⊆[1,k] h∈KJ( i∈J α i (a, b) → R h (a, b)) is equivalent to the conjunction J⊆J a,b h∈KJ R h (a, b), which can be simplified as h∈KJ a,b R h (a, b) because J ⊆ J a,b implies K J ⊆ K J a,b . Consequently, for all h ∈ [1, m], the minimal model ( w , R) of the Horn formula ϕ ′ satisfies the atom R h (a, b) iff h belongs to K J a,b . By definition, K J a,b := {h ∈ [1, m] | i∈J a,b θ i (x, y) → R h (x, y) is a tautology} or, equivalently, K J a,b := {h ∈ [1, m] | i∈J a,b θ i (a, b) → R h (a, b) is a tautology}.As a consequence of Lemma 11, the two conjunctionsi∈J a,b θ i (a, b) and h∈KJ a,b R h (a,b) have the same minimal model, which is also the restriction of the minimal model( w , R) of ϕ ′ to the set of atoms R h (a, b), for h ∈ [1, m]. Therefore, if i ∈ J a,b , then ( w , R) |= θ i (a, b). If i ∈ [1, k] \ J a,b , then we have ( w , R) |= ¬α i (a, b), by definition of J a,b . Therefore, for all i ∈ [1, k], we get ( w , R) |= ¬α i (a, b)∨θ i (a, b). In other words, for all (a, b) such that a + b = t: ( w , R) |= i∈[1,k] (α i (a, b) → θ i (a, b))

  (x, y) ⇐⇒ [ [ i=1,...,l (Q si (xa i ) ∧ x > a i ) ∧ j=1,...,m (Q tj (y + b j ) ∧ y ≤ nb j )] → R(x, y) ].Transforming the initialization clauses: Each initialization clause x = y ∧ Q s (xa) ∧ x > a → R(x, y), a ≥ 1, (resp. x = y ∧ Q s (y + b) ∧ y ≤ nb → R(x, y), b ≥ 1) is transformed into the clause x = y ∧ R x-a ←,s → R(x, y) (resp. x = y ∧ R y+b ←,s → R(x, y)).Transforming the computation clauses:To each clause (a) x < y ∧ S(x + 1, y) → R(x, y) add the following clauses justified by the identity x + 1a i = x -(a i -1):

  The state of the cell c at time t is denoted by c, t . The state of the cell c at time t > 1 is defined by the transition function:

To be complete, one should say that there is a fourth arrangement: place the input word on a side containing the output cell. In this case, the grid circuit behaves like a finite automaton (CA of dimension zero)...

K J := {h ∈ [1, m] | i∈J θ i (x, y) → R h (x, y) is a tautology}.

Acknowledgments: This paper would not exist without the inspiration and guidance of Véronique Terrier. Her teaching, her deep insights into cellular automata, the references and advice she generously gave us, as well as her careful reading, were essential in designing and finalizing our concepts and results.

APPENDICES Appendix A: Expressing natural problems in our logics

Expressing problems Palindrome and notPalindrome in inclusion logic. The problem Palindrome is expressed by the conjunction of the following clauses:

x

x < y ∧ notPal(x + 1, y -1) → notPal(x, y);

x ≤ y ∧ min(x) ∧ max(y) ∧ notPal(x, y) → ⊥.

The problem notPalindrome is expressed by the conjunction of the following clauses:

for all s ∈ Σ, and x ≤ y ∧ Pal(x, y) → ⊥.

Here, Successor(x, y) intuitively means x + 1 = y and is defined by the following clauses: x = y → Equal(x, y) and x < y ∧ Equal(x + 1, y) → Successor(x, y).

Appendix B: Complements of the proofs of Lemmas 1 and 2

Step 10 of Lemma 1: Elimination of atoms R(x, y) as hypotheses: The first idea is to group together in each computation clause the hypothesis atoms of the form R(x, y) and the conclusion of the clause. Accordingly, the formula obtained Φ can be rewritten in the form

where the C i 's are the input clauses and the contradiction clause and each computation clause is written in the form α i (x, y) → θ i (x, y) where α i (x, y) is a conjunction of formulas of the only forms R(x -1, y) ∧ ¬min(x), R(x, y -1) ∧ ¬min(y), but not R(x, y), and θ i (x, y) is a Horn clause all the atoms of which are of the form R(x, y).

We number R 1 , . . . , R m the computation predicates of R. To each subset J ⊆ [1, k] of the family of implications (α i (x, y) → θ i (x, y)) i∈ [1,k] let us associate the set