BRICS RS-96-41 S. Dziembowski: The Fixpoint Bounded-Variable Queries are PSPACE-Complete

BRICS

Basic Research in Computer Science

The Fixpoint Bounded-Variable Queries are PSPACE-Complete

Stefan Dziembowski

BRICS Report Series RS-96-41 ISSN 0909-0878 November 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through World Wide Web and anonymous FTP:

http://www.brics.dk/
ftp://ftp.brics.dk/pub/BRICS

This document in subdirectory RS/96/41/ The Fixpoint Bounded-Variable Queries are

PSPACE-complete ^{⋆}

Stefan Dziembowski

                       stefand@mimuw.edu.pl

Warsaw University, Department of Mathematics, Informatics and Mechanics, Institute of Informatics, Banacha 2, 02-097 Warszawa, Poland, phone: (+48-22) 658-31-65, fax: (+48-22) 658-31-64

Abstract. We study complexity of the evaluation of fixpoint boundedvariable queries in relational databases. We exhibit a finite database such that the problem whether a closed fixpoint formula using only 2 individual variables is satisfied in this database is PSPACE-complete. This clarifies the issues raised by Moshe Vardi in [Var95]. We study also the complexity of query evaluation for a number of restrictions of fixpoint logic. In particular we exhibit a sublogic for which the upper bound postulated by Vardi holds.

1 Introduction

In [Var95] Vardi studies computational complexity of queries expressed in various logics. There are three notions of the complexity of query evaluation.

1. We can fix a database and evaluate different queries expressible in a logic against this database. In this case we measure the complexity as a function of the length of the expression denoting the query. We call it the expression complexity of the logic.

2. We can fix a query and evaluate this query against different databases. In this case we measure the complexity as a function of the size of the database (data complexity of the logic).

3. We can evaluate different queries against different databases and measure the complexity as a function of the combined size of the database and the expression denoting the query (combined complexity of the logic).

Vardi remarks that for many logical languages there is a gap between the data complexity on the one side, and the expression and combined complexities on the other. For example the data complexity of first order logic (FO) is AC^{0} while the expression and combined complexities are complete in PSPACE, the data complexity of fixpoint logic (FP) is PTIME, while the expression and combined complexities are EXPTIME-complete.

⋆ Supported by Polish KBN grant No. 8 T11C 002 11. Part of this work was done at BRICS, a Center for Basic Research in Computer Science, Aarhus, Denmark.

The main idea of [Var95] is that when we consider logics with a uniformly bounded number of individual variables then this gap narrows. This syntax restriction captures the well-known technique of database programmers of avoiding large intermediate results.

We study the problem of measuring the expression and combined complexities of the bounded-variable version of the fixpoint first-order logic (FP^{k}). We show that both of them are PSPACE-complete. In [Var95] Vardi has proposed an NP algorithm for this problem, however the algorithm works only for a subclass of FP^{k} formulas.

We also consider various restrictions of the FP^{k} syntax and study their complexity. At first, we fix a number of second-order variables. We show that in this case the expression complexity is in ALOGTIME, but the combined complexity is still PSPACE-complete. Since ALOGTIME ≠ PSPACE, this is, up to our knowledge, first provable gap between expression complexity and combined complexity. We also study the combined and expression complexities of the prefix version of FP^{k} (formulas are of the form: prefix of fixpoint operators . first-order formula . arguments), showing the PSPACE-completeness. Finally, we present a sublogic of FP^{k} for which the NP ∩ co-NP upper bound for combined complexity holds.

Our results confirm the Vardi’s idea that bounding the number of variables may lead to narrowing the gap between data and combined complexity. Whether this gap is indeed more narrow does depend on the hypothesis that PSPACE ≠ EXPTIME.

2 Acknowledgments

I wish to thank several people for the help with my work. First of all, I wish to express my deep gratitude to Damian Niwiński, who spent a lot of time patiently explaining me numerous details and discussing my ideas. Without his interest, support and encouragement this paper would never come into existence. I would also like to thank Igor Walukiewicz for his valuable comments on my ideas and for patience and interest he showed when reading proofs. I also wish to thank Grzegorz Grudziński, Marcin Jurdziński and all other Warsaw University Applied Logic Group people.

3 Basic Definitions

Definitions presented in this section are based on the definitions from [CH82, Var82]. We change them a bit introducing a notion of a database signature, which is similar to the standard notion of a signature, used in mathematical logic. This technical modification makes the proofs in the paper more readable.

3.1 Databases and Queries

Definition 1. Database signature is a pair (S, C, ar), where – set of relational symbols S and set of constants C are finite disjoint sets of

natural numbers

– ar : S → IN is a function giving for each symbol in the set S its arity

Definition 2. A (relational) database under signature σ = (S, C, ar) is a tuple

B = ⟨|B|, σ, |[·]|_{B}⟩

where

– carrier set |B| is a finite subset of natural numbers

– interpretation |[·]|_{B} is a function giving for each c ∈ C an element of |B| and for each s ∈ S a relation on |B| of an arity ar(s).

The restriction that the set of symbols and the carrier set are subsets of natural numbers is technical (we need it, for example in the Definition 4). Usually we will not respect it and name symbols and carrier set elements in more convenient way. An expression ⟨B⟩ will denote a database B, with a carrier set B under a signature (∅, C, |[·]|), such that C = B and for every c ∈ C we have |[c]|_{B} = c. Any database can be extended by adding to it a new symbol with its interpretation. Formally we define it in the following way:

Definition 3. An extension of a database B = ⟨|B|, (S, C, ar), |[·]|_{B}⟩ with a symbol T with an interpretation Q and an arity a is a database:

B′ = ⟨|B|, (S ∪ {T }, C, ar′), |[·]|_{B′}⟩

where |[·]|_{B′} is equal to the function |[·]|_{B} on the set S \ {T }, and on the argument T it is equal to Q, similarly, functions ar′ and ar are equal on S \ {T } and ar′(T) = a. Such an extension will be denoted by B[Q/T : a]. When an arity a is clear from a context we will use abbreviation, writing B[Q/T] instead of B[Q/T : a].

Definition 4. For every database signature σ and every natural number n, an arbitrary function

