Quantum CPOs

TL;DR

This paper develops a new categorical framework called qCPO for quantum computation, enabling sound and adequate models for quantum programming languages with recursion and linear types.

Contribution

It introduces the monoidal closed category qCPO, unifying quantum cpos with classical cpos and von Neumann algebras, and constructs models for PQM and LNL-FPC languages.

Findings

qCPO is enriched over CPO and contains classical cpos and von Neumann algebras.

Constructs sound models for Proto-Quipper-M with recursion.

Provides sound and adequate models for LNL-FPC with quantum and linear features.

Abstract

We introduce the monoidal closed category qCPO of quantum cpos, whose objects are "quantized" analogs of omega-complete partial orders (cpos). The category qCPO is enriched over the category CPO of cpos, and contains both CPO, and the opposite of the category FdAlg of finite-dimensional von Neumann algebras as monoidal subcategories. We use qCPO to construct a sound model for the quantum programming language Proto-Quipper-M (PQM) extended with term recursion, as well as a sound and computationally adequate model for the Linear/Non-Linear Fixpoint Calculus (LNL-FPC), which is both an extension of the Fixpoint Calculus (FPC) with linear types, and an extension of a circuit-free fragment of PQM that includes recursive types.