The Proto-Quipper family of programming languages aims to provide a formal foundation for the Quipper quantum programming language. Unfortunately, Proto-Quipper languages have complex operational semantics: they are inherently effectful, and they rely on set-theoretic operations and fresh name generation to manipulate quantum circuits. This makes them difficult to reason about using standard programming language techniques and, ultimately, to mechanize. We introduce Proto-Quipper-A, a rational reconstruction of Proto-Quipper languages for static circuit generation. It uses a linear $\lambda$-calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. Adjoint-logical foundations integrate this circuit language with a linear/non-linear functional language and let us reconstruct Proto-Quipper's circuit programming abstractions using more primitive adjoint-logical operations. Proto-Quipper-A enjoys a simple call-by-value reduction semantics, and to illustrate its tractability as a foundation for Proto-Quipper languages, we show that it is normalizing. We show how to use standard logical relations to prove normalization of linear and substructural systems, thereby avoiding the inherent complexity of existing linear logical relations.

翻译：Proto-Quipper系列编程语言旨在为Quipper量子编程语言提供形式化基础。然而，Proto-Quipper语言具有复杂的操作语义：它们本质上是效应化的，并且依赖集合论操作与新鲜名称生成来操纵量子电路。这使得使用标准编程语言技术对其进行推理乃至机械化变得十分困难。我们提出Proto-Quipper-A，这是一种针对静态电路生成的Proto-Quipper语言的理性重构。它采用线性$\lambda$-演算来描述量子电路，其正规形式与盒线电路图紧密对应。伴随逻辑基础将该电路语言与线性/非线性函数式语言相集成，使我们能够利用更基本的伴随逻辑操作来重构Proto-Quipper的电路编程抽象。Proto-Quipper-A具有简单的按值调用规约语义，为展示其作为Proto-Quipper语言基础的易处理性，我们证明了该系统的正规化性质。我们展示了如何运用标准逻辑关系来证明线性及子结构系统的正规化，从而规避现有线性逻辑关系固有的复杂性。