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.

翻译：本文提出一种算法，可将线性量子λ演算中的任意项转化为量子电路。该算法的核心基础是Girard的交互几何理论——与文献中广为人知的应用方式不同，本研究利用该理论在最大程度上完成经典计算，同时生成一个电路，该电路在执行时将实现底层λ项中的所有量子操作。我们指出高阶控制流是解决当前问题实现高效编译的主要障碍。值得注意的是，交互几何展现出足够的灵活性，能够在多数情况下实现高效编译，同时仍支持完整的编译流程。最后，我们通过类型系统刻画了那些可进行高效编译的λ项类别。