From 33cee64f09d72b95e0c60c412e5047d5ca695e48 Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Sun, 3 Mar 2024 04:11:33 +0800 Subject: [PATCH] =?UTF-8?q?=E7=BB=9F=E4=B8=80=E6=9C=AF=E8=AF=AD?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 可决定 -> 可判定（Decidable） 采用可计算性理论的通用译法 上下文 -> 语境（Context） 我们在讨论语言，有语法、语义，当然也可以有语境。 --- README.md | 4 +- src/plfa/part1/Relations.lagda.md | 4 +- src/plfa/part2/Bisimulation.lagda.md | 4 +- src/plfa/part2/DeBruijn.lagda.md | 90 ++++++++++++++-------------- src/plfa/part2/Inference.lagda.md | 52 ++++++++-------- src/plfa/part2/Lambda.lagda.md | 36 +++++------ src/plfa/part2/More.lagda.md | 4 +- src/plfa/part2/Properties.lagda.md | 74 +++++++++++------------ src/plfa/part2/Untyped.lagda.md | 12 ++-- 9 files changed, 140 insertions(+), 140 deletions(-) diff --git a/README.md b/README.md index 91df1ce59..882c068d1 100644 --- a/README.md +++ b/README.md @@ -435,8 +435,8 @@ Agda 的编辑是通过使用「[洞][agda-readthedocs-holes]」来交互的， - `C-c C-空格`：填洞 - `C-c C-r`：用构造子精化（**r**efine） - `C-c C-a`：自动填洞（**a**utomatic） -- `C-c C-,`：目标类型和上下文 -- `C-c C-.`：目标类型，上下文，以及推断的类型 +- `C-c C-,`：目标类型和语境 +- `C-c C-.`：目标类型，语境，以及推断的类型 -我们用 `_` 来让 Agda 从上下文中推导**显式参数**的值。只有 `m` +我们用 `_` 来让 Agda 从语境中推导**显式参数**的值。只有 `m` 这一个值能够给出正确的证明，因此 Agda 愉快地填入了它。 如果 Agda 推导值失败，那么它会报一个错误。 @@ -293,7 +293,7 @@ either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`. ## Decidability --> -## 可决定性 +## 可判定性 此证明的结构与重命名的结构相似： -使用递归来重新构造每一个项，并在需要时扩充上下文（在这里，我们只需要在 λ 抽象的抽象体中使用）。 +使用递归来重新构造每一个项，并在需要时扩充语境（在这里，我们只需要在 λ 抽象的抽象体中使用）。 与之前一样，这个证明的结构于替换的结构类似：使用递归重新构造每一个项， -并在需要时扩充上下文（在这里，我们只需要在 λ 抽象的抽象体中使用）。 +并在需要时扩充语境（在这里，我们只需要在 λ 抽象的抽象体中使用）。 注意到，查询判断 `∋m` 和 `∋m′` 表示了两个名称同为 `"m"` 变量的不同约束。 -作为对比， 判断 `∋n` 和 `∋n′` 都表示变量 `"n"` 的约束，但是其上下文不同， -前者中 `"n"` 是上下文中最后一个约束，后者中则是在匹配表达式后继分支中 `"m"` 约束之后。 +作为对比， 判断 `∋n` 和 `∋n′` 都表示变量 `"n"` 的约束，但是其语境不同， +前者中 `"n"` 是语境中最后一个约束，后者中则是在匹配表达式后继分支中 `"m"` 约束之后。 -由于项是内在类型的，我们必须在定义项之前先定义类型和上下文。 +由于项是内在类型的，我们必须在定义项之前先定义类型和语境。 -上下文如同之前一样，但是我们舍去了名字。 -上下文如下形式化： +语境如同之前一样，但是我们舍去了名字。 +语境如下形式化： ```agda data Context : Set where @@ -467,9 +467,9 @@ context, and `Γ , A` for the context `Γ` extended by type `A`. For example --> -上下文就是一个类型的列表，其最近约束的变量出现在右边。 -如之前一样，我们使用 `Γ` 和 `Δ` 来表示上下文。 -我们用 `∅` 表示空上下文，用 `Γ , A` 表示以 `A` 扩充的上下文 `Γ`。 +语境就是一个类型的列表，其最近约束的变量出现在右边。 +如之前一样，我们使用 `Γ` 和 `Δ` 来表示语境。 +我们用 `∅` 表示空语境，用 `Γ , A` 表示以 `A` 扩充的语境 `Γ`。 例如： ```agda @@ -510,8 +510,8 @@ It looks exactly like the old lookup judgment, but with all variable names dropped: --> -表示上下文 `Γ` 中带有类型 `A` 的变量。 -查询判断由一个以上下文和类型索引的数据类型来形式化。 +表示语境 `Γ` 中带有类型 `A` 的变量。 +查询判断由一个以语境和类型索引的数据类型来形式化。 它和之前的查询判断看上去一样，但是变量名被舍去了： ```agda @@ -571,7 +571,7 @@ and `"s"` by `S Z` (as the next most recently bound variable). --> -在给出的上下文中，`"z"` 由 `Z` 表示（最近约束的变量）， +在给出的语境中，`"z"` 由 `Z` 表示（最近约束的变量）， `"s"` 由 `S Z` 表示（下一个最近约束的变量）。 -表示在上下文 `Γ` 中类型为 `A` 的项。 -这个判断用由上下文和类型索引的数据类型进行形式化。 +表示在语境 `Γ` 中类型为 `A` 的项。 +这个判断用由语境和类型索引的数据类型进行形式化。 它和之前的查询判断看上去一样，但是变量名被舍去了： ```agda @@ -707,7 +707,7 @@ We define a helper function that computes the length of a context, which will be useful in making sure an index is within context bounds: --> -我们定义一个辅助函数来计算上下文的长度，它会在之后确保一个因子在上下文约束中有帮助： +我们定义一个辅助函数来计算语境的长度，它会在之后确保一个因子在语境约束中有帮助： ```agda length : Context → ℕ @@ -719,7 +719,7 @@ length (Γ , _) = suc (length Γ) We can use a natural number to select a type from a context: --> -我们可以用一个自然数来从上下文中选择一个类型： +我们可以用一个自然数来从语境中选择一个类型： ```agda lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type @@ -732,14 +732,14 @@ We intend to apply the function only when the natural is shorter than the length of the context, which is witnessed by `p`. --> -我们希望只在自然数小于上下文长度的时候应用这个函数，由 `p` 来印证。 +我们希望只在自然数小于语境长度的时候应用这个函数，由 `p` 来印证。 -结合上述，我们可以将一个自然数转换成其对应的 de Bruijn 因子，从上下文中查询它的类型： +结合上述，我们可以将一个自然数转换成其对应的 de Bruijn 因子，从语境中查询它的类型： ```agda count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p @@ -773,13 +773,13 @@ against invoking `#_` on an `n` that is out of context bounds. Finally, in the return type `n∈Γ` is converted to a witness that `n` is within the bounds. --> -函数 `#_` 取一个隐式参数 `n∈Γ` 来证明 `n` 在上下文的约束内。 +函数 `#_` 取一个隐式参数 `n∈Γ` 来证明 `n` 在语境的约束内。 回忆 [`True`](/Decidable/#proof-by-reflection)、 [`_≤?_`](/Decidable/#the-best-of-both-worlds) 和 [`toWitness`](/Decidable/#decidables-from-booleans-and-booleans-from-decidables) 在 [Decidable](/Decidable/) 章节中定义。 -`n∈Γ` 的类型保证了 `#_` 不会在 `n` 超出上下文约束时被应用。 -最后，在返回类型中，`n∈Γ` 被转换为 `n` 在上下文约束内的证明。 +`n∈Γ` 的类型保证了 `#_` 不会在 `n` 超出语境约束时被应用。 +最后，在返回类型中，`n∈Γ` 被转换为 `n` 在语境约束内的证明。 -我们推广到任意上下文，因为我们在稍后给出 `two` 在内部约束时出现的例子。 +我们推广到任意语境，因为我们在稍后给出 `two` 在内部约束时出现的例子。 -如同之前那样，我们推广到任意上下文。 +如同之前那样，我们推广到任意语境。 同时，我们将 `twoᶜ` 和 `plusᶜ` 推广至任意类型的 Church 法表示的自然数。 @@ -896,7 +896,7 @@ chapter, but here the theorem that ensures renaming preserves typing also acts as code that performs renaming. --> -重命名是替换之前重要的一步，让我们可以将一个项从一个上下文中 「转移」 至另一个上下文。 +重命名是替换之前重要的一步，让我们可以将一个项从一个语境中 「转移」 至另一个语境。 它直接对应了上一章中的关于重命名的结论，但此处重命名保留类型的定理同时是进行重命名的代码。 -和之前一样，我们首先需要一条扩充引理，使我们可以到遇到约束时扩充我们的上下文。 -给定一个将一个上下文中的变量映射至另一个上下文中变量的映射，扩充会生成一个 -从扩充后的第一个上下文至以相同方法扩充的第二个上下文的映射。 +和之前一样，我们首先需要一条扩充引理，使我们可以到遇到约束时扩充我们的语境。 +给定一个将一个语境中的变量映射至另一个语境中变量的映射，扩充会生成一个 +从扩充后的第一个语境至以相同方法扩充的第二个语境的映射。 它看上去和之前的扩充引理完全一样，只是舍去了名字和项： ```agda @@ -953,8 +953,8 @@ terms in the second: --> 定义了扩充过后，重命名的定义就变得很直接了。 -如果一个上下文中的变量映射至另一个上下文中的变量，那么第一个上下文 -中的项映射至第二个上下文中： +如果一个语境中的变量映射至另一个语境中的变量，那么第一个语境 +中的项映射至第二个语境中： ```agda rename : ∀ {Γ Δ} @@ -1014,7 +1014,7 @@ terms that are well typed by the rules of simply-typed lambda calculus. --> -之前，重命名是一个将项在一个上下文中良类型的证明转换成项在另一个上下文中 +之前，重命名是一个将项在一个语境中良类型的证明转换成项在另一个语境中 良类型的结论；而现在，它直接转换了整个项，调整了其中的约束变了。 在 Agda 中类型检查这段代码保证了只有在简单类型的 λ-演算中良类型的项 可以作为参数或者作为返回项。 @@ -1087,7 +1087,7 @@ an arbitrary context, and need not be closed. 由于 de Bruijn 因子让我们免去了重命名的顾虑，给出一个更广义的替换的定义更加方便。 与其用一个闭项来替换一个单一的变量，广义的替换提供一个将原来项中各个自由变量至另一个项的映射。 -除此之外，被替换的项可以在任意上下文之中，不需要为闭项。 +除此之外，被替换的项可以在任意语境之中，不需要为闭项。 定义和证明的结构与重命名项类似。 -同样，我们首先需要一个扩充引理，让我们能够在遇到约束时扩充上下文。 -对比在重命名中我们使用从一个上下文中的变量至另一上下文中变量的映射， -替换使用的是将一个上下文中的变量至另一上下文中**项**的映射。 -给定一个将一个上下文中的变量映射至另一个上下文中项的映射，扩充会生成一个 -从扩充后的第一个上下文至以相同方法扩充的第二个上下文的映射。 +同样，我们首先需要一个扩充引理，让我们能够在遇到约束时扩充语境。 +对比在重命名中我们使用从一个语境中的变量至另一语境中变量的映射， +替换使用的是将一个语境中的变量至另一语境中**项**的映射。 +给定一个将一个语境中的变量映射至另一个语境中项的映射，扩充会生成一个 +从扩充后的第一个语境至以相同方法扩充的第二个语境的映射。 ```agda exts : ∀ {Γ Δ} @@ -1149,7 +1149,7 @@ to a term over the extended context `Δ , B`. --> 这也是为什么我们需要先定义重命名，因为我们需要这个定义来将 -上下文 `Δ` 中的项重命名至扩充后的上下文 `Δ , B`。 +语境 `Δ` 中的项重命名至扩充后的语境 `Δ , B`。 定义了扩充过后，替换的定义就变得很直接了。 -如果一个上下文中的变量映射至另一个上下文中的项，那么第一个上下文 -中的项映射至第二个上下文中： +如果一个语境中的变量映射至另一个语境中的项，那么第一个语境 +中的项映射至第二个语境中： ```agda subst : ∀ {Γ Δ} @@ -1245,10 +1245,10 @@ To do so, we use a map from the context `Γ , B` to the context type `B` and every other free variable to itself. --> -在一个上下文 `Γ , B` 中类型为 `A` 的项，我们将类型为 `B` 的变量 -替换为上下文 `Γ` 中一个类型为 `B` 的项。 -为了这么做，我们用一个从 `Γ , B` 上下文至 `Γ` 上下文的映射， -令上下文中最后一个变量映射至类型为 `B` 的替换项，令任何其他自由变量映射至其本身。 +在一个语境 `Γ , B` 中类型为 `A` 的项，我们将类型为 `B` 的变量 +替换为语境 `Γ` 中一个类型为 `B` 的项。 +为了这么做，我们用一个从 `Γ , B` 语境至 `Γ` 语境的映射， +令语境中最后一个变量映射至类型为 `B` 的替换项，令任何其他自由变量映射至其本身。 定义中指出，`M —→ N` 只能由类型**都**是 `Γ ⊢ A` 的两个项 `M` 和 `N` 组成， -其中 `Γ` 是一个上下文，`A` 是一个类型。 +其中 `Γ` 是一个语境，`A` 是一个类型。 换句话说，我们的定义中**内置**了规约保存类型的证明。 我们不需要额外证明保型性。 Agda 的类型检查器检验了每个项保存了类型。 @@ -1537,7 +1537,7 @@ _ = As before, we need to supply an explicit context to `` `zero ``. --> -和之前一样，我们需要给出为 `` `zero `` 给出显式的上下文。 +和之前一样，我们需要给出为 `` `zero `` 给出显式的语境。 -我们将上下文 `Γ` 和变量 `x` 作为输入，类型 `A` 作为输出。 +我们将语境 `Γ` 和变量 `x` 作为输入，类型 `A` 作为输出。 考虑下面的规则： ----------------- Z @@ -133,9 +133,9 @@ of the hypothesis determines the output of the conclusion. --> 从输入中，我们可以决定应用哪一条规则： -如果上下文中最后一个变量与给定的变量一致，那么应用第一条规则，否则应用第二条。 +如果语境中最后一个变量与给定的变量一致，那么应用第一条规则，否则应用第二条。 （对于 de Bruijn 因子来说，这更加简单：零对应第一条，后继对应第二条。） -对于第一条，输出类型可以直接从上下文中得到。 +对于第一条，输出类型可以直接从语境中得到。 对于第二条，结论中的输入可以作为假设的输入，而假设的输出决定了结论的输出。 -我们将上下文 `Γ` 和项 `M` 作为输入，类型 `A` 作为输出。 +我们将语境 `Γ` 和项 `M` 作为输入，类型 `A` 作为输出。 考虑下面的规则： Γ ∋ x ⦂ A @@ -190,10 +190,10 @@ determines the output of the conclusion. 变量使用第一条，抽象使用第二条，应用使用第三条。 我们把这样的规则叫做**语法导向的**（Syntax directed）规则。 对于变量的规则，结论的输入决定了结论的输出。 -抽象的规则也是一样——约束变量和参数从结论的输入流向假设中的上下文； +抽象的规则也是一样——约束变量和参数从结论的输入流向假设中的语境； 这得以实现，因为我们在抽象中加入了参数的类型。 对于应用的规则，我们加入第三条假设来检查函数类型中的作用域是否与参数的类型一致； -这条判断是在两个类型已知时是可决定的。 +这条判断是在两个类型已知时是可判定的。 结论的输入决定了前两个假设的输入，而前两个假设的输出决定了第三个假设的输入，而第一个假设的输出决定了结论的输出。 第一类判断**生成**（Synthesise）项的类型，如上，而第二类**继承**（Inherit）类型。 -在第一类中，上下文和项作为输入，类型作为输出； -而在第二类中，上下文、项和类型三者都作为输入。 +在第一类中，语境和项作为输入，类型作为输出； +而在第二类中，语境、项和类型三者都作为输入。 -我们试图证明赋型判断是**可决定**的： +我们试图证明赋型判断是**可判定**的： synthesize : ∀ (Γ : Context) (M : Term⁺) ------------------------------------ @@ -402,9 +402,9 @@ Similarly, given context `Γ`, inherited term `M`, and type `A`, we must decide whether `Γ ⊢ M ↓ A` holds, or its negation. --> -给定上下文 `Γ` 和生成项 `M`，我们必须判定是否存在一个类型 `A` 使得 `Γ ⊢ M ↑ A` 成立， +给定语境 `Γ` 和生成项 `M`，我们必须判定是否存在一个类型 `A` 使得 `Γ ⊢ M ↑ A` 成立， 或者其否定。 -同样，给定上下文 `Γ` 、继承项 `M` 和类型 `A`，我们必须判定 `Γ ⊢ M ↓ A` 成立，或者其否定。 +同样，给定语境 `Γ` 、继承项 `M` 和类型 `A`，我们必须判定 `Γ ⊢ M ↓ A` 成立，或者其否定。 -标识符、类型和上下文与之前一样： +标识符、类型和语境与之前一样： ```agda Id : Set @@ -897,7 +897,7 @@ one showing `Γ ∋ x ⦂ A` and one showing `Γ ∋ x ⦂ B`, it follows that `A` and `B` must be identical: --> -从上下文查询一个类型是唯一的。 +从语境查询一个类型是唯一的。 给定两个推导，其一证明 `Γ ∋ x ⦂ A`，另一个证明 `Γ ∋ x ⦂ B`，那么 `A` 和 `B` 一定是一样的： @@ -923,7 +923,7 @@ it is not. 如果两个推导都使用 `Z` 规则，那么唯一性即可直接得出； 如果两个推导都使用 `S` 规则，那么唯一性可以由归纳得出。 如果一个使用了 `Z` 规则，另一个使用了 `S` 规则，这则是一个矛盾， -因为 `Z` 要求我们查询的变量是上下文中的最后一个，而 `S` 要求不是这样。 +因为 `Z` 要求我们查询的变量是语境中的最后一个，而 `S` 要求不是这样。 -## 查询上下文中变量的类型 +## 查询语境中变量的类型 -给定上下文 `Γ` 和变量 `x`，我们可判断是否存在一个类型 `A` 使得 +给定语境 `Γ` 和变量 `x`，我们可判断是否存在一个类型 `A` 使得 `Γ ∋ x ⦂ A` 成立，或者其反命题： ```agda @@ -1019,20 +1019,20 @@ lookup (Γ , y ⦂ B) x with x ≟ y Consider the context: --> -考虑上下文的情况： +考虑语境的情况： -* 如果上下文为空，那么平凡地，我们没有任何可能的推导。 +* 如果语境为空，那么平凡地，我们没有任何可能的推导。 -* 如果上下文非空，比较给定的变量和最新的绑定： +* 如果语境非空，比较给定的变量和最新的绑定： - - 如果查询失败了，我们使用 `ext∋` 将变量不存在于内部的上下文中的证明扩充至扩充后的上下文。 + - 如果查询失败了，我们使用 `ext∋` 将变量不存在于内部的语境中的证明扩充至扩充后的语境。 -* 如果项是 `ƛ x ⇒ N`，而继承的类型是 `A ⇒ B`，我们用上下文 `Γ , x ⦂ A` 递归至 +* 如果项是 `ƛ x ⇒ N`，而继承的类型是 `A ⇒ B`，我们用语境 `Γ , x ⦂ A` 递归至 子项 `N` 继承类型 `B`： -首先，我们复制之前介绍过的智能构造子 `S′`，使得访问上下文中的变量更加便利： +首先，我们复制之前介绍过的智能构造子 `S′`，使得访问语境中的变量更加便利： ``` S′ : ∀ {Γ x y A B} @@ -1775,7 +1775,7 @@ It simply renames to the corresponding constructors in module `DB`. Next, we give the code to erase a context: --> -接下来，我们给出擦除上下文的代码： +接下来，我们给出擦除语境的代码： ```agda ∥_∥Cx : Context → DB.Context diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index bc84d7ea8..465a14c31 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -81,7 +81,7 @@ four. 这一章启发自《软件基础》（_Software Foundations_）/《程序语言基础》（_Programming Language Foundations_）中对应的 _Stlc_ 的内容。 -我们的不同之处在于使用显式的方法来表示上下文（由标识符和类型的序对组成的列表）， +我们的不同之处在于使用显式的方法来表示语境（由标识符和类型的序对组成的列表）， 而不是部分映射（从标识符到类型的部分函数）。 这样的做法与后续的 de Bruijn 索引表示方法能更好的对应。 我们使用自然数作为基础类型，而不是布尔值，这样我们可以表示更复杂的例子。 @@ -482,7 +482,7 @@ meta-language, Agda. 相似地来说，非正式的表达通常在**对象语言（Object Language）**（我们正在描述的语言） 和**元语言（Meta-Language）**（我们用来描述对象语言的语言） -中使用相同的记法来表示函数类型、λ-抽象和函数应用，相信读者可以通过上下文区分两种语言。 +中使用相同的记法来表示函数类型、λ-抽象和函数应用，相信读者可以通过语境区分两种语言。 而 Agda 并不能做到这样，因此我们在对象语言中使用 `ƛ x ⇒ N` 和 `L · M` ， 与我们使用的元语言 Agda 中的 `λ x → N` 和 `L M` 相对。 @@ -1706,7 +1706,7 @@ Thus: ### Contexts --> -### 上下文 +### 语境 -上下文（Context）将变量和类型联系在一起。 -我们用 `Γ` 和 `Δ` 来表示上下文。 -我们用 `∅` 表示空的上下文，用 `Γ , x ⦂ A` 表示扩充 `Γ` ，将变量 `x` 对应至类型 `A`。 +语境（Context）将变量和类型联系在一起。 +我们用 `Γ` 和 `Δ` 来表示语境。 +我们用 `∅` 表示空的语境，用 `Γ , x ⦂ A` 表示扩充 `Γ` ，将变量 `x` 对应至类型 `A`。 例如： * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ `` @@ -1738,14 +1738,14 @@ is the context that associates variable `` "s" `` with type `` `ℕ ⇒ `ℕ ``, and variable `` "z" `` with type `` `ℕ ``. --> -这个上下文将变量 `` "s" `` 对应至类型 `` `ℕ ⇒ `ℕ ``， +这个语境将变量 `` "s" `` 对应至类型 `` `ℕ ⇒ `ℕ ``， 将变量 `` "z" `` 对应至类型 `` `ℕ ``。 -上下文如下形式化： +语境如下形式化： ```agda infixl 5 _,_⦂_ @@ -1773,7 +1773,7 @@ For instance, the isomorphism relates the context For instance, the isomorphism relates the context --> -例如，如下的上下文 +例如，如下的语境 ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ @@ -1811,7 +1811,7 @@ It is called _lookup_. For example, --> -表示在上下文 `Γ` 中变量 `x` 的类型是 `A`。这样的判断叫做**查询（Lookup）**判断。 +表示在语境 `Γ` 中变量 `x` 的类型是 `A`。这样的判断叫做**查询（Lookup）**判断。 例如， * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "z" ⦂ `ℕ `` @@ -1834,7 +1834,7 @@ should return the most recently bound variable, which _shadows_ the other variables. For example, --> -如果上下文中有相同名称的两个变量，那么查询会返回被约束的最近的变量，它**遮盖（Shadow）** +如果语境中有相同名称的两个变量，那么查询会返回被约束的最近的变量，它**遮盖（Shadow）** 了另一个变量。例如： * `` ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ∋ "x" ⦂ `ℕ ``. @@ -1925,8 +1925,8 @@ Context `Γ` provides types for all the free variables in `M`. For example: --> -表示在上下文 `Γ` 中，项 `M` 有类型 `A`。 -上下文 `Γ` 为 `M` 中的所有自由变量提供了类型。 +表示在语境 `Γ` 中，项 `M` 有类型 `A`。 +语境 `Γ` 为 `M` 中的所有自由变量提供了类型。 例如： * `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ `` @@ -2027,7 +2027,7 @@ the three places where a bound variable is introduced. --> -另外需要注意的是有三处地方（`⊢ƛ`、`⊢case` 和 `⊢μ`），上下文被 `x` 和相应的类型 +另外需要注意的是有三处地方（`⊢ƛ`、`⊢case` 和 `⊢μ`），语境被 `x` 和相应的类型 所扩充，对应着三处约束变量的引入。 -与之前的例子不同，我们以任意上下文，而不是空上下文来赋型。 -这让我们能够在其他除了顶层之外的上下文中使用这个推导。 +与之前的例子不同，我们以任意语境，而不是空语境来赋型。 +这让我们能够在其他除了顶层之外的语境中使用这个推导。 这里的查询判断 `∋m` 和 `∋m′` 指代两个变量 `"m"` 的绑定。 -作为对比，查询判断 `∋n` 和 `∋n′` 指代同一个变量 `"n"` 的绑定，但是查询的上下文不同， -第一次 `"n"` 出现在在上下文的最后，第二次在 `"m"` 之后。 +作为对比，查询判断 `∋n` 和 `∋n′` 指代同一个变量 `"n"` 的绑定，但是查询的语境不同， +第一次 `"n"` 出现在在语境的最后，第二次在 `"m"` 之后。 -### 上下文 +### 语境 ```agda data Context : Set where @@ -2126,7 +2126,7 @@ its context adjusted via renaming in order for the right-hand side to be well typed. --> -注意到我们需要交换参数，而且 `W` 的上下文需要用重命名来调整，使得右手边的项保持良类型。 +注意到我们需要交换参数，而且 `W` 的语境需要用重命名来调整，使得右手边的项保持良类型。 -如果一个项在空上下文中是良类型的，那么它满足可进性： +如果一个项在空语境中是良类型的，那么它满足可进性： ```agda progress : ∀ {M A} @@ -402,7 +402,7 @@ Let's unpack the first three cases: * If the term is a lambda abstraction then it is a value. --> -* 这个项不可能是变量，因为没有变量在空上下文中是良类型的。 +* 这个项不可能是变量，因为没有变量在空语境中是良类型的。 * 如果这个项是一个 λ-抽象，可知它是一个值。 @@ -593,8 +593,8 @@ if any term is typeable under `Γ`, it has the same type under `Δ`. --> **重命名**： -考虑两个上下文 `Γ` 和 `Δ`，满足 `Γ` 中出现的每个变量同时 -也在 `Δ` 中出现且具有相同的类型。那么如果一个项在上下文 `Γ` 中 +考虑两个语境 `Γ` 和 `Δ`，满足 `Γ` 中出现的每个变量同时 +也在 `Δ` 中出现且具有相同的类型。那么如果一个项在语境 `Γ` 中 是可赋型的，它在 `Δ` 中也具有同样的类型。 接下来是三个重要的结论。 -**弱化（Weaken）**引理断言说如果一个项在空上下文中是良类型的，那么它在任意上下文中都是良类型的。 -**去除（Drop）**引理断言说如果一个项在给定上下文中是良类型的，且此上下文中同一个变量出现了两次， -此时去除上下文中被遮盖的变量，这个项仍然是良类型的。 -**交换（Swap）**引理断言说如果一个项在给定上下文中是良类型的，那么在通过交换上下文中两个变量后得到的 -上下文中，这个项仍然是良类型的。 +**弱化（Weaken）**引理断言说如果一个项在空语境中是良类型的，那么它在任意语境中都是良类型的。 +**去除（Drop）**引理断言说如果一个项在给定语境中是良类型的，且此语境中同一个变量出现了两次， +此时去除语境中被遮盖的变量，这个项仍然是良类型的。 +**交换（Swap）**引理断言说如果一个项在给定语境中是良类型的，那么在通过交换语境中两个变量后得到的 +语境中，这个项仍然是良类型的。 -赋型的三条规则（λ-抽象、对自然数分项与不动点）都有假设来拓展上下文以 -包含一个约束变量。三条规则的每一条中都有上下文 `Γ` 都出现在结论中，同时 -拓展后的上下文 `Γ , x ⦂ A` 出现在假设中。对于 λ-表达式，也就是： +赋型的三条规则（λ-抽象、对自然数分项与不动点）都有假设来拓展语境以 +包含一个约束变量。三条规则的每一条中都有语境 `Γ` 都出现在结论中，同时 +拓展后的语境 `Γ , x ⦂ A` 出现在假设中。对于 λ-表达式，也就是： Γ , x ⦂ A ⊢ N ⦂ B ------------------- ⊢ƛ @@ -758,7 +758,7 @@ both contexts: --> 对自然数分项和不动点亦是如此。 -要处理这类情况，我们首先证明一条论述 「如果一个上下文和另一个上下文之间存在映射， +要处理这类情况，我们首先证明一条论述 「如果一个语境和另一个语境之间存在映射， 在对两者添加同一个变量后映射仍然存在」 的引理： ```agda @@ -777,9 +777,9 @@ The proof is by case analysis of the evidence that `x` appears in the extended context `Γ , y ⦂ B`: --> -令 `ρ` 为这个映射，它将变量 `x` 出现在上下文 `Γ` 中的论据映射到 -变量 `x` 出现在上下文 `Δ` 中的论据。 -这是由分类讨论变量 `x` 出现在拓展后上下文 `Γ , y ⦂ B` 的论据证明的： +令 `ρ` 为这个映射，它将变量 `x` 出现在语境 `Γ` 中的论据映射到 +变量 `x` 出现在语境 `Δ` 中的论据。 +这是由分类讨论变量 `x` 出现在拓展后语境 `Γ , y ⦂ B` 的论据证明的： -像之前一样，令 `ρ` 为 「变量 `x` 出现在上下文 `Γ` 中的论据」 至 「变量 `x` 出现在 `Δ` 的论据」 的映射。 -我们对项 `M` 在上下文 `Γ` 中是良赋型的论据做归纳。我们首先来分析前三种情况： +像之前一样，令 `ρ` 为 「变量 `x` 出现在语境 `Γ` 中的论据」 至 「变量 `x` 出现在 `Δ` 的论据」 的映射。 +我们对项 `M` 在语境 `Γ` 中是良赋型的论据做归纳。我们首先来分析前三种情况： -* 如果项是一个变量，那么对该变量出现在上下文 `Γ` 的论据应用 `ρ` 就能得到 +* 如果项是一个变量，那么对该变量出现在语境 `Γ` 的论据应用 `ρ` 就能得到 所对应的该变量出现在 `Δ` 的证明。 -由于做归纳的对象是这个项良赋型的推演过程，拓展上下文不会使得归纳假设 +由于做归纳的对象是这个项良赋型的推演过程，拓展语境不会使得归纳假设 无效。等价地，此时的递归会停机，这是由于第二个参数在递归过程中总是变 小一些，尽管第一个参数有时候变大一些。 @@ -886,13 +886,13 @@ We have three important corollaries, each proved by constructing a suitable map between contexts. --> -我们有三条重要推论，每条都是通过构造一个恰当的上下文间映射证明的： +我们有三条重要推论，每条都是通过构造一个恰当的语境间映射证明的： -第一，一个闭项可以被弱化到任意上下文： +第一，一个闭项可以被弱化到任意语境： ```agda weaken : ∀ {Γ M A} @@ -913,14 +913,14 @@ Here the map `ρ` is trivial, since there are no possible arguments in the empty context `∅`. --> -这里的映射 `ρ` 是平凡的，由于在空上下文 `∅` 中不会出现可能的参数。 +这里的映射 `ρ` 是平凡的，由于在空语境 `∅` 中不会出现可能的参数。 -第二，如果上下文中的最后两个变量相等，我们就可以去除掉被遮盖的一个： +第二，如果语境中的最后两个变量相等，我们就可以去除掉被遮盖的一个： ```agda drop : ∀ {Γ x M A B C} @@ -956,7 +956,7 @@ contradiction (evidenced by `x≢x refl`). Third, if the last two variables in a context differ then we can swap them: --> -第三，如果上下文中的最后两个变量不同，我们可以交换它们： +第三，如果语境中的最后两个变量不同，我们可以交换它们： ```agda swap : ∀ {Γ x y M A B C} @@ -982,8 +982,8 @@ moving `x` from a position at the end to a position one from the end with `y` at the end, and requires the provided evidence that `x ≢ y`. --> -在这里重命名将上下文的最后一个变量映射到倒数第二个，反之亦然。 -第一行负责将 `x` 从上下文的最后一个位置移动到倒数第二个，并且 +在这里重命名将语境的最后一个变量映射到倒数第二个，反之亦然。 +第一行负责将 `x` 从语境的最后一个位置移动到倒数第二个，并且 将 `y` 置于最后，这要求提供 `x ≢ y` 的论据。 @@ -1026,8 +1026,8 @@ we require an arbitrary context `Γ`, as in the statement of the lemma. 我们所关注的是规约闭项，这意味着每当我们应用 `β`-规约时， 所替换的项只含有一个自由变量（也就是所对应 λ-抽象、 对自然数分项或不动点表达式的绑定变量）。然而，替换是通过 -递归定义的，在我们逐层深入项时遇到的绑定变量增长了上下文。 -所以为了进行归纳，我们需要一个任意的上下文 `Γ`，正如这条引理 +递归定义的，在我们逐层深入项时遇到的绑定变量增长了语境。 +所以为了进行归纳，我们需要一个任意的语境 `Γ`，正如这条引理 中所陈述的。 -我们对 `N` 在由 `x` 拓展 `Γ` 后得到的上下文中是良赋型的论据做归纳。 +我们对 `N` 在由 `x` 拓展 `Γ` 后得到的语境中是良赋型的论据做归纳。 -## 上下文 +## 语境 -和之前一样，上下文是类型的列表，最新出现的约束变量的类型出现在最右边： +和之前一样，语境是类型的列表，最新出现的约束变量的类型出现在最右边： ```agda data Context : Set where @@ -200,7 +200,7 @@ data Context : Set where We let `Γ` and `Δ` range over contexts. --> -我们使用 `Γ` 和 `Δ` 来指代上下文。 +我们使用 `Γ` 和 `Δ` 来指代语境。 因为 `★` 是唯一的类型，这样的判断并不会给出很多与类型相关的保证。 -但它确实确保了所有的变量在作用域内。例如，我们不能在只有两个约束变量的上下文中使用 `S S Z`。 +但它确实确保了所有的变量在作用域内。例如，我们不能在只有两个约束变量的语境中使用 `S S Z`。 如之前一样，我们可以将自然数转换为对应的 de Bruijn 因子。 -我们不再需要从上下文中查询变量的类型，因为每个变量都有一样的类型： +我们不再需要从语境中查询变量的类型，因为每个变量都有一样的类型： ```agda length : Context → ℕ @@ -1019,7 +1019,7 @@ The definition is as before, save that the empty context `∅` generalises to an arbitrary context `Γ`. --> -定义与之前一样，除了我们将空上下文 `∅` 推广至任意上下文 `Γ`。 +定义与之前一样，除了我们将空语境 `∅` 推广至任意语境 `Γ`。