编程语言基础：Agda 描述

module plfa.part2.Properties where

本章涵盖了上一章所介绍的简单类型 λ-演算的性质。在这些性质中最为重要的是可进性（Progress）与保型性（Preservation）。我们将在稍后介绍它们，并展示如何通过组合它们来使 Agda 为我们计算归约序列。

导入

open import Relation.Binary.PropositionalEquality
  using (_≡_; _≢_; refl; sym; cong; cong₂)
open import Data.String using (String; _≟_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product.Base
  using (_×_; proj₁; proj₂; ∃; ∃-syntax)
  renaming (_,_ to ⟨_,_⟩)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Relation.Nullary.Decidable using (Dec; yes; no)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Function.Base using (_∘_)
open import plfa.part1.Isomorphism
open import plfa.part2.Lambda

简介

在上一章中介绍了简单类型的 λ-演算，包括闭项、作为值的项、将一个项归约为另一个项和良类型的项的概念。

最终，我们将要展示我们能够通过持续地对一个项做归约，直到它达到一个值。例如，在上一章中我们展示了二加二的和是四，

plus · two · two  —↠  `suc `suc `suc `suc `zero

而这是通过一长链的归约步骤证明的，结束于链最右侧的值。链上的每一个项都具有相同的类型，即 `ℕ。我们还见到了第二个类似的例子，涉及了 Church 表示法表示的数字。

我们可能会希望任意一个项要么是一个值，要么可以进行一步归约。我们将会看到，此性质并不对所有项都成立，但对于所有良类型的闭项成立。

可进性：如果有 ∅ ⊢ M ⦂ A，那么要么项 M 是一个值，要么存在一个项 N 使得 M —→ N 成立。

所以要么我们有一个值，这时我们已经完成了归约；要么我们可以进行一步归约。当处于后者的情况时，我们想要再一次应用可进性。但这样做需要我们首先知道通过归约得到的项本身是良类型的闭项。事实上，只要我们归约的起点是一个良类型的闭项，所得到的项就满足这个性质。

保型性：如果 ∅ ⊢ M ⦂ A 且 M —→ N，那么 ∅ ⊢ N ⦂ A。

这给予我们一种自动化求值的策略。从一个良类型的闭项开始。由可进性，它要么是一个值，于是求值结束了；要么可以被归约为另一个项。由保型性，所以得到的另一个项本身也是一个良类型的闭项。重复这一过程。我们要么会陷入永久的循环中，此时求值过程将不会停机；要么最终会得到一个被确保是闭项且类型与原始项相同的值。接下来我们将这种策略转化为 Agda 代码，以计算 plus · two · two 和所对应 Church 表示法表示数字的变体的归约序列。

（这一章启发自《软件基础》（Software Foundations）/《程序语言基础》（Programming Language Foundations）中对应的 StlcProp 一章。事实上我们技术选择中的一个——通过显示地引入一条判断 Γ ∋ x ⦂ A，而不是将语境视作为一个从标识符映射到类型的函数——简化了开发过程。特别地，我们不需要额外地去归纳定义关系 appears_free_in 就可以证明替换保留了类型。）

值无法被归约

我们从一个简单的观察开始。值无法被归约：

V¬—→ : ∀ {M N}
  → Value M
    ----------
  → ¬ (M —→ N)
V¬—→ V-ƛ        ()
V¬—→ V-zero     ()
V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N

我们考虑值可能处于的三种情况：

如果它是一个 λ-抽象，那么不会匹配任何归约规则
如果它是零，也不会匹配任何归约规则
如果它是一个数的后继，那么它可能可以与规则 ξ-suc 相匹配，但由归纳证明它作为值本身还能进行归约的情况是不可能发生的。

作为推论，可以再进行归约的项不是值：

—→¬V : ∀ {M N}
  → M —→ N
    ---------
  → ¬ Value M
—→¬V M—→N VM  =  V¬—→ VM M—→N

如果我们将这些否定形式展开，可以得到

V¬—→ : ∀ {M N} → Value M → M —→ N → ⊥
—→¬V : ∀ {M N} → M —→ N → Value M → ⊥

可知原命题与推论是同一个函数，只是交换了参数顺序。

练习 `Canonical-≃` （实践）

良类型的式子都属于少数几种标准式（Canonical Form）中的一种。标准式提供了一种类似于 Value 的关系，关联值和它们所属的类型。一个 λ-表达式一定属于函数类型，同时零和后继表达式都属于自然数。更进一步说，此时函数的函数体必须在只包含它的约束变量的语境中是良类型的，后继的参数本身也必须是标准式：

infix  4 Canonical_⦂_

data Canonical_⦂_ : Term → Type → Set where

  C-ƛ : ∀ {x A N B}
    → ∅ , x ⦂ A ⊢ N ⦂ B
      -----------------------------
    → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)

  C-zero :
      --------------------
      Canonical `zero ⦂ `ℕ

  C-suc : ∀ {V}
    → Canonical V ⦂ `ℕ
      ---------------------
    → Canonical `suc V ⦂ `ℕ

证明 Canonical V ⦂ A 与 (∅ ⊢ V ⦂ A) × (Value V) 同构，也就是标准式即良类型的值。

-- 请将代码写在此处

可进性

我们可能希望任意一个项要么是值，要么可以进行一步归约。但并不是所有情况都是这样。考虑这样的项

`zero · `suc `zero

既不是一个值也无法进行一步归约。另外，如果 "s" ⦂ `ℕ ⇒ `ℕ，那么项

 ` "s" · `zero

也无法被归约，因为我们不知道哪个函数被绑定到了自由变量 "s" 上。上述例子中的第一个项是不良类型的，第二个项包含一个自由变量。只有良类型的闭项才有如下求证的性质：

可进性：如果有 ∅ ⊢ M ⦂ A，那么要么项 M 是一个值，要么存在一个项 N 使得 M —→ N 成立。

要陈述这一性质，我们首先需要引入一个关系来刻画什么样的项 M 才是进行的：

data Progress (M : Term) : Set where

  step : ∀ {N}
    → M —→ N
      ----------
    → Progress M

  done :
      Value M
      ----------
    → Progress M

一个进行的项 M 要么可以进行一步归约，这意味着存在一个项 N 使得 M —→ N，要么已经完成了归约，这意味着 M 是一个值。

如果一个项在空语境中是良类型的，那么它满足可进性：

