Proto-Quipper with Reversing and Control

The quantum programming language Quipper supports circuit operations such as reversing and controlling certain quantum circuits.Additionally, Quipper provides a function called with-computed, which can be used to program circuits of the form g; f ; g .The latter is a common pattern in quantum circuit design.One benefit of using with-computed, as opposed to constructing the circuit g; f ; g directly from g, f , and g , is that it facilitates an important optimization.Namely, if the resulting circuit is later controlled, only f needs to be controlled; the circuits g and g need not even be controllable.In this paper, we formalize a semantics for reversible and controllable circuits, using a dagger symmetric monoidal category R to interpret reversible circuits, and a new notion we call a controllable category N, which encompasses the control and with-computed operations in Quipper.We extend the language Proto-Quipper with reversing, control and the with-computed operation.Since not all circuits are reversible and/or controllable, we use a type system with modalities to track reversibility and controllability.This generalizes the modality of Fu-Kishida-Ross-Selinger 2023.We give an abstract categorical semantics, and show that the type system and operational semantics are sound with respect to this semantics.