-
Type-Based Verification of Connectivity Constraints in Lattice Surgery
Authors:
Ryo Wakizaka,
Yasunari Suzuki,
Atsushi Igarashi
Abstract:
Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve d…
▽ More
Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed.
This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present $\mathcal{Q}_{LS}$, a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem.
△ Less
Submitted 31 August, 2024;
originally announced September 2024.
-
Quantum Algorithm for Radiative Transfer Equation
Authors:
Asuka Igarashi,
Tadashi Kadowaki,
Shiro Kawabata
Abstract:
The radiation transfer equation is widely used for simulating such as heat transfer in engineering, diffuse optical tomography in healthcare, and radiation hydrodynamics in astrophysics. By combining the lattice Boltzmann method, we propose a quantum algorithm for radiative transfer. This algorithm encompasses all the essential physical processes of radiative transfer: absorption, scattering, and…
▽ More
The radiation transfer equation is widely used for simulating such as heat transfer in engineering, diffuse optical tomography in healthcare, and radiation hydrodynamics in astrophysics. By combining the lattice Boltzmann method, we propose a quantum algorithm for radiative transfer. This algorithm encompasses all the essential physical processes of radiative transfer: absorption, scattering, and emission. Although a sufficient number of measurements are required to precisely estimate the quantum state, and the initial encoding of the quantum state remains a challenging problem, our quantum algorithm exponentially accelerates radiative transfer calculations compared to classical algorithms. In order to verify the quantum algorithm, we perform quantum circuit simulation using IBM Qiskit Aer and find good agreement between our numerical result and the exact solution. The algorithm opens new application of fault-tolerant quantum computers for plasma engineering, telecommunications, nuclear fusion technology, healthcare and astrophysics.
△ Less
Submitted 7 March, 2024; v1 submitted 4 December, 2023;
originally announced December 2023.
-
Type-based Qubit Allocation for a First-Order Quantum Programming Language
Authors:
Ryo Wakizaka,
Atsushi Igarashi
Abstract:
Qubit allocation is a process to assign physical qubits to logical qubits in a quantum program. Since some quantum computers have connectivity constraints on applications of two-qubit operations, it is mainly concerned with finding an assignment and inserting instructions to satisfy the connectivity constraints. Many methods have been proposed for the qubit allocation problem for low-level quantum…
▽ More
Qubit allocation is a process to assign physical qubits to logical qubits in a quantum program. Since some quantum computers have connectivity constraints on applications of two-qubit operations, it is mainly concerned with finding an assignment and inserting instructions to satisfy the connectivity constraints. Many methods have been proposed for the qubit allocation problem for low-level quantum programs. This paper presents a type-based framework of qubit allocation for a quantum programming language with first-order functions. In our framework, the connectivity constraints are expressed by a simple graph of qubits called a coupling graph. We formalize (1) the source language, whose type system verifies that the number of qubits required for a given program to run does not exceed the number of nodes of the coupling graph, (2) the target language, whose qualified type system verifies that a well-typed program satisfies the connectivity constraints, and (3) an algorithm to translate a source program into a target program. We prove that both languages are type-safe and that the translation algorithm is type preserving.
△ Less
Submitted 2 June, 2023;
originally announced June 2023.
