Scott-Strachey 指称语义 — 给程序找一个独立于实现的数学含义

是什么

指称语义（denotational semantics）是把每段程序都映射成一个数学对象的方法。日常类比：菜谱本身（番茄炒蛋）只是字符串；一个程序的真正含义是它”应当做出来的那盘菜”，菜本身（味道、模样）才是不依赖任何厨房实现的客观物。

Scott 和 Strachey 1971 年说的是：

源代码（语法）  ─────语义函数 V[[·]]─────►  数学对象（domain 中的元素）
"x := x+1"     ──────────────────────────►  λs. s[x ↦ s(x)+1]

不靠”翻译到机器码”也不靠”在某台抽象机上跑一遍”，程序的含义就是一个数学函数。这门学科后来被叫做 denotational semantics，是编程语言理论的奠基支柱之一。

为什么重要

不理解指称语义，下面这些事都没法解释：

为什么《编译原理》/《PL 教科书》里反复出现 “operational / axiomatic / denotational” 三种语义——它们各自回答什么问题
为什么 Haskell / OCaml 这些函数式语言的标准能写得”像数学”，而 C 语言标准只能写成”理论上发生什么”
为什么 hindley-milner / system-f-reynolds-1974 / hoare-logic 都需要一个底层语义模型才能讨论”类型安全”或”程序正确”
为什么 1971 年的论文今天还在被引用——它解决了一个直到今天都没有更好替代的问题

核心要点

指称语义可以拆成 三层抽象：

语义函数 V[[·]]：每个语法构造对应一个数学对象。类比：字典——左边是”番茄”这个词，右边是那种红色蔬菜本身，词典本身不是蔬菜。
状态变换 S→S：命令式语言的命令是”状态到状态的函数”。类比：x := x+1 是一个机器，进去一个仓库快照，出来一个仓库快照（只有 x 那一格变了）。
不动点 fix(F)：递归 / 循环不能直接当数学函数，要在完全格上找最小不动点。先解释三个新词：⊥ 读作”还没算出来 / 未定义”（类比：Excel 里那一格是 #N/A）；完全格就是给元素排个”信息从少到多”的顺序，⊥ 在最底；最小不动点 fix(F) 是”满足 W=F(W) 的解里信息最少的那一个”——保守解，能算出多少算多少。

三者合起来：语法定义递归套娃（语法树），语义函数顺着语法树递归走一遍，每个节点都得到一个数学对象。

实践案例

案例 1：numeral 不等于 number

论文开头的最小例子：二进制字符串 101 是一个符号串（语法），数学对象 5 才是它指称的东西（语义）。

V[[ 0  ]] = 0          // 数字 0
V[[ 1  ]] = 1          // 数字 1
V[[ v0 ]] = 2 · V[[v]] // 末尾加 0：左移一位
V[[ v1 ]] = 2 · V[[v]] + 1

V[[101]] 算出来 = 5。同一个数 5 也可以写成 5（十进制）或 V（罗马），但语义函数把它们都映到同一个数学对象。符号 ≠ 概念 是整套理论的起点。

注意：左边方括号里的 101 是源语言里的字符串，右边是元语言（数学）里的数字。论文用 [[·]] 这对方括号专门把”语法对象”括起来，提醒读者不要把符号和数学概念混在一起。

案例 2：把赋值变成数学函数

先把数学符号 λ 桥接一下：λs. <表达式> 读作”接收一个 s，返回 <表达式>“——和 Python 的 lambda s: ... 完全是一回事。下面用得到。

考虑命令 x := x + 1。状态 S 是”变量名 → 值”的映射（一个仓库的当前快照）。这条命令的指称语义是：

C[[ x := x+1 ]] = λs. s[x ↦ s(x) + 1]

读法：“接收一个状态 s，返回新状态——只有 x 那一格被改成 s(x)+1，其他不变。” 这是个真正的数学函数 S→S，不依赖任何机器。

两段程序在指称语义下等价就是它们的 S→S 函数完全相等：

C[[ x := x+1 ; y := y+1 ]] = C[[ y := y+1 ; x := x+1 ]]

这种交换律可以靠”两边都是同一个数学函数”直接证明，而不必去比对执行轨迹。

案例 3：递归用最小不动点解

while b do c 自己定义自己：执行一次循环体后，还是要执行 while b do c。所以它的语义里 W 必然出现在自己的定义里——这是递归方程：

W = λs. if B[[b]](s) then W(C[[c]](s)) else s

