Classical Control, Quantum Circuits and Linear Logic in 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.

References in corpus (2)

• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

Cited by in corpus (12)

• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
• Integration of Quantum Accelerators with High Performance Computing -- A Review of Quantum Programming Tools
• The formal theory of relative monads
• Semantics for Variational Quantum Programming
• Quantum CPOs
• Join Inverse Rig Categories for Reversible Functional Programming, and Beyond
• The Quantum Effect: A Recipe for QuantumPi
• The Quantum Monadology
• Computational Complexity of Deciding Provability in Linear Logic and its Fragments
• Quantum Information Effects
• Compositional theories for host-core languages