Selinger gave a superoperator model of a first-order quantum programming language and proved that it is fully definable and hence fully abstract. This paper proposes an extension of the superoperator model to higher-order programs based on modules over superoperators or, equivalently, enriched presheaves over the category of superoperators. The enriched presheaf category can be easily proved to be a model of intuitionistic linear logic with cofree exponential, from which one can cave out a model of classical linear logic by a kind of bi-orthogonality construction. Although the structures of an enriched presheaf category are usually rather complex, a morphism in the classical model can be expressed simply as a matrix of completely positive maps. The model inherits many desirable properties from the superoperator model. A conceptually interesting property is that our model has only a state whose "total probability" is bounded by 1, i.e. does not have a state where true and false each occur with probability 2/3. Another convenient property inherited from the superoperator model is a $\omega$CPO-enrichment. Remarkably, our model has a sufficient structure to interpret arbitrary recursive types by the standard domain theoretic technique. We introduce Quantum FPC, a quantum $\lambda$-calculus with recursive types, and prove that our model is a fully abstract model of Quantum FPC.

翻译：Selinger给出了一个一阶量子编程语言的超算子模型，并证明了该模型是完全可定义因而是完全抽象的。本文基于超算子上的模（等价地，超算子范畴上的富化预层），将超算子模型扩展至高阶程序。富化预层范畴可轻松证明为携带余自由指数的直觉线性逻辑模型，进而通过一种双正交性构造可从中提取出经典线性逻辑模型。尽管富化预层范畴的结构通常较为复杂，经典模型中的态射可简洁地表示为完全正定映射构成的矩阵。该模型继承了超算子模型的诸多优良性质。一个概念上令人感兴趣的性质是：我们的模型中仅存在"总概率"不超过1的状态，即不存在真与假各以2/3概率同时出现的状态。另一个继承自超算子模型的便利性质是ωCPO-富化性。值得注意的是，我们的模型具有足够结构，可通过标准域论技术解释任意递归类型。我们引入量子FPC（一种携带递归类型的量子λ演算），并证明我们的模型是量子FPC的完全抽象模型。