“异常是最简单的非恢复例子： 的处理分支忽略 $k$，直接产生替代结果，对应异常语义丢弃当前普通续延。非确定选择 的处理器可分别以 、 调用 $k$，再合并两条结果；这需要 multi sho…”
形式陈述
异常语义把计算结果区分为正常返回与异常结果。可用结果类型 raise e 与 try e with x => h。典型规则包括：先求值被抛出的异常值；异常穿过普通求值上下文向外传播；到达最近匹配的处理器时，把异常值绑定给处理分支。
例如在大步形式中，可有
而正常结果直接穿过 try。具体语言还须规定异常类型匹配、清理动作以及未捕获异常的顶层行为。
在简单类型系统中，try 的正常分支与每个处理分支必须产生同一结果类型（或能汇合到共同上界）；效应系统还可在类型中静态记录哪些异常可能越过当前边界，但不会取代这里的传播与捕获规则。
直觉
异常是一种非局部控制转移：错误发生处不必逐层手写返回码，而是把当前普通续延丢弃，跳到最近的处理器。把结果想成“正常通道或异常通道”有助于理解传播规则；和类型能表示这一区分，但隐式异常还额外改变控制流。定义中“最近匹配处理器”很关键，否则同一异常可能有多个不确定去向。异常不会自动撤销已经发生的副作用，资源清理必须由 finally、作用域析构或线性资源机制另行保证。
例子与边界
表达式 try (1 + raise E) with E => 0 在计算右操作数时抛出 E，加法的剩余计算被跳过，最近处理器返回
边界是把异常当成普通返回值后仍假设控制流相同。显式 Result 值必须由每层模式匹配并转发，而语言级异常自动越过中间栈帧。另一边界是未捕获异常：它不是一个正常值，也不应被误判为“卡住”；语义通常把它定义为顶层错误结果。
推论与应用
异常语义连接操作语义、续延和效应系统。把正常与异常路径编译成成功/失败双续延的完整条款见CPS 变换；异常表与栈展开则是另一类常见运行时实现。在代数效应处理器中，异常可表现为 operation clause 忽略恢复点 catch。
类型系统可用已检查异常或效果行追踪可能抛出的异常；程序验证则需要说明异常后置条件和资源清理，而不仅是正常返回时的性质。
参考资料
- 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。