Descriptive Complexity

Last updated

Descriptive Complexity is a book in mathematical logic and computational complexity theory by Neil Immerman. It concerns descriptive complexity theory, an area in which the expressibility of mathematical properties using different types of logic is shown to be equivalent to their computability in different types of resource-bounded models of computation. It was published in 1999 by Springer-Verlag in their book series Graduate Texts in Computer Science.

Contents

Topics

The book has 15 chapters, roughly grouped into five chapters on first-order logic, three on second-order logic, and seven independent chapters on advanced topics. [1] [2]

The first two chapters provide background material in first-order logic (including first-order arithmetic, the BIT predicate, and the notion of a first-order query) and complexity theory (including formal languages, resource-bounded complexity classes, and complete problems). Chapter three begins the connection between logic and complexity, with a proof that the first-order-recognizable languages can be recognized in logarithmic space, and the construction of complete languages for logarithmic space, nondeterministic logarithmic space, and polynomial time. The fourth chapter concerns inductive definitions, fixed-point operators, and the characterization of polynomial time in terms of first-order logic with the least fixed-point operator. The part of the book on first-order topics ends with a chapter on logical characterizations of resource bounds for parallel random-access machines and circuit complexity. [1] [2] [3]

Chapter six introduces Ehrenfeucht–Fraïssé games, a key tool for proving logical inexpressibility, and chapter seven introduces second-order logic. It includes Fagin's theorem characterizing nondeterministic polynomial time in terms of existential second-order logic, the Cook–Levin theorem on the existence of NP-complete problems, and extensions of these results to the polynomial hierarchy. Chapter eight uses games to prove the inexpressibility of certain languages in second-order logic. [1] [2] [3]

Chapter nine concerns the complementation of languages and the transitive closure operator, including the Immerman–Szelepcsényi theorem that nondeterministic logarithmic space is closed under complementation. Chapter ten provides complete problems and a second-order logical characterization of polynomial space. Chapter eleven concerns uniformity in circuit complexity (the distinction between the existence of circuits for solving a problem, and their algorithmic constructibility), and chapter twelve concerns the role of ordering and counting predicates in logical characterizations of complexity classes. Chapter thirteen uses the switching lemma for lower bounds, and chapter fourteen concerns applications to databases and model checking. A final chapter outlines topics still in need of research in this area. [1] [2] [3]

Audience and reception

The book is primarily aimed as a reference to researchers in this area, [1] but it could also be used as the basis of a graduate course, and comes equipped with exercises for this purpose. Although it claims to be self-contained, reviewer W. Klonowski writes that its readers need to already understand both classical complexity and the basics of mathematical logic. [2]

Reviewer Anuj Dawar writes that some of the early promise of descriptive complexity has been dampened by its inability to bring logical tools to bear on the core problems of complexity theory, and by the need to add computation-like additions to logical languages in order to use them to characterize computation. Nevertheless, he writes, the book is useful as a way of introducing researchers to this line of research, and to a less heavily-explored way of approaching computational complexity. [4]

Related Research Articles

<span class="mw-page-title-main">PSPACE</span> Set of decision problems

In computational complexity theory, PSPACE is the set of all decision problems that can be solved by a Turing machine using a polynomial amount of space.

<span class="mw-page-title-main">Complexity class</span> Set of problems in computational complexity theory

In computational complexity theory, a complexity class is a set of computational problems "of related resource-based complexity". The two most commonly analyzed resources are time and memory.

In computational complexity theory, Savitch's theorem, proved by Walter Savitch in 1970, gives a relationship between deterministic and non-deterministic space complexity. It states that for any function ,

In computational complexity theory, P, also known as PTIME or DTIME(nO(1)), is a fundamental complexity class. It contains all decision problems that can be solved by a deterministic Turing machine using a polynomial amount of computation time, or polynomial time.

In computational complexity theory, NL is the complexity class containing decision problems that can be solved by a nondeterministic Turing machine using a logarithmic amount of memory space.