progress : ∀ {M A}
  → ∅ ⊢ M ⦂ A
    ----------
  → Progress M
progress (⊢` ())
progress (⊢ƛ ⊢N)                            =  done V-ƛ
progress (⊢L · ⊢M) with progress ⊢L
... | step L—→L′                            =  step (ξ-·₁ L—→L′)
... | done V-ƛ with progress ⊢M
...   | step M—→M′                          =  step (ξ-·₂ V-ƛ M—→M′)
...   | done VM                             =  step (β-ƛ VM)
progress ⊢zero                              =  done V-zero
progress (⊢suc ⊢M) with progress ⊢M
...  | step M—→M′                           =  step (ξ-suc M—→M′)
...  | done VM                              =  done (V-suc VM)
progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
... | step L—→L′                            =  step (ξ-case L—→L′)
... | done (V-zero)                         =  step β-zero
... | done (V-suc VL)                       =  step (β-suc VL)
progress (⊢μ ⊢M)                            =  step β-μ

我们对这个项良类型的论据做归纳。让我们首先分析前三个情况：

这个项不可能是变量，因为没有变量在空语境中是良类型的。
如果这个项是一个 λ-抽象，可知它是一个值。

如果这个项是一个函数应用 L · M，则考虑对项 L 良类型的推导过程递归应用可进性：
- 如果这个项还能够进行一步归约，我们就有了 L —→ L′ 的论据，再由 ξ-·₁，可知原来的项进行到 L′ · M。
- 如果这个项的归约结束了，我们就有了 L 是一个值的论据。则考虑对项 L 良类型的推导过程递归应用可进性：
  - 如果这个项还能够进行一步归约，我们就有了 M —→ M′ 的论据，再由 ξ-·₂，可知原来的项进行到 L′ · M。要应用归约步骤 ξ-·₂ 需要我们提供项 L 是一个值的论据，而之前对子项可进性的分析已经提供了需要的证明。
  - 如果这个项的归约结束了，我们便有了项 M 是一个值的论据。因此原来的项可以使用 β-ƛ 来进行一步归约。

剩下的情况都很类似。如果我们由归纳得到了一个可以继续进行归约的情况 step 则应用一条 ξ 规则；如果得到的是已经完成归约的情况 done 则要么我们已经得到了一个值，要么应用一条 β 规则。对于不动点，由于可以直接应用所对应的 β 规则，不需要再做归纳。

由于我们在处理 done 的情况之前先考虑了 step 的情况，我们的代码读起来还算简洁。当然我们也可以将其以相反的顺序写，但这样 ... 的简写形式便不再起作用了，我们便需要在所有情况都写出所有的参数。一般来说，推荐先考虑简单的情况（也就是此处的 step），然后再考虑较难的情况（此处的 done）。如果两个情况都比较难，此时你可能不得不将 ... 展开，或者引入一些辅助函数。

也可以用析取和存在量化来形式化可进性，而不是为 Progress M 定义一个数据类型：

postulate
  progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N)

但这会导致证明变得不那么明晰易懂。比起有助于记忆的 done 与 step，现在我们只能用 inj₁ 和 inj₂；同时项 N 也不再是隐式的，从而我们需要将其完整写出。当遇到 β-ƛ 的情况时，需要我们对 λ-表达式 L 做匹配，以决定它的约束变量和函数体，也就是形如 ƛ x ⇒ N 的形式，从而我们才能证明项 L · M 归约到了 N [ x := M ]。

练习 `Progress-≃`（实践）

证明 Progress M 与 Value M ⊎ ∃[ N ](M —→ N) 是同构的。

-- 请将代码写在此处

练习 `progress′`（实践）

补全 progress′ 的证明，并与之前 progress 的证明相对比。

-- 请将代码写在此处

练习 `value?`（实践）

通过将 progress 与 —→¬V 相组合，写一个程序判断一个良类型的项是否是一个值：

postulate
  value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)

证明保型性前的准备工作

归约过程保持类型是我们所期望去证明的另一个性质，而事实上这需要做一定程度的准备工作。在证明中有三个关键步骤。

第一步是证明重命名保持类型。

重命名：考虑两个语境 Γ 和 Δ，满足 Γ 中出现的每个变量同时也在 Δ 中出现且具有相同的类型。那么如果一个项在语境 Γ 中是可赋型的，它在 Δ 中也具有同样的类型。

用符号表示为：

∀ {x A} → Γ ∋ x ⦂ A  →  Δ ∋ x ⦂ A
---------------------------------
∀ {M A} → Γ ⊢ M ⦂ A  →  Δ ⊢ M ⦂ A

接下来是三个重要的结论。 弱化（Weaken）引理断言说如果一个项在空语境中是良类型的，那么它在任意语境中都是良类型的。 去除（Drop）引理断言说如果一个项在给定语境中是良类型的，且此语境中同一个变量出现了两次，此时去除语境中被遮盖的变量，这个项仍然是良类型的。 交换（Swap）引理断言说如果一个项在给定语境中是良类型的，那么在通过交换语境中两个变量后得到的语境中，这个项仍然是良类型的。

（重命名与《软件基础》中出现的 context invariance 引理类似，但在这里既不需要先定义 appears_free_in 引理，也不需要 free_in_context 引理。）

证明的第二步是论述替换保持类型。

替换：如果我们有一个类型为 A 的闭项 V，同时假定变量 x 的类型是 A、项 N 的类型是 B。此时用项 V 替换掉项 N 中的变量 x 得到的项的类型也为 B。

用符号表示为：

∅ ⊢ V ⦂ A
Γ , x ⦂ A ⊢ N ⦂ B
--------------------
Γ ⊢ N [ x := V ] ⦂ B

此结论不依赖于项 V 是一个值，但要求 V 是一个闭项；回忆我们之所以只关注闭项的替换，是为了避免重命名约束变量。我们将要做替换的项在语境 Γ 扩充上一个变量 x 中是良类型的；同时完成替换后的项在语境 Γ 中是良类型的。

这条引理证明了替换与赋型是可组合的：独立地对各组件赋型保证组合的结果也是良类型的。

第三步是证明保型性。

保型性：如果 ∅ ⊢ M ⦂ A 且 M —→ N，那么 ∅ ⊢ N ⦂ A。

我们对所有可能的归约步骤进行归纳来证明保型性，在证明的过程中替换引理起到了重要的作用，它论证了在替换过程中用到的每一条 β-规则都保留了类型。

现在继续我们的三步走。

重命名

我们常常会需要去「重建」一个类型推演过程，也就是将一个类型推演 Γ ⊢ M ⦂ A 替换为对应的推演 Δ ⊢ M ⦂ A。我们能够这样做的前提是每个在语境 Γ 中出现的变量同时也出现在语境 Δ 中，且它们的类型相同。

赋型的三条规则（λ-抽象、对自然数分项与不动点）都有假设来拓展语境以包含一个约束变量。三条规则的每一条中都有语境 Γ 都出现在结论中，同时拓展后的语境 Γ , x ⦂ A 出现在假设中。对于 λ-表达式，也就是：

Γ , x ⦂ A ⊢ N ⦂ B
------------------- ⊢ƛ
Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B

对自然数分项和不动点亦是如此。要处理这类情况，我们首先证明一条论述「如果一个语境和另一个语境之间存在映射，在对两者添加同一个变量后映射仍然存在」的引理：

ext : ∀ {Γ Δ}
  → (∀ {x A}     →         Γ ∋ x ⦂ A →         Δ ∋ x ⦂ A)
    -----------------------------------------------------
  → (∀ {x y A B} → Γ , y ⦂ B ∋ x ⦂ A → Δ , y ⦂ B ∋ x ⦂ A)
ext ρ Z           =  Z
ext ρ (S x≢y ∋x)  =  S x≢y (ρ ∋x)

令 ρ 为这个映射，它将变量 x 出现在语境 Γ 中的论据映射到变量 x 出现在语境 Δ 中的论据。这是由分类讨论变量 x 出现在拓展后语境 Γ , y ⦂ B 的论据证明的：

如果变量 x 与变量 y 相同，我们使用 Z 来访问拓展后 Γ 中的最后一个变量；类似地，访问拓展后 Δ 中的最后一个变量也是通过使用 Z 来完成的。

如果 x 与 y 不相同，我们则使用 S 来跳过拓展后 Γ 中的最后一个变量，在这里 x≢y 即是变量 x 与 y 不相同的论据，同时 ∋x 是变量 x 出现在语境 Γ 中的论据；类似地，我们使用 S 来跳过拓展后 Δ 的最后一个变量，应用 ρ 来寻找变量 x 出现在语境 Δ 中的论据。

有了拓展引理为我们所用，就可以直接写出重命名保持赋型的证明了：

rename : ∀ {Γ Δ}
  → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
    ----------------------------------
  → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename ρ (⊢` ∋w)    =  ⊢` (ρ ∋w)
rename ρ (⊢ƛ ⊢N)    =  ⊢ƛ (rename (ext ρ) ⊢N)
rename ρ (⊢L · ⊢M)  =  (rename ρ ⊢L) · (rename ρ ⊢M)
rename ρ ⊢zero      =  ⊢zero
rename ρ (⊢suc ⊢M)  =  ⊢suc (rename ρ ⊢M)
rename ρ (⊢case ⊢L ⊢M ⊢N)
                    =  ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N)
rename ρ (⊢μ ⊢M)    =  ⊢μ (rename (ext ρ) ⊢M)

像之前一样，令 ρ 为「变量 x 出现在语境 Γ 中的论据」至「变量 x 出现在 Δ 的论据」的映射。我们对项 M 在语境 Γ 中是良赋型的论据做归纳。我们首先来分析前三种情况：

如果项是一个变量，那么对该变量出现在语境 Γ 的论据应用 ρ 就能得到所对应的该变量出现在 Δ 的证明。

如果项是一个 λ-抽象，首先使用之前证明的引理来无误地拓展映射 ρ，然后通过归纳重命名这个 λ-抽象的函数体。

如果项是函数应用的形式，则通过归纳以重命名函数与对应的参数。

对剩下情况的证明大致相同，都是通过对各个子项做归纳，并且在构造引入一个约束变量时拓展映射。

由于做归纳的对象是这个项良赋型的推演过程，拓展语境不会使得归纳假设无效。等价地，此时的递归会停机，这是由于第二个参数在递归过程中总是变小一些，尽管第一个参数有时候变大一些。

我们有三条重要推论，每条都是通过构造一个恰当的语境间映射证明的：

第一，一个闭项可以被弱化到任意语境：

weaken : ∀ {Γ M A}
  → ∅ ⊢ M ⦂ A
    ----------
  → Γ ⊢ M ⦂ A
weaken {Γ} ⊢M = rename ρ ⊢M
  where
  ρ : ∀ {z C}
    → ∅ ∋ z ⦂ C
      ---------
    → Γ ∋ z ⦂ C
  ρ ()

这里的映射 ρ 是平凡的，由于在空语境 ∅ 中不会出现可能的参数。

第二，如果语境中的最后两个变量相等，我们就可以去除掉被遮盖的一个：

drop : ∀ {Γ x M A B C}
  → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C
    --------------------------
  → Γ , x ⦂ B ⊢ M ⦂ C
drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
  where
  ρ : ∀ {z C}
    → Γ , x ⦂ A , x ⦂ B ∋ z ⦂ C
      -------------------------
    → Γ , x ⦂ B ∋ z ⦂ C
  ρ Z                 =  Z
  ρ (S x≢x Z)         =  contradiction refl x≢x
  ρ (S z≢x (S _ ∋z))  =  S z≢x ∋z

在这里映射 ρ 不可能被较里出现的 x 调用，由于它被较外的出现遮盖了。忽略掉在首位的 x 的情况只可能发生在当前寻找的变量不同于 x 时（由 x≢x 或 z≢x 论证），但如果变量在第二个位置被发现了，并且也包含 x，便会导出矛盾（由 x≢x refl 论证）。

第三，如果语境中的最后两个变量不同，我们可以交换它们：

swap : ∀ {Γ x y M A B C}
  → x ≢ y
  → Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C
    --------------------------
  → Γ , x ⦂ A , y ⦂ B ⊢ M ⦂ C
swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
  where
  ρ : ∀ {z C}
    → Γ , y ⦂ B , x ⦂ A ∋ z ⦂ C
      --------------------------
    → Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
  ρ Z                   =  S x≢y Z
  ρ (S z≢x Z)           =  Z
  ρ (S z≢x (S z≢y ∋z))  =  S z≢y (S z≢x ∋z)

在这里重命名将语境的最后一个变量映射到倒数第二个，反之亦然。第一行负责将 x 从语境的最后一个位置移动到倒数第二个，并且将 y 置于最后，这要求提供 x ≢ y 的论据。

替换

证明保型性的关键——也正是证明最具有技巧性的部分——是一条证明替换保持赋型的引理。

回忆为了避免重命名约束变量，替换被限制为只替换闭项。我们所定义的替换并没有强加这一约束，而是由一条断言替换保持赋型的引理刻画的。

我们所关注的是归约闭项，这意味着每当我们应用 β-归约时，所替换的项只含有一个自由变量（也就是所对应 λ-抽象、对自然数分项或不动点表达式的绑定变量）。然而，替换是通过递归定义的，在我们逐层深入项时遇到的绑定变量增长了语境。所以为了进行归纳，我们需要一个任意的语境 Γ，正如这条引理中所陈述的。

下面是替换保持赋型的形式化陈述及其证明：

subst : ∀ {Γ x N V A B}
  → ∅ ⊢ V ⦂ A
  → Γ , x ⦂ A ⊢ N ⦂ B
    --------------------
  → Γ ⊢ N [ x := V ] ⦂ B
subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y
... | yes _         =  weaken ⊢V
... | no  x≢y       =  contradiction refl x≢y
subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y
... | yes refl      =  contradiction refl x≢y
... | no  _         =  ⊢` ∋x
subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
... | yes refl      =  ⊢ƛ (drop ⊢N)
... | no  x≢y       =  ⊢ƛ (subst ⊢V (swap x≢y ⊢N))
subst ⊢V (⊢L · ⊢M)  =  (subst ⊢V ⊢L) · (subst ⊢V ⊢M)
subst ⊢V ⊢zero      =  ⊢zero
subst ⊢V (⊢suc ⊢M)  =  ⊢suc (subst ⊢V ⊢M)
subst {x = y} ⊢V (⊢case {x = x} ⊢L ⊢M ⊢N) with x ≟ y
... | yes refl      =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (drop ⊢N)
... | no  x≢y       =  ⊢case (subst ⊢V ⊢L) (subst ⊢V ⊢M) (subst ⊢V (swap x≢y ⊢N))
subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y
... | yes refl      =  ⊢μ (drop ⊢M)
... | no  x≢y       =  ⊢μ (subst ⊢V (swap x≢y ⊢M))

