Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory

TL;DR

This paper develops categorical models for quantum circuit-based programming languages using enriched category theory, integrating linear logic and recursive types to advance the semantic understanding of quantum programming.

Contribution

It introduces enriched categorical semantics for quantum circuit languages embedded in host languages, extending models with recursive types and linking to linear/non-linear frameworks.

Findings

Enriched categories are crucial for modeling quantum circuit languages.

The semantics incorporate recursive types via dcpo-enriched categories.

The approach unifies linear logic, quantum circuits, and enriched category theory.

Abstract

We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.