Descriptive complexity for minimal time of cellular automata

TL;DR

This paper uses descriptive complexity and logical characterizations to analyze the minimal real-time computational complexity of one-dimensional cellular automata, providing a logical framework for understanding their capabilities.

Contribution

It establishes logical characterizations of real-time complexity classes for cellular automata using restrictions of existential second-order Horn logic, linking logic and parallel computation.

Findings

Logical characterizations of real-time classes for cellular automata

A normalization method transforming formulas into grid circuit mimics

Insights into designing parallel programs via logical frameworks

Abstract

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.

Equations

$$⟨w⟩:=([1,n];(Q_s{)}_{s\in \Sigma },\mathtt{min},\mathtt{max},\mathtt{suc},\mathtt{pred})$$

$$\mathtt{notBordered}\in {\mathtt{RealTime}}_{\mathtt{CA}}\setminus (\mathtt{TREILLIS}\cup {\mathtt{RealTime}}_{\mathtt{IA}}).$$

$${\Phi }^{\prime }:=\exists \mathbf{R}\forall x\forall y[\underset{i}{\bigwedge }{C}_i(x,y)$$

$$[\underset{i\in [1,k]}{\bigwedge }({\alpha }_i(x,y)\to {\theta }_i(x,y))]\to [\underset{i\in J}{\bigwedge }{\alpha }_i(x,y)\to \underset{h\in K_J}{\bigwedge }{R}_h(x,y)]$$

$$[\underset{i\in J}{\bigwedge }{\alpha }_i(x,y)\wedge \underset{i\in [1,k]}{\bigwedge }({\alpha }_i(x,y)\to {\theta }_i(x,y))]\to \underset{h\in K_J}{\bigwedge }{R}_h(x,y).$$

$${\phi }^{\prime }:=\forall x\forall y[\underset{i}{\bigwedge }{C}_i(x,y)$$

$$\phi :=\forall x\forall y[\underset{i}{\bigwedge }{C}_i(x,y)$$

$${\phi }_t:=\forall x\forall y[x+y\le t\to$$

$$J_{a,b}:=\{i\in [1,k]|(⟨w⟩,\mathbf{R})\models {\alpha }_i(a,b)\}.$$

$$(⟨w⟩,\mathbf{R})\models \underset{i\in [1,k]}{\bigwedge }({\alpha }_i(a,b)\to {\theta }_i(a,b))$$

Full text

1 Introduction

1.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 [1, 2], which characterizes $\mathtt{NP}$ as the class of problems definable in existential second-order logic ($\mathtt{ESO}$). Similarly, Immerman-Vardi’s Theorem [2, 3] and Grädel’s Theorem [4, 5] characterize the class $\mathtt{P}$ by first-order logic plus least fixed-point, 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 [6, 7]. 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.

1.2 Descriptive complexity and linear time on cellular automata

The present paper is in some sense the sequel of a recent paper [8] (see also [9]). First, [8] 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 [2, 5], [10]. 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, [8] defines a logic denoted $\mathtt{monot}$-$\mathtt{ESO}$-$\mathtt{HORN}^{d}(\forall^{d+1},\mathtt{arity}^{d+1})$ obtained from the logic $\mathtt{ESO}$-$\mathtt{HORN}$ tailored by Grädel [5] to characterize $\mathtt{P}$, by restricting both the number of first-order variables and the arity of second-order predicate symbols. Besides, it includes an additional restriction – the “monotonicity condition” – that reflects the geometrical consideration above-mentioned. [8] proves that this logic exactly characterizes the linear time complexity class of cellular automata: more precisely, for each integer $d\geq 1$, a set $L$ of $d$-dimensional pictures can be decided in linear time on a $d$-dimensional CA – written $L\in\mathtt{DLIN}^{d}_{\mathtt{CA}}$ – if and only if it can be expressed in $\mathtt{monot}$-$\mathtt{ESO}$-$\mathtt{HORN}^{d}(\forall^{d+1},\mathtt{arity}^{d+1})$. For short:

$\mathtt{DLIN}^{d}_{\mathtt{CA}}=\mathtt{monot}$-$\mathtt{ESO}$-$\mathtt{HORN}^{d}(\forall^{d+1},\mathtt{arity}^{d+1})$.

To summarize, expressing a concrete problem in this logic – which seems an easy task in practice and also is a necessary and sufficient condition according to the above equality – guarantees 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.

1.3 Logics for minimal time of cellular automata?

At this point, two natural questions arise:

Besides linear time, a robust and very expressive complexity class, what are the other significant and robust complexity classes of CA? 2. 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 well-studied for a long time in the literature of CA is real-time, i.e., minimal time [11, 12, 13]. 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 [14], [15]. 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 CA111By 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 $\mathtt{IA}$ (resp. OIA). have been proved to be distinct [11, 16, 17, 18]:

$\mathtt{RealTime}_{\mathtt{CA}}=\mathtt{RealTime}_{\mathtt{OIA}}$; 2. 2.

$\mathtt{Trellis}=\mathtt{RealTime}_{\mathtt{OCA}}$; 3. 3.

$\mathtt{RealTime}_{\mathtt{IA}}$.

The final and decisive step to establish this classification is a nice dichotomy of [18] on admissible neighborhoods222The neighborhood of a CA is the finite set of integers $\mathcal{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\in\mathcal{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. of CA, which can be rephrased as follows: for each neighborhood $\mathcal{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 $\mathcal{N}$,

• •

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

• •

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

Further, it is surprising to notice that

• •

the mutual relations between those three real-time classes are wholly elucidated: classes $\mathtt{Trellis}$ and $\mathtt{RealTime}_{\mathtt{IA}}$ are mutually incomparable for inclusion whereas we have the strict inclusion $\mathtt{Trellis}\cup\mathtt{RealTime}_{\mathtt{IA}}\subsetneqq\mathtt{RealTime}_{\mathtt{CA}}$ [11, 19, 20],

• •

while it is unknown whether the trivial inclusion $\mathtt{RealTime}_{\mathtt{CA}}\subseteq\mathtt{DLIN}^{1}_{\mathtt{CA}}$ is strict; worse, even whether the inclusion $\mathtt{RealTime}_{\mathtt{CA}}\subseteq\mathtt{LinSpace}$ is strict is an open problem!

1.4 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, $\mathtt{RealTime}_{\mathtt{CA}}$ is equal to the linear time class of one-way CA with parallel input mode. Similarly, [21] has proved the surprising result that $\mathtt{Trellis}$ is the class of languages generated by linear conjunctive grammars (see also [22]) and [23] has established that a language $L$ is in $\mathtt{RealTime}_{\mathtt{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 real-time 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\geq 1$, let $C_{n}$ be the grid circuit $n\times n$ where the state $q\in Q$ (for finite $Q$) of any site $(i,j)$, $1\leq i,j\leq n$, is determined by the states of its “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 ways333To 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)… to arrange an input word $w=w_{1}\ldots w_{n}$ of length $n$ on the grid $C_{n}$, see Figure 1:

$\mathtt{GRID}_{1}$: place the input on any side (or, equivalently, on both sides) that does (do) not contain the output cell; 2. 2.

$\mathtt{GRID}_{2}$: place the input on the diagonal opposite to the output cell; 3. 3.

$\mathtt{GRID}_{3}$: place the input on the diagonal that contains the output cell.

A simple (reversible) deformation transforms a grid circuit of $\mathtt{GRID}_{i}$, $i=1,2,3$, into a time-space diagram of a CA of the real-time class $i$ in concern (recall: 1: $\mathtt{RealTime}_{\mathtt{CA}}$; 2: $\mathtt{Trellis}$; 3: $\mathtt{RealTime}_{\mathtt{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 ($\mathtt{DLIN}^{1}_{\mathtt{CA}}=\mathtt{monot}$-$\mathtt{ESO}$-$\mathtt{HORN}^{1}(\forall^{2},\mathtt{arity}^{2})$), called respectively $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$, $\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ and $\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$ (defined in the next section), and we prove the following equalities:

$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{GRID}_{1}=\mathtt{RealTime}_{\mathtt{CA}}$ 2. 2.

$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{GRID}_{2}=\mathtt{Trellis}$ 3. 3.

$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{GRID}_{3}=\mathtt{RealTime}_{\mathtt{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 [21]. Section 5 gives conclusive remarks.

2 Preliminaries

2.1 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 $\mathbb{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,\Sigma,Q_{accept},\mathcal{N},\delta)$ where $Q$ is a finite set of states, $\Sigma\subset Q$ is the input alphabet, $Q_{accept}\subset Q$ is the set of accepting states, the neighborhood $\mathcal{N}$ is a finite ordered subset of $\mathbb{Z}$ and $\delta$ is the transition function from $Q^{|\mathcal{N}|}$ to $Q$. The state of the cell $c$ at time $t$ is denoted by $\langle c,t\rangle$. The state of the cell $c$ at time $t>1$ is defined by the transition function: $\langle c,t\rangle=\delta(\langle c+v,t-1\rangle:v\in\mathcal{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}\dots 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 $\mathcal{A}$ in real-time (denoted by $L(\mathcal{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 $\sharp$. Without information from the input a cell of index $[1,n]$ is in the quiescent state $\lambda$.

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 $\delta_{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 ($\mathcal{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 ($\mathcal{N}=\{-1,0\}$). The input mode of IA is no more parallel but sequential.

Definition 3** ($\mathtt{RealTime_{CA}}$).**

The class $\mathtt{RealTime_{CA}}$ is the set of languages accepted by real-time CA with a parallel input, the neighborhood $\mathcal{N}=\{-1,0,1\}$ and the first cell as the output cell.

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

Definition 4** ($\mathtt{Trellis}$).**

The class $\mathtt{Trellis}$ is the set of languages accepted by trellis automata or equivalently by OCA running in real-time with a parallel input, the neighborhood $\mathcal{N}=\{-1,0\}$ and the last cell as the output cell.

Definition 5** ($\mathtt{RealTime_{IA}}$).**

The class $\mathtt{RealTime_{IA}}$ is the set of languages accepted by IA running in real-time with a sequential input, the neighborhood $\mathcal{N}=\{-1,0,1\}$ and the first cell as the output cell.

The space-time diagrams of these real-time classes are depicted in Figure 2.

2.2 Our logics

The “local” nature of our logics requires that the underlying structure encoding an input word $w=w_{1}\ldots w_{n}$ on its index interval $[1,n]=\{1,\ldots,n\}$ only uses the successor and predecessor functions and the monadic predicates $\mathtt{min}$ and $\mathtt{max}$ as its only arithmetic functions/predicates:

Definition 6** (structure encoding a word).**

Each nonempty word $w=w_{1}\ldots w_{n}\in\Sigma^{n}$ on a fixed finite alphabet $\Sigma$ is represented by the first-order structure

[TABLE]

of domain $[1,n]$, monadic predicates $Q_{s}$, $s\in\Sigma$, $\mathtt{min}$ and $\mathtt{max}$ such that $Q_{s}(i)\iff w_{i}=s$, $\mathtt{min}(i)\iff i=1$, and $\mathtt{max}(i)\iff i=n$, and unary functions $\mathtt{suc}$ and $\mathtt{pred}$ such that $\mathtt{suc}(i)=i+1$ for $i<n$ and $\mathtt{suc}(n)=n$, $\mathtt{pred}(i)=i-1$ for $i>1$ and $\mathtt{pred}(1)=1$. Let $\mathcal{S}_{\Sigma}$ denote the signature $\{(Q_{s})_{s\in\Sigma},\mathtt{min},\mathtt{max},\mathtt{suc},\mathtt{pred}\}$ of structure $\langle w\rangle$. The monadic predicates $Q_{s}$, $s\in\Sigma$, $\mathtt{min}$, and $\mathtt{max}$ of $\mathcal{S}_{\Sigma}$ are called input predicates.

Let $x+k$ and $x-k$ abbreviate the terms $\mathtt{suc}^{k}(x)$ and $\mathtt{pred}^{k}(x)$, for a fixed integer $k\geq 0$.

Let us now define two of our logics:

Definition 7** (predecessor logics).**

*A predecessor Horn formula (resp. predecessor Horn formula with diagonal input-output) is a formula of the form $\Phi=\exists\mathbf{R}\forall x\forall y\psi(x,y)$ where $\psi$ is a conjunction of Horn clauses on the variables $x,y$,

– of signature $\mathcal{S}_{\Sigma}\cup\mathbf{R}$ (resp. $\mathcal{S}_{\Sigma}\cup\mathbf{R}\cup\{=\}$) where $\mathbf{R}$ is a set of binary predicates called computation predicates,

– of the form $\delta_{1}\land\ldots\land\delta_{r}\to\delta_{0}$ where the conclusion $\delta_{0}$ is either a computation atom $R(x,y)$ with $R\in\mathbf{R}$, or $\bot$ (False) and each hypothesis $\delta_{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)\land x=y$), for $s\in\Sigma$ and an integer $a\geq 0$,

• •

$U(x-a)$, $\lnot U(x-a)$, $U(y-a)$ or $\lnot U(y-a)$, for $U\in\{\mathtt{min},\mathtt{max}\}$ and an integer $a\geq 0$,

or a computation atom of the form $S(x-a,y-b)$ or $S(y-b,x-a)$, for $S\in\mathbf{R}$ and some integers $a,b\geq 0$.

Let $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ (resp. $\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{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 $\Phi=\exists\mathbf{R}\forall x\forall y\psi(x,y)$ where $\psi$ is a conjunction of Horn clauses of signature $\mathcal{S}_{\Sigma}\cup\mathbf{R}\cup\{=,\leq,<\}$ where $\mathbf{R}$ is a set of binary predicates called computation predicates, of the form $x\leq y\land\delta_{1}\land\ldots\land\delta_{r}\to\delta_{0}$ where the conclusion $\delta_{0}$ is either a computation atom $R(x,y)$ with $R\in\mathbf{R}$, or the atom $\bot$ (False), and each hypothesis $\delta_{i}$ is

either an input literal of the form 444Without loss of generality, assume that there is no negation over a predicate $Q_{s}$. $U(x+a)$, $\lnot U(x+a)$, $U(y+a)$ or $\lnot U(y+a)$, for $U\in\{(Q_{s})_{s\in\Sigma},\mathtt{min},\mathtt{max}\}$ and an integer $a\in\mathbb{Z}$, 2. 2.

or the (in)equality $x=y$ or $x<y$ 555Then, the hypothesis $x\leq y$ is redundant., 3. 3.

or a conjunction of the form

$S(x+a,y-b)\land x+a\leq y-b$**

for a computation atom $S(x+a,y-b)$, with $S\in\mathbf{R}$ and some integers $a,b\geq 0$.

Let $\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ denote the class of inclusion Horn formulas and, also, the class of languages they define.

Note that the “inclusion” meaning of logic $\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ is given by hypotheses $x\leq y$ and $x+a\leq y-b$. It means that the inductive computation of each value $R(x,y)$, for $x\leq y$ and $R\in\mathbf{R}$, only use values of the form $S(x+a,y-b)$, for $S\in\mathbf{R}$ and an included interval $[x+a,y-b]\subseteq[x,y]$.

Notation: We will freely use the intuitive abbreviations $x\leavevmode\nobreak\ >\leavevmode\nobreak\ a$, $x=a$, for a constant integer $a\geq 1$, and $x\leq n-a$, $x<n-a$, $x=n-a$, for a constant integer $a\geq 0$, and similarly for $y$. For example, $x>3$ is written in place of $\lnot\mathtt{min}(x-2)$ and $y\leq n-2$ is written in place of $\lnot\mathtt{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(x-a,y-b)$ or $S(y-b,x-a)$, for $a,b\geq 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}(x-a)$ or $Q_{s}(y-b)$, 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\leq n-a$ (resp. $y\leq n-a$). Similarly, for each atom $S(x+a,y-b)$, for $a,b\geq 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 $(\lnot)U(x+a)$, $(\lnot)U(y+a)$, for $U\in\{(Q_{s})_{s\in\Sigma},\mathtt{min},\mathtt{max}\}$ and $a\in\mathbb{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 $\mathtt{notBordered}$ is the set of all words $w\in\Sigma^{+}$ with no proper prefix equal to a proper suffix:

$\mathtt{notBordered}=\{w\mid\forall w^{\prime}$ such that $w=w^{\prime}u=vw^{\prime}$, $w^{\prime}=\epsilon$ or $w^{\prime}=w\}$.

This language can be defined by $\Phi_{\mathtt{notBordered}}\coloneqq\exists\mathtt{Border}\forall x\forall y\psi$ of $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ where $\psi$ is the conjunction of the following clauses where $\mathtt{Border}(x,y)$ means $w_{1}\dots w_{x}=w_{y-x+1}\dots w_{y}$ (see Figure 3):

$\mathtt{min}(x)\land\lnot\mathtt{min}(y)\land Q_{s}(x)\land Q_{s}(y)\to\mathtt{Border}(x,y)$ 2. 2.

$\lnot\mathtt{min}(x)\land\lnot\mathtt{min}(y)\land\mathtt{Border}(x-1,y-1)\land Q_{s}(x)\land Q_{s}(y)\to\mathtt{Border}(x,y)$, for all $s\in\Sigma$; 3. 3.

$\mathtt{max}(y)\land\mathtt{Border}(x,y)\to\bot$.

If $\mathtt{Border}(x,y)$ is true when $y$ is maximal, then $w_{1}\dots w_{x}=w_{n-x+1}\dots w_{n}$ and therefore $w\notin\mathtt{notBordered}$.

So, as a consequence of this paper, $\mathtt{notBordered}$ belongs to $\mathtt{RealTime}_{\mathtt{CA}}$. In fact, more is known [20]:

[TABLE]

3 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 $\Phi\in\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ (resp. $\Phi\in\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$) is equivalent to a formula $\Phi^{\prime}\in\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ (resp. $\Phi^{\prime}\in\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$) normalized as follows: each clause of $\Phi^{\prime}$ is of one of the following forms:

• •

input clause* of the form, for $s\in\Sigma$ and $R\in\mathbf{R}$:*

$\mathtt{min}(x)\land\mathtt{min}(y)\land Q_{s}(y)\to R(x,y)$, or

$\mathtt{min}(x)\land\lnot\mathtt{min}(y)\land Q_{s}(y)\to R(x,y)$

(resp. $x=y\land\mathtt{min}(x)\land Q_{s}(x)\to R(x,y)$, or

$x=y\land\lnot\mathtt{min}(x)\land Q_{s}(x)\to R(x,y)$).

• •

the contradiction clause, for a fixed $R_{\bot}\in\mathbf{R}$: $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$;

• •

computation clause* of the form $\delta_{1}\land\ldots\land\delta_{r}\to R(x,y)$, for $R\in\mathbf{R}$, where each hypothesis $\delta_{i}$ is a conjunction of the form $S(x-1,y)\land\lnot\mathtt{min}(x)$ or $S(x,y-1)\land\lnot\mathtt{min}(y)$, for $S\in\mathbf{R}$.*

Let $\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ (resp. $\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$) denote the class of formulas (languages) so defined.

Lemma 2** (normalization of inclusion logic).**

Each formula $\Phi\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ is equivalent to a formula $\Phi^{\prime}\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ normalized as follows: each clause of $\Phi^{\prime}$ is of one of the following forms:

• •

input clause* of the form $x=y\land Q_{s}(x)\to R(x,y)$, for $s\in\Sigma$ and $R\in\mathbf{R}$;*

• •

the contradiction clause, for a fixed $R_{\bot}\in\mathbf{R}$, $\mathtt{min}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$;

• •

computation clause* of the form666Note that the hypothesis $x<y$ is equivalent to the expected inequality $x+1\leq y$ or $x\leq y-1$. $x<y\land\delta_{1}\land\ldots\land\delta_{r}\to R(x,y)$, where $R\in\mathbf{R}$ and where each hypothesis $\delta_{i}$ is a computation atom of either form $S(x+1,y)$ or $S(x,y-1)$, for $S\in\mathbf{R}$.*

Let $\mathtt{normal}$-$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{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: $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{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 $\Phi\in\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$. For simplicity of notation, we first assume that the only computation atoms of $\Phi$ are of the form $R(x-a,y-b)$, $a,b\geq 0$ (no atom of the form $R(y-b,x-a)$). We will show at the end of the proof how to manage the general case. $\Phi$ will be transformed into an equivalent normalized form $\Phi^{\prime}$ by a sequence of 10 steps:

Processing the contradiction clauses; 2. 2.

Processing the input; 3. 3.

Restriction of computation atoms to $R(x-1,y)$, $R(x,y-1)$, and $R(x,y)$; 4. 4.

Elimination of atoms $x>a$, $x=a$, $y>a$, $y=a$; 5. 5.

Processing of $\mathtt{min}$ and $\mathtt{max}$; 6. 6.

Defining equality and inequalities; 7. 7.

Folding of the domain; 8. 8.

Deleting $\mathtt{max}$ in the initialization clauses; 9. 9.

From initialization clauses to input clauses; 10. 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 $\mathbf{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 $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$. Indeed, each contradiction clause $\ell_{1}\land\ldots\land\ell_{k}\to\bot$ can be equivalently replaced by the conjunction of computation clauses $\ell_{1}\land\ldots\land\ell_{k}\to R_{\bot}(x,y)$ with the clause $R_{\bot}(x,y)\to\bot$ where $R_{\bot}$ is a new computation predicate (intuitively, always false). However, in place of the previous clause, we “delay” the contradiction, by propagating predicate $R_{\bot}$ till point $(n,n)$, thanks to the conjunction of the “transport” clauses $R_{\bot}(x-1,y)\land\lnot\mathtt{min}(x)\to R_{\bot}(x,y)$ and $R_{\bot}(x,y-1)\land\lnot\mathtt{min}(y)\to R_{\bot}(x,y)$ and of the unique contradiction clause $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$ 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)\in[1,n]^{2}\}$, this by carrying out their transport thanks to new “transport” predicates $W^{x}_{s}$ and $W^{y}_{s}$, for $s\in\Sigma$, inductively defined by the following clauses:

$\bullet$ initialization clauses $Q_{s}(x)\land\mathtt{min}(y)\to W^{x}_{s}(x,y)$ and $Q_{s}(y)\land\mathtt{min}(x)\to W^{y}_{s}(x,y)$;

$\bullet$ transport clauses $W^{x}_{s}(x,y-1)\land\lnot\mathtt{min}(y)\to W^{x}_{s}(x,y)$ and $W^{y}_{s}(x-1,y)\land\lnot\mathtt{min}(x)\to W^{y}_{s}(x,y)$.

By transitivity, these clauses imply clauses $Q_{s}(x)\leavevmode\nobreak\ \to\leavevmode\nobreak\ W^{x}_{s}(x,y)$ and $Q_{s}(y)\leavevmode\nobreak\ \to\leavevmode\nobreak\ W^{y}_{s}(x,y)$.In other words, the minimal model of the conjunction of those clauses that expands structure $\langle w\rangle$ satisfies equivalences $\forall x\forall y\;(W^{x}_{s}(x,y)\iff Q_{s}(x))$ and $\forall x\forall y\;(W^{y}_{s}(x,y)\iff Q_{s}(y))$. This justifies the replacement of the input atoms of form $Q_{s}(x-a)$ and $Q_{s}(y-b)$ by the respective atoms $W^{x}_{s}(x-a,y)$ and $W^{y}_{s}(x,y-b)$ 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\in\mathbf{R}$: typically, we define the predicate $R^{x-a,y-b}$ that intuitively satisfies the equivalence $R^{x-a,y-b}(x,y)\iff R(x-a,y-b)$. Let us suggest the method by an example. Assume we have initially the Horn clause

$x>3\land y>2\land R(x-2,y-1)\land S(x-3,y-2)\to T(x,y).$

This clause is replaced by the clause

$x>3\land y>2\land R^{x-2}(x,y-1)\land S^{x-2,y-2}(x-1,y))\to T(x,y),$

for which the predicates $R^{x-1}$ and $R^{x-2}$ are defined by the clauses $x>1\land R(x-1,y)\to R^{x-1}(x,y)$ and $x>2\land R^{x-1}(x-1,y)\to R^{x-2}(x,y)$ which imply $x>2\land R(x-2,y)\to R^{x-2}(x,y)$ and then $x>2\land y>1\linebreak\land R(x-2,y-1)\to 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\land S(x-1,y)\to S^{x-1}(x,y)$,$x>2\land S^{x-1}(x-1,y)\to S^{x-2}(x,y)$,$x>2\land y>1\land S^{x-2}(x,y-1)\to S^{x-2,y-1}(x,y)$, and $x>2\land y>2\land S^{x-2,y-1}(x,y-1)\to S^{x-2,y-2}(x,y)$,which imply together the clause

$x>2\land y>2\land S(x-2,y-2)\to S^{x-2,y-2}(x,y)$ and then also $x>3\land y>2\land S(x-3,y-2)\to S^{x-2,y-2}(x-1,y)$.

Remark 1**.**

Atoms on $\mathtt{min}$ and $x$ are of the forms $\mathtt{min}(x-a)$ or $\lnot\mathtt{min}(x-a)$ for $a\geq 0$, or, equivalently, $x=a+1$ or $x>a+1$. Besides, for each integer $a\geq 1$, the atom $\mathtt{max}(x-a)$ is false. Therefore, one may consider that the only literals on $x$ involving $\mathtt{min}$ or $\mathtt{max}$ are of the form $\mathtt{min}(x)$, $\lnot\mathtt{min}(x)$, $\mathtt{max}(x)$, $\lnot\mathtt{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\geq 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 $\lnot\mathtt{min}(x)\to 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)\land\lnot\mathtt{min}(x)\to R^{x>a}(x,y).$ By recurrence on integer $a\geq 1$, these clauses imply $x>a\to 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 $\mathtt{min}$ or $\mathtt{max}$ are $(\lnot)\mathtt{min}(x)$, $(\lnot)\mathtt{max}(x)$, $(\lnot)\mathtt{min}(y)$, $(\lnot)\mathtt{max}(y)$.

5) Processing of $\mathtt{min}$ and $\mathtt{max}$: To each literal $\eta(x)$ of the form $\mathtt{min}(x)$, $\lnot\mathtt{min}(x)$, $\mathtt{max}(x)$ or $\lnot\mathtt{max}(x)$, associate the new binary predicate $R^{\eta(x)}$ defined by the conjunction of the initialization clause $\eta(x)\land\mathtt{min}(y)\to R^{\eta(x)}(x,y)$ and of the transport clause $R^{\eta(x)}(x,y-1)\land\lnot\mathtt{min}(y)\to R^{\eta(x)}(x,y)$. Do similarly for the literals $\eta(y)\in\{(\lnot)\mathtt{min}(y),(\lnot)\mathtt{max}(y)\}$. This justifies we replace each such literal $\eta(x)$ (resp. $\eta(y)$) by the “equivalent” atom $R^{\eta(x)}(x,y)$ (resp. $R^{\eta(y)}(x,y)$) in all the clauses, except in the above initialization clauses and in the contradiction clause or in case $\eta(x)$ (resp. $\eta(y)$) is $\lnot\mathtt{min}(x)$ (resp. $\lnot\mathtt{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:

an initialization clause of one of the two forms:

$\bullet$ initialization for $x=1$: $\mathtt{min}(x)\land\eta(y)\to R(x,y)$

with $\eta(y)\in\{(Q_{s}(y))_{s\in\Sigma},(\lnot)\mathtt{min}(y),(\lnot)\mathtt{max}(y)\}$;

$\bullet$ initialization for $y=1$: $\mathtt{min}(y)\land\eta(x)\to R(x,y)$

with $\eta(x)\in\{(Q_{s}(x))_{s\in\Sigma},(\lnot)\mathtt{min}(x),(\lnot)\mathtt{max}(x)\}$; 2. 2.

“the” contradiction clause $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$; 3. 3.

a computation clause of the form

$\delta_{1}(x,y)\land\ldots\land\delta_{r}(x,y)\to R(x,y)$, where each hypothesis $\delta_{i}$ is of one of the three forms $R(x,y)$, $R(x-1,y)\land\lnot\mathtt{min}(x)$, $R(x,y-1)\land\lnot\mathtt{min}(y)$.

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

1. (a)

$S(x-1,y)\land\lnot\mathtt{min}(x)\to R(x,y)$; 2. (b)

$S(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$; 3. (c)

$S(x,y)\land T(x,y)\to 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 $R_{1}(x-1,y)\land\lnot\mathtt{min}(x)\land R_{2}(x,y-1)\land\lnot\mathtt{min}(y)\land R_{3}(x,y)\to R_{4}(x,y)$ is “equivalent” to the conjunction of the following clauses using new predicates $R_{5},R_{6},R_{7}$: $R_{1}(x-1,y)\land\lnot\mathtt{min}(x)\to R_{5}(x,y)$; $R_{2}(x,y-1)\land\lnot\mathtt{min}(y)\to R_{6}(x,y)$; $R_{5}(x,y)\land R_{6}(x,y)\to R_{7}(x,y)$; $R_{7}(x,y)\land R_{3}(x,y)\to R_{4}(x,y)$.

We now plan to fold the square domain $\{(x,y)\in[1,n]^{2}\}$ along the diagonal $x=y$ on the over-diagonal triangle $T_{n}=\{(x,y)\in[1,n]^{2}|\ x\leq y\}$. This requires to first define equality and inequalities.

6) Defining equality and inequalities: Let us jointly define the predicates $R_{=}$ and $R_{\mathtt{pred}}$ of intuitive meaning $R_{=}(x,y)\iff x=y$ and $R_{\mathtt{pred}}(x,y)\iff x-1=y$by the following clauses: $\mathtt{min}(x)\land\mathtt{min}(y)\to R_{=}(x,y)$; $\lnot\mathtt{min}(x)\land R_{=}(x-1,y)\to R_{\mathtt{pred}}(x,y)$; $\lnot\mathtt{min}(y)\land R_{\mathtt{pred}}(x,y-1)\to R_{=}(x,y)$.

Then define the predicate $R_{<}$ such that $R_{<}(x,y)\iff x<y$ with the two clauses $\lnot\mathtt{min}(y)\land R_{=}(x,y-1)\to R_{<}(x,y)$ and $\lnot\mathtt{min}(y)\land R_{<}(x,y-1)\to R_{<}(x,y)$. Define similarly the predicate $R_{\leq}$ such that $R_{\leq}(x,y)\iff x\leq y$with the two clauses $\mathtt{min}(x)\land\mathtt{min}(y)\to R_{\leq}(x,y)$ and $\lnot\mathtt{min}(x)\land R_{<}(x-1,y)\to R_{\leq}(x,y)$.

For easy reading, we will freely write $x=y$, $x<y$ and $x\leq y$ in place of the atoms $R_{=}(x,y)$, $R_{<}(x,y)$ and $R_{\leq}(x,y)$, respectively.

7) Folding of the domain: Let us fold the square domain $\{(x,y)\in[1,n]^{2}\}$ along the diagonal $x=y$ on the over-diagonal triangle $T_{n}=\{(x,y)\in[1,n]^{2}|\ x\leq y\}$ so that each point $(y,x)$ such that $x\leq y$ is sent to its symmetrical point $(x,y)\in T_{n}$. For that purpose, let us associate to each predicate $R\in\mathbf{R}$ a new (inverse) predicate $R^{\mathtt{inv}}$ whose intuitive meaning is the following: for each $x\leq y$, we have $R^{\mathtt{inv}}(x,y)\iff 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^{\mathtt{inv}}$. Finally, we will express that each $R\in\mathbf{R}$ coincides with its inverse $R^{\mathtt{inv}}$ on the fold $x=y$.

Folding the initialization clauses: Each initialization clause of the form $\mathtt{min}(x)\land\eta(y)\to R(x,y)$ (with $\eta(y)\in\{Q_{s}(y)|s\in\Sigma\}\cup\{(\lnot)\mathtt{min}(y),(\lnot)\mathtt{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 $\mathtt{min}(y)\land\eta(x)\to R(x,y)$ (with $\eta(x)\in\{Q_{s}(x)|s\leavevmode\nobreak\ \in\leavevmode\nobreak\ \Sigma\}\cup\{(\lnot)\mathtt{min}(x),(\lnot)\mathtt{max}(x)\}$) is replaced by its folded version $\mathtt{min}(x)\land\eta(y)\to R^{\mathtt{inv}}(x,y)$.

Folding the computation clauses: Let us describe how to fold the clauses (a) or (b) (folding clauses (c) is easy):

$\bullet$ Folding of clauses (a): A clause of the form $S(x-1,y)\land\lnot\mathtt{min}(x)\to R(x,y)$ is equivalent to the conjunction of clauses i) $x\leq y\land S(x-1,y)\land\lnot\mathtt{min}(x)\to R(x,y)$ and

ii) $x>y\land S(x-1,y)\land\lnot\mathtt{min}(x)\to R(x,y)$. Notice that clause (i) applies to the triangle $T_{n}$ since $x\leq 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\land S(y-1,x)\land\lnot\mathtt{min}(y)\to R(y,x)$ whose folded (equivalent) form on $T_{n}$ is $x<y\land S^{\mathtt{inv}}(x,y-1)\land\lnot\mathtt{min}(y)\to R^{\mathtt{inv}}(x,y)$ since $x<y$ implies $x\leq y-1$.

$\bullet$ Folding of clauses (b): Similarly, a clause of the form $S(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$ is equivalent to the conjunction of clauses $x<y\land S(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$ and $x\leq y\land S^{\mathtt{inv}}(x-1,y)\land\lnot\mathtt{min}(x)\to R^{\mathtt{inv}}(x,y)$.

Folding the contradiction clause: Clearly, it is harmless to confuse the (contradiction) predicate $R_{\bot}$ and its inverse $(R_{\bot})^{\mathtt{inv}}$; consequently, the contradiction clause itself $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$ is its own folded version.

The diagonal fold: Finally, for each $R\in\mathbf{R}$, the following two clauses mean that $R$ coincides with its inverse $R^{\mathtt{inv}}$ on the diagonal: $x=y\land R(x,y)\to R^{\mathtt{inv}}(x,y)$; $x=y\land R^{\mathtt{inv}}(x,y)\to 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:

an initialization clause of the form: $\mathtt{min}(x)\land\eta(y)\to R(x,y)$ with $\eta(y)\in\{Q_{s}(y)|s\in\Sigma\}\cup\{(\lnot)\mathtt{min}(y),(\lnot)\mathtt{max}(y)\}$; 2. 2.

“the” contradiction clause $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$; 3. 3.

a computation clause of one of the following forms:

(a) $x\leq y\land S(x-1,y)\land\lnot\mathtt{min}(x)\to R(x,y)$;

(b) $x<y\land S(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$;

(c) $x\leq y\land S(x,y)\land T(x,y)\to R(x,y)$;

(d) $x=y\land S(x,y)\to R(x,y)$.

8) Deleting $\mathtt{max}$ in the initialization clauses: The idea is to consider in parallel for each point $(x,y)$ the case where the hypothesis $\mathtt{max}(y)$ holds and the contrary case where the negation $\lnot\mathtt{max}(y)$ holds. For that purpose, we duplicate each computation predicate $R$ in two new predicates denoted $R^{y}_{\leftarrow\mathtt{max}}$ and $R^{y}_{\leftarrow\lnot\mathtt{max}}$. Intuitively, the atom $R^{y}_{\leftarrow\mathtt{max}}(x,y)$ (resp. $R^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)$) expresses the implication $\mathtt{max}(y)\to R(x,y)$ (resp. $\lnot\mathtt{max}(y)\to R(x,y)$).

Transforming the initialization clauses: According to the desired semantics of $R^{y}_{\leftarrow\mathtt{max}}$ and $R^{y}_{\leftarrow\lnot\mathtt{max}}$, each initialization clause of the form $\mathtt{min}(x)\land\mathtt{max}(y)\to R(x,y)$ (resp. $\mathtt{min}(x)\land\lnot\mathtt{max}(y)\to R(x,y)$) should be rewritten as $\mathtt{min}(x)\to R^{y}_{\leftarrow\mathtt{max}}(x,y)$ (resp. $\mathtt{min}(x)\to R^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)$). Similarly, each initialization clause of the form $\mathtt{min}(x)\land\eta(y)\to R(x,y)$, for $\eta(y)\in\{Q_{s}(y)|s\in\Sigma\}\cup\{(\lnot)\mathtt{min}(y)\}$ should be replaced by the conjunction of the following two clauses: $\mathtt{min}(x)\land\eta(y)\to R^{y}_{\leftarrow\mathtt{max}}(x,y)$ and $\mathtt{min}(x)\land\eta(y)\to R^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)$.

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

$\bullet$ Each clause (a) $x\leq y\land S(x-1,y)\land\lnot\mathtt{min}(x)\to R(x,y)$ is replaced by the “equivalent” conjunction of the following two clauses $x\leq y\land S^{y}_{\leftarrow\mathtt{max}}(x-1,y)\land\lnot\mathtt{min}(x)\to R^{y}_{\leftarrow\mathtt{max}}(x,y)$ and $x\leq y\land S^{y}_{\leftarrow\lnot\mathtt{max}}(x-1,y)\land\lnot\mathtt{min}(x)\to R^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)$.

$\bullet$ Each clause (b) $x<y\land S(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$ is “equivalent” to $x<y\land S^{y}_{\leftarrow\lnot\mathtt{max}}(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$ since the hypothesis $\lnot\mathtt{max}(y-1)$ always holds. Consequently, clause (b) should be replaced by the “equivalent” conjunction of the following two clauses:

$x<y\land S^{y}_{\leftarrow\lnot\mathtt{max}}(x,y-1)\land\lnot\mathtt{min}(y)\to R^{y}_{\leftarrow\mathtt{max}}(x,y)$ and

$x<y\land S^{y}_{\leftarrow\lnot\mathtt{max}}(x,y-1)\land\lnot\mathtt{min}(y)\to R^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)$.

$\bullet$ Each clause (c) $x\leq y\land S(x,y)\land T(x,y)\to R(x,y)$ is replaced by the “equivalent” conjunction of the following two clauses: $x\leq y\land S^{y}_{\leftarrow\mathtt{max}}(x,y)\land T^{y}_{\leftarrow\mathtt{max}}(x,y)\to R^{y}_{\leftarrow\mathtt{max}}(x,y)$ and $x\leq y\land S^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)\land T^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)\to R^{y}_{\leftarrow\lnot\mathtt{max}}(x,y)$. $\bullet$ Make a similar substitution for each above clause (d).

Processing the contradiction clause: Obviously, the contradiction clause $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$ is equivalent to the formula $\mathtt{max}(x)\land\mathtt{max}(y)\land(\mathtt{max}(y)\to R_{\bot}(x,y))\to\bot$ and should be rewritten as $\mathtt{max}(x)\land\mathtt{max}(y)\land(R_{\bot})^{y}_{\leftarrow\mathtt{max}}(x,y)\to\bot$, which is of the required form if the predicate $(R_{\bot})^{y}_{\leftarrow\mathtt{max}}$ is renamed $R_{\bot}$.

9) From initialization clauses to input clauses: The initialization clauses are now of the form $\mathtt{min}(x)\to R(x,y)$ or $\mathtt{min}(x)\land\eta(y)\to R(x,y)$, for $\eta(y)\in\{Q_{s}(y)|s\in\Sigma\}\linebreak\cup\{(\lnot)\mathtt{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: $\mathtt{min}(x)\land\mathtt{min}(y)\land Q_{s}(y)\to R(x,y)$; $\mathtt{min}(x)\land\lnot\mathtt{min}(y)\land Q_{s}(y)\to 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 $\Phi:=\exists\mathbf{R}\forall x\forall y[\bigwedge_{i}C_{i}(x,y)\land\bigwedge_{i\in[1,k]}(\alpha_{i}(x,y)\to\theta_{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 $\alpha_{i}(x,y)\to\theta_{i}(x,y)$ where $\alpha_{i}(x,y)$ is a conjunction of formulas of the only forms $R(x-1,y)\land\lnot\mathtt{min}(x)$, $R(x,y-1)\land\lnot\mathtt{min}(y)$, but not $R(x,y)$, and $\theta_{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 $\theta_{i}$ (containing only atoms of the form $R(x,y)$) according to the input clauses and all the possible conjunctions of hypotheses $\alpha_{i}$ that may be true. Notice the two following facts: the hypotheses of the input clauses are input literals and the conjuncts of the $\alpha_{i}$’s are of the only forms $R(x-1,y)\land\lnot\mathtt{min}(x)$, $R(x,y-1)\land\lnot\mathtt{min}(y)$. So, we can prove by induction on the sum $x+y$ that the obtained formula $\Phi^{\prime}$ 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 $\Phi$. 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(y-b,x-a)$. 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\leq y$, $R(y,x)\iff R^{\mathtt{inv}}(x,y)$. See the details in the appendix.

This achieves the proof of the normalization result $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{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\land Q_{s}(x)\to W^{x}_{s}(x,y)$ and $x=y\land Q_{s}(y)\to 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\land Q_{s}(x)\to R(x,y)$; 2) $\mathtt{min}(x)\land\eta(y)\to R(x,y)$, with $\eta(y)\in\{(\lnot)\mathtt{min}(y),(\lnot)\mathtt{max}(y)\}$; 3) $\mathtt{min}(y)\land\eta(x)\to R(x,y)$, with $\eta(x)\in\{(\lnot)\mathtt{min}(x),(\lnot)\mathtt{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 $\mathtt{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\land Q_{s}(x)\to R(x,y)$; 2) $\mathtt{min}(x)\land\mathtt{min}(y)\to R(x,y)$; 3) $\mathtt{min}(x)\land\lnot\mathtt{min}(y)\to R(x,y)$. Clause 2 can be replaced by the equivalent clause 2’) $x=y\land\mathtt{min}(x)\to R(x,y)$.

Step 9 (from initialization clauses to input clauses) is modified as follows. Define the predicates $R^{\mathtt{min}(x)}$, $R^{\mathtt{min}(y)}$ and $R^{\lnot\mathtt{min}(y)}$ by the initialization clauses4) $x=y\land\mathtt{min}(x)\to R^{\mathtt{min}(x)}(x,y)$ and 5) $x=y\land\mathtt{min}(x)\to R^{\mathtt{min}(y)}(x,y)$, and the computation clauses $\lnot\mathtt{min}(y)\land R^{\mathtt{min}(x)}(x,y-1)\to R^{\mathtt{min}(x)}(x,y)$, $\lnot\mathtt{min}(y)\land R^{\mathtt{min}(y)}(x,y-1)\to R^{\lnot\mathtt{min}(y)}(x,y)$, and $\lnot\mathtt{min}(y)\land R^{\lnot\mathtt{min}(y)}(x,y-1)\to R^{\lnot\mathtt{min}(y)}(x,y)$. This allows to replace the initialization clause 3 by the computation clause $R^{\mathtt{min}(x)}(x,y)\land R^{\lnot\mathtt{min}(y)}(x,y)\to R(x,y)$. After those transformations all the initialization clauses are of the form $x=y\land Q_{s}(x)\to R(x,y)$ (clause 1 above) or $x=y\land\mathtt{min}(x)\to 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\land\mathtt{min}(x)\land Q_{s}(x)\to R(x,y)$, or $x=y\land\lnot\mathtt{min}(x)\land Q_{s}(x)\to 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 $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$. This achieves the proof of the equality $\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$. Lemma 1 is proved. $\square$

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_{\bot}$ till the point $(1,n)$ by the conjunction of the computation clauses $x<y\land R_{\bot}(x+1,y)\to R_{\bot}(x,y)$ and $x<y\land R_{\bot}(x,y-1)\to R_{\bot}(x,y)$ and of the unique contradiction clause $\mathtt{min}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$.

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\in\mathbb{Z}$, whose intuitive meaning is: $W^{x+a}_{s}(x,y)\iff Q_{s}(x+a)\land 1\leq x+a\leq n$ (resp. $W^{y+a}_{s}(x,y)\iff Q_{s}(y+a)\land 1\leq y+a\leq n$). They are inductively defined by the following clauses:

$\bullet$ Initialization clauses (on the diagonal):

$x=y\land Q_{s}(x)\to W_{s}^{x}(x,y)$; $(x=y)\land Q_{s}(x)\to W_{s}^{y}(x,y)$;

$x=y\land Q_{s}(x-a)\land x>a\to W_{s}^{x-a}(x,y)$, and

$x=y\land Q_{s}(x-a)\land x>a\to W_{s}^{y-a}(x,y)$, for $a>0$;

$x=y\land Q_{s}(y+a)\land y\leq n-a\to W_{s}^{x+a}(x,y)$, and

$x=y\land Q_{s}(y+a)\land y\leq n-a\to W_{s}^{y+a}(x,y)$, for $a>0$.

$\bullet$ Transport clauses, for $a\in\mathbb{Z}$:

$x<y\land W^{x+a}_{s}(x,y-1)\to W^{x+a}_{s}(x,y)$, and

$x<y\land W^{y+a}_{s}(x+1,y)\to W^{y+a}_{s}(x,y)$.

This allows to replace each input atom $Q_{s}(x+a)$ (resp. $Q_{s}(y+a)$), $a\in\mathbb{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}(x-a)$ (jointly with $x>a$), or $Q(y+a)$ (jointly with $y\leq n-a$), for $a>0$.

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

As we have done for the $Q_{s}$, we want to make available the information about $\mathtt{min}$ and $\mathtt{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\geq 1$, and $R^{x=n-a}$, $R^{x<n-a}$, for $a\geq 0$, and similarly for $y$, with obvious intuitive meaning: for instance, $R^{y>a}(x,y)\iff y>a$. For example, define the predicate $R^{x=a}$ (resp. $R^{y=a}$) by the two clauses $x=y\land x=a\to R^{x=a}(x,y)$ and $x<y\land R^{x=a}(x,y-1)\to R^{x=a}(x,y)$ (resp. $x=y\land x=a\to R^{y=a}(x,y)$ and $x<y\land R^{y=a}(x+1,y)\\ \to R^{y=a}(x,y)$). As another example, define $R^{x<n-a}$ by the clauses $x=y\land y<n-a\to R^{x<n-a}(x,y)$ and $x<y\land R^{x<n-a}(x,y-1)\to R^{x<n-a}(x,y)$.

This allows to replace the “extremum” atoms $x=a$, $x>a$, $x=n-a$, $x<n-a$ 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 $\mathtt{min}$ (resp. $\mathtt{max}$) only occurs in the form $x=a$ or $x>a$ (resp. in the form $y=n-a$ or $y<n-a$) 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\leavevmode\nobreak\ \in\leavevmode\nobreak\ \mathbf{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)\iff x+a\leq y-b\land R(x+a,y-b)$. As an example, the “normalized” clause $x<y\land S^{x+2,y-2}(x+1,y)\to 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):

an initialization clause $x=y\land\delta\to R(x,y)$, where $\delta$ is

• •

either an input atom $Q_{s}(x)$,

• •

or an equality $x=a$, for a fixed $a\geq 1$, or $y=n-b$, for a fixed $b\geq 0$,

• •

or a conjunction $Q_{s}(x-a)\land x>a$, or

$Q_{s}(y+b)\land y\leq n-b$, for $a,b\geq 1$; 2. 2.

a computation clause of one of the forms (a,b,c):

1. (a)

$x<y\land S(x+1,y)\to R(x,y)$; 2. (b)

$x<y\land S(x,y-1)\to R(x,y)$; 3. (c)

$x\preceq y\land S(x,y)\land T(x,y)\to R(x,y)$, where $\preceq\;\in\{<,=\}$; 3. 3.

“the” contradiction clause

$\mathtt{min}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$, which can be rephrased $x=1\land y=n\land R_{\bot}(x,y)\to\bot$.

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 $x<y\land R_{1}(x+1,y)\land R_{2}(x,y-1)\to R_{3}(x,y)$ is “equivalent” to the conjunction of the following clauses using new predicates $R_{4},R_{5}$: $x<y\land R_{1}(x+1,y)\to R_{4}(x,y)$; $x<y\land R_{2}(x,y-1)\to\\ R_{5}(x,y)$; $x<y\land R_{4}(x,y)\land R_{5}(x,y)\to 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 $\mathtt{max}$ in the initialization clauses). Roughly expressed, for any computation predicate $R\in\mathbf{R}$ and a hypothesis $\eta$, we introduce a new predicate $R_{\leftarrow}^{\eta}$ whose intuitive meaning is: $R_{\leftarrow}^{\eta}(x,y)\iff(\eta\to R(x,y))$.

**5) Elimination of equalities $x=a$ ($a\geq 1$) and $y=n-b$ ($b\geq 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=n-b$) of the clauses. For each $R\in\mathbf{R}$, we introduce the new predicates $R_{\leftarrow}^{x=a}$, $R_{\leftarrow}^{y=n-b}$ and $R_{\leftarrow}^{x=a,y=n-b}$, for all $a\in[1,A]$ and $b\in[0,B]$, whose intuitive meaning has been announced. For example, we should have $R_{\leftarrow}^{x=a,y=n-b}(x,y)\iff(x\leavevmode\nobreak\ =\leavevmode\nobreak\ a\land y=n-b\to R(x,y))$.

Transforming the initialization clauses: Each initialization clause $x=y\land x=a\to R(x,y)$ (resp. $x=y\land y=n-b\to R(x,y)$) is transformed into the clause $x=y\to R_{\leftarrow}^{x=a}(x,y)$ (resp. $x=y\to R_{\leftarrow}^{y=n-b}(x,y)$).

Transforming the computation clauses: To each clause (a) $x<y\land S(x+1,y)\to R(x,y)$ add the clauses $x<y\land S_{\leftarrow}^{x=a,y=n-b}(x+1,y)\to R_{\leftarrow}^{x=a-1,y=n-b}(x,y)$, for all $a\in[2,A]$ and $b\in[0,B]$ (justification: the hypothesis $x+1=a$ is equivalent to $x=a-1$). Similarly, for each clause (b) $x<y\land S(x,y-1)\to R(x,y)$ add the clauses$x<y\land S_{\leftarrow}^{x=a,y=n-b}(x,y-1)\to R_{\leftarrow}^{x=a,y=n-(b-1)}(x,y)$, for all $a\in[1,A]$ and $b\in[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\land S_{\leftarrow}^{x=a}(x+1,y)\to R_{\leftarrow}^{x=a-1}(x,y)$, for all $a\in[2,A]$, and $x<y\land S_{\leftarrow}^{y=n-b}(x+1,y)\to R_{\leftarrow}^{y=n-b}(x,y)$, for all $b\in[0,B]$.

For each clause (c) $x\preceq y\land S(x,y)\land T(x,y)\to R(x,y)$, where $\preceq\;\in\{<,=\}$, add clauses that cumulate the hypotheses provided they are compatible. More precisely, for all $a\in[1,A]$ and $b\in[0,B]$ and any two compatible (possibly empty) subsets $\eta,\theta$ of the set of two hypotheses $\{x=a,y=n-b\}$, we have the clause $x\preceq y\land S_{\leftarrow}^{\eta}(x,y)\land T_{\leftarrow}^{\theta}(x,y)\to R_{\leftarrow}^{\eta\cup\theta}(x,y)$. For example,

$x\preceq y\land S_{\leftarrow}^{x=a}(x,y)\land T_{\leftarrow}^{y=n-b}(x,y)\to R_{\leftarrow}^{x=a,y=n-b}(x,y)$ and $x\preceq y\land S_{\leftarrow}^{y=n-b}(x,y)\land T_{\leftarrow}^{x=a,y=n-b}(x,y)\to R_{\leftarrow}^{x=a,y=n-b}(x,y)$.

Processing the contradiction clause: The contradiction clause is equivalent to $x=1\land y=n\land(x=1\land y\leavevmode\nobreak\ =\leavevmode\nobreak\ n\to R_{\bot}(x,y))\to\bot$. Consequently, it should be replaced by the clause $x=1\land y=n\land(R_{\bot})_{\leftarrow}^{x=1,y=n}(x,y)\to\bot$, which is the contradiction clause required if the predicate $(R_{\bot})_{\leftarrow}^{x=1,y=n}$ is renamed $R_{\bot}$.

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\land Q_{s}(x)\to R(x,y)$ as required777Note that an initialization clause of the form $x=y\to R(x,y)$ can be rewritten $\bigwedge_{s\in\Sigma}(x=y\land Q_{s}(x)\to R(x,y))$ (separation in cases)..

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 $\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$, i.e., Lemma 2. $\square$

4 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\in\mathbf{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 $\mathbf{R}$ of predicates that will be used in formulas expressing the computation of an automaton $\mathcal{A}$, with $Q$ the set of its states, is $\mathbf{R}=\{R_{q}\mid q\in Q\}$. The intuitive meaning of this predicates is the following: $R_{q}(c,t)$ is true $\iff$ the cell $c$ is in the state $q$ at time $t$.

Encoding predicates by automata states

Let $\Phi$ be a formula defining a language $L$, in one of our logics, of the form $\Phi=\exists\mathbf{R}\forall x\forall y\psi(x,y)$ with $\mathbf{R}=(R_{1},\dots,R_{m})$ and $R_{1}=R_{\bot}$. The set of states that will be used by an automaton $\mathcal{A}$ accepting $L$ is $Q=\{\sharp,\lambda\}\cup\{0,1\}^{m}$ with $\sharp$ the permanent state and $\lambda$ the quiescent state. We denote by $(q)_{i}$ ($i\in[1,m]$), the $i^{th}$ bit of a state $q\in\{0,1\}^{m}$. Intuitively, $(q)_{i}$ refers to the predicate $R_{i}$. Since the predicate $R_{1}=R_{\bot}$ represents the “false”, the set of accepting states is the set of states $q\in\{0,1\}^{m}$ with the first bit $(q)_{1}$ equal to 0, that is $Q_{accept}=\{0\}\times\{0,1\}^{m-1}$.

4.1 Logical characterization of $\mathtt{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 $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$.

Theorem 1**.**

$\mathtt{RealTime_{CA}}=\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$

The proof will use the following inclusion scheme:

$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}\subseteq\mathtt{RealTime_{OIA}}$

$=\mathtt{RealTime_{CA}}\subseteq\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$

The equality $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ has already been proved in Section 3 and the other equality $\mathtt{RealTime_{OIA}}=\mathtt{RealTime_{CA}}$ is folklore in automata theory. Two inclusions are left to be proved.

Lemma 3**.**

$\mathtt{RealTime_{CA}}\subseteq\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$

Proof.

We will show that for each automaton $\mathcal{A}\in\mathtt{RealTime_{CA}}$ we can build a formula $\Phi\in\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ such that: $w\in L(\mathcal{A})\iff\langle w\rangle\text{ satisfies the formula }\Phi$.

First of all, one can be easily convinced that the computation power of a CA $\mathcal{A}\in\mathtt{RealTime_{CA}}$ with neighborhood $\mathcal{N}_{\mathcal{A}}=\{-1,0,1\}$ is equal to the computation power of a OCA $\mathcal{A}^{\prime}$ with neighborhood $\mathcal{N}_{\mathcal{A}^{\prime}}=\{-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 $\mathcal{A}$ with the variable change: $c\mapsto 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(\mathcal{A})=L(\mathcal{A^{\prime}})$.

Input: The parallel input of $\mathcal{A}^{\prime}$ is expressed by the conjunction $\psi_{input}=\bigwedge_{s\in\Sigma}(\mathtt{min}(t)\land Q_{s}(c)\to R_{s}(c,t))$ for $\Sigma$ the input alphabet: each cell $c$ is in the state $w_{c}\in\Sigma$ at the start of the computation.

Computation: The state evolution of a cell of $\mathcal{A}^{\prime}$ is given by the transition function:

$\langle c,t\rangle=\delta_{\mathcal{A}^{\prime}}(\langle c-2,t-1\rangle,\langle c-1,t-1\rangle,\langle c,t-1\rangle)$.

A transition rule $\delta_{\mathcal{A}^{\prime}}(q_{2},q_{1},q_{0})=q$ for $q_{2}\neq\sharp$ is expressed by the computation clause:

$c>t\land\lnot\mathtt{min}(t)\land R_{q_{2}}(c-2,t-1)\land R_{q_{1}}(c-1,t-1)\linebreak\land R_{q_{0}}(c,t-1)\to R_{q}(c,t)$.

The specific case where $q_{2}$ is the permanent state $\sharp$ ($\delta_{\mathcal{A}^{\prime}}(\sharp,q_{1},q_{0})=q$) is handled by the clause:

$c=t\land\lnot\mathtt{min}(t)\land R_{q_{1}}(c-1,t-1)\land R_{q_{0}}(c,t-1)\to R_{q}(c,t)$.

We denote $\psi_{compute}$ the conjunction of the above two sets of clauses.

Remark: By construction of $\psi_{input}$ and $\psi_{compute}$, we have the following equivalence for $\psi^{\prime}\coloneqq\psi_{input}\land\psi_{compute}$. The computation atom $R_{q}(c,t)$ is true in the minimal model ($\langle w\rangle,\mathbf{R}$) of $\forall c\forall t\psi^{\prime}(c,t)$ $\iff$ the cell $c$ is in the state $q$ at time $t$.

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

$\psi_{output}\coloneqq\bigwedge_{q\in Q\setminus Q_{accept}}(\mathtt{max}(c)\land\mathtt{max}(t)\land R_{q}(c,t)\to\bot)$

The formula $\psi$ expressing the computation of $\mathcal{A}^{\prime}$ is the conjunction $\psi\coloneqq\psi^{\prime}\land\psi_{output}$.

For each word $w=w_{1}\dots w_{n}\in\Sigma^{+}$ we have the following equivalences:

The cell $1$ of $\mathcal{A}$ is in an accepting state $q$ at time $n$

$\iff$

The cell $n$ of $\mathcal{A}^{\prime}$ is in an accepting state $q$ at time $n$

$\iff$

The conjunction $\bigwedge_{q\in Q\setminus Q_{accept}}R_{q}(n,n)$ is false in the minimal model $(\langle w\rangle,\mathbf{R})$ of $\forall c\forall t\psi^{\prime}(c,t)$

$\iff$

$\langle w\rangle$ satisfies the formula $\exists\mathbf{R}\forall c\forall t\psi(c,t)$.

This proves $L(\mathcal{A})\in\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$. ∎

Lemma 4**.**

$\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}\subseteq\mathtt{RealTime_{OIA}}$

Proof.

We will show that for every language $L\subseteq\Sigma^{+}$ defined by a formula $\Phi\in\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$, a one-way iterative array $\mathcal{A}\in\mathtt{RealTime_{OIA}}$ can be constructed such that $L=L(\mathcal{A})$.

Let $\Phi\in\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ be a formula of the form $\Phi=\exists\mathbf{R}\forall x\forall y\psi(x,y)$ where $\mathbf{R}=(R_{1},\dots,R_{m})$ with $R_{1}=R_{\bot}$ and $\psi$ is a conjunction of Horn clauses of the three following forms:

• •

input clause of either form:

$\mathtt{min}(x)\land\mathtt{min}(y)\land Q_{s}(y)\to R(x,y)$ or $\mathtt{min}(x)\land\lnot\mathtt{min}(y)\land Q_{s}(y)\to R(x,y)$,

• •

the contradiction clause $\mathtt{max}(x)\land\mathtt{max}(y)\land R_{\bot}(x,y)\to\bot$;

• •

computation clause of one of the following forms for some sets $H,H^{\prime}\subseteq[1,m]$ and $i\in[1,m]$:

• –

$\lnot\mathtt{min}(x)\land\bigwedge_{h\in H}R_{h}(x-1,y)\land\lnot\mathtt{min}(y)\land\bigwedge_{h\in H^{\prime}}R_{h}(x,y-1)\to R_{i}(x,y)$;

• –

$\lnot\mathtt{min}(x)\land\bigwedge_{h\in H}R_{h}(x-1,y)\to R_{i}(x,y)$;

• –

$\lnot\mathtt{min}(y)\land\bigwedge_{h\in H}R_{h}(x,y-1)\to R_{i}(x,y)$.

We will denote $\psi^{\prime}$ the formula $\psi$ without the contradiction clause.

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

For all $i\in[1,m]$ ; $s\in\Sigma$ ; $q,l,r\in Q\setminus\{\sharp,\lambda\}$:

Input transition function: $\delta_{\mathtt{input}}:\Sigma\times Q\to Q$. The bit $(\delta_{input}(s,\sharp))_{i}$ is $1$ if and only if there is an input clause $\mathtt{min}(x)\land\mathtt{min}(y)\land Q_{s}(y)\to R_{i}(x,y)$ in $\psi$. $(\delta_{input}(s,q))_{i}$ is $1$ if and only if there exists in $\psi$ an input clause $\mathtt{min}(x)\land\lnot\mathtt{min}(y)\land Q_{s}(y)\to R_{i}(x,y)$ or a computation clause $\lnot\mathtt{min}(y)\land\bigwedge_{h\in H}R_{h}(x,y-1)\to R_{i}(x,y)$ with $(q)_{h}=1$, for all $h\in H$.

Transition function: $\delta:Q\times Q\to Q$ applied on all cells $c\in[2,n]$. The bit $(\delta(l,r))_{i}$ is $1$ if and only if there exists in $\psi$ a computation clause $\bigwedge_{h\in H}R_{h}(x-1,y)\land\lnot\mathtt{min}(x)\land\bigwedge_{h\in H^{\prime}}R_{h}(x,y-1)\land\lnot\mathtt{min}(y)\to R_{i}(x,y)$ such that $(l)_{h}=1$ for all $h\in H$ and $(r)_{h}=1$ for all $h\in H^{\prime}$.

The bit $(\delta(l,\lambda))_{i}$ is $1$ if and only if there is in $\psi$ a computation clause $\lnot\mathtt{min}(x)\land\bigwedge_{h\in H}R_{h}(x-1,y)\to R_{i}(x,y)$ such that $(l)_{h}=1$, for all $h\in H$.

Let $\mathcal{A}=(Q,\Sigma,Q_{accept},\mathcal{N},\delta_{\mathtt{input}},\delta)$ be the OIA defined above after making the change of variables of Figure 5:$c=x$; $t=x+y-1$. By construction of $\mathcal{A}$, we have the following equivalences concluding the proof.

$\forall w\in\Sigma^{n}$:

$\forall(a,b)\in[1,n]^{2},\forall i\in[1,m]$, the atom $R_{i}(a,b)$ is true in the minimal model $(\langle w\rangle,\mathbf{R})$ of $\forall x\forall y\;\psi^{\prime}(x,y)$ $\iff$ The cell $c=a$ is at time $t=a+b-1$ in a state $q$ with $(q)_{i}=1$. 2. 2.

$\mathcal{A}$ accepts $w$ in real-time $\iff$ $\langle w\rangle$ satisfies $\Phi$.

∎

4.2 Logical characterization of $\mathtt{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 $\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$.

Theorem 2**.**

$\mathtt{RealTime_{IA}}=\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$.

The proof of Theorem 2 is close to the one of Theorem 1 and is obtained by the following inclusion scheme:

$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$

$\subseteq\mathtt{RealTime_{IA}}\subseteq\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$.

The equality $\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$ has been already proved in Section 3. We will now prove the two remaining inclusions.

Lemma 5**.**

$\mathtt{RealTime_{IA}}\subseteq\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$.

Proof.

Let $\mathcal{A}$ be an automaton in $\mathtt{RealTime_{IA}}$, we apply the transformation $c\mapsto c+t-1$ on its time-space diagram. This transformation gives us a new automaton $\mathcal{A^{\prime}}$ with the neighborhood $\mathcal{N^{\prime}}=\{-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 $\mathtt{RealTime_{IA}}$ and an automaton in $\mathtt{RealTime_{CA}}$, the computation clauses and the contradiction clauses will stay the same.

Input: The diagonal input of $\mathcal{A^{\prime}}$ is expressed by the conjunction of the input clauses:

$\psi_{input}\coloneqq\bigwedge_{s\in\Sigma}(t=c\land Q_{s}(c)\to R_{s}(c,t))$ for $\Sigma\subset Q$.

Computation: The conjunction $\psi_{compute}$ is defined from the transition rules of $\mathcal{A^{\prime}}$ as in the previous section.

Let $\psi^{\prime}$ be the conjunction $\psi_{input}\land\psi_{compute}$.

Output: The output reading is done on the same cell as in the previous section.

$\psi_{output}\coloneqq\bigwedge_{q\in Q\setminus Q_{accept}}(\mathtt{max}(c)\land\mathtt{max}(t)\land R_{q}(c,t)\to\bot)$

The formula $\psi$ of $\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$ expressing the computation of $\mathcal{A}^{\prime}$ is: $\psi\coloneqq\psi^{\prime}\land\psi_{output}$.

For each word $w=w_{1}\dots w_{n}\in\Sigma^{+}$ we have the following equivalences:

The cell $1$ of $\mathcal{A}$ is in an accepting state $q$ at time $n$

$\iff$

The cell $n$ of $\mathcal{A}^{\prime}$ is in an accepting state $q$ at time $n$

$\iff$

The conjunction $\bigwedge_{q\in Q\setminus Q_{accept}}R_{q}(n,n)$ is false in the minimal model $(\langle w\rangle,\mathbf{R})$ of $\forall c\forall t\psi^{\prime}(c,t)$

$\iff$

$\langle w\rangle$ satisfies the formula $\exists\mathbf{R}\forall c\forall t\psi(c,t)$.

This proves $L(\mathcal{A})\in\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}$.

∎

Lemma 6**.**

$\mathtt{normal}$-$\mathtt{pred}$-$\mathtt{dio}$-$\mathtt{ESO}$-$\mathtt{HORN}\subseteq\mathtt{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)\in[1,n]^{2}$ such that $x\leq y$ a site $(c,t)$ of the space-time diagram of an iterative array $\mathcal{A}$ running in real-time (see Figure 6). The sites $(x,y)\in[1,n]^{2}$ such that $x\geq y$ are similarly handled.

First, we apply to the set of sites $(x,y)$ of the dependency graph of $\Phi$ the variable change $c^{\prime}=y-x+1;t^{\prime}=x+y-1$. This variable change turns respectively the dependencies $(x-1,y)\to(x,y)$ and $(x,y-1)\to(x,y)$ into $(c^{\prime}+1,t^{\prime}-1)\to(c^{\prime},t^{\prime})$ and $(c^{\prime}-1,t^{\prime}-1)\to(c^{\prime},t^{\prime})$ expressing the two-way communication of an iterative array $\mathcal{A^{\prime}}$. The sites $(c^{\prime},t^{\prime})$ of the space-time diagram of $\mathcal{A^{\prime}}$ takes their values in $[1,n]\times[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 $\mathcal{A}$ running in real time, each site $(c,t)=(\left\lceil{c^{\prime}/2}\right\rceil,\left\lceil{t^{\prime}/2}\right\rceil)$ of this diagram will record the set of sites $\{(c^{\prime}-1,t^{\prime}-1),(c^{\prime},t^{\prime}),(c^{\prime}+1,t^{\prime}-1)\}$ of the space-time diagram of $\mathcal{A^{\prime}}$, with $c^{\prime}$ and $t^{\prime}$ odd and greater than $1$ (see Figure 6).

∎

4.3 Logical characterization of $\mathtt{Trellis}$ and linear conjunctive grammars

Conjunctive grammars, introduced by Okhotin [21], are an extension of context-free grammars. This class of formal grammars is obtained by allowing the use of a conjunction operator (denoted $\&$) in the right side of the context-free rules, meaning an intersection between derived languages. It has been shown in [21] 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 $\mathcal{G}=(\Sigma,N,P,S)$ in normal form is a rule of the form:

$A\to sB_{1}\&\dots\&sB_{\ell}\&C_{1}t\&\dots\&C_{p}t$ or $A\to s$

with $\ell+p\geq 1$, $A,B_{i},C_{j}\in N$ and $s,t\in\Sigma$;

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\to sB_{1}\&\dots\&sB_{\ell}\&C_{1}t\&\dots\&C_{p}t$

gives us the language equation:

$L(A)=sL(B_{1})\cap\dots\cap sL(B_{\ell})\cap L(C_{1})t\cap\dots\cap 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\in\Sigma^{+}$ we have:

$L\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ $\iff$ $(\Sigma^{+}\setminus L)\in LinConj$ .*

The theorem is proved in two steps.

Lemma 7**.**

$L\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}\Rightarrow(\Sigma^{+}\setminus L)\in LinConj$

Proof.

Let us show that for each language $L\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$ defined by a formula $\Phi\in\mathtt{normal}$-$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$, $\Phi=\exists\mathbf{R}\forall x\forall y\psi(x,y)$, we can build a grammar $G_{\Phi}=(\Sigma,N,P,S)$ such that: $w\in L\iff w\notin L(G_{\Phi})$

The grammar $G_{\Phi}$ is defined as follows.

The set of non-terminal symbols of $G_{\Phi}$ is $N=\mathbf{R}$ and $S=R_{\bot}$ is the start symbol. The rules of $\mathcal{G}_{\Phi}$ are the following:

To each input clause $x=y\land Q_{s}(x)\to R(x,y)$ of $\Phi$ we associate the rule $R\to s$.

To each computation clause of $\Phi$

$x<y\land S_{1}(x+1,y)\land\ldots\land S_{\ell}(x+1,y)\land T_{1}(x,y-1)\land\ldots\land T_{p}(x,y-1)\to R(x,y)$ we associate the rules

$R\to sS_{1}\&\ldots\&sS_{\ell}\&T_{1}t\&\ldots\&T_{p}t$, for all $s,t\in\Sigma$.

Let $\psi^{\prime}$ be the conjunction $\psi$ without the contradiction clause. By an easy induction, the following equivalence can be proved, for all $R\in\mathbf{R}$, all words $w=w_{1}\dots w_{n}\in\Sigma^{+}$, and all intervals $[a,b]\subseteq[1,n]$:

$w_{a}\dots w_{b}\in L(R)\iff$

$\left(\forall x\forall y\psi^{\prime}\land\bigwedge_{i\in[a,b]}Q_{w_{i}}(i)\right)\to R(a,b)$ is a tautology.

Taking $R=R_{\bot}$ and $[a,b]=[1,n]$ we obtain:

$w\in L(G_{\Phi})\iff\langle w\rangle\nvDash\Phi$ as claimed.

∎

Lemma 8**.**

$(\Sigma^{+}\setminus L)\in LinConj\Rightarrow L\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$

Proof.

Let $L$ be a language, subset of $\Sigma^{+}$, such that $(\Sigma^{+}\setminus L)\in LinConj$. We associate to the linear grammar $\mathcal{G}=(\Sigma,N,P,S)$ defining $(\Sigma^{+}\setminus L)$ with $N=\{A_{1},\ldots,A_{k}\}$ in normal form, as presented above, the formula $\Phi_{\mathcal{G}}:=\exists\mathbf{R}\forall x\forall y\psi(x,y)$ with $\mathbf{R}=\{A_{1},\ldots,A_{k}\}$ and $\psi$ the conjunction of the following Horn clauses:

the computation clause $x<y\land Q_{s}(x)\land\bigwedge_{i=1}^{\ell}B_{i}(x+1,y)\land\linebreak\bigwedge_{i=1}^{p}C_{i}(x,y-1)\land Q_{t}(y)\to A(x,y)$ for each rule $A\to sB_{1}\&\ldots\&sB_{\ell}\&C_{1}t\&\ldots\&C_{p}t$;

the clause $x=y\land Q_{s}(x)\to A(x,y)$ for each rule $A\to s$ ;

and the contradiction clause $\mathtt{min}(x)\land\mathtt{max}(y)\land S(x,y)\to\bot$.

The proof of the equivalence $w\in L(\mathcal{G})\iff\langle w\rangle\models\Phi_{\mathcal{G}}$ is the same as for the previous Lemma 7. ∎

Logical characterization of $\mathtt{Trellis}$

Clearly, the final state (result) $q$ of a trellis automaton $\mathcal{A}=(Q,\Sigma,Q_{accept},\delta)$ acting on a word $w_{x}\dots w_{y}$ of length greater than $1$ ($x<y$) is completely determined by the final state $q_{l}$ of $\mathcal{A}$ acting on the prefix $w_{x}\dots w_{y-1}$ and the final state $q_{r}$ of $\mathcal{A}$ acting on the suffix $w_{x+1}\dots w_{y}$: $q=\delta(q_{l},q_{r})$. This functional dependence $\left((x,y-1),(x+1,y)\right)\to(x,y)$ is exactly expressed by the computation clauses of the normalized inclusive logic. This suggests the following equality.

Theorem 4**.**

$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}=\mathtt{Trellis}$

The theorem is proved in two steps.

Lemma 9**.**

$\mathtt{Trellis}\subseteq\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$

Proof.

Let $\mathcal{A}$ be a trellis automaton that accepts a language $L\subseteq\Sigma^{+}$ and let be a word $w=w_{1}\dots w_{n}\in\Sigma^{+}$. Let us introduce the set of binary predicates $\mathbf{R}=\{R_{q}\mid q\in Q\}$ with intuitive meaning: $R_{q}(x,y)$ is true $\iff$ the final state of $\mathcal{A}$ acting on the subword $w_{x}\dots w_{y}$ is $q$. The following clauses describe the computation of $\mathcal{A}$.

Input clauses:

$\psi_{input}\coloneqq\bigwedge_{s\in\Sigma}(x=y\land Q_{s}(x)\to R_{s}(x,y))$, for $s\in\Sigma$.

Computation clauses:

$\psi_{compute}\coloneqq\bigwedge_{(q_{l},q_{r})\in Q^{2}}\left(x<y\land R_{q_{l}}(x,y-1)\land\right.\linebreak\left.R_{q_{r}}(x+1,y)\to R_{q}(x,y)\right)$ where $q=\delta(q_{l},q_{r})$.

Contradiction clauses:

$\psi_{output}\coloneqq\bigwedge_{q\in Q\setminus Q_{accept}}(\mathtt{min}(x)\land\mathtt{max}(y)\land R_{q}(x,y)\to\bot)$

Let $\psi^{\prime}\coloneqq\psi_{input}\land\psi_{compute}$ and $\psi\coloneqq\psi^{\prime}\land\psi_{output}$.

For each word $w=w_{1}\dots w_{n}\in\Sigma^{+}$ we have the following equivalences:

$\mathcal{A}$ accepts $w$ in time $n$

$\iff$

The conjunction $\bigwedge_{q\in Q\setminus Q_{accept}}R_{q}(1,n)$ is false in the minimal model $(\langle w\rangle,\mathbf{R})$ of $\forall x\forall y\psi^{\prime}(x,y)$

$\iff$

$\langle w\rangle$ satisfies the formula $\exists\mathbf{R}\forall x\forall y\psi(x,y)$.

This proves $L(\mathcal{A})\in\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$. ∎

Lemma 10**.**

$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}\subseteq\mathtt{Trellis}$

Proof sketch.

Let $\Phi$ be a formula of $\mathtt{normal}$-$\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{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 $\Phi$ as in sections 4.1 and 4.2.

∎

5 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 [18], and has several equivalent characterizations in other frameworks: e.g, $\mathtt{Trellis}$ is the class of linear conjunctive languages [21].

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 real-time. This is exemplified by languages $\mathtt{notBordered}$ and $\mathtt{Palindrome}$, which can be succinctly defined in $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{HORN}$ and $\mathtt{incl}$-$\mathtt{ESO}$-$\mathtt{HORN}$, respectively, and hence, belong to $\mathtt{RealTime}_{\mathtt{CA}}$ and $\mathtt{Trellis}$, respectively. Conversely, the problem $\mathtt{Prime}:=\{w\in\Sigma^{*}\;|\;|w|$ is a prime integer$\}$ belongs to $\mathtt{RealTime}_{\mathtt{CA}}$ (and to $\mathtt{RealTime}_{\mathtt{IA}})$ by Fischer’s algorithm [6, 7]; therefore, it belongs to $\mathtt{pred}$-$\mathtt{ESO}$-$\mathtt{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 [10], for easier programming inside these logics and without changing their real-time complexity.

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.

Appendix A: Expressing natural problems in our logics

Expressing problems $\mathtt{Palindrome}$ and $\mathtt{notPalindrome}$ in inclusion logic

The problem $\mathtt{Palindrome}$ is expressed by the conjunction of the following clauses:

$x<y\land Q_{s}(x)\land Q_{t}(y)\to\mathtt{notPal}(x,y)$, for all $s,t\in\Sigma$ with $s\neq t$;

$x<y\land\mathtt{notPal}(x+1,y-1)\to\mathtt{notPal}(x,y)$;

$x\leq y\land\mathtt{min}(x)\land\mathtt{max}(y)\land\mathtt{notPal}(x,y)\to\bot$.

The problem $\mathtt{notPalindrome}$ is expressed by the conjunction of the following clauses: $x=y\to\mathtt{Pal}(x,y)$,

$x\leq y\land\mathtt{Successor}(x,y)\land Q_{s}(x)\land Q_{s}(y)\to\mathtt{Pal}(x,y)$,

$x<y\land\mathtt{Pal}(x+1,y-1)\land Q_{s}(x)\land Q_{s}(y)\to\mathtt{Pal}(x,y)$, for all $s\in\Sigma$, and $x\leq y\land\mathtt{Pal}(x,y)\to\bot$.

Here, $\mathtt{Successor}(x,y)$ intuitively means $x+1=y$ and is defined by the following clauses: $x=y\to\mathtt{Equal}(x,y)$ and $x<y\land\mathtt{Equal}(x+1,y)\to\mathtt{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 $\Phi$ can be rewritten in the form

$\Phi:=\exists\mathbf{R}\forall x\forall y[\bigwedge_{i}C_{i}(x,y)\land\bigwedge_{i\in[1,k]}(\alpha_{i}(x,y)\to\theta_{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 $\alpha_{i}(x,y)\to\theta_{i}(x,y)$ where $\alpha_{i}(x,y)$ is a conjunction of formulas of the only forms $R(x-1,y)\land\lnot\mathtt{min}(x)$, $R(x,y-1)\land\lnot\mathtt{min}(y)$, but not $R(x,y)$, and $\theta_{i}(x,y)$ is a Horn clause all the atoms of which are of the form $R(x,y)$.

We number $R_{1},\ldots,R_{m}$ the computation predicates of $\mathbf{R}$. To each subset $J\subseteq[1,k]$ of the family of implications $(\alpha_{i}(x,y)\to\theta_{i}(x,y))_{i\in[1,k]}$ let us associate the set

$K_{J}:=\{h\in[1,m]\;|\;\bigwedge_{i\in J}\theta_{i}(x,y)\to R_{h}(x,y)$ is a tautology$\}$.

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\mapsto K_{J}$ is monotonous: for $J^{\prime}\subseteq J$, we have $K_{J^{\prime}}\subseteq K_{J}$ because $\bigwedge_{i\in J^{\prime}}\theta_{i}(x,y)\to R_{h}(x,y)$ implies $\bigwedge_{i\in J}\theta_{i}(x,y)\to R_{h}(x,y)$.

Clearly, it is enough to prove the following claim:

Claim 1**.**

The formula $\Phi$ is equivalent to the normalized formula

[TABLE]

Proof of the implication $\Phi\Rightarrow\Phi^{\prime}$: It is enough to prove the implication

[TABLE]

for all set $J\subseteq[1,k]$. The implication to be proved can be equivalently written:

[TABLE]

This implication is a straightforward consequence of the two following facts: The sub-formula between brackets above implies the conjunction $\bigwedge_{i\in J}\theta_{i}(x,y)$. As the implication $\bigwedge_{i\in J}\theta_{i}(x,y)\to\bigwedge_{h\in K_{J}}R_{h}(x,y)$ is a tautology (by definition of $K_{J}$), the implication to be proved is a tautology too.

The converse implication $\Phi^{\prime}\Rightarrow\Phi$ 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}\land\ldots\land p_{k}\to p_{0}$ where $k\geq 0$ and the $p_{i}$’s are propositional variables. Let $F^{\prime}$ be the conjunction of propositional variables $q$ such that the implication $F\to q$ is a tautology. $F$ has the same minimal model888For example, for $F:=p_{1}\land p_{3}\land(p_{1}\land p_{3}\to p_{5})\land(p_{1}\land p_{2}\to p_{4})$, we have $F^{\prime}:=p_{1}\land p_{3}\land 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$. as $F^{\prime}$.

Proof of the implication $\Phi^{\prime}\Rightarrow\Phi$: Let $\langle w\rangle$ be a model of $\Phi^{\prime}$ and let $(\langle w\rangle,\mathbf{R})$ be the minimal model of the Horn formula

[TABLE]

It is enough to show that $(\langle w\rangle,\mathbf{R})$ also satisfies the formula

[TABLE]

As each $\alpha_{i}$ is a conjunction of formulas of the form$R(x-1,y)\land\lnot\mathtt{min}(x)$, or $R(x,y-1)\land\lnot\mathtt{min}(y)$, we make an induction on the domain $\{(a,b)\in[1,n]^{2}\;|\;a+b\leq t\}$, for $t\in[1,2n]$. More precisely, we are going to prove, by recurrence on the integer $t\in[1,2n]$, that the minimal model $(\langle w\rangle,\mathbf{R})$ of $\varphi^{\prime}$ satisfies the “relativized” formula $\varphi_{t}$ of the formula $\varphi$ defined by

[TABLE]

As the hypothesis $x+y\leq 2n$ holds for all $x,y$ in the domain $[1,n]$, $\varphi_{2n}$ is equivalent to $\varphi$ on the structure $(\langle w\rangle,\mathbf{R})$.

Basis case: For $t=1$ the set $\{(a,b)\in[1,n]^{2}\;|\;a+b\leq t\}$ is empty so that the “relativized” formula $\varphi_{1}$ is trivially true in the minimal model $(\langle w\rangle,\mathbf{R})$ of $\varphi^{\prime}$.

Recurrence step: Suppose $(\langle w\rangle,\mathbf{R})\models\varphi_{t-1}$, for an integer $t\in[2,2n]$. It is enough to show that, for each couple $(a,b)\in[1,n]^{2}$ such that $a+b=t$, we have $(\langle w\rangle,\mathbf{R})\models\bigwedge_{i\in[1,k]}(\alpha_{i}(a,b)\to\theta_{i}(a,b))$. Let $J_{a,b}$ be the set of indices $i\in[1,k]$ such that the couple $(a,b)$ satisfies $\alpha_{i}$:

[TABLE]

Recall that each $\alpha_{i}(a,b)$ is a (possibly empty) conjunction of atoms $R(a^{\prime},b^{\prime})$ with $(a^{\prime},b^{\prime})=(a-1,b)$ or $(a^{\prime},b^{\prime})=(a,b-1)$, therefore such that $a^{\prime}+b^{\prime}=t-1$. Let any set $J\subseteq[1,k]$. Let us examine the two possible cases:

1. $J\subseteq J_{a,b}$: then the conjunction $\bigwedge_{i\in J}\alpha_{i}(a,b)$ holds in $(\langle w\rangle,\mathbf{R})$; hence, in $(\langle w\rangle,\mathbf{R})$, the conjunction $\bigwedge_{h\in K_{J}}(\bigwedge_{i\in J}\alpha_{i}(a,b)\to R_{h}(a,b))$ is equivalent to $\bigwedge_{h\in K_{J}}R_{h}(a,b)$;

2. $J\setminus J_{a,b}\neq\emptyset$: then the conjunction $\bigwedge_{i\in J}\alpha_{i}(a,b)$ is false in $(\langle w\rangle,\mathbf{R})$; hence, the conjunction $\bigwedge_{h\in K_{J}}(\bigwedge_{i\in J}\alpha_{i}(a,b)\to R_{h}(a,b))$ holds in $(\langle w\rangle,\mathbf{R})$.

From (1) and (2), we deduce that in $(\langle w\rangle,\mathbf{R})$ the conjunction $\bigwedge_{J\subseteq[1,k]}\bigwedge_{h\in K_{J}}(\bigwedge_{i\in J}\alpha_{i}(a,b)\to R_{h}(a,b))$ is equivalent to the conjunction $\bigwedge_{J\subseteq J_{a,b}}\bigwedge_{h\in K_{J}}R_{h}(a,b)$, which can be simplified as $\bigwedge_{h\in K_{J_{a,b}}}R_{h}(a,b)$ because $J\subseteq J_{a,b}$ implies $K_{J}\subseteq K_{J_{a,b}}$. Consequently, for all $h\in[1,m]$, the minimal model $(\langle w\rangle,\mathbf{R})$ of the Horn formula $\varphi^{\prime}$ satisfies the atom $R_{h}(a,b)$ iff $h$ belongs to $K_{J_{a,b}}$. By definition,

$K_{J_{a,b}}:=\{h\in[1,m]\;|\;\bigwedge_{i\in J_{a,b}}\theta_{i}(x,y)\to R_{h}(x,y)$ is a tautology$\}$

or, equivalently,

$K_{J_{a,b}}:=\{h\in[1,m]\;|\;\bigwedge_{i\in J_{a,b}}\theta_{i}(a,b)\to R_{h}(a,b)$ is a tautology$\}$.

As a consequence of Lemma 11, the two conjunctions $\bigwedge_{i\in J_{a,b}}\theta_{i}(a,b)$ and $\bigwedge_{h\in K_{J_{a,b}}}R_{h}(a,b)$ have the same minimal model, which is also the restriction of the minimal model $(\langle w\rangle,\mathbf{R})$ of $\varphi^{\prime}$ to the set of atoms $R_{h}(a,b)$, for $h\in[1,m]$. Therefore, if $i\in J_{a,b}$, then $(\langle w\rangle,\mathbf{R})\models\theta_{i}(a,b)$. If $i\in[1,k]\setminus J_{a,b}$, then we have $(\langle w\rangle,\mathbf{R})\models\lnot\alpha_{i}(a,b)$, by definition of $J_{a,b}$. Therefore, for all $i\in[1,k]$, we get $(\langle w\rangle,\mathbf{R})\models\lnot\alpha_{i}(a,b)\lor\theta_{i}(a,b)$. In other words, for all $(a,b)$ such that $a+b=t$:

[TABLE]

and then $(\langle w\rangle,\mathbf{R})\models\varphi_{t}$.

This concludes the inductive proof that $(\langle w\rangle,\mathbf{R})\models\varphi_{t}$, for all $t\in[1,2n]$, and then $\langle w\rangle\models\Phi$. This proves the converse implication $\Phi^{\prime}\Rightarrow\Phi$. Claim 1 is demonstrated. $\square$

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(y-b,x-a)$. 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)\land\lnot\mathtt{min}(x)\to R(x,y)$;

(b) $S(x,y-1)\land\lnot\mathtt{min}(y)\to R(x,y)$;

(c) $S(x,y)\land T(x,y)\to R(x,y)$; (d) $S(y,x)\to 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)\land\lnot\mathtt{min}(x)\land R_{2}(x,y-1)\linebreak\land\lnot\mathtt{min}(y)\land R_{3}(y,x)$ $\to 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)\land\lnot\mathtt{min}(x)\to R_{5}(x,y)$;

$R_{2}(x,y-1)\land\lnot\mathtt{min}(y)\to R_{6}(x,y)$; $R_{5}(x,y)\land R_{6}(x,y)\to R_{7}(x,y)$; $R_{3}(y,x)\to R_{8}(x,y)$; $R_{7}(x,y)\land R_{8}(x,y)\to 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)\to R(x,y)$.

Obviously, such a clause is equivalent to the conjunction of the two clauses (i) $x\leq y\land S(y,x)\to R(x,y)$ and (ii) $y\leq x\land S(y,x)\to R(x,y)$. The equivalent “folded” form of clause (i) is $x\leq y\land S^{\mathtt{inv}}(x,y)\to R(x,y)$. The clause (ii) is equivalent to the clause $x\leq y\land S(x,y)\to R(y,x)$ the equivalent “folded” form of which is $x\leq y\land S(x,y)\to R^{\mathtt{inv}}(x,y)$. Finally, steps 8-10 are not modified.

Step 6 of Lemma 2: Elimination of atoms $Q_{s}(x-a)$, $Q_{s}(y+b)$, for $a,b>0$: This step is quite similar to step 5. For each $R\in\mathbf{R}$, we introduce new predicates:

$R_{\leftarrow s_{1},\dots,s_{l},t_{1},\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y+b_{1},\dots,y+b_{m}}$ with $l,m\geq 0$, the $s_{i},t_{j}\in\Sigma$,

$0\leq a_{1}<a_{2}\ldots<a_{l}\leq A$ and $0\leq b_{1}<b_{2}\ldots<b_{m}\leq\leavevmode\nobreak\ 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_{\leftarrow s_{1},\dots,s_{l},t_{1},\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y+b_{1},\dots,y+b_{m}}(x,y)\iff$

$[\;[\bigwedge_{i=1,\ldots,l}(Q_{s_{i}}(x-a_{i})\land x>a_{i})$

$\land\bigwedge_{j=1,\ldots,m}(Q_{t_{j}}(y+b_{j})\land y\leq n-b_{j})]\to R(x,y)\;]$.

Transforming the initialization clauses: Each initialization clause $x=y\land Q_{s}(x-a)\land x>a\to R(x,y)$, $a\geq 1$, (resp. $x=y\land Q_{s}(y+b)\land y\leq n-b\to R(x,y)$, $b\geq 1$) is transformed into the clause $x=y\land R_{\leftarrow,s}^{x-a}\to R(x,y)$ (resp. $x=y\land R_{\leftarrow,s}^{y+b}\to R(x,y)$).

Transforming the computation clauses: To each clause (a) $x<y\land S(x+1,y)\to R(x,y)$ add the following clauses justified by the identity $x+1-a_{i}=x-(a_{i}-1)$:

$x<y\land S_{\leftarrow s_{1},\dots,s_{l},t_{1},\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y+b_{1},\dots,y+b_{m}}(x+1,y)$

$\to R_{\leftarrow s_{1},\dots,s_{l},t_{1},\dots,t_{m}}^{x-(a_{1}-1),\dots,x-(a_{l}-1),y+b_{1},\dots,y+b_{m}}(x,y)$.

Similarly, to each clause (b) $x<y\land S(x,y-1)\to R(x,y)$ add the clauses

$x<y\land S_{\leftarrow s_{1},\dots,s_{l},t_{1},\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y+b_{1},\dots,y+b_{m}}(x,y-1)$

$\to R_{\leftarrow s_{1},\dots,s_{l},t_{1},\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y+(b_{1}-1),\dots,y+(b_{m}-1)}(x,y)$.

Moreover, add for $a_{1}=0$ and each $s_{1}\in\Sigma$, the following “verification” clauses, which intuitively delete the hypothesis $Q_{s_{1}}(x)$ after verifying that it is satisfied because of the equivalence $W_{s_{1}}^{x}(x,y)\iff Q_{s_{1}}(x)$:

$x<y\land S_{\leftarrow s_{1},s_{2},\dots,s_{l},t_{1},\dots,t_{m}}^{x,x-a_{2},\dots,x-a_{l},y+b_{1},\dots,y+b_{m}}(x,y)\land W_{s_{1}}^{x}(x,y)$

$\to R_{\leftarrow s_{2},\dots,s_{l},t_{1},\dots,t_{m}}^{x-a_{2},\dots,x-a_{l},y+b_{1},\dots,y+b_{m}}(x,y)$.

Similarly, add for $b_{1}=0$ and each $t_{1}\in\Sigma$, the “verification” clauses (justified by $W_{t_{1}}^{y}(x,y)\iff Q_{t_{1}}(y)$) :

$x<y\land S_{\leftarrow s_{1},\dots,s_{l},t_{1},t_{2},\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y,y+b_{2},\dots,y+b_{m}}(x,y)\land W_{t_{1}}^{y}(x,y)$

$\to R_{\leftarrow s_{1},\dots,s_{l},t_{2}\dots,t_{m}}^{x-a_{1},\dots,x-a_{l},y+b_{2},\dots,y+b_{m}}(x,y)$.

For each clause (c) $x\preceq y\land S(x,y)\land T(x,y)\to R(x,y)$, where $\preceq\;\in\{<,=\}$, add similar clauses that cumulate the hypotheses provided they are compatible: for example, the clause

$x\preceq y\land S_{s_{1},s_{2},t_{1}}^{x-1,x-3,y+2}(x,y)\land T_{s_{1},t_{1},t_{2}}^{x-1,y+2,y+4}(x,y)$

$\to R_{s_{1},s_{2},t_{1},t_{2}}^{x-1,x-3,y+2,y+4}(x,y).$