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

TL;DR

This paper introduces a quantum first-order logic framework that captures the expressiveness of logarithmic-time and logarithmic-space quantum computations using specialized quantum connectives and quantifiers.

Contribution

It develops a novel quantum first-order logic that can express quantum logarithmic-time and space computability, extending classical logical frameworks to quantum computing.

Findings

Quantum first-order logic can express bounded-error quantum logarithmic-time computability.

Adding a quantum transitive closure operator characterizes quantum logarithmic-space computability.

Different quantum variables can achieve the same computational expressiveness.

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.