[定义] 范式与受阻 Glomzzz 2026-10-10 About 采用 [定义] 一步归约 的关系 ⟶。若不存在 𝑡 ′ 使 𝑡⟶𝑡 ′，称 𝑡 是范式（normal form）。按 [定义] 值与数值 判断，不是值的范式称为受阻的（stuck）。 References [定义] 值与数值 [values-and-numeric-values] [定义] 一步归约 [one-step-reduction] Backlinks [例] 归约到受阻 [reduction-to-a-stuck-term] [定义] 类型安全 [type-safety] [] 范式、受阻与多步归约 [normal-forms] [附注] 为什么译作“受阻” [translation-of-stuck] [] 类型安全：典范形式、进展与保型 [type-safety] [] 求值：用推导规则定义运行 [evaluation] [推论] 检查器接受的程序不会受阻 [accepted-programs-do-not-get-stuck] [附注] 求值策略、归约策略与合流性 [evaluation-strategies-reduction-strategies-and-confluence] Based on Typsite