我们对 N 在由 x 拓展 Γ 后得到的语境中是良赋型的论据做归纳。

首先我们注意到一个有关命名的小问题。在引理的陈述中，变量 x 是一个关于被替换的变量的隐式参数，同时在变量、抽象、对自然数分项和不动点的赋型规则中，变量 x 是一个关于关联变量的隐式参数。因此我们使用形同 {x = y} 的语法来将 y 与被替换的变量绑定，用 {x = x} 来将 x 与 ⊢`、⊢ƛ、⊢case 和 ⊢μ 中关联变量绑定。在这里用 y 这一名字也与前一章中替换的原始定义一致。在证明中从来没有提及过 x、y、V 或 N 的类型，因此在下面的内容中，我们尽可能方便地选择类型名称。

解决了命名问题，接下来我们来分析前三种情况：

当处于变量的情况时，我们必须证明：
```
∅ ⊢ V ⦂ B
Γ , y ⦂ B ⊢ ` x ⦂ A
------------------------
Γ ⊢ ` x [ y := V ] ⦂ A
```
此时第二个假设形如：
```
Γ , y ⦂ B ∋ x ⦂ A
```
此处有两种子情况，取决于该命题的论据：
- 查询判断由规则 Z 给出：
```
----------------
Γ , x ⦂ A ∋ x ⦂ A
```
  在此情况下，x 和 y 必须是一样的，同样 A 和 B 也是。尽管如此，我们必须要求值 x ≟ y 来化简替换的定义：
  - 如果变量相等，那么化简后我们必须证明：
```
∅ ⊢ V ⦂ A
---------
Γ ⊢ V ⦂ A
```
    由弱化可得。
  - 如果变量不相等，我们则得到了一个矛盾。
- 查询判断由规则 S 给出：
```
x ≢ y
Γ ∋ x ⦂ A
-----------------
Γ , y ⦂ B ∋ x ⦂ A
```
  在此情况下，x 和 y 必须是不同的。尽管如此，我们必须要求值 x ≟ y 来化简替换的定义：
  - 如果变量相等，我们则得到了一个矛盾。
  - 如果变量不相等，那么化简后我们必须证明：
```
∅ ⊢ V ⦂ B
x ≢ y
Γ ∋ x ⦂ A
-------------
Γ ⊢ ` x ⦂ A
```
    由变量的赋型规则可得。

