多步归约

单步规则描述局部变化，多步关系回答有限时间内能到哪里。零步分支很实用：已经是结果的项无需特殊规则，也满足 $v{\to }^{\ast }v$。传递性则让较长执行可以由已证明的片段组合。

${\to }^{\ast }$ 只量化有限序列。即使一条无限执行的每个有限前缀都存在，也没有一个“无穷步后的状态”自动加入闭包。发散需要无限轨迹或共归纳判断另行表达。

若左到右算术语义给出

便有 $(1+2)\times 4{\to }^{\ast }12$。同一项还满足 $(1+2)\times 4{\to }^{\ast }(1+2)\times 4$，因为允许零步；它通常不满足对应的 ${\to }^{+}$，除非能沿非空环路回到自身。

令 $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$。在完整 β-归约中，$\mathrm{\Omega }{\to }_{\beta }\mathrm{\Omega }$，所以 $\mathrm{\Omega }{\to }_{\beta }^{+}\mathrm{\Omega }$，并可构造任意长度的有限路径；这仍没有提供最终值。另一个边界是非确定分叉：$t\to u$ 与 $t\to v$ 会使 $t{\to }^{\ast }u$、$t{\to }^{\ast }v$ 同时成立，多步闭包不会替系统选择其中一条。

多步归约把小步语义理路小步操作语义Small-step operational semantics · Structural operational semantics用配置间的一步转移及有限或无限路径精确描述执行顺序、终止、卡住与发散。连接到终止结果：常把“$e$ 求值到值 $v$”写成 $e{\to }^{\ast }v$ 且 $v\in \mathrm{Val}$。仅要求 $v\nrightarrow$ 不够，因为卡住项也没有后继。

单步类型保持可按路径长度归纳理路数学归纳法Mathematical induction · Weak induction由基例和从 n 到 n+1 的归纳步推出性质对全部自然数成立。提升为多步保持：若 $\mathrm{\Gamma }⊢t:T$ 且 $t{\to }^{\ast }u$，则 $\mathrm{\Gamma }⊢u:T$。零步时 $u=t$，直接使用原判断；非零步时先写成 $t\to t_1{\to }^{\ast }u$，用单步保持取得 $\mathrm{\Gamma }⊢t_1:T$，再对剩余路径使用归纳假设。这里归纳的是有限推导长度，不是假定所有执行终止；即使语言存在无限执行，这个结论仍适用于每条有限前缀。

在并发系统中，${\to }^{\ast }$ 收集所有有限调度前缀；在编译正确性中，一个源步骤常对应零个、一个或多个目标步骤，因此模拟关系必须显式使用 ${\to }^{\ast }$。若需排除目标永远只走“零步”而不兑现源行为，还要增加进展或良基条件。