Q : {B : B is under signature σ} → P(IN^{n})

such, that Q(B) ⊆ |B|^{n}, will be called a database query of a signature σ → n

Definition 5. A query language is a set of expressions L together with a function Q giving for every e ∈ L a query Q_{e}.

Because we will study the complexity issues in the paper, we make here a formal assumption, that, together with a language, there is given a standard way of encoding its elements. We fix also some standard way of encoding databases. We skip here the details.

3.2 Logics as a query languages

In [Var95] Vardi studied various logical languages (interpreted in relational structures) considered as query languages. Every formula φ (without function symbols) in any such logic L induces a query defined in the following way: Suppose, that free first-order variables of φ belong to the set {x_{1}, …, x_{i}}, and free second-order variables (with an arity given by a function ar) belong to the set S. Any database B under the signature (S, C, ar) can be considered as a relational structure. For such a database, an expression e = ⟨(x_{1}, …, x_{l})φ, (S, ar)⟩ defines a query:

Q_{e} = {(b_{1}, …, b_{l}) ∈ B^{l} : B, [b_{1}/x_{1}, …, b_{l}/x_{l}] ⊧ φ}

(where [b_{1}/x_{1}, …, b_{l}/x_{l}] denotes a valuation of first-order variables, such that, for each i = 1, …, l we have v(x_{i}) = t_{i}). The following abbreviation is useful: For every database B, a valuation α, a tuple of variables x, a formula φ(x), and a tuple t of the carrier set elements we will often write B, α ⊧ φ(t) instead of B, α[t/x] ⊧ φ(x) (where α[t/x] denotes a valuation equal to α outside the variables x and such that for every i we have that α(x_{i}) = t_{i}).

3.3 Complexity

In this paper we will study the complexity of queries. We are interested in comparing complexity of queries expressible in different logical languages. Because queries are functions, we translate our task to the decision problem: given a tuple t, an expression e and a database B, does t ∈ Q_{e}(B) ^{2} hold ? Generally this problem has 3 parameters: t, e and B. Here we will focus on the following two instances:

– the database B and the language L are fixed, we measure the complexity of

the set:

Answer_{L}(B, ·, ·) = {⟨t, e⟩ | e ∈ L and t ∈ Q_{e}(B)}

– only language L is fixed, we measure the complexity of the set:

Answer_{L}(·, ·, ·) = {⟨t, B, e⟩ | e ∈ L and t ∈ Q_{e}(B)}

Complexity of the problems Answer_{L}(B, ·, ·) is called expression complexity; we say that

– the expression complexity of a language L belongs to a complexity class C iff for every B, the Answer_{L}(B, ·, ·) problem is in C

– the expression complexity of a language L is hard in a complexity class C iff there exists a database B, such that the Answer_{L}(B, ·, ·) problem is hard in C

2 Here and later on, t and B are understood to be of the correct arity.

The complexity of Answer_{L}(·, ·, ·) is called a combined complexity of the language L. Note that for every B, Answer_{L}(B, ·, ·) is reducible in PTIME to Answer_{L}(·, ·, ·), but need not be any B, such that the converse holds. Therefore Answer_{L}(·, ·, ·) is generally harder than Answer_{L}(B, ·, ·). Consequently, expression complexity of L is lower then its combined complexity. The following observation is useful:

Lemma 6. For an arbitrary database B and an arbitrary logic L (at least as strong as first-order logic) problems:

Answer_{L}(B, ·, ·) and Answer_{L}(B, ·) = {φ : φ is closed and B ⊧_{L} φ}

are PTIME-equivalent. Similar fact holds for

Answer_{L}(·, ·, ·) and Answer_{L}(·, ·) = {φ : φ is closed and B ⊧_{L} φ}

Proof. The reduction from right to left is trivial. Reduction in the opposite direction consists in replacing free variables in φ by constants form the tuple t.

□

From now on, when considering expression and combined complexities (greater or equal to PTIME) we will restrict ourselves to closed formulas. This restriction is not essential due to Lemma 6.

4 Fixpoint First-Order Logic

The FP language is an extension of the standard first-order logic with two dual fixpoint operators: μ and ν, denoting the least and the greatest fixpoint, respectively [CH82]. The syntax is extended in the following way. For an arbitrary FP formula φ and every second-order l-ary variable V appearing positively in it (i.e. not appearing under negation), the expressions: (μV(x_{1}, …, x_{l}).φ)(y_{1}, …, y_{l}) and (νV(x_{1}, …, x_{l}).φ)(y_{1}, …, y_{l}) (where x_{1}, … x_{l} are distinct first order variables and y_{1}, …, y_{l} are first order variables or constants) are formulas. Note, that we allow nesting of fixpoint operators. The set free_{1}(φ) of free first-order variables in φ is defined as in the standard first-order logic. For the fixpoint formulas we have: free_{1}(θV(x_{1}, …, x_{l}).φ) = free_{1}(φ)/{x_{1}, …, x_{l}}. The set free_{2}(φ) of free second-order variables in φ is also defined in the standard way (second-order variables are bound by μ and ν operators). In the sequel we will interpret FP formulas under databases such that for every free second-order variable in a formula there is a corresponding relation in a database. The semantics of the FP should be rather clear, except the semantics of the fixpoint subformulas. Consider a subformula (μV(y_{1}, …, y_{l}).φ)(x_{1}, …, x_{l}) in a database B. We can treat a second-order variable V in a formula φ as a relational symbol and evaluate this formula in a database B extended with this symbol. In this way, after fixing a valuation α of free first-order variables in φ we get an operator on l-ary relations, defined in the following way:

φ̂_{B}(Q) = {(z_{1}, …, z_{l}) : B[Q/V], α[z_{1}/y_{1}, …, z_{1}/y_{l}] ⊧_{FP} φ}

(where α[z/y] denotes a valuation equal to α outside y and equal z on y) Note, that φ may contain some free variables other than y_{1}, …, y_{l}. Because the variable V occurs in the formula φ positively, the operator φ̂_{B} is monotone. Thus, by the Knaster-Tarski theorem [Tar55] there exists the least fixpoint of this operator, equal to the sum of the following sequence:

∅ ⊆ φ̂_{B}(∅) ⊆ φ̂_{B}(φ̂_{B}(∅)) ⊆ ⋯  (1)

Denote this sum by φ_{B}^{∞}. In this way, for a given valuation α, the expression μV(y_{1}, …, y_{l}).φ in database B can be understood as an l-ary predicate. We can now define the semantics of μ-formulas in as follows:

B, α ⊧_{FP} (μV(y_{1}, …, y_{l}).φ)(x_{1}, …, x_{l}) iff (v(x_{1}), …, v(x_{l})) ∈ φ̂_{B}

(where v is equal to α on the set of variables and equal to |[·]| on the set of constants). Similarly we define the semantics of νS(x).φ(t), as the greatest fixpoint of φ̂ (in this case we take intersection of the sequence |B|^{|x|} ⊇ φ̂(|B|^{|x|}) ⊇ φ̂(φ̂(|B|^{|x|})) ⊇ ⋯). If a formula φ has no free variables, we will often write B ⊧_{FP} φ instead of B, α ⊧_{FP} φ. The following lemma will be useful:

Lemma 7. Let B be an arbitrary database, α an arbitrary valuation and φ(x) an arbitrary formula. Then set V = {t : B, α ⊧_{FP} (μV(x).φ(x))(t)}, is equal to

{t : B[V/V], α ⊧_{FP} φ(t)}  (2)

(where t denotes a tuple of the carrier set elements, and x a tuple of the firstorder variables, such, that |t| = |x|).

Proof. Let φ̂ be an operator induced by φ(x). We have that V = φ^{∞} = φ̂(φ^{∞}) = φ̂(V), what is equal to (2). □

5 The Complexity of FP^{k}

In [Var95] Vardi considered several languages, each L^{k} obtained from a certain language L by restricting the set of individual variables allowed in the formulas to {x_{1}, …, x_{k}}. Note, that this does not bound the quantifier depth since variables may be reused. In this way we get FP^{k} from FP. We will show that there exists a database B such that Answer_{FP}^{2}(B, ·) is PSPACE-hard and, consequently, that Answer_{FP}^{2}(·, ·) is PSPACE-hard. This is the best lower bound because on the other hand it is known that, for every k, Answer_{FP}_{k}(·, ·) is in PSPACE ([Var95]), and, consequently for every B, Answer_{FP}_{k}(B, ·) is in PSPACE.

Theorem 8. There exists a database B, such, that Answer_{FP}^{2}(B, ·) is PSPACEcomplete

Proof. From the previous remarks it suffices to show PSPACE-hardness. The proof goes by the reduction of the Quantified Boolean Formulas (QBF) problem. Recall that the syntax of QBF is given by the following grammar:

F ::= F ∧ F | F ∨ F | ∀x_{i}. F | ∃x_{i}. F | x_{i} | ¬x_{i}

The variables take the boolean values T and F. We can assume that each x_{i} is quantified only once. The QBF problem is a set {ψ : ψ is closed and ⊧_{QBF} ψ}. At first sight, one may think that we can reduce QBF to FP^{k} by taking a database B = ⟨{T, F}⟩ and translating a given QBF formula into a first-order formula by translating every x_{i} to (x_{i} = T) and ¬x_{i} to (x_{i} = F). This attempt is not satisfactory however, because the number of variables can not be bounded. Therefore we have to use a bit more sophisticated method and make use of fixpoint operators. Let B = ⟨{T, F, A}⟩. A function ξ transforming QBF formulas to FP^{2} formulas is defined by structural induction.

ξ(ψ_{1} ∧ ψ_{2}) = ξ(ψ_{1}) ∧ ξ(ψ_{2})
ξ(ψ_{1} ∨ ψ_{2}) = ξ(ψ_{1}) ∨ ξ(ψ_{2})
ξ(∀x_{i}.ψ) = ∀y ∈ \{T, F\}. μV_{i}(x). (∨ \begin{matrix}x ≠ A & ∧ & x = y \\ x = A & ∧ & ξ(ψ) \end{matrix} ) (A)

ξ(∃x_{i}.ψ) = ∃y ∈ \{T, F\}. μV_{i}(x). (∨ \begin{matrix}x ≠ A & ∧ & x = y \\ x = A & ∧ & ξ(ψ) \end{matrix} ) (A)
ξ(x_{i}) = V_{i}(T)
ξ(¬x_{i}) = V_{i}(F)

Note, that in this construction there is a bijection between variables x_{1}, …, x_{n} in a QBF formula and V_{1}, …, V_{n} in an FP formula. In formulas μV_{i} ⋯ there is a free variable y, so the least fixpoint defined by this formula depends on the actual value of y. If it is T then in the first iteration T enters to the least fixpoint (F will never enter). This information will be further used in the evaluation of subformulas V_{i}(T) and V_{i}(F).

Lemma 9. ⊧_{QBF} ψ iff B ⊧_{FP} ξ(ψ)

Proof: The proof goes by induction on the structure of a QBF formula. We show the following more general fact: Let ψ(x_{1}, …, x) be a QBF formula and α a valuation of the variables x_{1}, …, x_{l}

α ⊧_{QBF} ψ iff T^{ψ}(α) ⊧_{FP} ξ(ψ)  (3)

where T^{ψ}(v) = B[v(x_{1})/V_{1}, …, v(x_{l})/V_{l}]

1. Proof of the hypothesis for the literals x_{i} and ¬x_{i} is easy. We show it for ¬x_{i}: Let us fix a valuation v. If v ⊧_{QBF} ¬x_{i} then v(x_{i}) = F. Thus |[V_{i}]|_{T ^{ψ}(v)} = {F}. Therefore T^{ψ}(v) ⊧_{FP} ξ(¬x_{i}). On the other hand, if v |̸=_{QBF} ¬x_{i} then v(x_{i}) = T. Thus |[V_{i}]|_{T ^{ψ}(v)} = {T}. Therefore T^{ψ}(v) |̸=_{FP} ξ(¬x_{i}).

2. To prove the hypothesis for ∧ let us fix a valuation v and QBF formulas ψ_{1} and ψ_{2}. Now:

v ⊧_{QBF} ψ_{1} ∧ ψ_{2} iff v ⊧_{QBF} ψ_{1} and v ⊧_{QBF} ψ_{2}  (4)
(by the induction hypothesis) iff ( and \begin{matrix}T^{ψ_{1}}(v) ⊧_{FP} ξ(ψ_{1}) \\ T^{ψ_{2}}(v) ⊧_{FP} ξ(ψ_{2}) \end{matrix} ) (5)

Which, after extending T^{ψ_{1}}(v) and T^{ψ_{2}}(v) to T^{ψ_{1}∧ψ_{2}}(v) is equivalent to

T^{ψ_{1}∧ψ_{2}}(v) ⊧_{FP} ξ(ψ_{1}) and T^{ψ_{2}∧ψ_{2}}(v) ⊧_{FP} ξ(ψ_{2})

which holds if and only if T^{ψ_{1}∧ψ_{2}}(v) ⊧_{FP} ξ(ψ_{1} ∧ ψ_{2}). Similarly we can prove the induction step for ∨

3. The case of quantifiers is the most interesting one. Let us consider universal quantifier (the proof for existential quantifier is similar). Take a QBF formula ∀x_{i}.ψ and an arbitrary valuation v of its free variables. Suppose (3) holds for ψ. From the definition of ξ we get:

ξ(∀x_{i}.ψ) = ∀y ∈ {T, F}.(μV_{i}(x).φ(x, y))(A)  (6)

where

φ(x, y) = (∨ \begin{matrix}x ≠ A & ∧ & x = y \\ x = A & ∧ & ξ(ψ) \end{matrix} )  (7)

Formula (μV_{i}(x).φ(x, y))(A) has exactly one free variable: y. We will prove, that

for every value p ∈ {T, F}

T^{ψ}(v) ⊧_{FP} (μV_{i}(x).φ(x, p))(A) iff v[p/x_{i}] ⊧_{QBF} ψ

(8)

This fact is easily implies the induction hypothesis, because:

T^{ψ}(v) ⊧_{FP} ∀y ∈ {T, F}.(μV_{i}(x).φ(x, y))(A)
iff for every p ∈ {T, F} we have T^{ψ}(v) ⊧_{FP} (μV_{i}(x).φ(x, p))(A)
iff (from (8)) for every p ∈ {T, F} we have v[p/x_{i}] ⊧_{QBF} ψ
iff v ⊧_{QBF} ∀x_{i}.ψ

Let us now prove (8). Take an arbitrary p ∈ {T, F} as a value for y. We have, that

T^{ψ}(v) ⊧_{FP} (μV_{i}(x).φ(x, p))(A)  (9)

is equivalent to

A ∈ V  (10)

where V denotes the least fixpoint:

V = {r : T^{ψ}(v) ⊧_{FP} (μV_{i}(x).φ(x, p))(r)}  (11)

Now, after applying the Lemma 7 to the formula in (11), we get

V = {r : T^{ψ}(v)[V/V_{i}] ⊧_{FP} φ(r, p)}  (12)

This equation will be sufficient for evaluating the value of V. We are mostly interested in the value of this predicate on the element A. However, to evaluate it we have to know the value of V on the set {T, F}. Take an arbitrary q ∈ {T, F}. We have that q ∈ V if and only if T^{ψ}(v)[V/V_{i}] ⊧_{FP} φ(q, p) which, by the definition of φ (7), is equivalent to

T^{ψ}(v)[V/V_{i}] ⊧_{FP} (∨ \begin{matrix}q ≠ A & ∧ & q = p \\ q = A & ∧ & ξ(ψ) \end{matrix} )  (13)

Because q ≠ A, we have that (13) is equivalent to T^{ψ}(v)[V/V_{i}] ⊧_{FP} (q = p). Thus:

every q ∈ {T, F} belongs to V if and only if q = p  (14)

Let us now evaluate the value of V on A, (i.e. evaluate (10)). Note, that in the formula φ the variable V_{i} occurs only in the subformulas of the form V_{i}(T) and V_{i}(F). Thus, after applying (14) to the equation (12), we get, that the set V is equal to {r : T^{ψ}(v)[{p}/V_{i}] ⊧_{FP} φ(r, p)}. By the definition of T^{ψ} we have T^{ψ}(v)[{p}/V_{i}] = T^{ψ}(v[p/x_{i}]), thus by the definition of φ we get that (10) holds if and only if

T^{ψ}(v[p/x_{i}]) ⊧_{FP} (∨ \begin{matrix}A ≠ A & ∧ & A = p \\ A = A & ∧ & ξ(ψ) \end{matrix} )  (15)

which is equivalent to

T^{ψ}(v[p/x_{i}]) ⊧_{FP} ξ(ψ)  (16)

Now, from the induction hypothesis, (16) is equivalent to v[p/x_{i}] ⊧_{QBF} ψ This observation completes the proof. □

6 Complexity of restrictions of FP^{k}

In this section we study the complexity of queries over languages obtained from FP^{k} by various restrictions of the syntax.

6.1 Bounded Number of Second-Order Variables

One can ask whether the bijection between V_{i}’s and x_{i}’s in the proof of the Theorem 8 is essential, i.e. whether it is possible to prove PSPACE-hardness when we restrict also the number of second-order variables to some n. In this section we show that the answer is positive when we ask about the combined complexity, but it is negative for the expression complexity. Let FP_{n}^{k} be a sublogic of FP^{k}, such that the number of first-order variables in its formulas is bounded by k and the number of second-order variables in its formulas is bounded by n.

Combined Complexity. We will prove now the following

Theorem 10. For every k ≥ 3, n ≥ 2 the Answer_{FP}{k \atop n}(·, ·) problem is PSPACEhard

Proof: The membership in PSPACE is trivial. It remains to prove the PSPACEhardness of Answer_{FP}_{2}^{3}. Let us fix a QBF formula ψ (with variables x_{1}, …, x_{n}). We will show how to construct in a polynomial time a pair ⟨ database B_{ψ}, and an FP_{2}^{3} formula ρ(ψ) ⟩, such that:

