指称语义

指称语义研究如何把程序语言的语法映射到明确的数学对象。常用记号 ⟦p⟧ 表示程序 p 的指称，但括号本身不是解释：必须规定它属于什么集合、接受什么输入、给出什么结果。其组合性要求整体的含义由组成部分的含义以及连接它们的语法构造决定，而不靠逐个程序写一份说明。

以只含整数变量的简单命令式语言为例，状态 σ 可以是从变量名到整数的函数。算术表达式的指称把状态映射到整数，布尔表达式映射到真或假，命令则改变状态。这些数学对象描述语言选定的行为，不等于代码的文字释义，也不必保留具体处理器执行的全部细节。

参考：[1]

赋值 x:=x+1 的含义，是接收状态 σ，读出 σ(x)，再返回只把 x 更新为 σ(x)+1 的新状态。skip 的含义是不改变状态。若命令 c₁、c₂ 都能结束，c₁;c₂ 的含义就是先应用 c₁ 的状态变换，再把所得状态交给 c₂；这解释了为什么顺序通常不能随意交换。

例如初始 x=2，程序 x:=x+1; x:=2*x 的最终 x 为 6，反过来执行则为 5。这个区别来自两个状态变换的复合次序，而不需要枚举底层指令。条件命令 if b then c₁ else c₂ 则先在当前状态下解释 b，再选取相应分支的状态变换，并非同时执行两个分支后挑选结果。

参考：[1]

把所有命令都视为“状态到状态”的全函数会遗漏非终止程序，例如条件恒真的空循环没有最终状态。一种处理方法是使用部分函数；另一种方法是在结果域加入特殊元素 ⊥，以表示这类计算没有终止结果。这样命令可写成从状态集合 Σ 到扩充集合 Σ⊥ 的函数。

顺序组合还必须传播这种无结果情形：如果 c₁ 在某状态上得到 ⊥，便不能假装存在一个最终状态供 c₂ 接着处理。语义域不仅要容纳正常数值或状态，也要具备适合讨论近似与极限的结构。域中的信息序描述一个对象提供的信息不多于另一个，不应混同于整数大小或程序速度的排序。

参考：[1] [2]

循环 while b do c 可以展开为：若 b 为真，执行 c 后再次循环；否则结束。这给出一个形如 W=F(W) 的方程，W 是整个循环的状态变换，F 则把某个候选循环行为代入一次展开。方程中出现自身，不等于定义已经完成，更不保证随意挑一个解都符合程序行为。

常见构造从处处为 ⊥ 的最少信息函数开始，反复应用 F，逐渐获得能够在有限展开中确定的结果。在带最小元素的完备偏序上，若 F 满足相应的单调性与连续性条件，这条近似链的最小上界就是最小不动点。条件不可省略：任意函数反复迭代并不必然得到这样的语义。

操作语义以求值或转移规则描述计算，指称语义则把程序赋予数学含义。两者可以为同一语言相互参照，但要证明终止结果等性质对应，仍须核对各自定义并建立相应定理。共享一个语言名称，或在几个例子上得到相同答案，都不能代替这种证明。

参考：[1] [2]