一句话：用充实范畴为基于电路的量子函数式语言建立范畴语义，并连接线性/非线性模型。
本文研究如何为基于电路的量子函数式语言提供范畴语义，并处理电路语言嵌入宿主语言后的经典控制等问题。作者沿用 QWire 的思路，同时考虑简单的一阶线性电路语言和更强的宿主语言，使前者嵌入后者。宿主语言采用笛卡尔闭范畴与单子的标准语义；电路语言不再解释到普通范畴，而是解释到以宿主范畴为基的充实范畴中。作者进一步说明该结构与线性/非线性模型相关。作为扩展例子，他们利用 W*-代数范畴的 dcpo 充实性，为电路语言加入递归类型。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1711-05159,
title = {Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory},
author = {Mathys Rennela and Sam Staton},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:30)2020}
}