⊧_{QBF} ψ iff B_{ψ} ⊧_{FP} ρ(ψ)  (17)

In our new construction we define a database in such a way that we will be able to remember the valuation, representing it by relations in B. Let

B_{ψ} = ⟨{1, …, n, T, F, A}⟩ [{1, …, n}/V ar, ∅/V_{0}]

Below we present a function ρ that transforms the formula ψ to a FP_{n}^{k} formula, proceeding top-down. In φ we use binary relation variables V_{i}. Then we will show how to reduce the number of V_{i}’s to 2. States in the database B_{ψ} (all, except A) are used to remember the valuation in the following way: The subformulas (c.f. definition below) μV_{d+1} ⋯ are intended to represent valuation of the propositional variables x_{1}, …, x_{n} in the sense that V_{d}(i, T) holds iff the value of x_{i} is T and V_{d}(i, F) holds iff the value of x_{i} is F. Note, that the actual value of such subformulas will depend on the value of variables that occur free in this formula. In this way, using fix-point formulas we shall be able to capture the whole tree of possible valuations. We define a transformation ρ(ψ) = ξ(ψ, 0) using auxiliary function ξ(ψ : QBF formulas d : IN) which is defined inductively by the following clauses:

ξ(ψ_{1} ∧ ψ_{2}, d) = ξ(ψ_{1}, d) ∧ ξ(ψ_{2}, d)
ξ(ψ_{1} ∨ ψ_{2}, d) = ξ(ψ_{1}, d) ∨ ξ(ψ_{2}, d)
ξ(∀x_{i}.ψ, d) = ∀y ∈ \{T, F\}. μV_{d+1}(x, z). (∨ \begin{matrix}V ar(x) & ∧ & (∨ \begin{matrix}x = i ∧ & z = y \\ x ≠ i ∧ & V_{d}(x, z) \end{matrix} ) \\ x = A & ∧ & ξ(ψ, d + 1) \end{matrix} ) (A, 0)

ξ(∃x_{i}.ψ, d) = ∃y ∈ \{T, F\}. μV_{d+1}(x, z). (∨ \begin{matrix}V ar(x) & ∧ & (∨ \begin{matrix}x = i ∧ & z = y \\ x ≠ i ∧ & V_{d}(x, z) \end{matrix} ) \\ x = A & ∧ & ξ(ψ, d + 1) \end{matrix} ) (A, 0)
ξ(x_{i}, d) = V_{d}(i, T)
ξ(¬x_{i}, d) = V_{d}(i, F)

We claim, that (17) holds. The proof is similar to the one in Section 5. We will skip it here, showing only the induction hypothesis:

for every QBF formula ψ with free variables x_{1}, …, x_{n} every valuation v of these variables and every d ∈ IN we have that α ⊧_{QBF} ψ iff {(i, α(x_{i})) : i = 1, …, n} ⊧_{FP} ξ(ψ, d)

(18)

Now observe that in each subformula of ρ(ψ) of the form μV_{d+1}(x, z).φ, we have that free_{2}(φ) ∩ {V_{1}, …} = {V_{d}}, therefore all other V_{i}’s “are not visible” from φ and can be reused. Formally we do it by gluing all V_{2n}’s into one variable and all V_{2n+1}’s into another. □

Expression Complexity In the above construction the size of the database was not bounded, and could be even linear in the size of a given QBF formula. Below we argue that it is essential by showing the upper bound for the expression complexity. The proof is similar to the proof establishing the complexity of Answer_{FO}_{k} in [Var95]. The key observation is that for a fixed database, and a fixed number of the first- and second-order variables, the arity of all relations is fixed too, and thus the number of all definable relations (and relations on relations) is bounded. This gives us PTIME as an easy upper bound. We can improve it however by using a technique from [Lyn77]. Recall that a parenthesis grammar is a context-free grammar with two distinguished terminals: “(” and “)” such that each production is of the from A → (x) with x parenthesis free. Such a grammar generates a parenthesis language. In our proof we make use of the the fact from [Bus87] that all parenthesis languages are recognizable in ALOGTIME.

Theorem 11. The Answer_{FP}{k \atop n}(B) problem is in ALOGTIME for every database B every k and every n.

Proof sketch: Note, that we consider here complexity for which it is not known, whether it contains PTIME. Thus we can not use Lemma 6 here. In the proof therefore we do not forget about the tuple t and, for each database B, consider the Answer(B, ·, ·) problem. We will show how, for a given database B, a number k of the first-order variables and a number n of the second-order variables, to construct a parenthesis grammar G, such that every formula φ ∈ FP_{n}^{k} and every tuple t of the length l

B, t ⊧_{FP} (y_{1}, …, y_{l})φ iff t ⊧_{FP} (y_{1}, …, y_{l})φ ∈ L(G)  (19)

Suppose, that x_{1}, …, x_{k} are first order variables and V_{1}, …, V_{n} are second-order variables (each of arity ar(V_{i})). Let B = {|B|, σ, |[·]|} be an arbitrary database. Moreover let V al be a set of all valuations of the variables x_{1}, …, x_{k}, let B be a set of all extensions of a database B with symbols V_{1}, …, V_{n}, and let P(B × V al) = {T_{1}, …, T_{l}}. The grammar consists of

– initial symbol S and a set of nonterminal symbols: {T_{1}, …, T_{l}}

– a set of terminal symbols: all first-order variables, all tuples of them, all second order variables and all symbols in B, ¬, ∧, ∨, (,), ⊧_{FP}, ., μ, ν, ∃ and ∀

– productions:

For every T_{i}, T_{i_{1}}, T_{i_{2}}, every (D, v) ∈ T_{i} every two variables x and y, every two tuples of variables x and y we have: S → (t ⊧_{FP} (y_{1}, …, y_{l})T_{i}) where t = ((v(y_{1}), …, v(y_{l})))

