[推论] 检查器接受的程序不会受阻

  • Glomzzz
  • 2026-10-10
  • About

取 Rust 类型检查算法 type_of type_of ，以及 [定义] 多步归约 的关系 ⟶ ∗。若 type_of(t) = Some(T) type_of(t) = Some(T) 且 𝑡⟶ ∗𝑡 ′，则 𝑡 ′ 不会处于 [定义] 范式与受阻 定义的受阻状态。

证明
由 [定理] 算法可靠性 得 𝑡:𝑇，再由 [推论] 类型安全 即得。
∎

References

[定义] 范式与受阻 [normal-forms-and-stuck-terms]

[定理] 算法可靠性 [type-checking-algorithm-soundness]

[推论] 类型安全 [type-safety]

[] 规则与算法：可靠性与完备性 [rules-and-algorithms]

[定义] 多步归约 [multi-step-reduction]

Backlinks

[附注] 两个“可靠” [type-soundness-and-algorithm-soundness]

[] 回头看与延伸阅读 [summary]

Based on Typsite