基于交互几何的高阶量子计算语义

尽管当前量子计算研究多使用量子电路等低级形式化方法，近期已提出若干面向结构化量子编程的高级语言/演算。当前工作通过提供函数式量子编程语言的交互式语义，为这类语言的语义研究做出贡献；后者与 Selinger 和 Valiron 的类似，基于线性 lambda 演算并配备如 ! 模和递归等特性。所提出的指称模型是首个支持量子函数式编程语言全部特性的模型；我们证明了语义的充分性。我们模型的构造采用了一系列来自经典计算语义及进程理论的现有技术。其中最显著的是 Girard 的交互几何 (GoI)，由 Abramsky、Haghverdi 和 Scott 以范畴化形式表述。这些技术的数学通用性——主要源于其范畴化表述——被我们利用以实现从经典到量子的迁移。