W 出现在等式两边，不能直接代入算。Scott 的 domain theory 保证：在带 ⊥ 的完全格上、对单调连续的 F，方程 W = F(W) 一定有最小不动点 fix(F)，这就是 while 的指称。“循环不终止”对应的是结果 = ⊥（计算永远卡在”还没算出来”那一档）。

踩过的坑

把指称当操作语义的另一种写法：两者目标完全不同——操作语义给”执行步骤”，指称语义给”数学对象”。它们互为参照，不互相替代。混了的人写出来的笔记会变成”用数学符号假装的解释器”。
以为 while 可以直接当数学函数：循环可能不终止，对应的状态变换是部分函数。必须先扩展到带 ⊥ 的完全格，再用最小不动点定义，否则等式根本无解。
想用普通集合论硬构造递归域：论文末尾给出 V ≅ T + N + L + [S→S] + [V → [S → V × S]]——这个方程在普通集合论里没解（基数论上 [S→S] 比 S 大）。这正是 Scott 1969 发明 domain theory 的动机：把”集合”换成”信息序”。
把语义函数当成翻译器：V[[·]] 是数学定义不是程序，它不需要可计算。它是”程序应当是什么”的标准；具体实现是否符合标准是另一个问题（编译器正确性证明的核心议题）。

适用 vs 不适用场景

适用：

给函数式 / 高阶语言写”标准定义”——Haskell / Standard ML / Scheme 标准都用类似方法
证明编译器的正确性——拿源语言指称和目标语言指称对比
推导程序变换的合法性——两种写法等价当且仅当指称相等
为 hindley-milner / system-f-reynolds-1974 / hoare-logic 提供底层”含义”模型

不适用：

强调”执行细节 / 性能”的场景——指称抽掉了步骤，看不到时间和空间
并发 / 分布式语言——纯指称难处理交错执行（要扩展到 powerdomain / event structure）
工程一线快速理解某段代码在干什么——这种场景操作语义或动手跑更直接

历史小故事（可跳过）

1964 年：Strachey 在 IFIP 形式化语言会议上提出语义函数的雏形，但缺数学严谨性
1969 年：Scott 在牛津发明 domain theory（完全格 + 连续函数），同年秋与 Strachey 在 Oxford PRG 开始合作
1971 年 8 月：合作成果发表为 Oxford PRG-6 技术专著《Toward a Mathematical Semantics for Computer Languages》
1975 年：Strachey 早逝，Scott 后续独自把 domain theory 发展为 PCF 等模型
1977 年：Joseph Stoy 出版《Denotational Semantics》专著，把这套方法系统化为教科书内容

学到什么

程序的含义不必是”它怎么跑”——可以是”它对应哪个数学对象”，这是 50 年来 PL 理论最重要的视角切换之一
语法是符号、语义是数学对象——这条朴素分界让”等价 / 正确 / 安全”这些词有了精确含义
递归需要不动点，不动点需要完全格——理论里一切看起来神秘的”domain”其实是为了让递归方程有解
理论先行，工具跟上——指称语义比工业函数式语言早 10 年成熟，但反过来塑造了后来的语言设计

关联

lambda-calculus —— λ-演算是指称语义最早处理的对象，Scott 的 D∞ 模型就是为它造的
hoare-logic —— 公理语义路线，用前后条件刻画程序，与指称语义互补
hindley-milner —— 类型推导算法的”正确性”需要指称语义模型来定义
system-f-reynolds-1974 —— 多态 λ-演算，语义模型直接用 Scott domain
algol-60 —— Strachey 早期就是为 ALGOL 60 思考语义问题
godel-1931 —— 同样揭示”形式系统 vs 数学对象”分界的奠基工作
turing-1936 —— 给”计算”找数学定义；Scott-Strachey 给”程序含义”找数学定义

反向链接

algol-60 —— ALGOL 60 — BNF 与块结构
cousot-abstract-interpretation —— Cousot 抽象解释 — 给静态分析一套统一数学框架
frenetic-2011 —— Frenetic 2011 — 把 OpenFlow 流表换成函数式程序
game-semantics-pcf —— 博弈论语义与 PCF — 把程序解释成两个人轮流下的对话棋
godel-1931 —— Gödel 1931 — 不完备性定理
hindley-milner —— Hindley-Milner — 编译器自己猜变量类型
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
kahn-natural-semantics —— Kahn 自然语义 — 用一棵推理树说清楚程序求值
lambda-calculus —— λ-演算 — 用三条规则表达所有可计算函数
mycroft-strictness —— Mycroft 严格性分析 — 编译器替你判定哪些参数能”先算”
system-f-reynolds-1974 —— System F — 让类型也能像参数一样被传递
turing-1936 —— Turing 1936 可计算性