HOME

TheInfoList



OR:

Descriptive complexity is a branch of
computational complexity theory In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and explores the relationships between these classifications. A computational problem ...
and of finite model theory that characterizes
complexity class In computational complexity theory, a complexity class is a set (mathematics), set of computational problems "of related resource-based computational complexity, complexity". The two most commonly analyzed resources are time complexity, time and s ...
es by the type of
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
needed to express the
language Language is a structured system of communication that consists of grammar and vocabulary. It is the primary means by which humans convey meaning, both in spoken and signed language, signed forms, and may also be conveyed through writing syste ...
s 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 In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
. 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 machine In computer science, an abstract machine is a theoretical model that allows for a detailed and precise analysis of how a computer system functions. It is similar to a mathematical function in that it receives inputs and produces outputs based on p ...
s used to define them. Specifically, each
logical system A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms. In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
produces a set of queries expressible in it. The queries – when restricted to finite structures – correspond to the
computational problem In theoretical computer science, a computational problem is one that asks for a solution in terms of an algorithm. For example, the problem of factoring :"Given a positive integer ''n'', find a nontrivial prime factor of ''n''." is a computati ...
s of traditional complexity theory. The first main result of descriptive complexity was Fagin's theorem, shown by Ronald Fagin in 1974. It established that NP is precisely the set of languages expressible by sentences of existential
second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
; that is, second-order logic excluding
universal quantification In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", "for every", or "given an arbitrary element". It expresses that a predicate can be satisfied by e ...
over relations, functions, and
subset In mathematics, a Set (mathematics), set ''A'' is a subset of a set ''B'' if all Element (mathematics), elements of ''A'' are also elements of ''B''; ''B'' is then a superset of ''A''. It is possible for ''A'' and ''B'' to be equal; if they a ...
s. Many other classes were later characterized in such a manner.


The setting

When we use the logic formalism to describe a computational problem, the input is a finite structure, and the elements of that structure are the
domain of discourse In the formal sciences, the domain of discourse or universe of discourse (borrowing from the mathematical concept of ''universe'') is the set of entities over which certain variables of interest in some formal treatment may range. It is also ...
. Usually the input is either a string (of bits or over an alphabet) and the elements of the logical structure represent positions of the string, or the input is a graph and the elements of the logical structure represent its vertices. The length of the input will be measured by the size of the respective structure. Whatever the structure is, we can assume that there are relations that can be tested, for example "E(x,y) is true if and only if there is an edge from to " (in case of the structure being a graph), or "P(n) is true if and only if the th letter of the string is 1." These relations are the predicates for the first-order logic system. We also have constants, which are special elements of the respective structure, for example if we want to check reachability in a graph, we will have to choose two constants ''s'' (start) and ''t'' (terminal). In descriptive complexity theory we often assume that there is a total order over the elements and that we can check equality between elements. This lets us consider elements as numbers: the element represents the number if and only if there are (n-1) elements with y. Thanks to this we also may have the primitive predicate "bit", where bit(x,k) is true if only the th bit of the binary expansion of is 1. (We can replace addition and multiplication by ternary relations such that plus(x,y,z) is true if and only if x+y=z and times(x,y,z) is true if and only if x*y=z).


Overview of characterisations of complexity classes

If we restrict ourselves to ordered structures with a successor relation and basic arithmetical predicates, then we get the following characterisations: *
First-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
defines the class AC0, the languages recognized by polynomial-size circuits of bounded depth, which equals the languages recognized by a concurrent random access machine in constant time.Immerman 1999, p. 86 * First-order logic augmented with symmetric or deterministic
transitive closure In mathematics, the transitive closure of a homogeneous binary relation on a set (mathematics), set is the smallest Relation (mathematics), relation on that contains and is Transitive relation, transitive. For finite sets, "smallest" can be ...
operators yield L, problems solvable in logarithmic space. * First-order logic with a
transitive closure In mathematics, the transitive closure of a homogeneous binary relation on a set (mathematics), set is the smallest Relation (mathematics), relation on that contains and is Transitive relation, transitive. For finite sets, "smallest" can be ...
operator yields NL, the problems solvable in nondeterministic logarithmic space.Immerman 1999, p. 242 * First-order logic with a least fixed point operator gives P, the problems solvable in deterministic polynomial time. * Existential second-order logic yields NP. * Universal second-order logic (excluding existential second-order quantification) yields co-NP. * Second-order logic corresponds to the polynomial hierarchy PH. * Second-order logic with a
transitive closure In mathematics, the transitive closure of a homogeneous binary relation on a set (mathematics), set is the smallest Relation (mathematics), relation on that contains and is Transitive relation, transitive. For finite sets, "smallest" can be ...
(commutative or not) yields
PSPACE 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. Formal definition If we denote by SPACE(''f''(''n'')), the set of all problems that can ...
, the problems solvable in polynomial space. * Second-order logic with a least fixed point operator gives
EXPTIME In computational complexity theory, the complexity class EXPTIME (sometimes called EXP or DEXPTIME) is the set of all decision problems that are solvable by a deterministic Turing machine in exponential time, i.e., in O(2''p''(''n'')) time, w ...
, the problems solvable in exponential time. * HO, the complexity class defined by
higher-order logic In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...
, is equal to ELEMENTARY


