formal semantics · 交互式可视化
程序语义可视化实验室
把操作语义、指称语义、公理语义等抽象理论，变成可逐步推导、可观察状态变化的交互图形。点击左侧模块，使用每个模块的控制器单步执行，亲眼看到语义如何"运行"。
Small-step / Big-stepFixed-point
Hoare LogicCES Machine
ClosureCPS
Type SafetyBisimulation
MODULE 01
操作语义Operational Semantics
小步语义 (small-step) 把归约拆成单步 t → t'；大步语义 (big-step) 用推导树一次性证明 t ⇓ v。切换模式观察同一表达式的两种执行方式与所用推导规则。
expr ·
MODULE 02
指称语义Denotational Semantics
把程序映射到数学域。递归定义的语义通过最小不动点 fix(φ) 给出：从底元 ⊥ 出发反复应用 φ，逼近一个越来越"定义完整"的函数。
φ(f)(n) = n=0 ? 1 : n·f(n−1) · 阶乘
MODULE 03
公理语义Axiomatic Semantics
Hoare 逻辑用三元组 {P} S {Q} 描述程序。从后置条件 Q 出发，用最弱前置条件 wp 向后传播，逐条语句推出前置条件 P。
wp · backward propagation
MODULE 04
抽象机Abstract Machine · CESK
状态 ⟨e, ρ, σ, κ⟩：控制表达式 e、环境 ρ、存储 σ、续延 κ。单步转换让求值过程显式化，ref / ! / := 直接作用于存储。
⟨Control, Env, Store, Kont⟩
MODULE 05
环境与存储Environment & Store
闭包 = ⟨λx.e, ρ⟩，捕获定义处的环境。词法作用域下，调用时扩展的是闭包捕获的环境，而非当前环境链——因此 x 取到定义时的值。
lexical scope · closure capture
MODULE 06
控制流语义Control-Flow · Continuation
CPS 变换把"将来要做的事"显式化为续延 k。求值时续延栈随嵌套加深、随返回收缩，控制流从隐式调用栈变为显式的续延传递。
(+ 1 (* 2 3)) · continuation stack
MODULE 07
类型安全Type Safety
类型安全 = 进展 (Progress) + 保持 (Preservation)。每步归约后类型不变 (保持)，良类型项或为值或可继续 (进展)。
((λx:Nat. + x 1) 5) : Nat
MODULE 08
等价与细化Equivalence & Refinement
双模拟 (Bisimulation)：两个迁移系统的状态对 (P,Q) 满足——一方每个动作另一方都能用同样动作匹配到相关的状态。失配则不等价。
labelled transition systems · R