Merge pull request #187 from Agda-zh/soundness

Soundness: 翻译完毕

修正了部分术语：

规约 -> 归约

子归约，子扩展 -> 主体归约，主体扩展

src/plfa/part1/Decidable.lagda.md

@@ -319,7 +319,7 @@ may recursively invoke the function to produce evidence that `T (m ≤ᵇ n)`.
 -->
 
 如果证明是 `z≤n`，我们立即可以得到 `zero ≤ᵇ n` 为真，所以 `T (m ≤ᵇ n)` 由 `tt` 证明。
-如果证明是 `s≤s` 作用于 `m≤n`，那么 `suc m ≤ᵇ suc n` 规约到 `m ≤ᵇ n`，我们可以递归地使用函数
+如果证明是 `s≤s` 作用于 `m≤n`，那么 `suc m ≤ᵇ suc n` 归约到 `m ≤ᵇ n`，我们可以递归地使用函数
 来获得 `T (m ≤ᵇ n)` 的证明。
 
 <!--
@@ -1070,8 +1070,8 @@ guard.
   it will throw an error. For instance, if we call `3 - 5` we get `_n≤m_254 : ⊥`.
 -->
 
-- 如果 `n ≤ m` 成立，隐式参数的类型规约为 `⊤`。 然后 Agda 会欣然地提供隐式参数。
-- 否则，类型规约为 `⊥` ，Agda 无法为此类型提供对应的值，因此会报错。例如，如果我们调用 `3 - 5` 会得到 `_n≤m_254 : ⊥`。
+- 如果 `n ≤ m` 成立，隐式参数的类型归约为 `⊤`。 然后 Agda 会欣然地提供隐式参数。
+- 否则，类型归约为 `⊥` ，Agda 无法为此类型提供对应的值，因此会报错。例如，如果我们调用 `3 - 5` 会得到 `_n≤m_254 : ⊥`。
 
 <!--
 We obtain the witness for `n ≤ m` using `toWitness`, which we defined earlier:

src/plfa/part1/Naturals.lagda.md

@@ -1282,7 +1282,7 @@ definition to equivalent inference rules for judgments about equality:
 -->
 
 同理，无需利用循环性，我们的加法定义也是可以被赋予意义的。
-为此，我们需要将加法的定义规约到用于判断相等性的等价的推导规则上来。
+为此，我们需要将加法的定义归约到用于判断相等性的等价的推导规则上来。
 
     n : ℕ
     --------------

src/plfa/part2/BigStep.lagda.md

@@ -29,7 +29,7 @@ of the denotational semantics.
 -->
 
 传名调用求值策略（Call-by-name Evaluation Strategy）是在 λ-演算中计算程序值的一种确定性方法。
-也就是说，传名调用能够求出值当且仅当 β-规约能将程序规约为一个 λ-抽象。
+也就是说，传名调用能够求出值当且仅当 β-归约能将程序归约为一个 λ-抽象。
 在这一章节，我们将定义传名调用求值并且证明这个等价命题的必要性。
 充分性的部分较为复杂，通常通过 Curry-Feys 标准化证明。
 根据 Plotkin 的工作，我们给出这个证明的概要，
@@ -48,7 +48,7 @@ single sub-computation has been completed.
 我们将传名调用策略表示为一个输入表达式与输出值间的关系。
 因为这样的关系将输入表达式 `M` 和最终结果 `V` 直接相联系，
 它通常被叫做**大步语义（Big-stepsemantics）**，写做 `M ⇓ V`。
-而小步规约关系则被写做 `M —→ M′`，它仅通过一步子计算来将 `M` 规约为另一个表达式 `M′`。
+而小步归约关系则被写做 `M —→ M′`，它仅通过一步子计算来将 `M` 归约为另一个表达式 `M′`。
 
 
 <!--
@@ -236,14 +236,14 @@ straightforward induction on the two big-step derivations.
 ## Big-step evaluation implies beta reduction to a lambda
 -->
 
-## 大步求值蕴含 β-规约至 λ-抽象
+## 大步求值蕴含 β-归约至 λ-抽象
 
 <!--
 If big-step evaluation produces a value, then the input term can
 reduce to a lambda abstraction by beta reduction:
 -->
 