Sub-polynomial time


FO without any operators

In
circuit complexity In theoretical computer science, circuit complexity is a branch of computational complexity theory in which Boolean functions are classified according to the size or depth of the Boolean circuits that compute them. A related notion is the circui ...
, first-order logic with arbitrary predicates can be shown to be equal to AC0, the first class in the AC hierarchy. Indeed, there is a natural translation from FO's symbols to nodes of circuits, with \forall, \exists being \land and \lor of size . First-order logic in a signature with arithmetical predicates characterises the restriction of the AC0 family of circuits to those constructible in alternating logarithmic time. First-order logic in a signature with only the order relation corresponds to the set of star-free languages.


Transitive closure logic

First-order logic gains substantially in expressive power when it is augmented with an operator that computes the transitive closure of a binary relation. The resulting transitive closure logic is known to characterise non-deterministic logarithmic space (NL) on ordered structures. This was used by Immerman to show that NL is closed under complement (i. e. that NL = co-NL). When restricting the transitive closure operator to deterministic transitive closure, the resulting logic exactly characterises logarithmic space on ordered structures.


Second-order Krom formulae

On structures that have a successor function, NL can also be characterised by second-order Krom formulae. SO-Krom is the set of Boolean queries definable with second-order formulae in conjunctive normal form such that the first-order quantifiers are universal and the quantifier-free part of the formula is in Krom form, which means that the first-order formula is a conjunction of disjunctions, and in each "disjunction" there are at most two variables. Every second-order Krom formula is equivalent to an existential second-order Krom formula. SO-Krom characterises NL on structures with a successor function.Immerman 1999, p. 1534


Polynomial time

On ordered structures, first-order least fixed-point logic captures PTIME:


First-order least fixed-point logic

FO FPis the extension of first-order logic by a least fixed-point operator, which expresses the fixed-point of a monotone expression. This augments first-order logic with the ability to express recursion. The Immerman–Vardi theorem, shown independently by Immerman and Vardi, shows that FO FPcharacterises PTIME on ordered structures. As of 2022, it is still open whether there is a natural logic characterising PTIME on unordered structures. The Abiteboul–Vianu theorem states that FO FPFO FPon all structures if and only if FO FPFO FP hence if and only if P=PSPACE. This result has been extended to other fixpoints.Serge Abiteboul, Moshe Y. Vardi, Victor Vianu
Fixpoint logics, relational machines, and computational complexity
Journal of the ACM archive, Volume 44, Issue 1 (January 1997), Pages: 30-56,


Second-order Horn formulae

In the presence of a successor function, PTIME can also be characterised by second-order Horn formulae. SO-Horn is the set of Boolean queries definable with SO formulae in disjunctive normal form such that the first-order quantifiers are all universal and the quantifier-free part of the formula is in Horn form, which means that it is a big AND of OR, and in each "OR" every variable except possibly one are negated. This class is equal to P on structures with a successor function. Those formulae can be transformed to prenex formulas in existential second-order Horn logic.


Non-deterministic polynomial time


Fagin's theorem

