Deconstructed Proto-Quipper: A Rational Reconstruction

TL;DR

This paper introduces Proto-Quipper-A, a simplified, rational reconstruction of Proto-Quipper that uses linear calculus and logical foundations to facilitate reasoning, normalization, and mechanization of quantum circuit programming.

Contribution

It presents Proto-Quipper-A, a new formal language that simplifies Proto-Quipper's semantics using linear logic and adjoint-logical foundations, enabling easier reasoning and normalization.

Findings

Proto-Quipper-A has a simple call-by-value semantics.

It is proven to be normalizing.

Uses standard logical relations for proofs.

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 $\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.