Merge pull request #177 from Agda-zh/uni-term

统一术语

src/plfa/frontmatter/Preface.md

@@ -126,7 +126,7 @@ foundation of proof is on proud display.
 -->
 
 我发现自己热衷于用 Agda 重构此课程。在 Agda 中，我们不再需要学习策略了：
-这里只有依赖类型编程，简单纯粹。我们总是通过构造子来引入，通过模式匹配来消除。
+这里只有依值类型编程，简单纯粹。我们总是通过构造子来引入，通过模式匹配来消除。
 归纳不再是谜之独立的概念，它与我们熟悉的递归概念直接对应。混缀语法十分灵活，
 但每个概念只需要一个名字，例如代换就是 `_[_:=_]`。标准库虽不完美，但它的一致性却很合理。
 **命题即类型**作为证明的基础则被骄傲地展示了出来。
@@ -140,7 +140,7 @@ types than on the theory of programming languages.
 
 不过，此前还没有用 Agda 语言描述的编程语言理论教材。虽然 Stump 的
 [Verified Functional Programming in Agda][stump] 涵盖了相关的范围，
-但比起编程语言理论，却更多关注于依赖类型编程。
+但比起编程语言理论，却更多关注于依值类型编程。
 
 <!--
 The original goal was to simply adapt *Software Foundations*,

src/plfa/part1/Connectives.lagda.md

@@ -127,8 +127,8 @@ play a similar role.
 -->
 
 当 `⟨_,_⟩` 在等式右手边的项中出现的时候，我们将其称作**构造子（Constructor）**，
-当它出现在等式左边时，我们将其称作**析构器（Destructor）**。我们亦可将 `proj₁` 和 `proj₂`
-称作析构器，因为它们起到相似的效果。
+当它出现在等式左边时，我们将其称作**解构子（Destructor）**。我们亦可将 `proj₁` 和 `proj₂`
+称作解构子，因为它们起到相似的效果。
 
 <!--
 Other terminology refers to `⟨_,_⟩` as _introducing_ a conjunction, and
@@ -157,7 +157,7 @@ In this case, applying each destructor and reassembling the results with the
 constructor is the identity over products:
 -->
 
-在这样的情况下，先使用析构器，再使用构造子将结果重组，得到还是原来的积。
+在这样的情况下，先使用解构子，再使用构造子将结果重组，得到还是原来的积。
 
 ```agda
 η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
@@ -631,15 +631,15 @@ latter the name `⊎-E`.
 -->
 
 当 `inj₁` 和 `inj₂` 在等式右手边出现的时候，我们将其称作**构造子**，
-当它出现在等式左边时，我们将其称作**析构器**。我们亦可将 `case-⊎`
-称作析构器，因为它们起到相似的效果。其他术语将 `inj₁` 和 `inj₂` 称为**引入**析取，
+当它出现在等式左边时，我们将其称作**解构子**。我们亦可将 `case-⊎`
+称作解构子，因为它们起到相似的效果。其他术语将 `inj₁` 和 `inj₂` 称为**引入**析取，
 将 `case-⊎` 称为**消去**析取。前者亦被称为 `⊎-I₁` 和 `⊎-I₂`，后者 `⊎-E`。
 
 <!--
 Applying the destructor to each of the constructors is the identity:
 -->
 
-对每个构造子使用析构器得到的是原来的值：
+对每个构造子使用解构子得到的是原来的值：
 
 ```agda
 η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w

src/plfa/part1/Quantifiers.lagda.md

@@ -765,8 +765,8 @@ result is analogous to the one which tells us that negation
 of a disjunction is isomorphic to a conjunction of negations:
 -->
 
-存在量化的否定与否定的全称量化是同构的。考虑到存在量化是析构的推广，全称量化是合构的推广，
-这样的结果与析构的否定与否定的合构是同构的结果相似。
+存在量化的否定与否定的全称量化是同构的。考虑到存在量化是解构的推广，全称量化是合构的推广，
+这样的结果与解构的否定与否定的合构是同构的结果相似。
 
 ```agda
 ¬∃≃∀¬ : ∀ {A : Set} {B : A → Set}

src/plfa/part2/Bisimulation.lagda.md

@@ -613,7 +613,7 @@ In its structure, it looks a little bit like a proof of progress:
 
 这个证明由分情况讨论来完成，检查每一个 `M ~ M†` 的例子，和每一个 `M —→ M†` 的例子，
 并在规约是 `ξ` 规则时使用递归，也因此包括了另一个规约。
-证明的结构和进行性的证明也有些类似：
+证明的结构和可进性的证明也有些类似：
 
 <!--
 * If the related terms are variables, no reduction applies.

src/plfa/part2/DeBruijn.lagda.md

@@ -1395,7 +1395,7 @@ combined with a destructor, labelled with `β`:
 
 规约规则和之前给出的类似，除去我们必须给出每个项的类型。
 如同之前，兼容性规则规约一个项的一部分，用 `ξ` 标出；
-简化构造子与其析构子的规则用 `β` 标出：
+简化构造子与其解构子的规则用 `β` 标出：
 
 ```agda
 infix 2 _—→_
