形式陈述

指称语义为每类程序短语赋予数学对象。若命令 $C$$C$ 在状态集合 $\Sigma$$\mathrm{\Sigma }$ 上运行，一种简单解释是部分函数

$$ \llbracket C\rrbracket:\Sigma\rightharpoonup\Sigma, $$$$[[C]]:\mathrm{\Sigma }\rightharpoonup \mathrm{\Sigma },$$

未定义表示不终止；也可在带底元素 $\bot$$\mathrm{\perp }$ 的域中写成总函数 $\Sigma\to\Sigma_\bot$$\mathrm{\Sigma }\to {\mathrm{\Sigma }}_{\mathrm{\perp }}$。语义必须满足组合性：复合短语的指称只由其直接子短语的指称及相应语义算子决定。例如

$$ \llbracket C_1;C_2\rrbracket =\llbracket C_2\rrbracket\circ\llbracket C_1\rrbracket. $$$$[[C_1;C_2]]=[[C_2]]\circ [[C_1]].$$

递归通常解释为适当连续泛函的不动点。

直觉

指称语义把程序看成数学对象，而不是一串机器步骤。两个程序若得到同一指称，就在该语义观察能力下不可区分；组合性使大型程序的含义可由小部件逐层计算。

例子与边界

赋值命令 $x:=e$$x:=e$ 可解释为状态更新函数

$$ \sigma\mapsto \sigma[x\mapsto\llbracket e\rrbracket\sigma]. $$$$\sigma \mapsto \sigma [x\mapsto [[e]]\sigma ].$$

简单地把所有程序解释为普通集合上的全函数会遗漏不终止；而递归方程也未必在任意序结构中有合适最小解，因此域、单调性和连续性条件不是装饰。

推论与应用

指称语义支持语义等价、编译正确性和程序优化证明，并把递归、非终止和高阶函数连接到序理论与域论。它不必精确记录执行时间、并发交错或概率分布；要表达这些观察量必须选择更丰富的语义域。

参考资料

• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993，Chs. 5–8。
• Dana Scott and Christopher Strachey, Toward a Mathematical Semantics for Computer Languages, Technical Monograph PRG-6, Oxford University Computing Laboratory, 1971，Full monograph, especially §§1–4。