Ronald Fagin's 1974 proof that the complexity class NP was characterised exactly by those classes of structures axiomatizable in existential second-order logic was the starting point of descriptive complexity theory. Since the complement of an existential formula is a universal formula, it follows immediately that co-NP is characterized by universal second-order logic. SO, unrestricted second-order logic, is equal to the Polynomial hierarchy PH. More precisely, we have the following generalisation of Fagin's theorem: The set of formulae in prenex normal form where existential and universal quantifiers of second order alternate ''k'' times characterise the ''k''th level of the polynomial hierarchy. Unlike most other characterisations of complexity classes, Fagin's theorem and its generalisation do not presuppose a total ordering on the structures. This is because existential second-order logic is itself sufficiently expressive to refer to the possible total orders on a structure using second-order variables.


Beyond NP


Partial fixed point is PSPACE

The class of all problems computable in polynomial space,
PSPACE 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. Formal definition If we denote by SPACE(''f''(''n'')), the set of all problems that can ...
, can be characterised by augmenting first-order logic with a more expressive partial fixed-point operator. Partial fixed-point logic, FO FP is the extension of first-order logic with a partial fixed-point operator, which expresses the fixed-point of a formula if there is one and returns 'false' otherwise. Partial fixed-point logic characterises
PSPACE 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. Formal definition If we denote by SPACE(''f''(''n'')), the set of all problems that can ...
on ordered structures.


Transitive closure is PSPACE

Second-order logic can be extended by a transitive closure operator in the same way as first-order logic, resulting in SO C The TC operator can now also take second-order variables as argument. SO Ccharacterises
PSPACE 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. Formal definition If we denote by SPACE(''f''(''n'')), the set of all problems that can ...
. Since ordering can be referenced in second-order logic, this characterisation does not presuppose ordered structures.


Elementary functions

The
time complexity In theoretical computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations ...
class ELEMENTARY of elementary functions can be characterised by HO, the
complexity class In computational complexity theory, a complexity class is a set (mathematics), set of computational problems "of related resource-based computational complexity, complexity". The two most commonly analyzed resources are time complexity, time and s ...
of structures that can be recognized by formulas of
higher-order logic In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...
. Higher-order logic is an extension of
first-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
and
second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
with higher-order quantifiers. There is a relation between the ith order and non-deterministic algorithms the time of which is bounded by i-1 levels of exponentials.


Definition

We define higher-order variables. A variable of order i>1 has an arity k and represents any set of k-
tuple In mathematics, a tuple is a finite sequence or ''ordered list'' of numbers or, more generally, mathematical objects, which are called the ''elements'' of the tuple. An -tuple is a tuple of elements, where is a non-negative integer. There is o ...
s of elements of order i-1. They are usually written in upper-case and with a natural number as exponent to indicate the order. Higher-order logic is the set of first-order formulae where we add quantification over higher-order variables; hence we will use the terms defined in the FO article without defining them again. HO^i is the set of formulae with variables of order at most i. HO^i_j is the subset of formulae of the form \phi=\exists \overline\forall\overline\dots Q \overline\psi, where Q is a quantifier and Q \overline means that \overline is a tuple of variable of order i with the same quantification. So HO^i_j is the set of formulae with j alternations of quantifiers of order i, beginning with \exists, followed by a formula of order i-1. Using the standard notation of the
tetration In mathematics, tetration (or hyper-4) is an operation (mathematics), operation based on iterated, or repeated, exponentiation. There is no standard mathematical notation, notation for tetration, though Knuth's up arrow notation \uparrow \upa ...
, \exp_2^0(x)=x and \exp_2^(x)=2^. \exp_2^(x)=2^ with i times 2


Normal form

Every formula of order ith is equivalent to a formula in prenex normal form, where we first write quantification over variable of ith order and then a formula of order i-1 in normal form.


Relation to complexity classes

HO is equal to the class ELEMENTARY of elementary functions. To be more precise, \mathsf^i_0 = \mathsf(\exp_2^(n^)), meaning a tower of (i-2) 2s, ending with n^c, where c is a constant. A special case of this is that \exists\mathsf=\mathsf^2_0=\mathsf(n^)=, which is exactly Fagin's theorem. Using oracle machines in the polynomial hierarchy, \mathsf^i_j=(\exp_2^(n^)^)


Notes


References

* {{Cite book, first=Neil, last=Immerman, url=http://worldcat.org/oclc/901297152, title=Descriptive complexity, date=1999, publisher=Springer, isbn=0-387-98600-6, oclc=901297152


External links


Neil Immerman's descriptive complexity page
including a diagram Computational complexity theory Finite model theory