-如果大步求值能够求出值，那么输入项能被 β-规约规约为一个 λ-抽象：
+如果大步求值能够求出值，那么输入项能被 β-归约归约为一个 λ-抽象：
 
       ∅' ⊢ M ⇓ clos (ƛ N′) δ
       -----------------------------
@@ -262,7 +262,7 @@ the environment `γ` to an equivalent substitution `σ`.
 
 该证明通过对大步推导归纳来完成。通常，我们需要推广命题以完成归纳。
 在 `⇓-app`（函数应用）的情况下，参数被添加到环境中，导致环境变得非空。
-相应的 β-规约将参数替换进 λ-抽象的主体中。
+相应的 β-归约将参数替换进 λ-抽象的主体中。
 所以我们将引理推广为允许任意环境 `γ` 并且添加一个前提将环境 `γ` 与等价的替代 `σ` 相关联。
 
 <!--
@@ -441,7 +441,7 @@ below.
 -->
 
 我们到达了主要引理：如果 `M` 在环境 `γ` 中大步求值为闭包 `V`，并且 `γ ≈ₑ σ`，
-那么 `subst σ M` 将规约为某个等价于 `V` 的项 `N`。我们如下叙述该证明。
+那么 `subst σ M` 将归约为某个等价于 `V` 的项 `N`。我们如下叙述该证明。
 
 ```agda
 ⇓→—↠×≈ : ∀{Γ}{γ : ClosEnv Γ}{σ : Subst Γ ∅}{M : Γ ⊢ ★}{V : Clos}
@@ -585,7 +585,7 @@ With the main lemma complete, we establish the forward direction
 of the equivalence between the big-step semantics and beta reduction.
 -->
 
-证明了主要引理后，我们便建立起大步语义与 β-规约等价关系的必要性。
+证明了主要引理后，我们便建立起大步语义与 β-归约等价关系的必要性。
 
 ```agda
 cbn→reduce :  ∀{M : ∅ ⊢ ★}{Δ}{δ : ClosEnv Δ}{N′ : Δ , ★ ⊢ ★}
@@ -626,7 +626,7 @@ with `M`. Prove that `M ↓ N` implies `M —↠ N`.
 ## Beta reduction to a lambda implies big-step evaluation
 -->
 
-## β-规约至 λ-抽象蕴含大步求值
+## β-归约至 λ-抽象蕴含大步求值
 
 <!--
 The proof of the backward direction, that beta reduction to a lambda
@@ -645,56 +645,56 @@ lambda. Plotkin proves that `M` reduces to `L` if and only if `M` is
 related to `L` by a standard reduction sequence.
 -->
 
-充分性的证明，也就是 β-规约至 λ-抽象蕴含大步语义求值是更困难的。
-困难源于通过 `ζ` 规则在 λ-抽象下的规约过程。
-传名调用语义在 λ-演算中并不会规约，因此直接通过归纳规约序列来证明是不可能的。
+充分性的证明，也就是 β-归约至 λ-抽象蕴含大步语义求值是更困难的。
+困难源于通过 `ζ` 规则在 λ-抽象下的归约过程。
+传名调用语义在 λ-演算中并不会归约，因此直接通过归纳归约序列来证明是不可能的。
 在文章 **Call-by-name, call-by-value, and the λ-calculus** 中，
-Plotkin使用两个辅助规约关系分两步完成了证明。
+Plotkin使用两个辅助归约关系分两步完成了证明。
 第一步使用了 Curry-Feys 标准化这一经典方法，
-它依赖于 **标准规约序列（Standard Reduction Sequence）** 的概念，
-通过在 λ-演算下将传名调用扩展以包括规约，
-标准规约序列充当了完整 β-规约与传名调用求值的中间点。
-Plotkin证明了 `M` 能被规约为 `L` 当且仅当 `M` 与 `L` 通过一个标准规约序列相关。
+它依赖于 **标准归约序列（Standard Reduction Sequence）** 的概念，
+通过在 λ-演算下将传名调用扩展以包括归约，
+标准归约序列充当了完整 β-归约与传名调用求值的中间点。
+Plotkin证明了 `M` 能被归约为 `L` 当且仅当 `M` 与 `L` 通过一个标准归约序列相关。
 
 <!--
     Theorem 1 (Standardisation)
     `M —↠ L` if and only if `M` goes to `L` via a standard reduction sequence.
 -->
 
     定理 1（标准化）
