Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantum First-Order Logics That Capture Logarithmic-Time/Space Quantum Computability

Tomoyuki Yamakami

TL;DR

This work introduces a quantum analogue of first-order logic (QFO) to express time- and space-bounded quantum computations via quantum connectives and quantum quantifiers over fixed-dimension states. By grounding QFO in recursion-theoretic schematic definitions of quantum functions and introducing constructs like quantum transitive closure ($\mathrm{QTC}$) and functional quantum variables, the authors map logical expressiveness to quantum complexity classes such as $\mathrm{BQLOGTIME}$ and $\mathrm{BQL}$. They establish inclusions and equivalences like $\mathrm{classicQFO} \subseteq \mathrm{BQLOGTIME}$, $\mathrm{QFO} \subseteq \mathrm{HBQLOGTIME}$, and $\mathrm{QFO}+QTC = \mathrm{ptime}-\mathrm{HBQL}$, while showing that $\mathrm{QFO}+\exists^Q$-functional captures $\mathrm{BQLOGTIME}$ under certain conditions. The findings provide a framework connecting quantum computation and descriptive complexity, with implications for understanding quantum expressiveness, hierarchies, and potential extensions to higher-order quantum logics and proof complexity.

Abstract

We introduce a quantum analogue of classical first-order logic (FO) and develop a theory of quantum first-order logic as a basis of the productive discussions on the power of logical expressiveness toward quantum computing. The purpose of this work is to logically express "quantum computation" by introducing specially-featured quantum connectives and quantum quantifiers that quantify fixed-dimensional quantum states. Our approach is founded on the recently introduced recursion-theoretical schematic definitions of time-bounded quantum functions, which map finite-dimensional Hilbert spaces to themselves. The quantum first-order logic (QFO) in this work therefore looks quite different from the well-known old concept of quantum logic based on lattice theory. We demonstrate that quantum first-order logics possess an ability of expressing bounded-error quantum logarithmic-time computability by the use of new "functional" quantum variables. In contrast, an extra inclusion of quantum transitive closure operator helps us characterize quantum logarithmic-space computability. The same computability can be achieved by the use of different "functional" quantum variables.

Quantum First-Order Logics That Capture Logarithmic-Time/Space Quantum Computability

TL;DR

This work introduces a quantum analogue of first-order logic (QFO) to express time- and space-bounded quantum computations via quantum connectives and quantum quantifiers over fixed-dimension states. By grounding QFO in recursion-theoretic schematic definitions of quantum functions and introducing constructs like quantum transitive closure () and functional quantum variables, the authors map logical expressiveness to quantum complexity classes such as and . They establish inclusions and equivalences like , , and , while showing that -functional captures under certain conditions. The findings provide a framework connecting quantum computation and descriptive complexity, with implications for understanding quantum expressiveness, hierarchies, and potential extensions to higher-order quantum logics and proof complexity.

Abstract

We introduce a quantum analogue of classical first-order logic (FO) and develop a theory of quantum first-order logic as a basis of the productive discussions on the power of logical expressiveness toward quantum computing. The purpose of this work is to logically express "quantum computation" by introducing specially-featured quantum connectives and quantum quantifiers that quantify fixed-dimensional quantum states. Our approach is founded on the recently introduced recursion-theoretical schematic definitions of time-bounded quantum functions, which map finite-dimensional Hilbert spaces to themselves. The quantum first-order logic (QFO) in this work therefore looks quite different from the well-known old concept of quantum logic based on lattice theory. We demonstrate that quantum first-order logics possess an ability of expressing bounded-error quantum logarithmic-time computability by the use of new "functional" quantum variables. In contrast, an extra inclusion of quantum transitive closure operator helps us characterize quantum logarithmic-space computability. The same computability can be achieved by the use of different "functional" quantum variables.
Paper Structure (20 sections, 19 theorems, 2 figures)

This paper contains 20 sections, 19 theorems, 2 figures.

Table of Contents

  1. Background, Motivations, and Challenges
  2. Quantum Computing and Quantum Logic
  3. Quick Review on the Classical First-Order Logic or FO
  4. Our Challenges in This Work
  5. Basic Definitions
  6. Numbers, Languages, and Promise Problems
  7. Classical First-Order Logic
  8. Quantum States and Quantum Operations
  9. Definition of Quantum First-Order Logic
  10. A Preliminary Discussion on Quantum First-Order Logic
  11. Syntax
  12. Semantics
  13. Basic Properties
  14. Quantum First-Order Logic or QFO
  15. Complexity Classes Characterized by QFO
  16. ...and 5 more sections

Key Result

Lemma 3.10

(1) If $(P\wedge Q) \wedge R$ and $P\wedge (Q\wedge R)$ are well-formed, then they are semantically equivalent to each other. (2) If $P\wedge (x[1])[Q_1\:\|\: Q_2]$ and $(x[1])[P\wedge Q_1\:\|\: P\wedge Q_2]$, then they are semantically equivalent to each other.

Figures (2)

  • Figure 1: Inclusion relationships among the complexity classes discussed in this work. In BIS90, HLOGTIME was expressed as HL.
  • Figure 2: A hardware of a QTM equipped with an input tape, an index tape, and a work tape.

Theorems & Definitions (33)

  • Definition 3.1: Quantum terms
  • Definition 3.2: Quantum formulas
  • Definition 3.3: Well-formedness
  • Example 3.4
  • Definition 3.5: Consequential/introductory quantum quantifiers
  • Definition 3.6: Structure
  • Definition 3.7: Interpretation
  • Definition 3.8: Evaluation
  • Definition 3.9: Satisfiability, semantical validity
  • Lemma 3.10
  • ...and 23 more