形式陈述

给定单步关系 $\to$$\to$，多步归约 $\to^*$${\to }^{\ast }$ 是其自反传递闭包：$t\to^*t$$t{\to }^{\ast }t$，且若 $t\to u$$t\to u$、$u\to^*v$$u{\to }^{\ast }v$，则 $t\to^*v$$t{\to }^{\ast }v$。正传递闭包 $\to^+$${\to }^{+}$ 要求至少一步。多步关系只编码有限步可达性；无限执行需用序列或共归纳定义。

直觉

单步语义描述一次机器动作，多步语义把有限动作串起来，便于陈述“程序最终到达某状态”。

例子与边界

若 $e\to e_1\to e_2$$e\to e_1\to e_2$，则 $e\to^*e_2$$e{\to }^{\ast }{e}_2$，并且 $e\to^*e$$e{\to }^{\ast }e$。证明保持性常先证单步，再按多步长度归纳推广。把 $\to^*$${\to }^{\ast }$ 误当作对称闭包会混淆可达性与等价性；等价通常还需逆向闭包。

推论与应用

多步归约用于终止、正规化、模拟、编译正确性和小步—大步等价证明。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Parts I–XVIII。
• Gordon D. Plotkin, A Structural Approach to Operational Semantics, DAIMI FN-19, 1981; reprinted 2004，Full report。