-    `M —↠ L` 当且仅当 `M` 能通过一个标准规约序列规约成 `L`。
+    `M —↠ L` 当且仅当 `M` 能通过一个标准归约序列归约成 `L`。
 
 <!--
 Plotkin then introduces _left reduction_, a small-step version of
 call-by-name and uses the above theorem to prove that beta reduction
 and left reduction are equivalent in the following sense.
 -->
 
-Plotkin 接着引入了**左规约（Left Reduction）** 作为传名调用的小步描述，
-并且用上方的定理证明了 β-规约与左规约在下述情况下等价。
+Plotkin 接着引入了**左归约（Left Reduction）** 作为传名调用的小步描述，
+并且用上方的定理证明了 β-归约与左归约在下述情况下等价。
 
 <!--
     Corollary 1
     `M —↠ ƛ N` if and only if `M` goes to `ƛ N′`, for some `N′`, by left reduction.
 -->
 
     推论 1
-    `M —↠ ƛ N` 当且仅当对于某个 `N′`，`M`能通过左规约成 `ƛ N′`。
+    `M —↠ ƛ N` 当且仅当对于某个 `N′`，`M`能通过左归约成 `ƛ N′`。
 
 <!--
 The second step of the proof connects left reduction to call-by-name
 evaluation.
 -->
 
-证明的下一步将左规约与传名调用求值联系起来。
+证明的下一步将左归约与传名调用求值联系起来。
 
 <!--
     Theorem 2
     `M` left reduces to `ƛ N` if and only if `⊢ M ⇓ ƛ N`。
 -->
 
     定理 2
-    `M` 左规约成 `ƛ N` 当且仅当 `⊢ M ⇓ ƛ N`。
+    `M` 左归约成 `ƛ N` 当且仅当 `⊢ M ⇓ ƛ N`。
 
 <!--
 (Plotkin's call-by-name evaluator uses substitution instead of
@@ -710,7 +710,7 @@ Putting Corollary 1 and Theorem 2 together, Plotkin proves that
 call-by-name evaluation is equivalent to beta reduction.
 -->
 
-将推论 1 和定理 2 相结合，Plotkin 证明了传名调用求值与 β-规约等价。
+将推论 1 和定理 2 相结合，Plotkin 证明了传名调用求值与 β-归约等价。
 
 <!--
     Corollary 2

src/plfa/part2/Bisimulation.lagda.md

@@ -1,5 +1,5 @@
 ---
-title      : "Bisimulation: 联系不同的规约系统"
+title      : "Bisimulation: 联系不同的归约系统"
 permalink  : /Bisimulation/
 translators: ["Fangyi Zhou"]
 progress   : 100
@@ -31,7 +31,7 @@ over terms of the source, and `M†`, `N†` range over terms of the
 target.  We define a relation
 -->
 
-给定两个不同的系统，它们有不同的项和不同的规约规则，我们定义诸如
+给定两个不同的系统，它们有不同的项和不同的归约规则，我们定义诸如
 『一个系统**模拟（Simulate）**了另一个系统』此类断言的意义。
 假设两个系统分别叫做**源**（Source）和**目标**（Target），我们用
 `M` 和 `N` 表示源系统的项，`M†` 和 `N†` 表示目标系统的项。
@@ -47,7 +47,7 @@ in the target:
 -->
 
 于两个系统对应的项之上。
-如果每个源系统的每一个规约都有一个对应的规约序列，那我们就有了一个**模拟**。
+如果每个源系统的每一个归约都有一个对应的归约序列，那我们就有了一个**模拟**。
 
 <!--
 _Simulation_: For every `M`, `M†`, and `N`:
@@ -79,7 +79,7 @@ corresponds to a reduction (rather than a reduction sequence)
 in the target:
 -->
 
-有时我们会使用一个更强的条件，使得每个源系统的规约对应目标系统的规约（而不是规约序列）：
+有时我们会使用一个更强的条件，使得每个源系统的归约对应目标系统的归约（而不是归约序列）：
 
     M  --- —→ --- N
     |             |
@@ -109,7 +109,7 @@ _converse_ relations. Hence, if `~` is a relation from source to target,
 its converse is a relation from target to source.)
 -->
 