@@ -1658,7 +1658,7 @@ values.
 ## Progress
 -->
 
-## 进行性
+## 可进性
 
 <!--
 As before, every term that is well typed and closed is either
@@ -1667,7 +1667,7 @@ is just as before, but annotated with types:
 -->
 
 和之前一样，每一个良类型的闭项要么是一个值，要么可以进行规约。
-进行性的形式化与之前一样，但是附上了类型：
+可进性的形式化与之前一样，但是附上了类型：
 
 ```agda
 data Progress {A} (M : ∅ ⊢ A) : Set where
@@ -1688,7 +1688,7 @@ The statement and proof of progress is much as before,
 appropriately annotated:
 -->
 
-进行性的声明和证明与之前大抵相同，加上了适当的附注：
+可进性的声明和证明与之前大抵相同，加上了适当的附注：
 
 ```agda
 progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
@@ -1723,7 +1723,7 @@ We can do much the same here, but we no longer need to explicitly
 refer to preservation, since it is built-in to the definition of reduction.
 -->
 
-之前，我们将保型性和进行性结合来对一个项求值。
+之前，我们将保型性和可进性结合来对一个项求值。
 我们在此处也可以这么做，但是我们不再需要显式地参考保型性，因为它内置于规约的定义中。
 
 <!--

src/plfa/part2/Inference.lagda.md

@@ -247,7 +247,7 @@ same purpose as the argument type decoration of the previous section.
 -->
 
 什么项生成类型，什么项继承类型的？
-我们的宗旨是**析构器**中的主项使用生成来赋型，而**构造子**使用继承。
+我们的宗旨是**解构子**中的主项使用生成来赋型，而**构造子**使用继承。
 比如，函数应用中的函数由生成来赋型，而抽象是由继承来赋型。
 抽象中继承的类型和之前我们为参数额外增加的注解起到一样的作用。
 
@@ -266,10 +266,10 @@ the type in the input context.  Fixed points will be naturally
 typed by inheritance.
 -->
 
-析构某一类型的值的项总有一个主项（提供一个所需类型的参数），且经常有副项。
+解构某一类型的值的项总有一个主项（提供一个所需类型的参数），且经常有副项。
 对于函数应用来说，主项提供了函数，副项提供了参数。
 对于分情况讨论来说，主项提供了自然数，副项则是两种情况不同的情况。
-在析构器中，主项使用生成进行赋型，而副项使用继承进行赋型。
+在解构子中，主项使用生成进行赋型，而副项使用继承进行赋型。
 我们将看到，这自然地导致函数应用作为整体由生成进行赋型，而分情况讨论作为整体则使用继承进行赋型。
 变量一般使用生成进行赋型，因为我们可以直接从上下文中查询其类型。
 不动点自然是用继承来赋型。
@@ -329,7 +329,7 @@ level declarations.
 
 `M ↓ A` 这种形式表示了我们唯一需要用类型来装饰的项。
 它只在从生成切换成继承时出现，
-即当一个**析构**某一类型的值的项的主项中包含了一个**构造**某一类型的值的时候，
+即当一个**解构**某一类型的值的项的主项中包含了一个**构造**某一类型的值的时候，
 也就是说，这是在 `β` 规约发生的地方出现。
 一般来说，我们只需要在顶层声明中需要这样的装饰。
 
@@ -586,7 +586,7 @@ in deconstructors inherit.
 -->
 
 至于每个项是由继承或者生成来赋型，我们在上文中已经讨论过，并且可以直接上文的非形式化语法中直接得来。
-析构器中的主项由生成赋型，析构器中的构造子和副项由继承赋型。
+解构子中的主项由生成赋型，解构子中的构造子和副项由继承赋型。
 
 <!--
 ## Example terms

src/plfa/part2/Lambda.lagda.md

@@ -46,7 +46,7 @@ of variants of lambda calculus.
 
 在本章中，我们将形式化简单类型的 λ-演算，给出它的语法、小步语义和类型规则。
 在下一章 [Properties](/Properties/) 中，我们将
-证明它的主要性质，包括进行性与保型性。
+证明它的主要性质，包括可进性与保型性。
 后续的章节将研究 λ-演算的不同变体。
 
 <!--
@@ -165,9 +165,9 @@ correspond to introduction rules and deconstructors to eliminators.
 
 除了变量和不动点以外，每一个项要么构造了一个给定类型的值
 （抽象产生了函数，零和后继产生了自然数），
