指称语义

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

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

边界是“映射到同一个数学函数”未必自动等于语言中的上下文等价；若语义域忽略时间、异常或资源，而上下文能观察这些差异，语义就不充分。相反，过细的模型可能区分语言无法观察的实现细节。完全抽象要求两种等价恰好一致，是额外而非自动得到的性质。

指称语义为程序等价、递归定义和编译优化提供代数化基础。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 连续性。两边都出现最小不动点，但前提、对象与用途不能互换。