[引理] 典范形式（canonical forms）

  • Glomzzz
  • 2026-10-10
  • About

值与数值使用 [定义] 值与数值 的定义，类型关系使用 [定义] 类型与类型判断 。

  1. 若 𝑣 是值且 𝑣: Bool，则 𝑣 是 true 或 false。
  2. 若 𝑣 是值且 𝑣: Nat，则 𝑣 是数值。
证明

由 [定义] 值与数值 ，值只有三种形状：true、false、数值。

  1. 若 𝑣 是数值，它是 0（由 [引理] 反演 第 1 条，类型只能是 Nat）或 （由第 3 条，类型只能是 Nat）。由 [定理] 类型唯一 ，它不可能同时是 Bool。所以类型为 Bool 的值只能是另两种。
  2. 同理，由 [引理] 反演 第 1 条，true、false 的类型只能是 Bool，所以类型为 Nat 的值只能是数值。
∎

References

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

[定理] 类型唯一 [uniqueness-of-types]

[定义] 值与数值 [values-and-numeric-values]

[引理] 反演 [typing-inversion]

Backlinks

[定理] 进展 [progress]

[例] 进展 [progress]

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

Based on Typsite