-要么析构了一个这样的值（应用使用了函数，匹配使用了自然数）。
+要么解构了一个这样的值（应用使用了函数，匹配使用了自然数）。
 我们在给项赋予类型的时候将重新探讨这一对应关系。
-构造子对应了引入规则，析构子对应了消去规则。
+构造子对应了引入规则，解构子对应了消去规则。
 
 <!--
 Here is the syntax of terms in Backus-Naur Form (BNF):
@@ -1030,7 +1030,7 @@ letter `β` (_beta_) and such rules are traditionally called _beta rules_.
 
 规则可以分为两类。
 兼容性规则让我们规约一个项的一部分。我们用希腊字母 `ξ` （_xi_）开头的规则表示。
-当一个项规约到足够的时候，它将会包括一个构造子和一个析构子，在这里是 `ƛ` 和 `·`，
+当一个项规约到足够的时候，它将会包括一个构造子和一个解构子，在这里是 `ƛ` 和 `·`，
 我们可以直接规约。这样的规则我们用希腊字母 `β` （_beta_）表示，也被称为 **β-规则**。
 
 <!--
@@ -2018,7 +2018,7 @@ case expressions use naturals).
 我们从上往下阅读时，引入和消去的规则一目了然：前者**引入**了一个带有连接符的式子，
 其出现在结论中，而不是条件中；后者**消去**了带有连接符的式子，其出现在条件中，而不是结论中。
 引入规则表示了如何构造一个给定类型的值（抽象产生函数、零和后继产生自然数），而消去规则
-表示了如何析构一个给定类型的值（应用使用函数，匹配表达式使用自然数）。
+表示了如何解构一个给定类型的值（应用使用函数，匹配表达式使用自然数）。
 
 <!--
 Note also the three places (in `⊢ƛ`, `⊢case`, and `⊢μ`) where the

src/plfa/part2/More.lagda.md

@@ -1875,7 +1875,7 @@ V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′)  =  V¬—→ VN N—
 ## Progress
 -->
 
-## 进行性
+## 可进性
 
 ```agda
 data Progress {A} (M : ∅ ⊢ A) : Set where

src/plfa/part2/Properties.lagda.md

@@ -1,5 +1,5 @@
 ---
-title     : "Properties: 进行性与保型性"
+title     : "Properties: 可进性与保型性"
 permalink : /Properties/
 translators : ["starxingchenc","alissa-tung"]
 progress  : 100
@@ -18,7 +18,7 @@ sequences for us.
 -->
 
 本章涵盖了上一章所介绍的简单类型 λ-演算的性质。
-在这些性质中最为重要的是进行性（Progress）与保型性（Preservation）。
+在这些性质中最为重要的是可进性（Progress）与保型性（Preservation）。
 我们将在稍后介绍它们，并展示如何通过组合它们来使 Agda 为我们计算归约序列。
 
 <!--
@@ -95,7 +95,7 @@ _Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` s
 that `M —→ N`.
 -->
 
-**进行性**：如果有 `∅ ⊢ M ⦂ A`，那么要么项 `M` 是一个值，要么存在一个项 `N` 使
+**可进性**：如果有 `∅ ⊢ M ⦂ A`，那么要么项 `M` 是一个值，要么存在一个项 `N` 使
 得 `M —→ N` 成立。
 
 <!--
@@ -107,7 +107,7 @@ well-typed term.
 -->
 
 所以要么我们有一个值，这时我们已经完成了规约；要么我们可以进行一步规约。
-当处于后者的情况时，我们想要再一次应用进行性。
+当处于后者的情况时，我们想要再一次应用可进性。
 但这样做需要我们首先知道通过规约得到的项本身是良类型的闭项。
 事实上，只要我们规约的起点是一个良类型的闭项，所得到的项就满足这个性质。
 
@@ -131,7 +131,7 @@ and its Church numeral variant.
 
 这给予我们一种自动化求值的策略。
 从一个良类型的闭项开始。
-由进行性，它要么是一个值，于是求值结束了；要么可以被规约为另一个项。
+由可进性，它要么是一个值，于是求值结束了；要么可以被规约为另一个项。
 由保型性，所以得到的另一个项本身也是一个良类型的闭项。
 重复这一过程。
 我们要么会陷入永久的循环中，此时求值过程将不会停机；
@@ -288,7 +288,7 @@ that is, the canonical forms are exactly the well-typed values.
 ## Progress
 -->
 
-## 进行性
+## 可进性
 
 <!--
 We would like to show that every term is either a value or takes a