当处于抽象的情况时，我们必须证明：

∅ ⊢ V ⦂ B
Γ , y ⦂ B ⊢ (ƛ x ⇒ N) ⦂ A ⇒ C
--------------------------------
Γ ⊢ (ƛ x ⇒ N) [ y := V ] ⦂ A ⇒ C

其中第二条假设可由下得出：

Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C

我们求值 x ≟ y 来化简替换的定义：

如果变量相等，那么化简后我们必须证明：

∅ ⊢ V ⦂ B
Γ , x ⦂ B , x ⦂ A ⊢ N ⦂ C
-------------------------
Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ C

由去除引理可得：

Γ , x ⦂ B , x ⦂ A ⊢ N ⦂ C
-------------------------
Γ , x ⦂ A ⊢ N ⦂ C

抽象的赋型规则给出了所需的结论。

如果变量不相等，那么化简后我们必须证明：

∅ ⊢ V ⦂ B
x ≢ y
Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
--------------------------------
Γ ⊢ ƛ x ⇒ (N [ y := V ]) ⦂ A ⇒ C

由交换引理可得：

x ≢ y
Γ , y ⦂ B , x ⦂ A ⊢ N ⦂ C
-------------------------
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C

归纳假设给出了：

∅ ⊢ V ⦂ B
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
----------------------------
Γ , x ⦂ A ⊢ N [ y := V ] ⦂ C

抽象的赋型规则给出了所需的结论。

当处于应用的情况时，我们必须证明：

∅ ⊢ V ⦂ C
Γ , y ⦂ C ⊢ L · M ⦂ B
--------------------------
Γ ⊢ (L · M) [ y := V ] ⦂ B

其中第二条假设可由下两条判断中得出：

