[推论] 类型安全

  • Glomzzz
  • 2026-10-10
  • About

由 [定义] 项的集合 、 [定义] 一步归约 与 [定义] 类型与类型判断 规定的布尔值／自然数语言是类型安全的（ [定义] 类型安全 ）：若 𝑡:𝑇 且 𝑡⟶ ∗𝑡 ′，则 𝑡 ′ 没有受阻。

证明

对 𝑡⟶ ∗𝑡 ′ 的步数归纳（ [定义] 多步归约 的两条规则）。

  • 零步：𝑡 ′=𝑡，于是 𝑡 ′:𝑇。
  • 至少一步：𝑡⟶𝑡 1 且 𝑡 1⟶ ∗𝑡 ′。由 [定理] 保型 ，𝑡 1:𝑇；对 𝑡 1 用 归纳假设 即可。

归纳给出的其实是更强的结论：𝑡 ′:𝑇。最后对 𝑡 ′ 用 [定理] 进展 ：它是值或能归约，总之不是受阻的。

∎

References

[定义] 类型安全 [type-safety]

[定义] 项的集合 [set-of-terms]

[定理] 进展 [progress]

[定义] 一步归约 [one-step-reduction]

[定理] 保型 [preservation]

[定义] 类型与类型判断 [types-and-typing-judgments]

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

[定义] 归纳假设 [induction-hypothesis]

Backlinks

[附注] 测试不是证明 [testing-is-not-proof]

[注记] 莱布尼茨与弗雷格 [leibniz-and-frege]

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

[附注] 显式错误规则与 Kotlin 的底类型 [explicit-errors-and-kotlin-bottom-type]

[] 类型安全：典范形式、进展与保型 [type-safety]

[注记] 证伪与证实 [falsification-and-verification]

[推论] 检查器接受的程序不会受阻 [accepted-programs-do-not-get-stuck]

[附注] 类型系统是保守的 [conservative-type-systems]

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

[附注] 静态类型与动态类型 [static-and-dynamic-typing]

[] 类型：语法导向、反演与唯一性 [typing]

[注记] 约定与必然 [convention-and-necessity]

Based on Typsite