Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction

Kostia Chardonnet, Ugo Dal Lago, Naohiko Hoshino, Paolo Pistone

TL;DR

Girard's geometry of interaction is leveraged to perform as much of the classical computation as possible, at the same time producing a circuit that performs all the quantum operations in the underlying $\lambda$-term.

Abstract

We present an algorithm turning any term of a linear quantum $λ$-calculus into a quantum circuit. The essential ingredient behind the proposed algorithm is Girard's geometry of interaction, which, differently from its well-known uses from the literature, is here leveraged to perform as much of the classical computation as possible, at the same time producing a circuit that, when evaluated, performs all the quantum operations in the underlying $λ$-term. We identify higher-order control flow as the primary obstacle towards efficient solutions to the problem at hand. Notably, geometry of interaction proves sufficiently flexible to enable efficient compilation in many cases, while still supporting a total compilation procedure. Finally, we characterize through a type system those $λ$-terms for which compilation can be performed efficiently.

Compiling Quantum Lambda-Terms into Circuits via the Geometry of Interaction

TL;DR

Girard's geometry of interaction is leveraged to perform as much of the classical computation as possible, at the same time producing a circuit that performs all the quantum operations in the underlying -term.

Abstract

We present an algorithm turning any term of a linear quantum -calculus into a quantum circuit. The essential ingredient behind the proposed algorithm is Girard's geometry of interaction, which, differently from its well-known uses from the literature, is here leveraged to perform as much of the classical computation as possible, at the same time producing a circuit that, when evaluated, performs all the quantum operations in the underlying -term. We identify higher-order control flow as the primary obstacle towards efficient solutions to the problem at hand. Notably, geometry of interaction proves sufficiently flexible to enable efficient compilation in many cases, while still supporting a total compilation procedure. Finally, we characterize through a type system those -terms for which compilation can be performed efficiently.
Paper Structure (26 sections, 18 theorems, 40 equations, 11 figures)

This paper contains 26 sections, 18 theorems, 40 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Outline
  3. A Bird's Eye View on the Problem
  4. The $\lambda^Q\xspace$-Calculus
  5. Syntax
  6. Type System
  7. Operational Semantics
  8. Quantum Circuits
  9. Quantum Circuits with Classical Control Flow
  10. Semantics of Circuits
  11. Eliminating Classical Control Flow
  12. The Quantum Circuit Token Machine
  13. Extended Circuits
  14. The $\textsf{QCSIAM}$ Machine
  15. Soundness
  16. ...and 11 more sections

Key Result

theorem 1

For any circuit $\Gamma\rhd C\rhd \Delta$ of size $n$, there exists a plain circuit $\Gamma\rhd D\rhd \Delta$ of size $\mathcal{O}(n)$ such that $\llbracket C\rrbracket=\llbracket D\rrbracket$.

Figures (11)

  • Figure 1: Example of evaluation of a closure.
  • Figure 2: Circuit Typing Rules.
  • Figure 3: Interpretation of Circuits.
  • Figure 4: Extended Circuit Typing Rules.
  • Figure 5: Illustration of the configurations of the $\textsf{QCSIAM}$.
  • ...and 6 more figures

Theorems & Definitions (38)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6: Quantum Closure selinger2009quantum
  • definition 7: Pseudo-Distributions
  • definition 8: Values, Evaluation Contexts, and Substitution
  • definition 9
  • definition 10
  • ...and 28 more