-如果从目标系统到源系统也有一个模拟：即每个目标系统的规约在源目标系统中有对应的规约序列，
+如果从目标系统到源系统也有一个模拟：即每个目标系统的归约在源目标系统中有对应的归约序列，
 我们对这样的情况尤其感兴趣。换句话说，`~` 是一个从源到目标的模拟，而 `~`
 的逆是一个从目标的源的模拟。这样的情况被称为**互模拟**（Bisimulation）。
   (In general, if < and > are arbitrary relations such
@@ -124,8 +124,8 @@ reduction step in the source we must show a corresponding reduction
 sequence in the target.
 -->
 
-要建立模拟，我们需要分情况讨论所有的可能规约，以及所有它们可能联系的项。
-对于每个源系统中规约的步骤，我们必须给出目标系统中对应的规约系列。
+要建立模拟，我们需要分情况讨论所有的可能归约，以及所有它们可能联系的项。
+对于每个源系统中归约的步骤，我们必须给出目标系统中对应的归约系列。
 
 <!--
 For instance, the source might be lambda calculus with _let_
@@ -612,7 +612,7 @@ In its structure, it looks a little bit like a proof of progress:
 -->
 
 这个证明由分情况讨论来完成，检查每一个 `M ~ M†` 的例子，和每一个 `M —→ M†` 的例子，
-并在规约是 `ξ` 规则时使用递归，也因此包括了另一个规约。
+并在归约是 `ξ` 规则时使用递归，也因此包括了另一个归约。
 证明的结构和可进性的证明也有些类似：
 
 <!--
@@ -623,10 +623,10 @@ In its structure, it looks a little bit like a proof of progress:
     Recursive invocation gives us
 -->
 
-* 如果相关的项是变量，那么无可应用的规约。
-* 如果相关的项是 λ 抽象，那么无可应用的规约。
+* 如果相关的项是变量，那么无可应用的归约。
+* 如果相关的项是 λ 抽象，那么无可应用的归约。
 * 如果相关的项是应用，那么有三种子情况：
-  - 源项由 `ξ-·₁` 规约，在此情况下目标项也一样。递归应用可以让我们得到：
+  - 源项由 `ξ-·₁` 归约，在此情况下目标项也一样。递归应用可以让我们得到：
 
         L  --- —→ ---  L′
         |              |
@@ -655,7 +655,7 @@ In its structure, it looks a little bit like a proof of progress:
     Recursive invocation gives us
   -->
 
-  - 源项由 `ξ-·₂` 规约，在此情况下目标项也一样。递归应用可以让我们得到：
+  - 源项由 `ξ-·₂` 归约，在此情况下目标项也一样。递归应用可以让我们得到：
 
         M  --- —→ ---  M′
         |              |
@@ -689,7 +689,7 @@ In its structure, it looks a little bit like a proof of progress:
   - The source term reduces via `β-ƛ`, in which case the target term does as well:
   -->
 
-  - 源项由 `β-ƛ` 规约，在此情况下目标项也一样：
+  - 源项由 `β-ƛ` 归约，在此情况下目标项也一样：
 
          (ƛ x ⇒ N) · V  --- —→ ---  N [ x := V ]
               |                           |
@@ -720,7 +720,7 @@ In its structure, it looks a little bit like a proof of progress:
     reduces via `ξ-·₂`.  Recursive invocation gives us
   -->
 
-  - 源项由 `ξ-let` 规约，在此情况下目标项由 `ξ-·₂` 规约。递归应用可以让我们得到：
+  - 源项由 `ξ-let` 归约，在此情况下目标项由 `ξ-·₂` 归约。递归应用可以让我们得到：
 
         M  --- —→ ---  M′
         |              |
@@ -749,7 +749,7 @@ In its structure, it looks a little bit like a proof of progress:
     term reduces via `β-ƛ`:
   -->
 
-  - 源项由 `β-let` 规约，在此情况下目标项由 `β-ƛ` 规约：
+  - 源项由 `β-let` 归约，在此情况下目标项由 `β-ƛ` 归约：
 
         let x = V in N  --- —→ ---  N [ x := V ]
               |                         |