形式陈述

异常把计算结果扩展为正常值或异常结果。小步语义中，$\operatorname{raise}\,v$$\mathrm{raise}v$ 沿求值上下文向外传播，跳过普通计算帧，直到最近的匹配处理器；例如

$$ \operatorname{try}\;(\operatorname{raise}v)\;\operatorname{with}\;x\Rightarrow e \longrightarrow e[v/x]. $$$$\mathrm{try}(\mathrm{raise}v)\mathrm{with}x\Rightarrow e⟶e[v/x].$$

未捕获异常成为程序的异常终止。类型系统可给异常统一的可抛出类型，或以效果标注追踪可能抛出的异常；处理分支与正常分支必须产生兼容结果类型。

直觉

异常是跨越普通返回路径的非局部控制转移：一旦抛出，当前上下文被逐层丢弃，直到找到愿意接管该异常的处理点。

例子与边界

解析函数可正常返回语法树，失败时抛出带位置的错误；外围处理器把它转成用户诊断。异常与和类型相关，但显式 Result 值必须由每层函数主动传播，异常传播由动态语义隐式完成。finally、资源释放和多种异常匹配需要额外规则；异常也不自动回滚已经发生的状态更新。

推论与应用

异常语义用于证明处理器范围、异常安全和控制流分析，并连接代数效应与续延。工程上它区分可恢复失败、未捕获终止和资源清理，类型系统则可选择是否静态暴露这些效果。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Ch. 29, exceptions and handlers。
• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993，Chs. 5–7, abrupt termination and exception rules。