Inductive definitions in logic versus programs of real-time cellular automata

Descriptive complexity provides intrinsic, i.e. machine-independent , characterizations of the main complexity classes. On the other hand, logic can be useful for designing programs in a natural declarative way. This is especially important for parallel computation models such as cellular automata, since designing parallel programs is considered a difficult task. This paper establishes three logical characterizations of the three classical complexity classes modeling minimal time, called real-time , of one-dimensional cellular automata according to their canonical variations: unidirectional or bidirectional communication, input word given in a parallel or sequential way. Our three logics are natural restrictions of existential second-order Horn logic with built-in successor and predecessor functions. These logics correspond exactly to the three ways of deciding a language on a square grid circuit of side ������ according to one of the three natural locations of an input word of length ������: along a side of the grid, on the diagonal that contains the output cell - placed on the vertex (n,n) of the square grid-, or on the diagonal opposite to the output cell. The key ingredient to our results is a normalization method that transforms a formula from one of our three logics into an equivalent normalized formula that closely mimics a grid circuit. Then, we extend our logics by allowing a limited use of negation on hypotheses like in Stratified Datalog. By revisiting in detail a number of representative classical problems -recognition of the set of primes by Fisher's algorithm, Dyck language recognition, Firing Squad Synchronization problem, etc. -we show that this extension makes easier programming and we prove that it does not change the real-time complexity of our logics. Finally, based on our experience in expressing these representative problems in logic, we argue that our logics are high-level programming languages: they make it possible to express in a natural, complete and synthetic way the algorithms of the literature, based on signals - and even to design new inductive algorithms -, and to translate them automatically into cellular automata of the same complexity.