Γ , y ⦂ C ⊢ L ⦂ A ⇒ B
Γ , y ⦂ C ⊢ M ⦂ A

根据替换的定义，我们必须证明：

∅ ⊢ V ⦂ C
Γ , y ⦂ C ⊢ L ⦂ A ⇒ B
Γ , y ⦂ C ⊢ M ⦂ A
---------------------------------------
Γ ⊢ (L [ y := V ]) · (M [ y := V ]) ⦂ B

对于 L 和 M 应用归纳引理，加上应用的赋型规则给出了所需的结论。

对剩下情况的证明大致相同，都是通过对各个子项做归纳。当构造引入一个约束变量时我们需要将其与被替换的变量进行比较，如果它们相同则应用去除引理，如果它们不同则应用交换引理。

对于 Agda 来说，我们写 x ≟ y 还是写 y ≟ x 是有区别的。在交互式证明中，Agda 将显示 _[_:=_] 定义中的哪些剩余 with 子句需要简化，而 subst 中的 with 子句需要精确匹配这些子句。指导准则是 Agda 对于对称性和交换性一无所知，这需要调用适当的引理，因此考虑参数的顺序和保持一致性非常重要。

练习 `subst`（延伸）

重写 subst 的定义，使得它与在上一章练习中修改过的 _[_:=_]′ 定义相兼容。和之前一样，需要将处理约束变量的部分提取成一个单独的函数，与替换保持类型的证明一同互递归定义。

-- 请将代码写在此处

保型性

一旦我们证明了替换保持类型，证明归约保持类型是简单的：

preserve : ∀ {M N A}
  → ∅ ⊢ M ⦂ A
  → M —→ N
    ----------
  → ∅ ⊢ N ⦂ A
preserve (⊢` ())
preserve (⊢ƛ ⊢N)                 ()
preserve (⊢L · ⊢M)               (ξ-·₁ L—→L′)     =  (preserve ⊢L L—→L′) · ⊢M
preserve (⊢L · ⊢M)               (ξ-·₂ VL M—→M′)  =  ⊢L · (preserve ⊢M M—→M′)
preserve ((⊢ƛ ⊢N) · ⊢V)          (β-ƛ VV)         =  subst ⊢V ⊢N
preserve ⊢zero                   ()
preserve (⊢suc ⊢M)               (ξ-suc M—→M′)    =  ⊢suc (preserve ⊢M M—→M′)
preserve (⊢case ⊢L ⊢M ⊢N)        (ξ-case L—→L′)   =  ⊢case (preserve ⊢L L—→L′) ⊢M ⊢N
preserve (⊢case ⊢zero ⊢M ⊢N)     (β-zero)         =  ⊢M
preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV)       =  subst ⊢V ⊢N
preserve (⊢μ ⊢M)                 (β-μ)            =  subst (⊢μ ⊢M) ⊢M

证明从来没有提到 M 或 N 的类型，因此在下面的内容中，我们尽可能方便地选择类型名称。

让我们分析归约规则的两种情况：

规则 ξ-·₁。我们有

L —→ L′
----------------
L · M —→ L′ · M

其中左手侧由

Γ ⊢ L ⦂ A ⇒ B
Γ ⊢ M ⦂ A
-------------
Γ ⊢ L · M ⦂ B

赋型。

根据归纳，我们有

Γ ⊢ L ⦂ A ⇒ B
L —→ L′
--------------
Γ ⊢ L′ ⦂ A ⇒ B

其中右手侧的赋型可以直接得出。

规则 β-ƛ。我们有

Value V
-----------------------------
(ƛ x ⇒ N) · V —→ N [ x := V ]

其中左手侧由

Γ , x ⦂ A ⊢ N ⦂ B
-------------------
Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B    Γ ⊢ V ⦂ A
--------------------------------
Γ ⊢ (ƛ x ⇒ N) · V ⦂ B

赋型。

根据替换引理，我们有

Γ ⊢ V ⦂ A
Γ , x ⦂ A ⊢ N ⦂ B
--------------------
Γ ⊢ N [ x := V ] ⦂ B

其中右手侧的赋型可以直接得出。

剩余情况与此类似，对每个 ξ 规则使用归纳，对每个 β 规则使用替换引理。

求值

通过重复应用可进性和保型性，我们可以对任何良类型的项求值。在这一节，我们将介绍一个 Agda 函数，该函数可以求得任意给定良类型的闭项到其值的归约序列，如果该序列存在。

一些项将永远归约下去。这是一个例子：

sucμ  =  μ "x" ⇒ `suc (` "x")

_ =
  begin
    sucμ
  —→⟨ β-μ ⟩
    `suc sucμ
  —→⟨ ξ-suc β-μ ⟩
    `suc `suc sucμ
  —→⟨ ξ-suc (ξ-suc β-μ) ⟩
    `suc `suc `suc sucμ
  --  ...
  ∎

由于每个 Agda 计算都必须终止，我们不能仅仅要求 Agda 将项归约为值。相反，我们将向 Agda 提供一个自然数，并允许它在需要比给定的数更多的归约步骤时终止归约。

加密货币也存在类似的问题。使用智能合约的系统要求维护区块链的矿工评估体现合约的程序。例如，验证以太坊上的交易可能需要为以太坊虚拟机（EVM）执行一个程序。一个长期运行或非终止的程序可能会导致矿工在验证合同上投入任意多的努力，但回报很少或没有回报。为了避免这种情况，每笔交易都伴随着一定数量的燃料（Gas）可用于计算。在 EVM 上执行的每个步骤都会收取公告数量的燃料，交易以公布的费率支付燃料：每单位燃料支付给定数量的以太币（以太坊的货币）。

以此类推，我们将使用燃料作为参数的名称，该参数限制了归约步骤的数量。Gas 由一个自然数指定。

record Gas : Set where
  constructor gas
  field
    amount : ℕ

当我们的求值器返回了一个项 N，它要么证明 N 是一个值，要么表明它耗尽了燃料：

data Finished (N : Term) : Set where

  done :
      Value N
      ----------
    → Finished N

  out-of-gas :
      ----------
      Finished N

给定一个类型为 A 的项 L，对于某个 N，求值器将返回从 L 到 N 的归约序列以及归约是否完成的指示：

data Steps (L : Term) : Set where

  steps : ∀ {N}
    → L —↠ N
    → Finished N
      ----------
    → Steps L

求值器使用燃料和项是良类型的论据，并返回相应的步骤：

eval : ∀ {L A}
  → Gas
  → ∅ ⊢ L ⦂ A
    ---------
  → Steps L
eval {L} (gas zero)    ⊢L                     =  steps (L ∎) out-of-gas
eval {L} (gas (suc m)) ⊢L with progress ⊢L
... | done VL                                 =  steps (L ∎) (done VL)
... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M)
...    | steps M—↠N fin                       =  steps (L —→⟨ L—→M ⟩ M—↠N) fin

令 L 是我们要归约的项的名称，⊢L 是项 L 是良类型的论据。我们考虑剩余的燃料量。此处有两种可能：

如果是零，则我们过早地停止了。我们将返回简单的归约序列 L —↠ L，并标明我们用尽了燃料。

如果非零，则在下一个步骤中我们还剩下 m 燃料。将进度应用于项 L 是良类型的论据。此处有两种可能：
- 项 L 是一个值，则我们已经完成了。我们将返回简单的归约序列 L —↠ L，以及 L 是值的论据。
- 项 L 步进至另一个项 M。保型性提供了 M 也是良类型的论据，我们对剩余的燃料递归调用 eval。结果将得到 M —↠ N 的论据以及 N 是良类型的论据和归约是否完成的标识。我们将 L —→ M 和 M —↠ N 的论据结合来得到 L —↠ N 以及归约是否完成的标识。

例子

现在我们可以用 Agda 来计算之前给出的不停机的归约序列。首先我们证明项 sucμ 是良赋型的：

⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ
⊢sucμ = ⊢μ (⊢suc (⊢` ∋x))
  where
  ∋x = Z