In computational complexity theory, L is the complexity class containing decision problems that can be solved by a deterministic Turing machine using a logarithmic amount of writable memory space. Formally, the Turing machine has two tapes, one of which encodes the input and can only be read, whereas the other tape has logarithmic size but can be read as well as written. Logarithmic space is sufficient to hold a constant number of pointers into the input and a logarithmic number of boolean flags, and many basic logspace algorithms use the memory in this way.

Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

<span class="mw-page-title-main">Neil Immerman</span> American theoretical computer scientist

Neil Immerman is an American theoretical computer scientist, a professor of computer science at the University of Massachusetts Amherst. He is one of the key developers of descriptive complexity, an approach he is currently applying to research in model checking, database theory, and computational complexity theory.

Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.

In computational complexity theory, the Immerman–Szelepcsényi theorem states that nondeterministic space complexity classes are closed under complementation. It was proven independently by Neil Immerman and Róbert Szelepcsényi in 1987, for which they shared the 1995 Gödel Prize. In its general form the theorem states that NSPACE(s(n)) = co-NSPACE(s(n)) for any function s(n) ≥ log n. The result is equivalently stated as NL = co-NL; although this is the special case when s(n) = log n, it implies the general theorem by a standard padding argument. The result solved the second LBA problem.

In computer science, st-connectivity or STCON is a decision problem asking, for vertices s and t in a directed graph, if t is reachable from s.

Fagin's theorem is the oldest result of descriptive complexity theory, a branch of computational complexity theory that characterizes complexity classes in terms of logic-based descriptions of their problems rather than by the behavior of algorithms for solving those problems. The theorem states that the set of all properties expressible in existential second-order logic is precisely the complexity class NP.

In computational complexity theory, NL-complete is a complexity class containing the languages that are complete for NL, the class of decision problems that can be solved by a nondeterministic Turing machine using a logarithmic amount of memory space. The NL-complete languages are the most "difficult" or "expressive" problems in NL. If a deterministic algorithm exists for solving any one of the NL-complete problems in logarithmic memory space, then NL = L.

AC<sup>0</sup>

AC0 is a complexity class used in circuit complexity. It is the smallest class in the AC hierarchy, and consists of all families of circuits of depth O(1) and polynomial size, with unlimited-fanin AND gates and OR gates (we allow NOT gates only at the inputs). It thus contains NC0, which has only bounded-fanin AND and OR gates.

In mathematics and computer science, the BIT predicate, sometimes written , is a predicate that tests whether the th bit of the number is 1, when is written as a binary number. Its mathematical applications include modeling the membership relation of hereditarily finite sets, and defining the adjacency relation of the Rado graph. In computer science, it is used for efficient representations of set data structures using bit vectors, in defining the private information retrieval problem from communication complexity, and in descriptive complexity theory to formulate logical descriptions of complexity classes.

In computational complexity theory, a certificate is a string that certifies the answer to a computation, or certifies the membership of some string in a language. A certificate is often thought of as a solution path within a verification process, which is used to check whether a problem gives the answer "Yes" or "No".

<span class="mw-page-title-main">Structural complexity theory</span>

In computational complexity theory of computer science, the structural complexity theory or simply structural complexity is the study of complexity classes, rather than computational complexity of individual problems and algorithms. It involves the research of both internal structures of various complexity classes and the relations between different complexity classes.

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.

References

  1. 1 2 3 4 5 Lindell, Steven (December 2001), "Review of Descriptive Complexity", The Bulletin of Symbolic Logic , 7 (4): 525–527, doi:10.2307/2687799, JSTOR   2687799
  2. 1 2 3 4 5 Klonowski, W. (2001), "Review of Descriptive Complexity", Discrete Dynamics in Nature and Society, 6: 57–62, doi: 10.1155/S1026022601000061
  3. 1 2 3 Schöning, Uwe, "Review of Descriptive Complexity", zbMATH , Zbl   0918.68031
  4. Dawar, Anuj (2001), "Review of Descriptive Complexity", Mathematical Reviews , MR   1732784