T_{i} → (x = y)  iff v(x) = v(y)
T_{i} → (x ≠ y)  iff v(x) ≠ v(y)
T_{i} → (R_{j}(x)) iff T_{i} = {(D, v) : D, v ⊧_{FP} (R_{j}(x)}
T_{i} → (¬R_{j}(x)) iff T_{i} = {(D, v) : D, v |̸=_{FP} (R_{j}(x)}
T_{i} → (V_{j}(x)) iff T_{i} = {(D, v) : D, v ⊧_{FP} (V_{j}(x)}
T_{i} → (T_{i_{1}} ∧ T_{i_{2}}) iff T_{i} = T_{i_{1}} ∩ T_{i_{2}}
T_{i} → (T_{i_{1}} ∨ T_{i_{2}}) iff T_{i} = T_{i_{1}} ∪ T_{i_{2}}
T_{i} → (∃y.T_{h}) iff T_{i} = {(D, v) : ∃p. (D, v[p/y]) ∈ T_{h}}
T_{i} → (∀y.T_{h}) iff T_{i} = {(D, v) : ∀p. (D, v[p/y]) ∈ T_{h}}

The most interesting is the case of the fixpoint formulas. Note, that for every T_{h} induces a following operator on relations on |B|:

ρ_{T_{h}(x)}(V) = {z : (D[V/V_{j}], v[z/x]) ∈ T_{h}}

For every T_{i} and every T_{h}, such that the operator ρ_{T_{h}}(x) is monotone, there exists a least fixpoint ρ_{T_{h}(x)}^{∞} of the ρ_{T_{h}(x)} operator. For an arbitrary tuples y and z (of the length ar(V_{j})) of first-order variables we say that

T_{i} → ((μV_{j}(x).T_{h})(y)) iff T_{i} = {(D, v) : (v(y_{1}), …, v(y_{l})) ∈ ρ_{T_{h}(x)}^{∞}}

A production for the greatest fixpoint is defined similarly.

We skip here the formal proof of (19) □

6.2 Prefix Form

Define \overline{FP}^{k} formulas as an FP^{k} formulas of the form

prefix of fix-point operators . first-order formula . arguments

(where arguments can be variables or constants). In the \overline{FP}^{k} formulas we will write μV(x)←(y).φ instead of (μV(x).φ)(y). This makes them more readable. It this section we will show, that the expression and combined complexities of F̂P^{k} are PSPACE-complete. Namely we show the following

Theorem 12. There exists a database B, such that the Answer_{FP}_{k} problem is PSPACE-complete.

Proof sketch Let B = ⟨{0, 1, Set, T, F}⟩ [{1}/W_{p_{−1}}]. For a given QBF formula ϕ = ∀p_{1}∃p_{2} … ∀p_{n−1}∃p_{n}.φ (where φ is a sentence which variables are among

p_{1}, …, p_{n}) we will show how to construct in PTIME an F̂P^{k} formula χ, such that

⊧_{QBF} ϕ iff B ⊧_{FP} χ  (20)

This will complete the proof since the QBF problem remains PSPACE-complete, even when we restrict ourselves to formulas in the prefix form. The formula χ is complex. To define it we first define a function ξ by the following clauses:

\begin{aligned}ξ(φ_{1} ∧ φ_{2}) & = & ξ(φ_{1}) ∧ ξ(φ_{2}) \\ ξ(φ_{1} ∨ φ_{2}) & = & ξ(φ_{1}) ∨ ξ(φ_{2}) \end{aligned}  \begin{aligned}ξ(¬p_{n}) & = & W_{p_{n}}(F) \\ ξ(p_{n}) & = & W_{p_{n}}(T) \end{aligned}

Then, using it, we define a formula FORM_{j}^{i} (Table 1). Finally we define χ = FORM_{n}^{1}(Set, T, 0). Note, that in subformulas of the form

μW_{p_{i}}(x)←(x).(FORM_{n}^{i+1}(x, y, z))  (21)

there are two parameters: y and z. Thus the value of the fixpoints defined by them depends on the value of y and z. Moreover it can be shown, by applying 2∗(n−1)+ 1 times Lemma 7 to (21), that every x, y, z ∈ {T, F, 0, 1} satisfy (21) iff x = y or x = z. In this way we are able remember valuations of QBF variables. We define C(p_{1}, …, p_{i}) to be an extension of the database B with symbols W_{p_{1}}, …, W_{p_{n}}.

FORM_{j}^{i}(x, y, z) = μV_{p_{i}} (x, y, z)←(x, y, z). μW_{p_{i}} (x)←(x). ; ⋮ ; μV_{p_{j}} (x, y, z)←(x, y, z). μW_{p_{j}} (x)←(x). (x = Set ∧ W_{p_{−1}}(1) ∧ W_{p_{0}}(0) ∧ W_{p_{1}}(0) ∧ ((V_{p_{1}}(Set, T, 1)) ∧ (V_{p_{1}}(Set, F, 1)))) ∨ (x = Set ∧ W_{p_{0}}(0) ∧ W_{p_{1}}(1) ∧ W_{p_{2}}(1) ∧ ((V_{p_{2}}(Set, T, 0)) ∨ (V_{p_{2}}(Set, F, 0)))) ⋮ ∨ (x = Set ∧ W_{p_{l}}(0) ∧ W_{p_{l+1}}(1) ∧ W_{p_{l+2}}(1) ∧ ((V_{p_{l+2}}(Set, T, 0)) ∨ (V_{p_{l+2}}(Set, F, 0)))) ∨ (x = Set ∧ W_{p_{l+1}}(1) ∧ W_{p_{l+2}}(0) ∧ W_{p_{l+3}}(0) ∧ ((V_{p_{l+3}}(Set, T, 1)) ∧ (V_{p_{l+3}}(Set, F, 1)))) ⋮ ∨ (x = Set ∧ W_{p_{n−3}}(0) ∧ W_{p_{n−2}}(1) ∧ W_{p_{n−1}}(1) ∧ ((V_{p_{n−1}}(Set, T, 0)) ∨ (V_{p_{n−1}}(Set, F, 0)))) ∨ (x = Set ∧ W_{p_{n−2}}(1) ∧ W_{p_{n−1}}(0) ∧ W_{p_{n}}(0) ∧ ((V_{p_{n}}(Set, T, 1)) ∧ (V_{p_{n}}(Set, F, 1)))) ∨ (x = Set ∧ W_{p_{n−1}}(0) ∧ W_{p_{n}}(1) ∧ ξ(φ)) ∨ (x = y) ∨ (x = z)

Table 1. The definition of FORM_{j}^{i} (we assume that the number l occuring in the formula is even)

The interpretation of these symbols is given in the following table (here we assume that i is even):

W_{p_{0}} W_{p_{1}} W_{p_{2}} W_{p_{3}} · · · · · · W_{p_{i−2}} W_{p_{i−1}} W_{p_{i}} W_{p_{i+1}} · · · · · · W_{p_{n−1}} W_{p_{n}}
0, T 1, p_{1} 0, p_{2} 1, p_{3}  0, p_{i−2} 1, p_{i−1} 0, p_{i} 0, p_{i}  0, p_{i} 0, p_{i}

(in case i odd we have W_{p_{i}} = ⋯ = W_{p_{n}} = {1, p_{i}}). In the proof we show that for every odd i = 1, …, n and every b ∈ {T, F} we have that

B ⊧_{FP} χ iff ∀p_{1}.∃p_{2}…. ∃p_{i−1}.∀p_{i}.C(p_{1}, …, p_{i}) ⊧_{FP} FORM_{n}^{i+1}(Set,p_{i}, 0)

(for i even, the quantifier prefix is: ∀p_{1}.∃p_{2}…. ∀p_{i−1}.∃p_{i}.). Thus, for i = n, we get that, B ⊧_{FP} χ holds iff

∀p_{1}.∃p_{2}…. ∀p_{n−1}.∃p_{n}.C(p_{1}, …, p_{n}) ⊧_{FP} (FORM_{n}^{n+1}(Set,p_{n}, 0)) (22)

what is equivalent to

∀p_{1}.∃p_{2}…. ∀p_{n−1}.∃p_{n}.B [{T}/W_{p_{0}}, {p_{1}}/W_{p_{1}}, …, {p_{n}}/W_{p_{n}}] ⊧_{FP} ξ(φ)

(23)

Now, form the definition of ξ, it can be easily seen that (23) holds iff ψ holds (recall, that p_{0} does not occur in ξ(φ)). □

6.3 When Does the NP ∩ co-NP Bound Hold?

In this section we will show a syntax restriction of FP^{k}, the combined complexity of which is in NP ∩ co-NP.

Definition 13. F̂P_{k} formulas are the FP_{k} formulas satisfying the following condition:

• For every subformula (θV (x_{1}, …, x_{n}).φ)(y_{1}, …, y_{n}) we require the set of free variables in φ to be contained in {x_{1}, …, x_{n}}.

In the sequel we will use some results on the modal μ-calculus. We recall here that the modal μ-calculus, as introduced by Kozen [Koz83], is a modal logic with two dual fixpoint operators μ and ν. Its formulas are evaluated in the structures of the form:

M = ⟨S, Act, P rop, Q : Act → (S × S) → bool, ρ : P rop → S → bool⟩

where: Act = {a_{1}, …, a_{n}} is the set of actions

P rop = {p_{1}, …, p_{m}} is the set of propositional constants Q is a function assigning binary relations on S to actions in Act ρ is a function assigning the subset of S to every constant in P rop

The syntax of the modal μ-calculus is given by the following grammar:

F ::= F ∧ F | F ∨ F | μx_{i}. F | νx_{i}. F | ⟨a⟩ F | [a] F | x_{i} | p_{i} | ¬p_{i}

Formal definition of the modal μ-calculus semantics can be found in [Koz83]. We write M ⊧ ψ to mean that ψ is satisfied in every state of M (i.e. s ∈ |[ψ]|_{M}).

We will show that, for a fixed k ≥ 2, F̂P^{k} is PTIME-equivalent to the modal μ-calculus in the following sense:

Lemma 14. There exists a polynomial-time transformation that for a given database B produces a model M_{B} and for a given F̂P^{k} formula φ produces a modal μ-calculus formula ψ_{φ}, such that B ⊧ φ iff M_{B} ⊧ ψ_{φ}.

Lemma 15. There exists a polynomial-time transformation that for a given model M produces a database B_{M} and for a given modal μ-calculus formula ψ produces an F̂P^{2} formula φ_{ψ}, such that B_{M} ⊧ φ_{ψ} iff M ⊧ ψ.

The proof Lemma 15 is easy and we will skip it here. Since model-checking for the modal μ-calculus is in NP ∩ co-NP [EJS93], Lemma 14 gives us:

Theorem 16. The Answer_{FP}_{k}(·, ·) problem is in NP ∩ co-NP By Lemma 15 all lower bounds for the modal μ-calculus apply also to the Answer_{FP}_{k}. Thus [ZSS94] we get:

Theorem 17. The Answer_{FP}_{k}(·, ·) problem is PTIME-hard

Proof sketch of Lemma 14:

– every database B with a carrier set B and relational symbols R_{1}, …, R_{n} is

translated to a model M_{B} = ⟨S, Act, P rop, Q, ρ⟩

where S = B^{k}
P rop = {Rel_{1}, …, Rel_{n}, equality}
Act = {change_{1}, …, change_{k}} ∪ {1, …, k}^{k} (remember that k ≥ 2 is fixed)
ρ(Rel_{i}) = |[R_{i}]|_{B} for i = 1, …, n (w.o.l.g we assume that all relations are k-ary)
ρ(equality) = {(x_{1}, …, x_{k}) : x_{1} = x_{2}}
Q(change_{i}) = {⟨(x_{1}, …, x_{k}), (x_{1}, …, x_{i−1}, z, x_{i+1}, …, x_{k})⟩ :
x_{1}, …, x_{k}, z ∈ S}
Q((i_{1}, …, i_{k})) = {⟨(x_{1}, …, x_{k}), (x_{i_{1}}, …, x_{i_{k}})⟩ : x_{1}, …, x_{k} ∈ S}

– The function τ transforming F̂P_{k} formulas into modal μ-calculus formulas is given below. Recall, that we consider here only formulas satisfying condition •. Thus, if the arity of a relation variable is less than k, we can always extend it. Thus we can assume that all relation variables are of arity k. The variables in the modal μ-calculus formula are z_{1} … z_{n} and they correspond to the relational variables V_{1} … V_{n} in an F̂P_{k} formula.

τ(ψ_{1} ∧ ψ_{2}) = τ(ψ_{1}) ∧ τ(ψ_{2})
τ(ψ_{1} ∨ ψ_{2}) = τ(ψ_{1}) ∨ τ(ψ_{2})
τ(∀x_{i}.ψ) = [change_{i}]τ(ψ)
τ(∃x_{i}.ψ) = ⟨change_{i}⟩τ(ψ)
τ((μV_{i}(x_{1}, …, x_{k}).ψ)(x_{i_{1}}, …, x_{i_{k}})) = ⟨(i_{1}) … (i_{k})⟩(μz_{i}.τ(ψ))
τ((νV_{i}(x_{1}, …, x_{k}).ψ)(x_{i_{1}}, …, x_{i_{k}})) = ⟨(i_{1}) … (i_{k})⟩(νz_{i}.τ(ψ))
τ(x_{i} = x_{j}) = [(i, j, 1, …, 1)]equality
τ(R_{j}(x_{i_{1}}, …, x_{i_{k}})) = [(i_{1}, …, i_{k})](Rel_{j})
τ(V_{j}(x_{i_{1}}, …, x_{i_{k}})) = [(i_{1}, …, i_{k})](z_{j})

Now it is easy to prove by structural induction that B, α ⊧_{FP} ψ iff α ∈ |[τ(ψ)]|_{M_{B}}, what implies the correctness of the construction. It is worth to note, that Lemmas 14 and 15 give us translations between models and formulas independently. Thus the expression complexity of F̂P^{k} is PTIMEequivalent to the expression complexity of the modal μ-calculus. The best known lower bound for it is PTIME [DJN96].

We also want to emphasize, that Vardi’s algorithm for evaluating FP^{k} queries from [Var95] works properly for F̂P^{k}. Thus, as announced by Vardi, his algorithm still can be viewed as a new proof of the membership of the model-checking problem for the modal μ-calculus in NP ∩ co-NP.

7 Conclusion

Below we summarize the results from this paper.

Language expression complexity combined complexity
FP^{k}  PSPACE-complete PSPACE-complete
\overline{FP}^{k}  PSPACE-complete PSPACE-complete
FP_{n}^{k}  ALOGTIME  PSPACE-complete
F̂P^{k}  NP ∩ co-NP  NP ∩ co-NP

We recall, that FP^{k} denotes the fixpoint first-order logic with bounded number of first-order variables, \overline{FP}^{k} denotes the prefix version of FP^{k}, sublogic FP_{n}^{k} denotes

FP^{k} with bounded number of second-order variables and F̂P^{k} denotes the sublogic of FP^{k} defined in the Definition 13.

References

[Bus87] S.R. Buss. The boolean formula value problem is in ALOGTIME. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing (New York City, May 25–27, 1987), pages 123–131, New York, 1987. ACM, ACM Press.

[CH82] A. Chandra and D. Harel. Structure and complexity of relational queries. J. Comput. Syst. Sci., 25(1):99–128, August 1982.

[DJN96] S. Dziembowski, M. Jurdziński, and D. Niwiński. On the expression complexity of the modal μ-calculus model checking. unpublished manuscript, 1996.

[EJS93] E. A. Emerson, C. S. Jutla, and A. Sistla. On model-checking for fragments of μ calculus. In CAV’93, volume 679 of LNCS, pages 385–396, 1993.

[Koz83] D. Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27(3):333–354, 1983.

[Lyn77] N. Lynch. Log space recognition and translation of parenthesis languages. J. ACM, 24:583–590, 1977.

[Tar55] A. Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.

[Var82] M.Y. Vardi. The complexity of relational query languages. In Proceedings of the 14th Ann. ACM Symposium on Theory of Computing (San Francisco, CA), pages 137–146, New York, 1982. ACM, ACM Press.

[Var95] M. Y. Vardi. On the complexity of bounded-variable queries. In Proceedings of the 14th ACM Symposium on Principles of Database Systems, pages 266–276, 1995.

[ZSS94] Shipei Zhang, Oleg Sokolsky, and Scott A. Smolka. On the parallel complexity of model checking in the modal mu-calculus. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 154–163, Paris, France, 4–7 July 1994. IEEE Computer Society Press.

This article was processed using the L^{A}TEX macro package with LLNCS style

Recent Publications in the BRICS Report Series

RS-96-41 Stefan Dziembowski. The Fixpoint Bounded-Variable Queries are PSPACE-Complete. November 1996. 16 pp. Presented at the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-40 Gerth St�lting Brodal, Shiva Chaudhuri, and Jaikumar Radhakrishnan. The Randomized Complexity of Maintaining the Minimum. November 1996. 20 pp. To appear in a special issue of Nordic Journal of Computing devoted to the proceedings of SWAT ’96. Appears in Karlson and Lingas, editors, Algorithm Theory: 5th Scandinavian Workshop, SWAT ’96 Proceedings, LNCS 1097, 1996, pages 4�15.

RS-96-39 Hans H� uttel and Sandeep Shukla. On the Complexity of Deciding Behavioural Equivalences and Preorders � A Survey. October 1996. 36 pp.

RS-96-38 Hans H� uttel and Josva Kleist. Objects as Mobile Processes. October 1996. 23 pp.

RS-96-37 Gerth St�lting Brodal and Chris Okasaki. Optimal Purely Functional Priority Queues. October 1996. 27 pp. To appear in Journal of Functional Programming, 6(6), December 1996.

RS-96-36 Luca Aceto, Willem Jan Fokkink, and Anna Ing� olfsd� ottir. On a Question of A. Salomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based. October 1996. 16 pp.

RS-96-35 Gian Luca Cattani and Glynn Winskel. Presheaf Models for Concurrency. October 1996. 16 pp. Presented at the 10th Annual International Conference of the European Association for Computer Science Logic, CSL ’96.

RS-96-34 John Hatcliff and Olivier Danvy. A Computational Formalization for Partial Evaluation (Extended Version). October 1996. To appear in Mathematical Structures in Computer Science.