1000/1000

Hot
Most Recent

Submitted Successfully!

To reward your contribution, here is a gift for you: A free trial for our video production service.

Thank you for your contribution! You can also upload a video entry or images related to this topic.

Do you have a full video?

Are you sure to Delete?

Cite

If you have any further questions, please contact Encyclopedia Editorial Office.

HandWiki. FO (Complexity). Encyclopedia. Available online: https://encyclopedia.pub/entry/32619 (accessed on 22 June 2024).

HandWiki. FO (Complexity). Encyclopedia. Available at: https://encyclopedia.pub/entry/32619. Accessed June 22, 2024.

HandWiki. "FO (Complexity)" *Encyclopedia*, https://encyclopedia.pub/entry/32619 (accessed June 22, 2024).

HandWiki. (2022, November 03). FO (Complexity). In *Encyclopedia*. https://encyclopedia.pub/entry/32619

HandWiki. "FO (Complexity)." *Encyclopedia*. Web. 03 November, 2022.

Copy Citation

In descriptive complexity, a branch of computational complexity, FO is a complexity class of structures that can be recognized by formulas of first-order logic, and also equals the complexity class AC0. Descriptive complexity uses the formalism of logic, but does not use several key notions associated with logic such as proof theory or axiomatization. Restricting predicates to be from a set X yields a smaller class FO[X]. For instance, FO[Similarly, extensions of first-order logic formed by the addition of operators give rise to other well-known complexity classes. This allows the complexity of some problems to be established without reference to algorithms.

fosimilarly
first-order logic
axiomatization

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. 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 "[math]\displaystyle{ E(x,y) }[/math] is true iff there is an edge from x to y" (in case of the structure being a graph), or "[math]\displaystyle{ P(n) }[/math] is true iff the nth 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 almost always suppose 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 x represents the number n iff there are [math]\displaystyle{ (n-1) }[/math] elements y with [math]\displaystyle{ y\lt x }[/math]. Thanks to this we also may have the primitive predicate "bit", where [math]\displaystyle{ bit(x,k) }[/math] is true if only the kth bit of the binary expansion of n is 1. (We can replace addition and multiplication by ternary relations such that [math]\displaystyle{ plus(x,y,z) }[/math] is true iff [math]\displaystyle{ x+y=z }[/math] and [math]\displaystyle{ times(x,y,z) }[/math] is true iff [math]\displaystyle{ x*y=z }[/math]).

Let *X* be a set of predicates on [math]\displaystyle{ \mathbb{N} }[/math]. The language FO[*X*] is defined as the closure by conjunction ([math]\displaystyle{ \wedge }[/math]), negation ([math]\displaystyle{ \neg }[/math]) and universal quantification ([math]\displaystyle{ \forall }[/math]) over elements of the structures. Existential quantification ([math]\displaystyle{ \exists }[/math]) and disjunction ([math]\displaystyle{ \vee }[/math]) are also often used but those can be defined by means of the first three symbols. The base case is the predicates of *X* applied to some variables. One always implicitly has a predicate [math]\displaystyle{ P_a(x) }[/math] for each letter a of an alphabet, stating that the letter at position x is an a.

The semantics of the formulae in FO is straightforward, [math]\displaystyle{ \neg A }[/math] is true iff A is false, [math]\displaystyle{ A\wedge B }[/math] is true iff A is true and B is true, and [math]\displaystyle{ \forall x P(x) }[/math] is true iff [math]\displaystyle{ P(v) }[/math] is true for all values v that x may take in the underlying universe. For *P* a *c*-ary predicate, [math]\displaystyle{ P(x_1,\dots, x_c) }[/math] is true if and only if when [math]\displaystyle{ x_i }[/math] is interpreted as [math]\displaystyle{ n_i }[/math] [math]\displaystyle{ P(n_1,\dots, n_c) }[/math] is true.

A query in FO will then be to check if a first-order formula is true over a given structure representing the input to the problem. One should not confuse this kind of problem with checking if a quantified boolean formula is true, which is the definition of QBF, which is PSPACE-complete. The difference between those two problems is that in QBF the size of the problem is the size of the formula and elements are just boolean variables, whereas in FO the size of the problem is the size of the structure and the formula is fixed.

This is similar to Parameterized complexity but the size of the formula is not a fixed parameter.

Disregarding empty structures, every formula is equivalent to a formula in prenex normal form (where all quantifiers are written first, followed by a quantifier-free formula).

In circuit complexity, FO(ARB) where ARB is the set of all predicates, the logic where we can use arbitrary predicates, can be shown to be equal to AC^{0}, the first class in the AC hierarchy. Indeed, there is a natural translation from FO's symbols to nodes of circuits, with [math]\displaystyle{ \forall, \exists }[/math] being [math]\displaystyle{ \land }[/math] and [math]\displaystyle{ \lor }[/math] of size n.

FO(BIT) is the restriction of AC^{0} family of circuit constructible in alternating logarithmic time. FO(<) is the set of star-free languages.

FO(PFP,*X*) is the set of boolean queries definable in FO(X) where we add a partial fixed point operator.

Let k be an integer, [math]\displaystyle{ x, y }[/math] be vectors of k variables, P be a second-order variable of arity k, and φ be a FO(PFP,X) function using x and P as variables. We can iteratively define [math]\displaystyle{ (P_i)_{i\in N} }[/math] such that [math]\displaystyle{ P_0(x)=false }[/math] and [math]\displaystyle{ P_i(x)=\phi(P_{i-1},x) }[/math] (meaning φ with [math]\displaystyle{ P_{i-1} }[/math] substituted for the second-order variable P). Then, either there is a fixed point, or the list of [math]\displaystyle{ (P_i) }[/math]s is cyclic.

[math]\displaystyle{ \operatorname{PFP}(\phi_{P,x})(y) }[/math] is defined as the value of the fixed point of [math]\displaystyle{ (P_i) }[/math] on y if there is a fixed point, else as false. Since Ps are properties of arity k, there are at most [math]\displaystyle{ 2^{n^k} }[/math] values for the [math]\displaystyle{ P_i }[/math]s, so with a polynomial-space counter we can check if there is a loop or not.

It has been proven that FO(PFP,BIT) is equal to PSPACE. This definition is equivalent to [math]\displaystyle{ \mathsf{FO}[2^{n^{O(1)}}] }[/math].

FO(LFP,X) is the set of boolean queries definable in FO(PFP,X) where the partial fixed point is limited to be monotone. That is, if the second order variable is P, then [math]\displaystyle{ P_i(x) }[/math] always implies [math]\displaystyle{ P_{i+1}(x) }[/math].

We can guarantee monotonicity by restricting the formula φ to only contain positive occurrences of P (that is, occurrences preceded by an even number of negations). We can alternatively describe [math]\displaystyle{ \operatorname{LFP}(\phi_{P,x}) }[/math] as [math]\displaystyle{ \operatorname{PFP}(\psi_{P,x}) }[/math] where [math]\displaystyle{ \psi(P,x)=\phi(P,x)\vee P(x) }[/math].

Due to monotonicity, we only add vectors to the truth table of P, and since there are only [math]\displaystyle{ n^k }[/math] possible vectors we will always find a fixed point before [math]\displaystyle{ n^k }[/math] iterations. The Immerman-Vardi theorem, shown independently by Immerman^{[1]} and Vardi,^{[2]} shows that FO(LFP,BIT)=P. This definition is equivalent to [math]\displaystyle{ \mathsf{FO}[n^{O(1)}] }[/math].

FO(TC,X) is the set of boolean queries definable in FO(X) with a transitive closure (TC) operator.

TC is defined this way: let k be a positive integer and [math]\displaystyle{ u,v,x,y }[/math] be vector of k variables. Then [math]\displaystyle{ \mathsf{TC}(\phi_{u,v})(x,y) }[/math] is true if there exist n vectors of variables [math]\displaystyle{ (z_i) }[/math] such that [math]\displaystyle{ z_1=x, z_n=y }[/math], and for all [math]\displaystyle{ i\lt n }[/math], [math]\displaystyle{ \phi(z_i,z_{i+1}) }[/math] is true. Here, φ is a formula written in FO(TC) and [math]\displaystyle{ \phi(x,y) }[/math] means that the variables u and v are replaced by x and y.

FO(TC,BIT) is equal to NL.

FO(DTC,X) is defined as FO(TC,X) where the transitive closure operator is deterministic. This means that when we apply [math]\displaystyle{ \operatorname{DTC}(\phi_{u,v}) }[/math], we know that for all u, there exists at most one v such that [math]\displaystyle{ \phi(u,v) }[/math].

We can suppose that [math]\displaystyle{ \operatorname{DTC}(\phi_{u,v}) }[/math] is syntactic sugar for [math]\displaystyle{ \operatorname{TC}(\psi_{u,v}) }[/math] where [math]\displaystyle{ \psi(u,v)=\phi(u,v)\wedge \forall x (x=v \vee \neg \phi(u,x)) }[/math].

It has been shown that FO(DTC,BIT) is equal to L.

Any formula with a fixed point (resp. transitive closure) operator can without loss of generality be written with exactly one application of the operators applied to 0 (resp. [math]\displaystyle{ 0,(n-1) }[/math])

We will define first-order with iteration, [math]\displaystyle{ \mathsf{FO}[t(n)] }[/math]; here [math]\displaystyle{ t(n) }[/math] is a (class of) functions from integers to integers, and for different classes of functions [math]\displaystyle{ t(n) }[/math] we will obtain different complexity classes [math]\displaystyle{ \mathsf{FO}[t(n)] }[/math].

In this section we will write [math]\displaystyle{ (\forall x P) Q }[/math] to mean [math]\displaystyle{ (\forall x (P\Rightarrow Q)) }[/math] and [math]\displaystyle{ (\exists x P) Q }[/math] to mean [math]\displaystyle{ (\exists x (P \wedge Q)) }[/math]. We first need to define quantifier blocks (QB), a quantifier block is a list [math]\displaystyle{ (Q_1 x_1, \phi_1)...(Q_k x_k, \phi_k) }[/math] where the [math]\displaystyle{ \phi_i }[/math]s are quantifier-free FO-formulae and [math]\displaystyle{ Q_i }[/math]s are either [math]\displaystyle{ \forall }[/math] or [math]\displaystyle{ \exists }[/math]. If Q is a quantifiers block then we will call [math]\displaystyle{ [Q]^{t(n)} }[/math] the iteration operator, which is defined as Q written [math]\displaystyle{ t(n) }[/math] time. One should pay attention that here there are [math]\displaystyle{ k*t(n) }[/math] quantifiers in the list, but only k variables and each of those variable are used [math]\displaystyle{ t(n) }[/math] times.

We can now define [math]\displaystyle{ \mathsf{FO}[t(n)] }[/math] to be the FO-formulae with an iteration operator whose exponent is in the class [math]\displaystyle{ t(n) }[/math], and we obtain those equalities:

- [math]\displaystyle{ \mathsf{FO}[(\log n)^i] }[/math] is equal to FO-uniform AC
^{i}, and in fact [math]\displaystyle{ \mathsf{FO}[t(n)] }[/math] is FO-uniform AC of depth [math]\displaystyle{ t(n) }[/math]. - [math]\displaystyle{ \mathsf{FO}[(\log n)^{O(1)}] }[/math] is equal to NC.
- [math]\displaystyle{ \mathsf{FO}[n^{O(1)}] }[/math] is equal to PTIME, it is also another way to write FO(LFP).
- [math]\displaystyle{ \mathsf{FO}[2^{n^{O(1)}}] }[/math] is equal to PSPACE, it is also another way to write FO(PFP).

Let the successor relation, *succ*, be a binary relation such that [math]\displaystyle{ \operatorname{succ}(x,y) }[/math] is true if and only if [math]\displaystyle{ x+1=y }[/math].

Over first order logic, *succ* is strictly less expressive than <, which is less expressive than +, which is less expressive than *bit*, while + and × are as expressive as *bit*.

It is possible to define the *plus* and then the *bit* relations with a deterministic transitive closure.

[math]\displaystyle{ \operatorname{plus}(a,b,c)=(\operatorname{DTC}_{v,x,y,z} \operatorname{succ}(v,y) \land \operatorname{succ}(z,x)) (a,b,c,0) }[/math] and

[math]\displaystyle{ \operatorname{bit}(a,b)=(\operatorname{DTC}_{a,b,a',b'}\psi)(a,b,1,0) }[/math] with

[math]\displaystyle{ \psi=\text{if } b=0 \text{ then } (\text{if } \exists m(a=m+m+1) \text{ then }(a'=1\land b'=0)\text{ else } \bot)\text{ else } (\operatorname{succ}(b',b) \land (a+a=a'\lor a+a+1=a') }[/math]

This just means that when we query for bit 0 we check the parity, and go to (1,0) if a is odd (which is an accepting state), else we reject. If we check a bit [math]\displaystyle{ b\gt 0 }[/math], we divide a by 2 and check bit [math]\displaystyle{ b-1 }[/math].

Hence it makes no sense to speak of operators with successor alone, without the other predicates.

FO[LFP] and FO[PFP] are two logics without any predicates, apart from the equality predicates between variables and the letters predicates. They are equal respectively to *relational-P* and FO(PFP) is *relational-PSPACE*, the classes P and PSPACE over relational machines.^{[3]}

The Abiteboul-Vianu Theorem states that FO(LFP)=FO(PFP) if and only if FO(<,LFP)=FO(<,PFP), hence if and only if P=PSPACE. This result has been extended to other fixpoints.^{[3]} This shows that the order problem in first order is more a technical problem than a fundamental one.

- Immerman, Neil (1986). "Relational queries computable in polynomial time" (in en). Information and Control 68 (1–3): 86–104. doi:10.1016/s0019-9958(86)80029-8. https://dx.doi.org/10.1016%2Fs0019-9958%2886%2980029-8
- Vardi, Moshe Y. (1982). The Complexity of Relational Query Languages (Extended Abstract). STOC '82. New York, NY, USA: ACM. 137–146. doi:10.1145/800070.802186. ISBN 978-0897910705. https://dx.doi.org/10.1145%2F800070.802186
- 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, ISSN 0004-5411 http://portal.acm.org/citation.cfm?id=256295

More

Information

Subjects:
Others

Contributor
MDPI registered users' name will be linked to their SciProfiles pages. To register with us, please refer to https://encyclopedia.pub/register
:

View Times:
349

Entry Collection:
HandWiki

Update Date:
03 Nov 2022