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

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

[约定] 元变量 [metavariables]

[注记] 存在与生成 [being-and-becoming]

[例] 多步归约到值 [multi-step-reduction-to-a-value]

[引理] 值不可归约 [values-do-not-reduce]

[附注] 为什么要“对 $𝑇$ 一般化” [generalizing-the-type-in-preservation-proofs]

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

[定理] 确定性 [determinism]

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

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

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

[附注] Rust 的 ? ? 运算符 [rust-question-mark-operator]

[约定] 元变量 [metavariables]

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

[定理] 进展 [progress]

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

[定理] 对推导归纳 [induction-on-derivations]

[附注] 什么是归纳 [meaning-of-induction]

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

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

[例] 一棵推导 [reduction-derivation]

[附注] 分支顺序里藏着证明 [proofs-behind-pattern-matching-order]

[注记] “最小 + 归纳”的历史 [history-of-least-sets-and-induction]

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

[例] 保型 [preservation]

[附注] 为什么 E-PredSucc 要求 [numeric-value-restriction-in-predecessor-reduction]

[定义] 对象语言与元语言 [object-language-and-metalanguage]

[附注] 为什么译作“受阻” [translation-of-stuck]

[定理] 保型 [preservation]

[附注] Rust 也是元语言 [rust-as-a-metalanguage]

[附注] 归纳假设不只限于直接子项 [scope-of-induction-hypotheses]

[约定] 阅读约定 [reading-conventions]

[例] 进展 [progress]

[附注] 求值策略、归约策略与合流性 [evaluation-strategies-reduction-strategies-and-confluence]

[约定] 箭头 $⟶$ 的读法与用法 [reading-the-reduction-arrow]

[] 范式、受阻与多步归约 [normal-forms]

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

[例] 归约到受阻 [reduction-to-a-stuck-term]

[注记] 意义即使用 [meaning-as-use]