Feasible computation through model theory
Anuj Dawar · 1993
The computational complexity of a problem is usually defined in terms of the resources required on some machine model of computation. An alternative view looks at the complexity of describing the problem (seen as a collection of relational structures) in a logic, measuring logical resources such as the number of variables, quantifiers, operators, etc. A close correspondence has been observed between these two, with many natural logics corresponding exactly to independently defined complexity classes. For the complexity classes that are generally identified with feasible computation, such characterizations require the presence of a linear order on the domain of every structure, in which case the class PTIME is characterized by an extension of first-order logic by means of an inductive operator. No logical characterization of feasible computation is known for unordered structures. We approach this question from two directions. On the one hand, we seek to accurately characterize the expressive power of inductive logics over classes of structures where no linear order is present. On the other hand, we study extensions of inductive logic by means of generalized quantifiers to determine if such extensions might exactly express the PTIME properties. For the two investigations, we develop a common set of tools and techniques, based on notions from model theory. Basic notions, such as those of elementary equivalence and element type are adapted to the context of finite relational structures, in particular, by restricting the number of distinct variables that can appear in any formula. We use these tools to show that there is no extension of the inductive logic by means of a finite number of generalized quantifiers that exactly expresses the PTIME properties of finite relational structures. We also show that, if there is any descriptive characterization of the PTIME properties, indeed if the PTIME properties are recursively indexable, then there is a characterization by means of an extension of first-order logic by a uniform, infinite sequence of generalized quantifiers. This is established through a general result linking the recursive indexability of a complexity class with the existence of complete problems via weak logical reductions.