指称语义

Denotational semantics 为每个程序构造赋予一个数学对象，使程序组合对应对象的组合。对有限维量子系统，常把命令解释为 completely positive trace-nonincreasing map（CPTNI）；没有失败或提前终止时则是 trace-preserving。若程序 $C_1$ 后接 $C_2$，其含义是 $\llbracket C_2;C_1\rrbracket=\llbracket C_2\rrbracket\circ\llbracket C_1\rrbracket$。并行系统通常使用 tensor product。相关的 categorical view 见量子态与量子操作。

基本构造

skip 解释为恒等映射 $\mathrm{id}(\rho)=\rho$；unitary $U$ 解释为

而 Kraus 表示为 $\mathcal E(\rho)=\sum_iK_i\rho K_i^\dagger$。测量若保留 outcome，可把结果放在 classical-quantum 状态中；若 outcome 被 discard，则把各分支映射相加。例如 projective measurement 的无条件语义为 $\rho\mapsto\sum_mP_m\rho P_m$，这会去掉相应基底间的相干项。这样的区分是指称语义中“观察结果是否可用”的一部分。

语义关系与边界

操作语义逐步描述配置如何变化，指称语义直接描述最终映射；二者若满足 adequacy 或 full abstraction 等关系，才能把程序推理转移到数学模型。循环、递归和非终止需要不动点或部分映射，含 classical store 时还要扩展状态空间。CPTNI 模型不自动涵盖所有开放系统细节、有限精度或硬件噪声。本文给出教学级骨架，不声称为某个具体语言完成了语义正确性证明。可用最弱前置条件把该映射转为 predicate transformer。

参考文献：

• Selinger，Towards a quantum programming language，Cambridge DOI。
• Abramsky 与 Coecke，A categorical semantics of quantum protocols，arXiv:quant-ph/0402130。