[定义] 多步归约 Glomzzz 2026-10-10 About 以 [定义] 一步归约 的关系 ⟶ 为基础，𝑡⟶ ∗𝑡 ′ 读作“𝑡 多步归约到 𝑡 ′”，表示从 𝑡 出发经过零步或有限多步一步归约到达 𝑡 ′。精确地说，它是对下面两条规则封闭的最小关系： References [定义] 一步归约 [one-step-reduction] Backlinks [附注] 求值策略、归约策略与合流性 [evaluation-strategies-reduction-strategies-and-confluence] [定义] 类型安全 [type-safety] [例] 多步归约到值 [multi-step-reduction-to-a-value] [约定] 箭头 ⟶ 的读法与用法 [reading-the-reduction-arrow] [推论] 类型安全 [type-safety] [推论] 检查器接受的程序不会受阻 [accepted-programs-do-not-get-stuck] Based on Typsite