我们花三步量的燃料来进行求值，以展示这个无穷归约序列的前三步：

_ : eval (gas 3) ⊢sucμ ≡
  steps
   (μ "x" ⇒ `suc ` "x"
   —→⟨ β-μ ⟩
    `suc (μ "x" ⇒ `suc ` "x")
   —→⟨ ξ-suc β-μ ⟩
    `suc (`suc (μ "x" ⇒ `suc ` "x"))
   —→⟨ ξ-suc (ξ-suc β-μ) ⟩
    `suc (`suc (`suc (μ "x" ⇒ `suc ` "x")))
   ∎)
   out-of-gas
_ = refl

类似地，我们可以用 Agda 计算前一章节中给出的归约序列。我们从计算 Church 表示法表示数字的数字二应用到后继和数字零开始。提供 100 步量的燃料就已远超过需求了：

_ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡
  steps
   ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
   · `zero
   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
     `zero
   —→⟨ β-ƛ V-zero ⟩
    (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero)
   —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    (ƛ "n" ⇒ `suc ` "n") · `suc `zero
   —→⟨ β-ƛ (V-suc V-zero) ⟩
    `suc (`suc `zero)
   ∎)
   (done (V-suc (V-suc V-zero)))
_ = refl

上面的例子是通过首先使用组合键 C-c C-n 来范式化等式的左侧，然后将结果粘贴到等式右侧的方式生成的。前一章中归约的例子便是通过使用这一方式导出结果、重新排版并且将展开的表达式对应地重写为 twoᶜ 和 sucᶜ 的形式得到的。

接下来，我们来证明二加二的和是四：

_ : eval (gas 100) ⊢2+2 ≡
  steps
   ((μ "+" ⇒
     (ƛ "m" ⇒
      (ƛ "n" ⇒
       case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
       ])))
    · `suc (`suc `zero)
    · `suc (`suc `zero)
   —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
    (ƛ "m" ⇒
     (ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒
      `suc
      ((μ "+" ⇒
        (ƛ "m" ⇒
         (ƛ "n" ⇒
          case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
          ])))
       · ` "m"
       · ` "n")
      ]))
    · `suc (`suc `zero)
    · `suc (`suc `zero)
   —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    (ƛ "n" ⇒
     case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒
     `suc
     ((μ "+" ⇒
       (ƛ "m" ⇒
        (ƛ "n" ⇒
         case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
         ])))
      · ` "m"
      · ` "n")
     ])
    · `suc (`suc `zero)
   —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒
    `suc
    ((μ "+" ⇒
      (ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
        ])))
     · ` "m"
     · `suc (`suc `zero))
    ]
   —→⟨ β-suc (V-suc V-zero) ⟩
    `suc
    ((μ "+" ⇒
      (ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
        ])))
     · `suc `zero
     · `suc (`suc `zero))
   —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
    `suc
    ((ƛ "m" ⇒
      (ƛ "n" ⇒
       case ` "m" [zero⇒ ` "n" |suc "m" ⇒
       `suc
       ((μ "+" ⇒
         (ƛ "m" ⇒
          (ƛ "n" ⇒
           case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
           ])))
        · ` "m"
        · ` "n")
       ]))
     · `suc `zero
     · `suc (`suc `zero))
   —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
    `suc
    ((ƛ "n" ⇒
      case `suc `zero [zero⇒ ` "n" |suc "m" ⇒
      `suc
      ((μ "+" ⇒
        (ƛ "m" ⇒
         (ƛ "n" ⇒
          case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
          ])))
       · ` "m"
       · ` "n")
      ])
     · `suc (`suc `zero))
   —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
    `suc
    case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
    `suc
    ((μ "+" ⇒
      (ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
        ])))
     · ` "m"
     · `suc (`suc `zero))
    ]
   —→⟨ ξ-suc (β-suc V-zero) ⟩
    `suc
    (`suc
     ((μ "+" ⇒
       (ƛ "m" ⇒
        (ƛ "n" ⇒
         case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
         ])))
      · `zero
      · `suc (`suc `zero)))
   —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
    `suc
    (`suc
     ((ƛ "m" ⇒
       (ƛ "n" ⇒
        case ` "m" [zero⇒ ` "n" |suc "m" ⇒
        `suc
        ((μ "+" ⇒
          (ƛ "m" ⇒
           (ƛ "n" ⇒
            case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
            ])))
         · ` "m"
         · ` "n")
        ]))
      · `zero
      · `suc (`suc `zero)))
   —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
    `suc
    (`suc
     ((ƛ "n" ⇒
       case `zero [zero⇒ ` "n" |suc "m" ⇒
       `suc
       ((μ "+" ⇒
         (ƛ "m" ⇒
          (ƛ "n" ⇒
           case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
           ])))
        · ` "m"
        · ` "n")
       ])
      · `suc (`suc `zero)))
   —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
    `suc
    (`suc
     case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
     `suc
     ((μ "+" ⇒
       (ƛ "m" ⇒
        (ƛ "n" ⇒
         case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
         ])))
      · ` "m"
      · `suc (`suc `zero))
     ])
   —→⟨ ξ-suc (ξ-suc β-zero) ⟩
    `suc (`suc (`suc (`suc `zero)))
   ∎)
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl

再一次地，上一章中的推导是通过编辑上述内容得出的。

类似地，我们可以计算 Church 表示法表示的数字的相应项。

_ : eval (gas 100) ⊢2+2ᶜ ≡
  steps
   ((ƛ "m" ⇒
     (ƛ "n" ⇒
      (ƛ "s" ⇒ (ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z")))))
    · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
    · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
    · (ƛ "n" ⇒ `suc ` "n")
    · `zero
   —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
    (ƛ "n" ⇒
     (ƛ "s" ⇒
      (ƛ "z" ⇒
       (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" ·
       (` "n" · ` "s" · ` "z"))))
    · (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")))
    · (ƛ "n" ⇒ `suc ` "n")
    · `zero
   —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ "s" ⇒
     (ƛ "z" ⇒
      (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" ·
      ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · ` "s" · ` "z")))
    · (ƛ "n" ⇒ `suc ` "n")
    · `zero
   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒
     (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
     ·
     ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
      · ` "z"))
    · `zero
   —→⟨ β-ƛ V-zero ⟩
    (ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
    ·
    ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
     · `zero)
   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
    ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n")
     · `zero)
   —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
    ((ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
     `zero)
   —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
    ((ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `zero))
   —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
    ((ƛ "n" ⇒ `suc ` "n") · `suc `zero)
   —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
    (ƛ "z" ⇒ (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · ` "z")) ·
    `suc (`suc `zero)
   —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    (ƛ "n" ⇒ `suc ` "n") · ((ƛ "n" ⇒ `suc ` "n") · `suc (`suc `zero))
   —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    (ƛ "n" ⇒ `suc ` "n") · `suc (`suc (`suc `zero))
   —→⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
    `suc (`suc (`suc (`suc `zero)))
   ∎)
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
_ = refl

再一次地，上一节中的示例是通过编辑上述内容得出的。

练习 `mul-eval`（推荐）

用这个求值器来验证二乘二的积是四。

-- 请将代码写在此处

练习 `progress-preservation` （实践）

不阅读上面的陈述，写下简单类型 λ-演算可进性和保型性的定理。

-- 请将代码写在此处

练习 `subject_expansion` （实践）

如果 M —→ N，我们便称 M 归约至 N，相同的情形也被称作 N 扩展（Expand）至 M。保型性有时也被叫做主体归约（Subject Reduction）。它的对应是主体扩展（Subject Expansion），如果 M —→ N 和 ∅ ⊢ N ⦂ A 蕴含 ∅ ⊢ M ⦂ A。找到两个主体扩展的反例，一个涉及 case 表达式而另一个不涉及。

-- 请将代码写在此处

良类型的项不会卡住

一个项是范式，如果它不能被归约。

Normal : Term → Set
Normal M  =  ∀ {N} → ¬ (M —→ N)

一个项被卡住，如果它是一个范式但不是一个值。

Stuck : Term → Set
Stuck M  =  Normal M × ¬ Value M

使用可进性，很容易证明没有良类型的项会被卡住。

postulate
  unstuck : ∀ {M A}
    → ∅ ⊢ M ⦂ A
      -----------
    → ¬ (Stuck M)

使用保型性，很容易证明在经过任意多次步进后，良类型的项依旧是良类型的。

postulate
  preserves : ∀ {M N A}
    → ∅ ⊢ M ⦂ A
    → M —↠ N
      ---------
    → ∅ ⊢ N ⦂ A

一个简单地结果是，从一个良类型的项开始，进行任意多次步进，将得到一个不被卡住的项。

postulate
  wttdgs : ∀ {M N A}
    → ∅ ⊢ M ⦂ A
    → M —↠ N
      -----------
    → ¬ (Stuck N)

Felleisen 与 Wright 通过可进性和保型性引入了证明，并将其总结为 良类型的项不会卡住 的口号。（他们提及了 Robin Milner 早期的工作，他使用指称而非操作语义。他引入了「错误」作为带有类型错误的术语的指称，并展示了 良类型的项不会出错。）

练习 `stuck` （实践）

给出一个会被卡住的不良类型的项的例子。

-- 请将代码写在此处

练习 `unstuck` （推荐）

提供上文中 unstuck、preserves 和 wttdgs 三个假设的证明。

-- 请将代码写在此处

归约是确定的

当我们引入归约时，我们声称它是确定的。为完整起见，我们在此提供正式的证明。

我们的证明需要一个合同变体来处理四个参数的函数（处理case_[zero⇒_|suc_⇒_]）。它与之前定义的 cong 和 cong₂ 完全类似：

cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E)
  {s w : A} {t x : B} {u y : C} {v z : D}
  → s ≡ w → t ≡ x → u ≡ y → v ≡ z → f s t u v ≡ f w x y z
cong₄ f refl refl refl refl = refl

现在证明归约是确定的十分简单。

det : ∀ {M M′ M″}
  → (M —→ M′)
  → (M —→ M″)
    --------
  → M′ ≡ M″
det (ξ-·₁ L—→L′)   (ξ-·₁ L—→L″)     =  cong₂ _·_ (det L—→L′ L—→L″) refl
det (ξ-·₁ L—→L′)   (ξ-·₂ VL M—→M″)  =  contradiction L—→L′ (V¬—→ VL)
det (ξ-·₁ L—→L′)   (β-ƛ _)          =  contradiction L—→L′ (V¬—→ V-ƛ)
det (ξ-·₂ VL _)    (ξ-·₁ L—→L″)     =  contradiction L—→L″ (V¬—→ VL)
det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″)   =  cong₂ _·_ refl (det M—→M′ M—→M″)
det (ξ-·₂ _ M—→M′) (β-ƛ VM)         =  contradiction M—→M′ (V¬—→ VM)
det (β-ƛ _)        (ξ-·₁ L—→L″)     =  contradiction L—→L″ (V¬—→ V-ƛ)
det (β-ƛ VM)       (ξ-·₂ _ M—→M″)   =  contradiction M—→M″ (V¬—→ VM)
det (β-ƛ _)        (β-ƛ _)          =  refl
det (ξ-suc M—→M′)  (ξ-suc M—→M″)    =  cong `suc_ (det M—→M′ M—→M″)
det (ξ-case L—→L′) (ξ-case L—→L″)   =  cong₄ case_[zero⇒_|suc_⇒_]
                                         (det L—→L′ L—→L″) refl refl refl
det (ξ-case L—→L′) β-zero           =  contradiction L—→L′ (V¬—→ V-zero)
det (ξ-case L—→L′) (β-suc VL)       =  contradiction L—→L′ (V¬—→ (V-suc VL))
det β-zero         (ξ-case M—→M″)   =  contradiction M—→M″ (V¬—→ V-zero)
det β-zero         β-zero           =  refl
det (β-suc VL)     (ξ-case L—→L″)   =  contradiction L—→L″ (V¬—→ (V-suc VL))
det (β-suc _)      (β-suc _)        =  refl
det β-μ            β-μ              =  refl

证明通过对可能的归约进行归纳来完成。我们考虑三种典型的情况：

两个关于 ξ-·₁ 的实例：

L —→ L′                 L —→ L″
--------------- ξ-·₁    --------------- ξ-·₁
L · M —→ L′ · M         L · M —→ L″ · M

根据归纳我们有 L′ ≡ L″，因此根据合同性有 L′ · M ≡ L″ · M。

一个关于 ξ-·₁ 的实例和一个关于 ξ-·₂ 的实例：
```
                        Value L
L —→ L′                 M —→ M″
--------------- ξ-·₁    --------------- ξ-·₂
L · M —→ L′ · M         L · M —→ L · M″
```
左侧的规则要求 L 被归约，但右侧的规则要求 L 是一个值。这是一个矛盾，因为值无法被归约。如果值的约束从 ξ-·₂ 或任何其他归约规则中被移除，那么确定性将不再适用。

两个关于 β-ƛ 的实例：

Value V                              Value V
----------------------------- β-ƛ    ----------------------------- β-ƛ
(ƛ x ⇒ N) · V —→ N [ x := V ]        (ƛ x ⇒ N) · V —→ N [ x := V ]

因为左侧是相同的，所以右侧也是相同的。形式证明只是对 refl 的调用。

上述证明中的 18 行中有 5 行是多余的，例如，当一个规则是 ξ-·₁ 而另一个是 ξ-·₂ 的情况被考虑两次，一次是先有 ξ-·₁，然后有 ξ-·₂，另一次将两者互换。我们可能想做的是删除多余的行并在证明的底部添加

det M—→M′ M—→M″ = sym (det M—→M″ M—→M′)

但这不起作用：停机检查器报错，因为参数只是被交换了顺序，而且没有任何一个变得更小。

小测验

假设我们加入了一个新项 zap 以及以下归约规则

-------- β-zap
M —→ zap

和以下赋型规则：

----------- ⊢zap
Γ ⊢ zap ⦂ A

在这些规则存在的情况下，以下哪些属性仍然成立？对于每个属性，写下「仍为真」或「变为假」。如果一个属性变为假，请举出一个反例：

确定性
可进性
保型性

小测验

假设我们加入了一个新项 foo 以及以下归约规则：

------------------ β-foo₁
(λ x ⇒ ` x) —→ foo

----------- β-foo₂
foo —→ zero

在此规则存在的情况下，以下哪些属性仍然成立？对于每个属性，写下「仍为真」或「变为假」。如果一个属性变为假，请举出一个反例：

确定性
可进性
保型性

小测验

假设我们从步进关系中移除了规则 ξ·₁。在此规则不存在的情况下，以下哪些属性仍然成立？对于每个属性，写下「仍为真」或「变为假」。如果一个属性变为假，请举出一个反例：

确定性
可进性
保型性

小测验

我们可以通过按照字典序写出所有类型为 `ℕ ⇒ `ℕ 的程序来遍历所有从自然数到自然数的可计算函数。将这个列表中的第 i 个函数写作 fᵢ。

假设我们添加了一个赋性规则，应用上述遍历来将一个自然数解释为一个从自然数到自然数的函数：

Γ ⊢ L ⦂ `ℕ
Γ ⊢ M ⦂ `ℕ
-------------- _·ℕ_
Γ ⊢ L · M ⦂ `ℕ

并且我们添加了相应的归约规则：

fᵢ(m) —→ n
---------- δ
i · m —→ n

在此规则存在的情况下，以下哪些属性仍然成立？对于每个属性，写下「仍为真」或「变为假」。如果一个属性变为假，请举出一个反例：

确定性
可进性
保型性

在这种情况下是否保留了所有属性？我们是否希望对系统进行任何其他更改？

Unicode

本章使用了下列 Unicode：

ƛ  U+019B  LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-)
Δ  U+0394  GREEK CAPITAL LETTER DELTA (\GD or \Delta)
β  U+03B2  GREEK SMALL LETTER BETA (\Gb or \beta)
δ  U+03B4  GREEK SMALL LETTER DELTA (\Gd or \delta)
μ  U+03BC  GREEK SMALL LETTER MU (\Gm or \mu)
ξ  U+03BE  GREEK SMALL LETTER XI (\Gx or \xi)
ρ  U+03B4  GREEK SMALL LETTER RHO (\Gr or \rho)
ᵢ  U+1D62  LATIN SUBSCRIPT SMALL LETTER I (\_i)
ᶜ  U+1D9C  MODIFIER LETTER SMALL C (\^c)
–  U+2013  EM DASH (\em)
₄  U+2084  SUBSCRIPT FOUR (\_4)
↠  U+21A0  RIGHTWARDS TWO HEADED ARROW (\rr-)
⇒  U+21D2  RIGHTWARDS DOUBLE ARROW (\=>)
∅  U+2205  EMPTY SET (\0)
∋  U+220B  CONTAINS AS MEMBER (\ni)
≟  U+225F  QUESTIONED EQUAL TO (\?=)
⊢  U+22A2  RIGHT TACK (\vdash or \|-)
⦂  U+2982  Z NOTATION TYPE COLON (\:)

导入

简介

值无法被归约

练习 Canonical-≃ （实践）

可进性

练习 Progress-≃（实践）

练习 progress′（实践）

练习 value?（实践）