Deconstructed Proto-Quipper: A Rational Reconstruction
Ryan Kavanagh, Chuta Sano, Brigitte Pientka
TL;DR
This paper presents Proto-Quipper-A, a rational reconstruction of Proto-Quipper-M that replaces complex meta-operations with a linear $\lambda$-calculus inside a symmetric monoidal category, enabling reasoning about circuits as morphisms. It uses adjoint logic to integrate a linear circuit language with a linear/non-linear functional language under a pure call-by-value semantics, so that circuits are constructed and reduced without needing a separate circuit state. A central technical contribution is a simple logical-relations-based normalization proof via a structural approximation, Proto-Quipper-X, avoiding the heavy substitutions typically required for substructural systems. The work demonstrates reconstruction of Proto-Quipper abstractions such as box and apply from primitive operations and discusses mechanization prospects and potential extensions to dynamic lifting and broader circuit optimization.
Abstract
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 $λ$-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.