Papers
量子线路描述语言的范畴模型
A Categorical Model for a Quantum Circuit Description Language
Rios 与 Selinger 为 Proto-Quipper-M 建立参数与状态的范畴模型，并证明类型安全、健全性与适切性。
论文信息（2018，EPTCS 266，pp. 164–178；预印本：2017）：Francisco Rios、Peter Selinger。DOI；arXiv:1706.02630
工作
本文形式化 Quipper 的一个小而有用的片段 Proto-Quipper-M。语言区分电路生成时已知的 parameter 与执行时才确定的 state，并在任意对称幺半范畴中描述态射族，量子线路只是其中一种实例。作者先建立参数与状态的范畴模型，再据此定义语言、操作语义和指称语义。
主要贡献
- 为 Proto-Quipper-M 建立参数与状态的范畴模型。
- 给出类型安全的电路描述语言及其操作、指称语义。
- 证明类型安全、soundness 和 adequacy 等性质。
- 将量子线路语言推广到一般对称幺半范畴中的态射族。
局限与适用范围
Proto-Quipper-M 是 Quipper 的核心片段，不是完整工业语言或后端编译器。范畴模型提供语义保证，却不自动解决噪声、门集、设备连通性、资源成本或高阶宿主语言的全部工程问题。安全性和适切性结论依赖所选模型与语言假设。
与其他工作的关系
本文是 Quipper 的语义化核心，也与 QWIRE 一样关注可嵌入的线路语言与类型安全。与 QML 和 Dagger 紧闭范畴与完全正映射 相比，它更明确处理电路生成阶段的参数与执行阶段的状态。
原论文
Francisco Rios and Peter Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266, 164–178 (2018), DOI: 10.4204/EPTCS.266.11. arXiv:1706.02630
本词条用于学习导览。正式引用与技术细节请以文末原始文献为准。
继续阅读Clifford+T 量子力学 ZX 演算的完备公理化→