@@ -325,7 +325,7 @@ _Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` s
 that `M —→ N`.
 -->
 
-**进行性**：如果有 `∅ ⊢ M ⦂ A`，那么要么项 `M` 是一个值，要么存在一个项 `N` 使
+**可进性**：如果有 `∅ ⊢ M ⦂ A`，那么要么项 `M` 是一个值，要么存在一个项 `N` 使
 得 `M —→ N` 成立。
 
 <!--
@@ -362,7 +362,7 @@ exists a term `N` such that `M —→ N`, or if it is done, meaning that
 If a term is well typed in the empty context then it satisfies progress:
 -->
 
-如果一个项在空上下文中是良类型的，那么它满足进行性：
+如果一个项在空上下文中是良类型的，那么它满足可进性：
 
 ```agda
 progress : ∀ {M A}
@@ -420,13 +420,13 @@ Let's unpack the first three cases:
     that `M` is well typed:
 -->
 
-* 如果这个项是一个函数应用 `L · M`，则考虑对项 `L` 良类型的推导过程递归应用进行性：
+* 如果这个项是一个函数应用 `L · M`，则考虑对项 `L` 良类型的推导过程递归应用可进性：
 
   + 如果这个项还能够进行一步规约，我们就有了 `L —→ L′` 的论据，再由 `ξ-·₁`，
     可知原来的项进行到 `L′ · M`。
 
   + 如果这个项的规约结束了，我们就有了 `L` 是一个值的论据。
-    则考虑对项 `L` 良类型的推导过程递归应用进行性：
+    则考虑对项 `L` 良类型的推导过程递归应用可进性：
 
     <!--
     - If the term steps, we have evidence that `M —→ M′`,
@@ -438,7 +438,7 @@ Let's unpack the first three cases:
 
     - 如果这个项还能够进行一步规约，我们就有了 `M —→ M′` 的论据，再由 `ξ-·₂`，
       可知原来的项进行到 `L′ · M`。要应用规约步骤 `ξ-·₂` 需要我们提供项 `L` 是
-      一个值的论据，而之前对子项进行性的分析已经提供了需要的证明。
+      一个值的论据，而之前对子项可进性的分析已经提供了需要的证明。
 
     <!--
     - If the term is done, we have evidence that `M` is
@@ -484,7 +484,7 @@ Instead of defining a data type for `Progress M`, we could
 have formulated progress using disjunction and existentials:
 -->
 
-也可以用析取和存在量化来形式化进行性，
+也可以用析取和存在量化来形式化可进性，
 而不是为 `Progress M` 定义一个数据类型：
 
 ```agda
@@ -1542,7 +1542,7 @@ function that computes the reduction sequence from any given closed,
 well-typed term to its value, if it has one.
 -->
 
-通过重复应用进行性和保型性，我们可以对任何良类型的项求值。
+通过重复应用可进性和保型性，我们可以对任何良类型的项求值。
 在这一节，我们将介绍一个 Agda 函数，
 该函数可以求得任意给定良类型的闭项到其值的规约序列，如果该序列存在。
 
@@ -2105,7 +2105,7 @@ and preservation theorems for the simply typed lambda-calculus.
 -->
 
 不阅读上面的陈述，
-写下简单类型 λ-演算进行性和保型性的定理。
+写下简单类型 λ-演算可进性和保型性的定理。
 
 
 
@@ -2176,7 +2176,7 @@ Stuck M  =  Normal M × ¬ Value M
 Using progress, it is easy to show that no well-typed term is stuck:
 -->
 
-使用进行性，很容易证明没有良类型的项会被卡住。
+使用可进性，很容易证明没有良类型的项会被卡住。
 
 ```agda
 postulate
@@ -2229,7 +2229,7 @@ introduced `wrong` as the denotation of a term with a type error, and
 showed _well-typed terms don't go wrong_.)
 -->
 
-Felleisen 与 Wright 通过进行性和保型性引入了证明，并将其总结为 **良类型的项不会卡住** 的口号。
+Felleisen 与 Wright 通过可进性和保型性引入了证明，并将其总结为 **良类型的项不会卡住** 的口号。
 （他们提及了 Robin Milner 早期的工作，他使用指称而非操作语义。
 他引入了「错误」作为带有类型错误的术语的指称，并展示了 **良类型的项不会出错**。）
 
@@ -2466,7 +2466,7 @@ false, give a counterexample:
 
   - 确定性
 
-  - 进行性
+  - 可进性
 
   - 保型性
 
@@ -2511,7 +2511,7 @@ false, give a counterexample:
 
   - 确定性
 
-  - 进行性
+  - 可进性
 
   - 保型性
 
@@ -2545,7 +2545,7 @@ false, give a counterexample:
 
   - 确定性
 
-  - 进行性
+  - 可进性
 
   - 保型性
 
@@ -2609,7 +2609,7 @@ false, give a counterexample:
 
   - 确定性
 
-  - 进行性
+  - 可进性
 
   - 保型性