指称语义

操作语义问程序怎样一步步运行，指称语义问程序作为一个整体“是什么数学对象”。组合性是核心约束：一个大程序的含义应从部件含义拼出，而不必重新观察其内部执行。纯函数可解释为数学函数，命令可解释为状态变换，概率程序可解释为分布变换；递归则由有限展开逐步逼近整体含义。

一个可以完整算出的有限模型 ​

固定语言 L理路上下文等价Contextual equivalence · 程序上下文等价固定类型、语言与观察后，以所有良类型闭合程序上下文能否区分两个部件来定义可替换性。：弱传名 Bool/箭头演算，含条件式与原始发散常量 $\mathrm{\Omega }:\mathsf{Bool}$。它没有一般递归。取

基类型只有 $\mathrm{\perp }\le T$、$\mathrm{\perp }\le F$，$T,F$ 不可比。函数序为逐点序，底元 ${\mathrm{\perp }}_{A\to B}$ 是 $a\mapsto {\mathrm{\perp }}_B$。按类型归纳，每个域都有限：基域有三个元素，两个有限集合之间只有有限多个函数。它们也有每个有向集的上确界：有限有向集含一个最大元素，函数域的有向上确界逐点取得并保持单调。因此这里的单调函数自动保持有向上确界，即 Scott 连续；不需要求无限递归方程就能使用这些域。

环境 $\rho$ 给每个 $x:A$ 指派 $D_A$ 元素。解释的全部子句为

最后一式的 $B$ 是分支结果类型，可能本身为箭头。条件式只在守卫上严格；没有选择的分支不影响结果。结构归纳验证这些解释关于环境单调：应用中若 $f\le f^{\prime }$ 且 $a\le a^{\prime }$，则 $f(a)\le f^{\prime }(a)\le f^{\prime }(a^{\prime })$；条件式的守卫从底提高时，结果从底提高，守卫已为布尔值时则只需所选分支单调。抽象因此确实产生函数域中的元素。

例如常函数 $k=\lambda x:\mathsf{Bool}.\mathsf{true}$ 与严格函数 $s=\lambda x:\mathsf{Bool}.\mathsf{if}x\mathsf{then}\mathsf{true}\mathsf{else}\mathsf{true}$ 的解释为

应用子句于是给出 $[[k\mathrm{\Omega }]]=T$、$[[s\mathrm{\Omega }]]=\mathrm{\perp }$，恰对应一次传名返回与严格守卫发散。

组合性怎样覆盖洞在绑定器内部的情形 ​

任意闭合程序上下文 $C:A\Rightarrow \mathsf{Bool}$ 都诱导数学函数 $F_C:D_A\to D_{\mathsf{Bool}}$：把洞换成新变量 $z:A$，令 $F_C(d)=[[C[z]]][z\mapsto d]$。语义替换引理给出

$[[C[e]]]=F_C([[e]]).$

该式可直接对上下文文法归纳。洞分支为恒等映射；应用与条件式由对应解释子句传递；λ 分支对每个输入 $a$ 在扩展环境中使用归纳假设，再取函数外延相等，所以洞在绑定器内部也被覆盖。填项闭合，故新增绑定不会捕获它的变量。以 $C=[]\mathrm{\Omega }$ 为例，$F_C(f)=f(\mathrm{\perp })$。由一般等式，替换相等指称总给出相等整体指称；再结合基类型充分性，才能得到真实程序观察相同。

对无副作用算术表达式，$[[x+1]]\rho =\rho (x)+1$。命令 x := x+1 可解释为状态函数 $\sigma \mapsto \sigma [x\mapsto \sigma (x)+1]$。while b do c 的含义不是有限语法递归可直接给出的，它如何由有限轮展开构成整体状态变换，见最小不动点语义条目。

模型必须与选定的观察匹配。若模型把两个程序解释为同一对象，而某个上下文能通过时间、异常或资源区分它们，语义相等便失去了上下文可靠性。反过来，过细的模型可能区分语言无法观察的实现细节。完全抽象要求两种等价恰好一致；前一种问题破坏从语义相等到上下文等价的方向，后一种问题破坏反方向。

计算充分性的fix扩充理路计算充分性Computational adequacy · 计算适当性以形式近似证明布尔指称与求值对应，在有限Bool/箭头域上补齐fix基本引理，并由组合性导出上下文可靠性。在保持Bool/箭头类型域不变时加入显式不动点构造，证明从底开始的语义迭代有限稳定，并补出类型推导的递归分支。基线 $L$ 仍无一般递归；扩充后的语义近似稳定也不等于程序必定终止。

指称语义为程序等价、递归定义和编译优化提供代数化基础。DCPO理路有向完备偏序Directed-complete partial order · DCPO · Directed complete poset每个非空有向子集都具有上确界的偏序，用于汇聚相容的信息近似。负责组织信息近似，Scott 连续性理路Scott 连续映射Scott-continuous function · Scott continuity保持有向上确界的单调映射，使有限信息逼近与计算相容。保证近似极限与语义构造相容，Kleene 不动点定理理路Kleene 不动点定理Kleene fixed-point theorem · Kleene fixed point theorempointed DCPO 上 Scott 连续自映射的最小不动点由底元的有限迭代上确界给出。证明迭代上确界是最小不动点，最后由最小不动点语义解释循环与递归；结构、映射、定理和应用分别承担不同证明责任。

与操作语义理路操作语义Operational semantics以配置、推导规则和转移关系规定程序怎样执行及其可观察结果。之间的充分性、可靠性证明可检验模型是否准确。静态分析先以收集语义理路收集语义Collecting semantics · Reachability semantics at program points为每个程序点收集所有可达具体状态，作为静态分析需要可靠逼近的具体语义基准。汇总程序点上的全部可达具体状态，再由抽象解释理路抽象解释Abstract interpretation · Theory of sound static approximation以具体与抽象语义、可靠转移和不动点逼近统一组织静态程序分析的数学框架。映到较粗但可计算的性质域。该路线通常在完备格理路完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。上使用单调算子与Knaster–Tarski 定理理路Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。；递归指称语义则依靠 DCPO 中的有向近似与 Scott 连续性。两边都出现最小不动点，但前提、对象与用途不能互换。