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

TL;DR

This paper introduces an algorithm that converts linear quantum lambda calculus terms into quantum circuits using Girard's geometry of interaction, enabling efficient and total compilation for many cases.

Contribution

It leverages geometry of interaction to perform classical computation during quantum circuit compilation, addressing higher-order control flow challenges.

Findings

Efficient compilation in many cases due to flexible geometry of interaction

Total compilation procedure supported for a broad class of lambda-terms

Characterization of lambda-terms suitable for efficient compilation via a type system

Abstract

We present an algorithm turning any term of a linear quantum $\lambda$-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 $\lambda$-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 $\lambda$-terms for which compilation can be performed efficiently.