A programming language characterizing quantum polynomial time

TL;DR

This work introduces FOQ, a first-order quantum programming language whose terminating programs are reversible, and isolates a tractable subset PFOQ with bounded width that precisely captures the functional quantum class FBQP. It provides a rigorous framework: detailed syntax and semantics, a derivation-level measure for non-superposed recursion, and a polynomial-time soundness result via QTM simulations, establishing PFOQ as fbqp-complete. The paper also delivers a constructive, tractable compiler that converts any PFOQ program into a polynomial-size quantum circuit, using compr and optimize to merge recursive calls across quantum-branch cases. By connecting Yamakami’s fbqp-complete function algebra to PFOQ and offering explicit circuit-generation techniques, the work advances high-level quantum programming with certified polynomial-time guarantees and practical circuit synthesis capabilities.

Abstract

We introduce a first-order quantum programming language, named FOQ, whose terminating programs are reversible. We restrict FOQ to a strict and tractable subset, named PFOQ, of terminating programs with bounded width, that provides a first programming language-based characterization of the quantum complexity class FBQP. Finally, we present a tractable semantics-preserving algorithm compiling a PFOQ program to a quantum circuit of size polynomial in the number of input qubits.

Figures (5)

• Figure 1: Syntax of foq programs
• Figure 2: Semantics of expressions
• Figure 3: Semantics of statements
• Figure 4: Example of circuit $U(cs,l)$
• Figure 5: Example of circuit optimization.

Theorems & Definitions (26)

• Theorem 1
• definition 1
• Lemma 1
• definition 2
• definition 3: PFOQ
• Lemma 2
• Theorem 2
• definition 4
• definition 5: BernsteinVazirani
• Lemma 3