Definition. 多步规约

以一步规约的关系 $⟶$ 为基础， $𝑡 ⟶^{*} 𝑡^{'}$ 读作“ $𝑡$ 多步规约到 $𝑡^{'}$ ”，表示从 $𝑡$ 出发经过零步或有限多步一步规约到达 $𝑡^{'}$ ．精确地说，它是对下面两条规则封闭的最小关系：

M-Refl：前提无；结论 t ⟶^(∗) t M-Step：前提 t ⟶ t'；t' ⟶^(∗) t''；结论 t ⟶^(∗) t''

References