From cfb874e0e6b24dc6c4f0b5a1374b64bd315d517d Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Thu, 21 Mar 2024 02:12:10 +0800 Subject: [PATCH 1/4] =?UTF-8?q?Soundness:=20=E5=BC=80=E5=A7=8B=E7=BF=BB?= =?UTF-8?q?=E8=AF=91?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/plfa/part3/Compositional.lagda.md | 7 ++-- src/plfa/part3/Denotational.lagda.md | 5 +-- src/plfa/part3/Soundness.lagda.md | 57 +++++++++++++++++++++++++-- 3 files changed, 59 insertions(+), 10 deletions(-) diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md index 651a86a4f..238684d72 100644 --- a/src/plfa/part3/Compositional.lagda.md +++ b/src/plfa/part3/Compositional.lagda.md @@ -1,6 +1,7 @@ --- -title : "Compositional: 指称语义是可组合的" -permalink : /Compositional/ +title : "Compositional: 指称语义是可组合的" +permalink : /Compositional/ +translators : ["OlingCat"] --- ```agda @@ -550,7 +551,7 @@ is a congruence. --> 接下来我们证明指称相等对于应用也满足合同性：`ℰ L ≃ ℰ L′` 和 `ℰ M ≃ ℰ M′` -蕴含 `ℰ (L · M) ≃ ℰ (L′ · M′)`。等式 `app-equiv` 将其规约为 `●` +蕴含 `ℰ (L · M) ≃ ℰ (L′ · M′)`。等式 `app-equiv` 将其归约为 `●` 运算符是否满足合同性的问题。 ```agda diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 961042a5f..ad90ce524 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -1,8 +1,7 @@ --- -title : "Denotational: 无类型 λ-演算的指称语义" -permalink : /Denotational/ +title : "Denotational: 无类型 λ-演算的指称语义" +permalink : /Denotational/ translators : ["OlingCat"] -progress : 100 --- ```agda diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md index 7bdc0c150..f9a68f5fa 100644 --- a/src/plfa/part3/Soundness.lagda.md +++ b/src/plfa/part3/Soundness.lagda.md @@ -1,6 +1,7 @@ --- -title : "Soundness: Soundness of reduction with respect to denotational semantics" -permalink : /Soundness/ +title : "Soundness: 指称语义归约的可靠性" +permalink : /Soundness/ +translators : ["OlingCat"] --- ```agda @@ -8,13 +9,22 @@ module plfa.part3.Soundness where ``` + +## 简介 + + + +本章中我们会证明指称语义的归约语义是可靠（Sound）的，即对于任意项 `L`： - L —↠ ƛ N implies ℰ L ≃ ℰ (ƛ N) + L —↠ ƛ N 蕴含 ℰ L ≃ ℰ (ƛ N) + + +证明可通过对归约序列进行归纳得出，因此主引理涉及单个归约步骤。 +我们需要证明，如果任何项 `M` 步进到项 `N`，则 `M` 和 `M` 的指称相等。 +我们将分别证明「当且仅当」的两个方向，一个方向类似于保型性（type preservation）的证明， +另一个方向类似于反向归约（即展开）的保型性证明。回想一下， +保型性有时称为主体归约（subject reduction）。 +反向的保型性是一个众所周知的属性，称为 **主体展开（subject expansion）**。 +众所周知，大多数类型化 λ-演算都不满足主体展开！ +（译注：一个 subject 是形如 `(1*2+3) : Int` 这样已经确定类型的项。 +类型化 λ-演算会失去保型性的原因参见 https://www.bananaspace.org/wiki/%E7%B1%BB%E5%9E%8B%E4%B8%8D%E5%8F%98%E6%80%A7） + + +## 导入 ```agda open import Relation.Binary.PropositionalEquality @@ -53,7 +78,11 @@ open import plfa.part3.Denotational open import plfa.part3.Compositional using (lambda-inversion; var-inv) ``` + + +## 向前归约保持指称不变 The proof of preservation in this section mixes techniques from previous chapters. Like the proof of preservation for the STLC, we are @@ -66,7 +95,11 @@ concerning all of the auxiliary functions used in the reduction relation: substitution, renaming, and extension. + + +### 同时代换保持指称不变 Our next goal is to prove that simultaneous substitution preserves meaning. That is, if `M` results in `v` in environment `γ`, then applying a @@ -139,7 +172,11 @@ cases are for variables and lambda abstractions. terms that result in the appropriate values. + + +### 单一代换保持指称不变 For β reduction, `(ƛ N) · M —→ N [ M ]`, we need to show that the semantics is preserved when substituting `M` for de Bruijn index 0 in @@ -175,7 +212,11 @@ Let `y` be an arbitrary variable (de Bruijn index). `γ ⊢ x ↓ γ x` by rule `var`. + + +### 归约保持指称不变 With the substitution lemma in hand, it is straightforward to prove that reduction preserves denotations. @@ -208,7 +249,11 @@ the reduction. * The rest of the cases are straightforward. + + +## 归约反射了指称 This section proves that reduction reflects the denotation of a term. That is, if `N` results in `v`, and if `M` reduces to `N`, then @@ -230,6 +275,10 @@ using `⊔`. If `M` occurred 0 times, then we do not need any information about `M` and can therefore use `⊥` for the value of `M`. + + ### Renaming reflects meaning Previously we showed that renaming variables preserves meaning. Now @@ -669,6 +718,6 @@ soundness {Γ} (L —→⟨ r ⟩ M—↠N) γ v = ## Unicode -This chapter uses the following unicode: +本章使用了以下 Unicode： ≟ U+225F QUESTIONED EQUAL TO (\?=) From 210fef81dbddf4325072b1845526e8bc9de0dde4 Mon Sep 17 00:00:00 2001 From: Oling Cat Date: Thu, 21 Mar 2024 02:13:36 +0800 Subject: [PATCH 2/4] =?UTF-8?q?=E4=BF=AE=E6=AD=A3=E6=9C=AF=E8=AF=AD?= =?UTF-8?q?=EF=BC=9A=E8=A7=84=E7=BA=A6=20->=20=E5=BD=92=E7=BA=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 规约（rule）是规则，约定的意思； 归约（reduction）是归纳，约化（化简）的意思， 二者不应混淆。 --- src/plfa/part1/Decidable.lagda.md | 6 +- src/plfa/part1/Naturals.lagda.md | 2 +- src/plfa/part2/BigStep.lagda.md | 46 +++++------ src/plfa/part2/Bisimulation.lagda.md | 30 +++---- src/plfa/part2/Confluence.lagda.md | 92 ++++++++++----------- src/plfa/part2/DeBruijn.lagda.md | 30 +++---- src/plfa/part2/Inference.lagda.md | 2 +- src/plfa/part2/Lambda.lagda.md | 90 ++++++++++----------- src/plfa/part2/More.lagda.md | 38 ++++----- src/plfa/part2/Properties.lagda.md | 112 +++++++++++++------------- src/plfa/part2/Untyped.lagda.md | 60 +++++++------- src/plfa/part3/Compositional.lagda.md | 2 +- src/plfa/part3/Denotational.lagda.md | 16 ++-- 13 files changed, 263 insertions(+), 263 deletions(-) diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index aebeaae8f..1a5007337 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/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)` 的证明。 -- 如果 `n ≤ m` 成立，隐式参数的类型规约为 `⊤`。 然后 Agda 会欣然地提供隐式参数。 -- 否则，类型规约为 `⊥` ，Agda 无法为此类型提供对应的值，因此会报错。例如，如果我们调用 `3 - 5` 会得到 `_n≤m_254 : ⊥`。 +- 如果 `n ≤ m` 成立，隐式参数的类型归约为 `⊤`。 然后 Agda 会欣然地提供隐式参数。 +- 否则，类型归约为 `⊥` ，Agda 无法为此类型提供对应的值，因此会报错。例如，如果我们调用 `3 - 5` 会得到 `_n≤m_254 : ⊥`。 同理，无需利用循环性，我们的加法定义也是可以被赋予意义的。 -为此，我们需要将加法的定义规约到用于判断相等性的等价的推导规则上来。 +为此，我们需要将加法的定义归约到用于判断相等性的等价的推导规则上来。 n : ℕ -------------- diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md index 9f0f34615..f7b932cbc 100644 --- a/src/plfa/part2/BigStep.lagda.md +++ b/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′`。 -## 大步求值蕴含 β-规约至 λ-抽象 +## 大步求值蕴含 β-归约至 λ-抽象 -如果大步求值能够求出值，那么输入项能被 β-规约规约为一个 λ-抽象： +如果大步求值能够求出值，那么输入项能被 β-归约归约为一个 λ-抽象： ∅' ⊢ M ⇓ clos (ƛ N′) δ ----------------------------- @@ -262,7 +262,7 @@ the environment `γ` to an equivalent substitution `σ`. 该证明通过对大步推导归纳来完成。通常，我们需要推广命题以完成归纳。 在 `⇓-app`（函数应用）的情况下，参数被添加到环境中，导致环境变得非空。 -相应的 β-规约将参数替换进 λ-抽象的主体中。 +相应的 β-归约将参数替换进 λ-抽象的主体中。 所以我们将引理推广为允许任意环境 `γ` 并且添加一个前提将环境 `γ` 与等价的替代 `σ` 相关联。 我们到达了主要引理：如果 `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 --> -## β-规约至 λ-抽象蕴含大步求值 +## β-归约至 λ-抽象蕴含大步求值 -充分性的证明，也就是 β-规约至 λ-抽象蕴含大步语义求值是更困难的。 -困难源于通过 `ζ` 规则在 λ-抽象下的规约过程。 -传名调用语义在 λ-演算中并不会规约，因此直接通过归纳规约序列来证明是不可能的。 +充分性的证明，也就是 β-归约至 λ-抽象蕴含大步语义求值是更困难的。 +困难源于通过 `ζ` 规则在 λ-抽象下的归约过程。 +传名调用语义在 λ-演算中并不会归约，因此直接通过归纳归约序列来证明是不可能的。 在文章 **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` 通过一个标准归约序列相关。 定理 1（标准化） - `M —↠ L` 当且仅当 `M` 能通过一个标准规约序列规约成 `L`。 + `M —↠ L` 当且仅当 `M` 能通过一个标准归约序列归约成 `L`。 -Plotkin 接着引入了**左规约（Left Reduction）** 作为传名调用的小步描述， -并且用上方的定理证明了 β-规约与左规约在下述情况下等价。 +Plotkin 接着引入了**左归约（Left Reduction）** 作为传名调用的小步描述， +并且用上方的定理证明了 β-归约与左归约在下述情况下等价。 推论 1 - `M —↠ ƛ N` 当且仅当对于某个 `N′`，`M`能通过左规约成 `ƛ N′`。 + `M —↠ ƛ N` 当且仅当对于某个 `N′`，`M`能通过左归约成 `ƛ N′`。 -证明的下一步将左规约与传名调用求值联系起来。 +证明的下一步将左归约与传名调用求值联系起来。 定理 2 - `M` 左规约成 `ƛ N` 当且仅当 `⊢ M ⇓ ƛ N`。 + `M` 左归约成 `ƛ N` 当且仅当 `⊢ M ⇓ ƛ N`。 -将推论 1 和定理 2 相结合，Plotkin 证明了传名调用求值与 β-规约等价。 +将推论 1 和定理 2 相结合，Plotkin 证明了传名调用求值与 β-归约等价。 -给定两个不同的系统，它们有不同的项和不同的规约规则，我们定义诸如 +给定两个不同的系统，它们有不同的项和不同的归约规则，我们定义诸如 『一个系统**模拟（Simulate）**了另一个系统』此类断言的意义。 假设两个系统分别叫做**源**（Source）和**目标**（Target），我们用 `M` 和 `N` 表示源系统的项，`M†` 和 `N†` 表示目标系统的项。 @@ -47,7 +47,7 @@ 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. --> -要建立模拟，我们需要分情况讨论所有的可能规约，以及所有它们可能联系的项。 -对于每个源系统中规约的步骤，我们必须给出目标系统中对应的规约系列。 +要建立模拟，我们需要分情况讨论所有的可能归约，以及所有它们可能联系的项。 +对于每个源系统中归约的步骤，我们必须给出目标系统中对应的归约系列。 这个证明由分情况讨论来完成，检查每一个 `M ~ M†` 的例子，和每一个 `M —→ M†` 的例子， -并在规约是 `ξ` 规则时使用递归，也因此包括了另一个规约。 +并在归约是 `ξ` 规则时使用递归，也因此包括了另一个归约。 证明的结构和可进性的证明也有些类似： -* 如果相关的项是变量，那么无可应用的规约。 -* 如果相关的项是 λ 抽象，那么无可应用的规约。 +* 如果相关的项是变量，那么无可应用的归约。 +* 如果相关的项是 λ 抽象，那么无可应用的归约。 * 如果相关的项是应用，那么有三种子情况： - - 源项由 `ξ-·₁` 规约，在此情况下目标项也一样。递归应用可以让我们得到： + - 源项由 `ξ-·₁` 归约，在此情况下目标项也一样。递归应用可以让我们得到： 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 ] | | diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md index 0504b2441..9ed42968e 100644 --- a/src/plfa/part2/Confluence.lagda.md +++ b/src/plfa/part2/Confluence.lagda.md @@ -23,10 +23,10 @@ reduction sequences from any term `L` to two different terms `M₁` and some common term `N`. In pictures: --> -在这一章我们将证明 β-规约是**合流的（Confluent）** +在这一章我们将证明 β-归约是**合流的（Confluent）** （又被称作 *Church-Rosser* 性质）： -如果有从任一项 `L` 至两个不同项 `M₁` 和 `M₂` 的规约序列， -那么一定存在从这两个项至某个相同项 `N` 的规约序列。 +如果有从任一项 `L` 至两个不同项 `M₁` 和 `M₂` 的归约序列， +那么一定存在从这两个项至某个相同项 `N` 的归约序列。 如图： L @@ -72,7 +72,7 @@ Unfortunately, reduction in the lambda calculus does not satisfy the diamond property. Here is a counter example. --> -不幸的是 λ-演算的规约并不满足菱形性质。这是一个反例： +不幸的是 λ-演算的归约并不满足菱形性质。这是一个反例： (λ x. x x)((λ x. x) a) —→ (λ x. x x) a (λ x. x x)((λ x. x) a) —→ ((λ x. x) a) ((λ x. x) a) @@ -82,7 +82,7 @@ Both terms can reduce to `a a`, but the second term requires two steps to get there, not one. --> -两个项都可以规约至 `a a`，但第二项需要两步来完成，而不是一步。 +两个项都可以归约至 `a a`，但第二项需要两步来完成，而不是一步。 -为了回避这个问题，我们将定义一个辅助规约关系， -称为**平行规约（Parallel Reduction）** ， -它可以同时执行许多规约并因此满足菱形性质。 -更进一步地，我们将证明在两个项间存在平行规约序列当且仅当这两个项间存在 β-规约序列。 -因此，我们可以将 β-规约序列合流性的证明约化为平行规约合流性的证明。 +为了回避这个问题，我们将定义一个辅助归约关系， +称为**平行归约（Parallel Reduction）** ， +它可以同时执行许多归约并因此满足菱形性质。 +更进一步地，我们将证明在两个项间存在平行归约序列当且仅当这两个项间存在 β-归约序列。 +因此，我们可以将 β-归约序列合流性的证明约化为平行归约合流性的证明。 -## 平行规约 +## 平行归约 -平行规约关系被定义如下。 +平行归约关系被定义如下。 ```agda infix 2 _⇛_ @@ -164,8 +164,8 @@ parts simultaneously. The last rule reduces a lambda term and term in parallel followed by a beta step. --> -前三种规则是同时规约每个部分的合同性。 -最后一个规则平行地规约一个 λ-项和另一个项，接着是一步 β-规约。 +前三种规则是同时归约每个部分的合同性。 +最后一个规则平行地归约一个 λ-项和另一个项，接着是一步 β-归约。 -平行规约是自反的。 +平行归约是自反的。 ```agda par-refl : ∀{Γ A}{M : Γ ⊢ A} → M ⇛ M @@ -193,7 +193,7 @@ par-refl {Γ} {★} {L · M} = papp par-refl par-refl We define the sequences of parallel reduction as follows. --> -我们定义平行规约序列如下。 +我们定义平行归约序列如下。 ```agda infix 2 _⇛*_ @@ -226,7 +226,7 @@ showing that the diamond property holds for parallel reduction in that case. --> -回顾上文中菱形性质的反例，证明在这种情况下平行规约具有菱形性质。 +回顾上文中菱形性质的反例，证明在这种情况下平行归约具有菱形性质。 @@ -239,7 +239,7 @@ case. ## Equivalence between parallel reduction and reduction --> -## 平行规约与规约间等价性 +## 平行归约与归约间等价性 证明了该引理后我们便可完成必要性的证明， -即 `M —↠ N` 蕴含 `M ⇛* N`。该证明是对 `M —↠ N` 规约序列的简单归纳。 +即 `M —↠ N` 蕴含 `M ⇛* N`。该证明是对 `M —↠ N` 归约序列的简单归纳。 ```agda betas-pars : ∀{Γ A} {M N : Γ ⊢ A} @@ -291,7 +291,7 @@ reductions. So instead we shall prove that `M ⇛ N` implies `M —↠ N`. 现在考虑命题的充分性，即 `M ⇛* N` 蕴含 `M —↠ N`。 充分性的证明有一点不同，因为它不是 `M ⇛ N` 蕴含 `M —→ N` 的情形。 -毕竟 `M ⇛ N` 执行了许多规约， +毕竟 `M ⇛ N` 执行了许多归约， 所以我们应当证明 `M ⇛ N` 蕴含 `M —↠ N`。 ```agda @@ -353,7 +353,7 @@ The proof is by induction on `M ⇛ N`. * 假定 `(ƛ N) · M ⇛ N′ [ M′ ]` 因为 `N ⇛ N′` 和 `M ⇛ M′`。 根据类似的原因，我们有 `(ƛ N) · M —↠ (ƛ N′) · M′`， - 接着应用 β-规约我们得到 `(ƛ N′) · M′ —→ N′ [ M′ ]`。 + 接着应用 β-归约我们得到 `(ƛ N′) · M′ —→ N′ [ M′ ]`。 -## 平行规约的替换引理 +## 平行归约的替换引理 -我们的下一个目标是对平行规约证明菱形性质。 -为了完成该证明，我们还需证明替换遵从平行规约。 +我们的下一个目标是对平行归约证明菱形性质。 +为了完成该证明，我们还需证明替换遵从平行归约。 也就是说，如果有 `N ⇛ N′` 和 `M ⇛ M′`，那么 `N [ M ] ⇛ N′ [ M′ ]`。 我们不能直接通过归纳证明它，所以我们将其推广为： -如果 `N ⇛ N′` 并且替换 `σ` 逐点（Pointwise）平行规约至 `τ`， +如果 `N ⇛ N′` 并且替换 `σ` 逐点（Pointwise）平行归约至 `τ`， 则 `subst σ N ⇛ subst τ N′`。 -我们如下定义逐点平行规约。 +我们如下定义逐点平行归约。 ```agda par-subst : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set @@ -467,8 +467,8 @@ are straightforward so we just consider the last one for `pbeta`. * 假定 `(ƛ N) · M ⇛ N′ [ M′ ]` 因为 `N ⇛ N′` 和 `M ⇛ M′`。 根据归纳假设，我们有 `rename (ext ρ) N ⇛ rename (ext ρ) N′` 和 `rename ρ M ⇛ rename ρ M′`。 所以根据 `pbeta` 我们有 `(ƛ rename (ext ρ) N) · (rename ρ M) ⇛ (rename (ext ρ) N) [ rename ρ M ]`。 - 然而，为了得出结论我们需要平行规约至 `rename ρ (N [ M ])`。 - 值得庆幸的是，重命名和规约可以相互交换。 + 然而，为了得出结论我们需要平行归约至 `rename ρ (N [ M ])`。 + 值得庆幸的是，重命名和归约可以相互交换。 -为了证明替换遵从平行规约关系，我们需要证明的下一个引理如下文所示， -它声称同时规约可以与单步规约相交换。 +为了证明替换遵从平行归约关系，我们需要证明的下一个引理如下文所示， +它声称同时归约可以与单步归约相交换。 我们从 [Substitution](/Substitution/) 章节导入这个引理， 并重申如下。 @@ -511,7 +511,7 @@ subst-commute {N = N} = plfa.part2.Substitution.subst-commute {N = N} We are ready to prove that substitution respects parallel reduction. --> -我们准备好去证明替换遵从平行规约。 +我们准备好去证明替换遵从平行归约。 ```agda subst-par : ∀{Γ Δ A} {σ τ : Subst Γ Δ} {M M′ : Γ ⊢ A} @@ -582,13 +582,13 @@ We proceed by induction on `M ⇛ M′`. 同样我们根据 `par-subst-exts` 来得到 `par-subst (exts σ) (exts τ)`。 所以根据归纳假设，我们有 `subst (exts σ) N ⇛ subst (exts τ) N′` 和 `subst σ M ⇛ subst τ M′`。 - 接着根据 `pbeta` 规则，我们平行规约至 `subst (exts τ) N′ [ subst τ M′ ]`。 + 接着根据 `pbeta` 规则，我们平行归约至 `subst (exts τ) N′ [ subst τ M′ ]`。 替换在以下意义中与自身交换： 对于任意 σ、 N 和 M， 我们有 (subst (exts σ) N) [ subst σ M ] ≡ subst σ (N [ M ]) - 所以我们平行规约得到 `subst τ (N′ [ M′ ])`。 + 所以我们平行归约得到 `subst τ (N′ [ M′ ])`。 -显然，若 `M ⇛ M′`，则 `subst-zero M` 逐点平行规约至 `subst-zero M′`。 +显然，若 `M ⇛ M′`，则 `subst-zero M` 逐点平行归约至 `subst-zero M′`。 ```agda par-subst-zero : ∀{Γ}{A}{M M′ : Γ ⊢ A} @@ -611,7 +611,7 @@ We conclude this section with the desired corollary, that substitution respects parallel reduction. --> -我们以所期望的推论来结束本节，即替换遵从平行规约。 +我们以所期望的推论来结束本节，即替换遵从平行归约。 ```agda sub-par : ∀{Γ A B} {N N′ : Γ , A ⊢ B} {M M′ : Γ ⊢ A} @@ -626,7 +626,7 @@ sub-par pn pm = subst-par (par-subst-zero pm) pn ## Parallel reduction satisfies the diamond property --> -## 平行规约满足菱形性质 +## 平行归约满足菱形性质 -## 平行规约合流性的证明 +## 平行归约合流性的证明 -像在开始承诺的那样，平行规约合流性的证明现在十分简单， +像在开始承诺的那样，平行归约合流性的证明现在十分简单， 因为我们知道它满足三角性质。 我们只需证明带状引理（Strip Lemma），它声称若有 `M ⇛ N` 和 `M ⇛* N′`， 则对于某个 `L` 有 `N ⇛* L` 和 `N′ ⇛ L`。 @@ -857,7 +857,7 @@ induction on the sequence `M ⇛* N`, using the above lemma in the induction step. --> -平行规约合流性的证明现在通过对序列 `M ⇛* N` 归纳来完成，并在归纳步骤使用上述引理。 +平行归约合流性的证明现在通过对序列 `M ⇛* N` 归纳来完成，并在归纳步骤使用上述引理。 ```agda par-confluence : ∀{Γ A} {L M₁ M₂ : Γ ⊢ A} @@ -908,7 +908,7 @@ induction. ## Proof of confluence for reduction --> -## 规约合流性的证明 +## 归约合流性的证明 -规约的合流性是平行规约合流性的一个推论。 +归约的合流性是平行归约合流性的一个推论。 从 `L —↠ M₁` 和 `L —↠ M₂` 根据 `betas-pars` 我们有 `L ⇛* M₁` 和 `L ⇛* M₂`。 接着根据合流性我们得到对于某个 `L` 有 `M₁ ⇛* N` 和 `M₂ ⇛* N`。 因此我们根据 `pars-betas` 得出 `M₁ —↠ N` 和 `M₂ —↠ N`。 diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index fe3f6973d..cf594309a 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -378,7 +378,7 @@ incorporates preservation, which no longer requires a separate proof. 项的语法现在包含了它们的赋型规则。 替换的定义现在更加深入，但包括了之前证明中最棘手的部分，即替换保留了类型。 -规约的定义现在包括了保型性，不需要额外的证明。 +归约的定义现在包括了保型性，不需要额外的证明。 -## 规约 +## 归约 -规约规则和之前给出的类似，除去我们必须给出每个项的类型。 -如同之前，兼容性规则规约一个项的一部分，用 `ξ` 标出； +归约规则和之前给出的类似，除去我们必须给出每个项的类型。 +如同之前，兼容性规则归约一个项的一部分，用 `ξ` 标出； 简化构造子与其解构子的规则用 `β` 标出： ```agda @@ -1456,7 +1456,7 @@ definition of substitution. 定义中指出，`M —→ N` 只能由类型**都**是 `Γ ⊢ A` 的两个项 `M` 和 `N` 组成， 其中 `Γ` 是一个语境，`A` 是一个类型。 -换句话说，我们的定义中**内置**了规约保存类型的证明。 +换句话说，我们的定义中**内置**了归约保存类型的证明。 我们不需要额外证明保型性。 Agda 的类型检查器检验了每个项保存了类型。 在 `β` 规则的情况中，保型性依赖于替换保存类型的性质，而它内置于替换的定义之中。 @@ -1543,7 +1543,7 @@ As before, we need to supply an explicit context to `` `zero ``. Next, a sample reduction demonstrating that two plus two is four: --> -接下来，展示二加二得四的规约例子： +接下来，展示二加二得四的归约例子： ```agda _ : plus {∅} · two · two —↠ `suc `suc `suc `suc `zero @@ -1582,7 +1582,7 @@ _ = And finally, a similar sample reduction for Church numerals: --> -最后，用 Church 数规约同样的例子： +最后，用 Church 数归约同样的例子： ```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero {∅} @@ -1620,7 +1620,7 @@ _ = ## Values do not reduce --> -## 值不再规约 +## 值不再归约 -使用上文的表示方法，证明值不再规约；以及它的推论：可规约的项不是值。 +使用上文的表示方法，证明值不再归约；以及它的推论：可归约的项不是值。 @@ -1666,7 +1666,7 @@ a value or takes a reduction step. The formulation of progress is just as before, but annotated with types: --> -和之前一样，每一个良类型的闭项要么是一个值，要么可以进行规约。 +和之前一样，每一个良类型的闭项要么是一个值，要么可以进行归约。 可进性的形式化与之前一样，但是附上了类型： ```agda @@ -1724,7 +1724,7 @@ refer to preservation, since it is built-in to the definition of reduction. --> 之前，我们将保型性和可进性结合来对一个项求值。 -我们在此处也可以这么做，但是我们不再需要显式地参考保型性，因为它内置于规约的定义中。 +我们在此处也可以这么做，但是我们不再需要显式地参考保型性，因为它内置于归约的定义中。 -给定类型为 `A` 的项 `L`，求值器会返回一个从 `L` 到某个 `N` 的求值序列，并提示规约是否完成： +给定类型为 `A` 的项 `L`，求值器会返回一个从 `L` 到某个 `N` 的求值序列，并提示归约是否完成： ```agda data Steps {A} : ∅ ⊢ A → Set where @@ -1826,7 +1826,7 @@ To compute the first three steps of the infinite reduction sequence, we evaluate with three steps worth of gas: --> -为了计算无限规约序列的前三步，我们使用满足三步的汽油： +为了计算无限归约序列的前三步，我们使用满足三步的汽油： ```agda _ : eval (gas 3) sucμ ≡ @@ -2083,7 +2083,7 @@ We omit the proof that reduction is deterministic, since it is tedious and almost identical to the previous proof. --> -我们省去规约是确定的证明，因为它很繁琐，而且与之前的证明几乎完全相同。 +我们省去归约是确定的证明，因为它很繁琐，而且与之前的证明几乎完全相同。 -会规约为 `` `suc `suc `suc `suc `zero ``。 +会归约为 `` `suc `suc `suc `suc `zero ``。 -会规约为 `` `suc `suc `suc `suc `zero ``。 +会归约为 `` `suc `suc `suc `suc `zero ``。 Agda 会抱怨它无法为隐式参数找到一个底类型的值。 -注意此处隐式参数的类型在 `t` 不是变量时会规约至 `⊥`。 +注意此处隐式参数的类型在 `t` 不是变量时会归约至 `⊥`。 我们将没有自由变量的项叫做**闭项**，否则它是一个**开项**。 -上面的三个项中，第一个是闭项，剩下两个是开项。我们在讨论规约时，会注重闭项。 +上面的三个项中，第一个是闭项，剩下两个是开项。我们在讨论归约时，会注重闭项。 -## 规约 +## 归约 -我们接下来给出 λ-演算的传值规约规则。 -规约一个应用时，我们首先规约左手边，直到它变成一个值（必须是抽象）； -接下来我们规约右手边，直到它变成一个值； +我们接下来给出 λ-演算的传值归约规则。 +归约一个应用时，我们首先归约左手边，直到它变成一个值（必须是抽象）； +接下来我们归约右手边，直到它变成一个值； 最后我们使用替换，把变量替换成参数。 -在非正式的操作语言表达中，我们可以如下写出应用的规约规则： +在非正式的操作语言表达中，我们可以如下写出应用的归约规则： L —→ L′ --------------- ξ-·₁ @@ -1029,9 +1029,9 @@ letter `β` (_beta_) and such rules are traditionally called _beta rules_. --> 规则可以分为两类。 -兼容性规则让我们规约一个项的一部分。我们用希腊字母 `ξ` （_xi_）开头的规则表示。 -当一个项规约到足够的时候，它将会包括一个构造子和一个解构子，在这里是 `ƛ` 和 `·`， -我们可以直接规约。这样的规则我们用希腊字母 `β` （_beta_）表示，也被称为 **β-规则**。 +兼容性规则让我们归约一个项的一部分。我们用希腊字母 `ξ` （_xi_）开头的规则表示。 +当一个项归约到足够的时候，它将会包括一个构造子和一个解构子，在这里是 `ƛ` 和 `·`， +我们可以直接归约。这样的规则我们用希腊字母 `β` （_beta_）表示，也被称为 **β-规则**。 -一些额外的术语：可以匹配规约规则左手边的项被称之为**可规约项（Redex）**。 -在可规约项 `(ƛ x ⇒ N) · V` 中，我们把 `x` 叫做函数的**形式参数（形参，Formal Parameter）**， +一些额外的术语：可以匹配归约规则左手边的项被称之为**可归约项（Redex）**。 +在可归约项 `(ƛ x ⇒ N) · V` 中，我们把 `x` 叫做函数的**形式参数（形参，Formal Parameter）**， 把 `V` 叫做函数应用的**实际参数（实参，Actual Parameter）**。 -β-规约将形参用实参来替换。 +β-归约将形参用实参来替换。 -如果一个项已经是一个值，它就没有可以规约的规则； -反过来说，如果一个项可以被规约，那么它就不是一个值。 -我们在下一章里证明这概括了所有的情况——所以良类型的项要么可以规约要么是一个值。 +如果一个项已经是一个值，它就没有可以归约的规则； +反过来说，如果一个项可以被归约，那么它就不是一个值。 +我们在下一章里证明这概括了所有的情况——所以良类型的项要么可以归约要么是一个值。 -对于数字来说，零不可以规约，后继可以对它的子项进行规约。 -匹配表达式先将它的参数规约至一个数字，然后根据它是零还是后继选择相应的分支。 +对于数字来说，零不可以归约，后继可以对它的子项进行归约。 +匹配表达式先将它的参数归约至一个数字，然后根据它是零还是后继选择相应的分支。 不动点会把约束变量替换成整个不动点项——这是我们唯一一处用项、而不是值进行的替换。 -我们小心地设计这些规约规则，使得一个项的子项在整项被规约之前先被规约。 -这被称为**传值（Call-by-value）**规约。 +我们小心地设计这些归约规则，使得一个项的子项在整项被归约之前先被归约。 +这被称为**传值（Call-by-value）**归约。 -除此之外，我们规定规约的顺序是从左向右的。 -这意味着规约是**确定的（Deterministic）**：对于任何一个项，最多存在一个可以被规约至的项。 -换句话说，我们的规约关系 `—→` 实际上是一个函数。 +除此之外，我们规定归约的顺序是从左向右的。 +这意味着归约是**确定的（Deterministic）**：对于任何一个项，最多存在一个可以被归约至的项。 +换句话说，我们的归约关系 `—→` 实际上是一个函数。 这种解释项的含义的方法叫做**小步操作语义（Small-step Operational Semantics）**。 -如果 `M —→ N`，我们称之为项 `M` **规约**至项 `N`，也称之为项 `M` **步进（Step to）**至项 `N`。 -每条兼容性规则以另一条规约规则作为前提；因此每一步都会用到一条 β-规则，用零或多条兼容性规则进行调整。 +如果 `M —→ N`，我们称之为项 `M` **归约**至项 `N`，也称之为项 `M` **步进（Step to）**至项 `N`。 +每条兼容性规则以另一条归约规则作为前提；因此每一步都会用到一条 β-规则，用零或多条兼容性规则进行调整。 步进并不是故事的全部。 -总的来说，对于一个封闭的项，我们想要对它反复地步进，直到规约至一个值。 +总的来说，对于一个封闭的项，我们想要对它反复地步进，直到归约至一个值。 这样可以用定义步进关系 `—→` 的自反传递闭包 `—↠` 来完成。 -* 对于项 `M`，我们可以一步也不规约而得到类型为 `M —↠ M` 的步骤，写作 `M ∎`。 +* 对于项 `M`，我们可以一步也不归约而得到类型为 `M —↠ M` 的步骤，写作 `M ∎`。 -在下一部分我们可以看到，这样的记法可以让我们用清晰的步骤来表示规约的例子。 +在下一部分我们可以看到，这样的记法可以让我们用清晰的步骤来表示归约的例子。 -在讨论规约关系时，有一个重要的性质是**合流性（Confluence）**。 -如果项 `L` 规约至两个项 `M` 和项 `N`，那么它们都可以规约至同一个项 `P`。 +在讨论归约关系时，有一个重要的性质是**合流性（Confluence）**。 +如果项 `L` 归约至两个项 `M` 和项 `N`，那么它们都可以归约至同一个项 `P`。 我们可以用下面的图来展示这个性质： L @@ -1391,8 +1391,8 @@ steps it is called the diamond property. In symbols: --> 图中，`L`、`M` 和 `N` 由全称量词涵盖，而 `P` 由存在量词涵盖。 -如果图中的每条线代表了零或多步规约步骤，这样的性质被称为合流性。 -如果上面的两条线代表一步规约步骤，下面的两条线代表零或多步规约步骤， +如果图中的每条线代表了零或多步归约步骤，这样的性质被称为合流性。 +如果上面的两条线代表一步归约步骤，下面的两条线代表零或多步归约步骤， 这样的性质被称为菱形性质（Diamond Property）。用符号表示为： ```agda @@ -1413,7 +1413,7 @@ The reduction system studied in this chapter is deterministic. In symbols: --> -在本章中我们讨论的规约系统是确定的。用符号表示为： +在本章中我们讨论的归约系统是确定的。用符号表示为： ```agda postulate @@ -1430,9 +1430,9 @@ the diamond and confluence properties. Hence, all the reduction systems studied in this text are trivially confluent. --> -我们可以简单地证明任何确定的规约关系满足菱形性质， -任何满足菱形性质的规约关系满足合流性。 -因此，我们研究的规约系统平凡地满足了合流性。 +我们可以简单地证明任何确定的归约关系满足菱形性质， +任何满足菱形性质的归约关系满足合流性。 +因此，我们研究的归约系统平凡地满足了合流性。 -下面的例子中我们规约二加二至四： +下面的例子中我们归约二加二至四： ```agda _ : plus · two · two —↠ `suc `suc `suc `suc `zero _ = @@ -1515,7 +1515,7 @@ _ = And here is a similar sample reduction for Church numerals: --> -我们用 Church 数规约同样的例子： +我们用 Church 数归约同样的例子： ```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero _ = @@ -1554,7 +1554,7 @@ _ = In the next chapter, we will see how to compute such reduction sequences. --> -下一章节中，我们研究如何计算这样的规约序列。 +下一章节中，我们研究如何计算这样的归约序列。 -使用规约序列，证明一加一得二。 +使用归约序列，证明一加一得二。 @@ -1715,7 +1715,7 @@ we must first type its subterms, and in particular in the body of an abstraction its bound variable may appear free. --> -在规约时，我们只讨论封闭的项，但是在赋型时，我们必须考虑带有自由变量的项。 +在归约时，我们只讨论封闭的项，但是在赋型时，我们必须考虑带有自由变量的项。 给一个项赋型时，我们必须先给它的子项赋型。而在给一个抽象的抽象体赋型时， 抽象的约束变量在抽象体内部是自由的。 @@ -2415,5 +2415,5 @@ We compose reduction `—→` from an em dash `—` and an arrow `→`. Similarly for reflexive and transitive closure `—↠`. --> -我们用短划 `—` 和箭头 `→` 来构造规约 `—→`。 +我们用短划 `—` 和箭头 `→` 来构造归约 `—→`。 自反传递闭包 `—↠` 也类似。 diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md index 13d60cc3d..7ebde9702 100644 --- a/src/plfa/part2/More.lagda.md +++ b/src/plfa/part2/More.lagda.md @@ -74,7 +74,7 @@ correctness of translations will be the subject of the next chapter. --> 到现在，使用符号来解释应该可以比文字更简洁、更精确、更易于跟随。 -对于每一种构造，我们给出它的语法、赋型、规约和例子。 +对于每一种构造，我们给出它的语法、赋型、归约和例子。 在需要的时候，我们也会给出构造的翻译；在下个章节我们会正式地证明翻译的正确性。 -### 规约 +### 归约 -### 规约 +### 归约 M —→ M′ --------------------------------------- ξ-let @@ -349,7 +349,7 @@ construct to a calculus without the construct. ### Reduction --> -### 规约 +### 归约 M —→ M′ ------------------------- ξ-⟨,⟩₁ @@ -404,7 +404,7 @@ and reduction rules: 与其使用两种消去积类型的方法，我们可以使用一个匹配表达式来同时绑定两个变量， 作为积的替代表示方法。 -我们重复完整的语法，但只给出新的赋型和规约规则： +我们重复完整的语法，但只给出新的赋型和归约规则： -### 规约 +### 归约 L —→ L′ --------------------------------------------------- ξ-case× @@ -534,9 +534,9 @@ and `` `proj₂ `` many times or not at all. --> 但是这样的话它们表现的不一样。 -第一项总是在规约 `N` 之前规约 `L`，它只计算 `` `proj₁ `` 和 `` `proj₂ ``一次。 -第二项在规约 `N` 之前不先将 `L` 规约至值，取决于 `x` 和 `y` 在 `N` 中出现的次数， -它将规约 `L` 很多次或者根本不规约，因此它会计算 `` `proj₁ `` 和 `` `proj₂ `` +第一项总是在归约 `N` 之前归约 `L`，它只计算 `` `proj₁ `` 和 `` `proj₂ ``一次。 +第二项在归约 `N` 之前不先将 `L` 归约至值，取决于 `x` 和 `y` 在 `N` 中出现的次数， +它将归约 `L` 很多次或者根本不归约，因此它会计算 `` `proj₁ `` 和 `` `proj₂ `` 很多次或者根本不计算。 -### 规约 +### 归约 M —→ M′ ------------------- ξ-inj₁ @@ -677,7 +677,7 @@ There are no reduction rules. --> 对于单元类型来说，有一种方法引入单元类型，但是没有消去单元类型的方法。 -单元类型没有规约规则。 +单元类型没有归约规则。 -### 规约 +### 归约 -### 规约 +### 归约 L —→ L′ ------------------------------------- ξ-case⊤ @@ -875,7 +875,7 @@ construct plays a role similar to `⊥-elim` in Agda: --> 对于空类型来说，只有一种消去此类型的值的方法，但是没有引入此类型的值的方法。 -没有空类型的值，也没有规约规则，但是有 β 规则。 +没有空类型的值，也没有归约规则，但是有 β 规则。 `case⊥` 构造和 Agda 中的 `⊥-elim` 的作用相似： -### 规约 +### 归约 L —→ L′ ------------------------- ξ-case⊥ @@ -1023,7 +1023,7 @@ Here is the isomorphism between `A` and ``A `⊎ `⊥``: ### Reduction --> -### 规约 +### 归约 M —→ M′ ----------------- ξ-∷₁ @@ -1576,7 +1576,7 @@ not fixed by the given arguments. ## Reduction --> -## 规约 +## 归约 -## 值不再规约 +## 值不再归约 ```agda V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A} diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index 96d2d1fbd..f3b63ea23 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -87,7 +87,7 @@ a reduction step. As we will see, this property does _not_ hold for every term, but it does hold for every closed, well-typed term. --> -我们可能会希望任意一个项要么是一个值，要么可以进行一步规约。 +我们可能会希望任意一个项要么是一个值，要么可以进行一步归约。 我们将会看到，此性质**并不**对所有项都成立，但对于所有良类型的闭项成立。 -所以要么我们有一个值，这时我们已经完成了规约；要么我们可以进行一步规约。 +所以要么我们有一个值，这时我们已经完成了归约；要么我们可以进行一步归约。 当处于后者的情况时，我们想要再一次应用可进性。 -但这样做需要我们首先知道通过规约得到的项本身是良类型的闭项。 -事实上，只要我们规约的起点是一个良类型的闭项，所得到的项就满足这个性质。 +但这样做需要我们首先知道通过归约得到的项本身是良类型的闭项。 +事实上，只要我们归约的起点是一个良类型的闭项，所得到的项就满足这个性质。 -## 值无法被规约 +## 值无法被归约 -我们从一个简单的观察开始。值无法被规约： +我们从一个简单的观察开始。值无法被归约： ```agda V¬—→ : ∀ {M N} @@ -193,18 +193,18 @@ We consider the three possibilities for values: that reduces, which by induction cannot occur. --> -* 如果它是一个 λ-抽象，那么不会匹配任何规约规则 +* 如果它是一个 λ-抽象，那么不会匹配任何归约规则 -* 如果它是零，也不会匹配任何规约规则 +* 如果它是零，也不会匹配任何归约规则 * 如果它是一个数的后继，那么它可能可以与规则 `ξ-suc` 相匹配， - 但由归纳证明它作为值本身还能进行规约的情况是不可能发生的。 + 但由归纳证明它作为值本身还能进行归约的情况是不可能发生的。 -作为推论，可以再进行规约的项不是值： +作为推论，可以再进行归约的项不是值： ```agda —→¬V : ∀ {M N} @@ -295,7 +295,7 @@ We would like to show that every term is either a value or takes a reduction step. However, this is not true in general. The term --> -我们可能希望任意一个项要么是值，要么可以进行一步规约。 +我们可能希望任意一个项要么是值，要么可以进行一步归约。 但并不是所有情况都是这样。考虑这样的项 `zero · `suc `zero @@ -305,7 +305,7 @@ is neither a value nor can take a reduction step. And if `` "s" ⦂ `ℕ ⇒ ` then the term --> -既不是一个值也无法进行一步规约。另外，如果 `` "s" ⦂ `ℕ ⇒ `ℕ ``，那么项 +既不是一个值也无法进行一步归约。另外，如果 `` "s" ⦂ `ℕ ⇒ `ℕ ``，那么项 ` "s" · `zero @@ -316,7 +316,7 @@ second has a free variable. Every term that is well typed and closed has the desired property. --> -也无法被规约，因为我们不知道哪个函数被绑定到了自由变量 `"s"` 上。 +也无法被归约，因为我们不知道哪个函数被绑定到了自由变量 `"s"` 上。 上述例子中的第一个项是不良类型的，第二个项包含一个自由变量。 只有良类型的闭项才有如下求证的性质： @@ -355,8 +355,8 @@ exists a term `N` such that `M —→ N`, or if it is done, meaning that `M` is a value. --> -一个进行的项 `M` 要么可以进行一步规约，这意味着存在一个项 `N` 使得 `M —→ N`， -要么已经完成了规约，这意味着 `M` 是一个值。 +一个进行的项 `M` 要么可以进行一步归约，这意味着存在一个项 `N` 使得 `M —→ N`， +要么已经完成了归约，这意味着 `M` 是一个值。 - - 如果这个项还能够进行一步规约，我们就有了 `M —→ M′` 的论据，再由 `ξ-·₂`， - 可知原来的项进行到 `L′ · M`。要应用规约步骤 `ξ-·₂` 需要我们提供项 `L` 是 + - 如果这个项还能够进行一步归约，我们就有了 `M —→ M′` 的论据，再由 `ξ-·₂`， + 可知原来的项进行到 `L′ · M`。要应用归约步骤 `ξ-·₂` 需要我们提供项 `L` 是 一个值的论据，而之前对子项可进性的分析已经提供了需要的证明。 - - 如果这个项的规约结束了，我们便有了项 `M` 是一个值的论据。 - 因此原来的项可以使用 `β-ƛ` 来进行一步规约。 + - 如果这个项的归约结束了，我们便有了项 `M` 是一个值的论据。 + 因此原来的项可以使用 `β-ƛ` 来进行一步归约。 -剩下的情况都很类似。如果我们由归纳得到了一个可以继续进行规约的 -情况 `step` 则应用一条 `ξ` 规则；如果得到的是已经完成规约的 +剩下的情况都很类似。如果我们由归纳得到了一个可以继续进行归约的 +情况 `step` 则应用一条 `ξ` 规则；如果得到的是已经完成归约的 情况 `done` 则要么我们已经得到了一个值，要么应用一条 `β` 规则。 对于不动点，由于可以直接应用所对应的 `β` 规则，不需要再做归纳。 @@ -505,7 +505,7 @@ determine its bound variable and body, `ƛ x ⇒ N`, so we can show that 比起有助于记忆的 `done` 与 `step`，现在我们只能用 `inj₁` 和 `inj₂`； 同时项 `N` 也不再是隐式的，从而我们需要将其完整写出。 当遇到 `β-ƛ` 的情况时，需要我们对 λ-表达式 `L` 做匹配，以决定它的约束变量和函数体， -也就是形如 `ƛ x ⇒ N` 的形式，从而我们才能证明项 `L · M` 规约到了 `N [ x := M ]`。 +也就是形如 `ƛ x ⇒ N` 的形式，从而我们才能证明项 `L · M` 归约到了 `N [ x := M ]`。 -规约过程保持类型是我们所期望去证明的另一个性质， +归约过程保持类型是我们所期望去证明的另一个性质， 而事实上这需要做一定程度的准备工作。 在证明中有三个关键步骤。 @@ -707,7 +707,7 @@ the substitution lemma is crucial in showing that each of the `β` rules that uses substitution preserves types. --> -我们对所有可能的规约步骤进行归纳来证明保型性， +我们对所有可能的归约步骤进行归纳来证明保型性， 在证明的过程中替换引理起到了重要的作用， 它论证了在替换过程中用到的每一条 `β`-规则都保留了类型。 @@ -1023,7 +1023,7 @@ variables the context grows. So for the induction to go through, we require an arbitrary context `Γ`, as in the statement of the lemma. --> -我们所关注的是规约闭项，这意味着每当我们应用 `β`-规约时， +我们所关注的是归约闭项，这意味着每当我们应用 `β`-归约时， 所替换的项只含有一个自由变量（也就是所对应 λ-抽象、 对自然数分项或不动点表达式的绑定变量）。然而，替换是通过 递归定义的，在我们逐层深入项时遇到的绑定变量增长了语境。 @@ -1404,7 +1404,7 @@ Once we have shown that substitution preserves types, showing that reduction preserves types is straightforward: --> -一旦我们证明了替换保持类型，证明规约保持类型是简单的： +一旦我们证明了替换保持类型，证明归约保持类型是简单的： ```agda preserve : ∀ {M N A} @@ -1437,7 +1437,7 @@ so in what follows we choose type name as convenient. Let's unpack the cases for two of the reduction rules: --> -让我们分析规约规则的两种情况： +让我们分析归约规则的两种情况： -一些项将永远规约下去。这是一个例子： +一些项将永远归约下去。这是一个例子： ```agda sucμ = μ "x" ⇒ `suc (` "x") @@ -1577,9 +1577,9 @@ number of reduction steps. --> 由于每个 Agda 计算都必须终止， -我们不能仅仅要求 Agda 将项规约为值。 +我们不能仅仅要求 Agda 将项归约为值。 相反，我们将向 Agda 提供一个自然数， -并允许它在需要比给定的数更多的规约步骤时终止规约。 +并允许它在需要比给定的数更多的归约步骤时终止归约。 以此类推，我们将使用**燃料**作为参数的名称， -该参数限制了规约步骤的数量。`Gas` 由一个自然数指定。 +该参数限制了归约步骤的数量。`Gas` 由一个自然数指定。 ```agda record Gas : Set where @@ -1648,7 +1648,7 @@ reduction finished: --> 给定一个类型为 `A` 的项 `L`，对于某个 `N`， -求值器将返回从 `L` 到 `N` 的规约序列以及规约是否完成的指示： +求值器将返回从 `L` 到 `N` 的归约序列以及归约是否完成的指示： ```agda data Steps (L : Term) : Set where @@ -1687,7 +1687,7 @@ evidence that `L` is well typed. We consider the amount of gas remaining. There are two possibilities: --> -令 `L` 是我们要规约的项的名称，`⊢L` 是项 `L` 是良类型的论据。 +令 `L` 是我们要归约的项的名称，`⊢L` 是项 `L` 是良类型的论据。 我们考虑剩余的燃料量。此处有两种可能： -* 如果是零，则我们过早地停止了。我们将返回简单的规约序列 `L —↠ L`， +* 如果是零，则我们过早地停止了。我们将返回简单的归约序列 `L —↠ L`， 并标明我们用尽了燃料。 @@ -1715,7 +1715,7 @@ remaining. There are two possibilities: --> + 项 `L` 是一个值，则我们已经完成了。 - 我们将返回简单的规约序列 `L —↠ L`，以及 `L` 是值的论据。 + 我们将返回简单的归约序列 `L —↠ L`，以及 `L` 是值的论据。 -现在我们可以用 Agda 来计算之前给出的不停机的规约序列。 +现在我们可以用 Agda 来计算之前给出的不停机的归约序列。 首先我们证明项 `sucμ` 是良赋型的： ```agda @@ -1761,7 +1761,7 @@ sequence, we evaluate with three steps worth of gas: --> 我们花三步量的燃料来进行求值， -以展示这个无穷规约序列的前三步： +以展示这个无穷归约序列的前三步： ```agda _ : eval (gas 3) ⊢sucμ ≡ @@ -1784,7 +1784,7 @@ in the previous chapter. We start with the Church numeral two applied to successor and zero. Supplying 100 steps of gas is more than enough: --> -类似地，我们可以用 Agda 计算前一章节中给出的规约序列。 +类似地，我们可以用 Agda 计算前一章节中给出的归约序列。 我们从计算 Church 表示法表示数字的数字二应用到后继和数字零开始。 提供 100 步量的燃料就已远超过需求了： @@ -1816,7 +1816,7 @@ writing `twoᶜ` and `sucᶜ` in place of their expansions. --> 上面的例子是通过首先使用组合键 `C-c C-n` 来范式化等式的左侧， -然后将结果粘贴到等式右侧的方式生成的。前一章中规约的例子便是 +然后将结果粘贴到等式右侧的方式生成的。前一章中归约的例子便是 通过使用这一方式导出结果、重新排版并且将展开的表达式对应地重 写为 `twoᶜ` 和 `sucᶜ` 的形式得到的。 @@ -2130,9 +2130,9 @@ Find two counter-examples to subject expansion, one with case expressions and one not involving case expressions. --> -如果 `M —→ N`，我们便称 `M` **规约**至 `N`， +如果 `M —→ N`，我们便称 `M` **归约**至 `N`， 相同的情形也被称作 `N` **扩展（Expand）**至 `M`。 -保型性有时也被叫做**子规约（Subject Reduction）**。 +保型性有时也被叫做**子归约（Subject Reduction）**。 它的对应是**子扩展（Subject Expansion）**， 如果 `M —→ N` 和 `∅ ⊢ N ⦂ A` 蕴含 `∅ ⊢ M ⦂ A`。 找到两个子扩展的反例，一个涉及 `case` 表达式而另一个不涉及。 @@ -2154,7 +2154,7 @@ with case expressions and one not involving case expressions. A term is _normal_ if it cannot reduce: --> -一个项是**范式**，如果它不能被规约。 +一个项是**范式**，如果它不能被归约。 ```agda Normal : Term → Set @@ -2273,7 +2273,7 @@ Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` abo ## Reduction is deterministic --> -## 规约是确定的 +## 归约是确定的 -现在证明规约是确定的十分简单。 +现在证明归约是确定的十分简单。 ```agda det : ∀ {M M′ M″} @@ -2338,7 +2338,7 @@ The proof is by induction over possible reductions. We consider three typical cases: --> -证明通过对可能的规约进行归纳来完成。我们考虑三种典型的情况： +证明通过对可能的归约进行归纳来完成。我们考虑三种典型的情况： - 左侧的规则要求 `L` 被规约，但右侧的规则要求 `L` 是一个值。 - 这是一个矛盾，因为值无法被规约。如果值的约束从 `ξ-·₂` 或任何其他规约规则中被移除， + 左侧的规则要求 `L` 被归约，但右侧的规则要求 `L` 是一个值。 + 这是一个矛盾，因为值无法被归约。如果值的约束从 `ξ-·₂` 或任何其他归约规则中被移除， 那么确定性将不再适用。 -假设我们加入了一个新项 `zap` 以及以下规约规则 +假设我们加入了一个新项 `zap` 以及以下归约规则 -------- β-zap M —→ zap @@ -2482,7 +2482,7 @@ Suppose instead that we add a new term `foo` with the following reduction rules: --> -假设我们加入了一个新项 `foo` 以及以下规约规则： +假设我们加入了一个新项 `foo` 以及以下归约规则： ------------------ β-foo₁ (λ x ⇒ ` x) —→ foo diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index b2bedf669..e63aaaf17 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -36,8 +36,8 @@ In this chapter we play with variations on a theme: where reduction continues underneath a lambda. --> -* 之前的章节中讨论了**弱头部范式**（Weak Head Normal Form），其规约止步于 - λ 抽象；我们这次讨论**完全正规化**（Full Normalisation），其在 λ 抽象之下仍然继续规约。 +* 之前的章节中讨论了**弱头部范式**（Weak Head Normal Form），其归约止步于 + λ 抽象；我们这次讨论**完全正规化**（Full Normalisation），其在 λ 抽象之下仍然继续归约。 -* 之前的章节中讨论了**确定性**（Deterministic）的规约，每个项中至多有一个可规约项； - 我们这次讨论**非确定性**（Non-deterministic）的规约，每个项中可能有多个可规约项，而每一个都可规约。 +* 之前的章节中讨论了**确定性**（Deterministic）的归约，每个项中至多有一个可归约项； + 我们这次讨论**非确定性**（Non-deterministic）的归约，每个项中可能有多个可归约项，而每一个都可归约。 -在之前，我们在遇到 λ 抽象时停止规约，因此我们需要计算 +在之前，我们在遇到 λ 抽象时停止归约，因此我们需要计算 `` plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero `` -来确保我们规约至自然数四。 -现在，规约在 λ 之下继续进行，所以我们不需要额外的参数。 +来确保我们归约至自然数四。 +现在，归约在 λ 之下继续进行，所以我们不需要额外的参数。 为了便利，我们定义用 Church 数来表示二和四的项。 -## 规约步骤 +## 归约步骤 -规约规则从传值调用改为传名调用，以实现完全范式化： +归约规则从传值调用改为传名调用，以实现完全范式化： * 规则 `ξ₂` 之中，项 `L` 是值的要求现在被丢弃了。 - 所以这条规则现在与 `ξ₁` 重合，且规约是**非确定的**。 - 现在可选择规约 `L` 或者 `M` 中的项。 + 所以这条规则现在与 `ξ₁` 重合，且归约是**非确定的**。 + 现在可选择归约 `L` 或者 `M` 中的项。 * 规则 `β` 之中，参数是值的要求现在被丢弃了，对应了传名调用的求值。 - 这引入了更多的非确定性，由于 `β` 与 `ξ₂` 在参数中有可规约项时重合。 + 这引入了更多的非确定性，由于 `β` 与 `ξ₂` 在参数中有可归约项时重合。 -* 额外了新规则 `ζ`，使得 λ 抽象下可以继续规约。 +* 额外了新规则 `ζ`，使得 λ 抽象下可以继续归约。 如果我们想要传值调用，但需要项范式化其中的项的话，要怎么样修改规则？ -假设 `β` 在除了两个项都是范式时，不允许规约。 +假设 `β` 在除了两个项都是范式时，不允许归约。 ```agda -- 请将代码写在此处。 @@ -717,9 +717,9 @@ permits reduction when both terms are values (that is, lambda abstractions). What would `2+2ᶜ` reduce to in this case? --> -如果我们想要传值调用，但项不在 λ 之下规约的话，要怎么样修改规则？ -假设 `β` 在双项均为值（即 λ 抽象）时允许规约。 -`2+2ᶜ` 在这种情况下会规约成什么？ +如果我们想要传值调用，但项不在 λ 之下归约的话，要怎么样修改规则？ +假设 `β` 在双项均为值（即 λ 抽象）时允许归约。 +`2+2ᶜ` 在这种情况下会归约成什么？ ```agda @@ -771,7 +771,7 @@ begin M—↠N = M—↠N ## Example reduction sequence --> -## 规约序列的例子 +## 归约序列的例子 -可进性相应地也变更了。之前我们说每个项要么是值，要么可以规约一步；我们现在说每个项要么是范式，要么可以规约一步。 +可进性相应地也变更了。之前我们说每个项要么是值，要么可以归约一步；我们现在说每个项要么是范式，要么可以归约一步。 -如果一个项可以规约一步，或其为范式，那么它具有可进性： +如果一个项可以归约一步，或其为范式，那么它具有可进性： ```agda data Progress {Γ A} (M : Γ ⊢ A) : Set where @@ -983,7 +983,7 @@ a reduction sequence from `L` to `N` and an indication of whether reduction finished: --> -给定类型 `A` 的项 `L`，求值器会对于某 `N` 返回自 `L` 至 `N` 的规约序列，并提示规约是否完成： +给定类型 `A` 的项 `L`，求值器会对于某 `N` 返回自 `L` 至 `N` 的归约序列，并提示归约是否完成： ```agda data Steps : ∀ {Γ A} → Γ ⊢ A → Set where @@ -1169,7 +1169,7 @@ Applying successor to the zero indeed reduces to the Scott numeral for one. --> -对零使用后继的确规约至 Scott 数表示的一： +对零使用后继的确归约至 Scott 数表示的一： ```agda _ : eval (gas 100) (`suc_ {∅} `zero) ≡ @@ -1247,8 +1247,8 @@ but they do both reduce to the same normal term. --> 由于 `` `suc `` 是定义的项，而不是原语项， -`plus · two · two` 不再规约至 `four`， -但是它们都规约至相同的范式。 +`plus · two · two` 不再归约至 `four`， +但是它们都归约至相同的范式。 -## 多步规约是传递的 +## 多步归约是传递的 在我们对自反传递闭包的形式化，即 `—↠` 关系中，没有出现直接的传递性规则。 -取而代之的是，这个关系模仿了列表形式，有一种空规约序列的情况，也有一种将一步规约加在规约序列之前的情况。 +取而代之的是，这个关系模仿了列表形式，有一种空归约序列的情况，也有一种将一步归约加在归约序列之前的情况。 下面是传递性的证明，其与列表的附加 `_++_` 函数的结构相似。 ```agda @@ -1358,7 +1358,7 @@ L —↠⟨ L—↠M ⟩ M—↠N = —↠-trans L—↠M M—↠N ## Multi-step reduction is a congruence --> -## 多步规约是合同性的 +## 多步归约是合同性的 -规则 `ξ₁` 、`ξ₂` 和 `ζ` 保证了规约关系对于无类型的 λ 演算满足合同性。 -多步规约也是一个合同关系，我们在下面三条引理中证明。 +规则 `ξ₁` 、`ξ₂` 和 `ζ` 保证了归约关系对于无类型的 λ 演算满足合同性。 +多步归约也是一个合同关系，我们在下面三条引理中证明。 ```agda appL-cong : ∀ {Γ} {L L' M : Γ ⊢ ★} @@ -1407,7 +1407,7 @@ The proof of `appL-cong` is by induction on the reduction sequence `L —↠ L'` facts together using `_—→⟨_⟩_`. --> -`appL-cong` 的证明对于规约序列 `L —↠ L'` 进行归纳。 +`appL-cong` 的证明对于归约序列 `L —↠ L'` 进行归纳。 * 若 `L —↠ L` 由 `L ∎` 成立。那我们可从 `L · M ∎` 得 `L · M —↠ L · M` 。 * 若 `L —↠ L''` 由 `L —→⟨ r ⟩ rs` 成立，那么 `L —→ L'` 由 `r` 成立，且 `L' —↠ L''` 由 `rs` 成立。 diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md index 238684d72..6599c119c 100644 --- a/src/plfa/part3/Compositional.lagda.md +++ b/src/plfa/part3/Compositional.lagda.md @@ -169,7 +169,7 @@ above. The inversion lemma is useful in proving that denotations are preserved by reduction. --> -λ-抽象的「反演引理」是上面定理的一种特例。反演引理在证明「规约会保持指称不变」时会很有用。 +λ-抽象的「反演引理」是上面定理的一种特例。反演引理在证明「归约会保持指称不变」时会很有用。 ```agda lambda-inversion : ∀{Γ}{γ : Env Γ}{N : Γ , ★ ⊢ ★}{v₁ v₂ : Value} diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index ad90ce524..387a86c60 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -654,7 +654,7 @@ the result of the application is `⊥`. --> 你可能会担心这种语义是否可以处理发散的程序。值 `⊥` 和规则 `⊥-intro` -提供了一种处理它们的方法（`⊥-intro` 规则也是 β-规约能够应用于不停机参数的原因）。 +提供了一种处理它们的方法（`⊥-intro` 规则也是 β-归约能够应用于不停机参数的原因）。 经典的 `Ω` 程序是一个特别简单的发散程序，它将 `Δ` 应用于自身，语义赋予 `Ω` 含义 `⊥`。有多种方法可以得出它，我们将从使用 `⊔-intro` 规则的方法开始。 首先，`denot-Δ` 告诉我们 `Δ` 的计算结果为 `((⊥ ↦ ⊥) ⊔ ⊥) ↦ ⊥`（选择 @@ -919,7 +919,7 @@ make, but they usually boil down to a single bit of information: * termination: the program `M` halts. --> -接下来我们研究指称语义和规约语义是否等价。回想一下，一个语言的语义的作用， +接下来我们研究指称语义和归约语义是否等价。回想一下，一个语言的语义的作用， 就是描述给定程序 `M` 的可观测行为。对于 λ-演算，我们可以做出多种选择， 但它们通常可以归结为一点信息： @@ -933,7 +933,7 @@ We can characterize divergence and termination in terms of reduction. * termination: `M —↠ ƛ N` for some term `N`. --> -我们可以用规约的项来刻画发散和停机： +我们可以用归约的项来刻画发散和停机： * 发散：对于任意项 `N`，有 `¬ (M —↠ ƛ N)`。 * 停机：对于某个项 `N`，有 `M —↠ ƛ N` 。 @@ -969,7 +969,7 @@ semantics are equivalent. (∃ N. M —↠ ƛ N) iff (∃ N. ℰ M ≃ ℰ (ƛ N)) --> -所以问题在于规约语义和指称语义是否等价： +所以问题在于归约语义和指称语义是否等价： (∃ N. M —↠ ƛ N) 当且仅当 (∃ N. ℰ M ≃ ℰ (ƛ N)) @@ -984,7 +984,7 @@ literature. --> 我们将在第二章和第三章中讨论等价的每个方向。在第二章中，我们证明了 -λ-抽象的规约蕴含 λ-抽象的指称相等。此性质在文献中被称为**可靠性（Soundness）**。 +λ-抽象的归约蕴含 λ-抽象的指称相等。此性质在文献中被称为**可靠性（Soundness）**。 M —↠ ƛ N 蕴含 ℰ M ≃ ℰ (ƛ N) @@ -996,7 +996,7 @@ is called _adequacy_ in the literature. ℰ M ≃ ℰ (ƛ N) implies M —↠ ƛ N′ for some N′ --> -在第三章中，我们证明了 λ-抽象的指称相等蕴含 λ-抽象的规约。 +在第三章中，我们证明了 λ-抽象的指称相等蕴含 λ-抽象的归约。 此性质在文献中被称为**充分性（Adequacy）**。 ℰ M ≃ ℰ (ƛ N) 蕴含 M —↠ ƛ N′ 对于某个 N′ @@ -1045,7 +1045,7 @@ in proving that reduction implies denotational equality. 我们将证明重命名变量并更改环境中对应的项仍能保持项的含义。 我们推广了重命名引理，以允许新环境中的值等于或大于原始值， -这种推广有助于证明规约蕴含了指称相等。 +这种推广有助于证明归约蕴含了指称相等。 + +本节中对指称不变性的证明使用了前一章中的技术。和 STLC +的不变性证明一样，我们保留了独立于语法定义的关系，这与内在类型项相反。 +另一方面，我们对变量使用了 de Bruijn 索引。 + + +证明的大纲保持不变，因为我们必须证明归约关系中使用的所有辅助函数的引理： +代换、重命名和扩展。 + +我们接下来的目标是证明同时代换变量和环境会保持含义不变。也就是说，若 `M` +在环境 `γ` 中的结果是 `v`，那么代换 `σ` 应用到 `M` 所得的程序，其结果仍然是 `v`， +但环境转移到了 `δ` 中。该环境中对于每一个变量 `x`，`σ x` 产生的结果值与原始环境 +`γ` 中的 `x` 的值相同。我们将这种情况写作 `` δ `⊢ σ ↓ γ ``。 ```agda infix 3 _`⊢_↓_ @@ -114,10 +132,16 @@ _`⊢_↓_ : ∀{Δ Γ} → Env Δ → Subst Γ Δ → Env Γ → Set _`⊢_↓_ {Δ}{Γ} δ σ γ = (∀ (x : Γ ∋ ★) → δ ⊢ σ x ↓ γ x) ``` + + +和之前一样，为了证明 λ-抽象，我们需要证明一个扩展引理， +该引理说明了将 `exts` 函数应用于代换会产生一个新的代换，该代换将变量映射到项， +使得当对 `δ , v` 求值时会产生 `γ , v` 中的值。 ```agda subst-ext : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} @@ -129,6 +153,7 @@ subst-ext σ d Z = var subst-ext σ d (S x′) = rename-pres S_ (λ _ → ⊑-refl) (d x′) ``` + + +该证明通过对 de Bruijn 索引 `x` 进行情况分析来论证： + +* 若索引为 `Z`，那么我们需要证明 `δ , v ⊢ # 0 ↓ v`， + 它可通过规则 `var` 得证。 + +* 若索引为 `S x′` 那么我们需要证明 + `δ , v ⊢ rename S_ (σ x′) ↓ γ x′`， + 它可通过 `rename-pres` 引理证明。 + + +有了这个扩展引理，同时代换会保留含义的证明就很直白了，我们继续深入： ```agda subst-pres : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} {M : Γ ⊢ ★} @@ -159,6 +198,7 @@ subst-pres σ s (⊔-intro d₁ d₂) = subst-pres σ s (sub d lt) = sub (subst-pres σ s d) lt ``` + + +我们通过对 `M` 的语义进行归纳来证明。两个有趣的情况分别对应于变量和 +λ-抽象： + +* 对于变量 `x`，我们有 `v = γ x`，于是需要证明 `δ ⊢ σ x ↓ v`。 + 将前提应用到 `x`，我们有 `δ ⊢ σ x ↓ γ x`，即 `δ ⊢ σ x ↓ v`. + +* 对于 λ-抽象，我们必须为归纳假设扩展代换。应用 `subst-ext` 引理可证明 + 扩展的代换会将变量映射到产生对应值的项。 + +对于 β-规约 `(ƛ N) · M —→ N [ M ]`，我们需要证明当用 `M` 代换项 `N` +中的 de Bruijn 索引 0 时，语义保持不变。通过对规则 `↦-elim` 和 `↦-intro` +进行反演，我们可得到 `γ , v ⊢ M ↓ w` 和 `γ ⊢ N ↓ v`。因此，我们需要证明 +`γ ⊢ M [ N ] ↓ w`，或等价地证明 `γ ⊢ subst (subst-zero N) M ↓ w`。 ```agda substitution : ∀ {Γ} {γ : Env Γ} {N M v w} @@ -199,6 +256,7 @@ substitution{Γ}{γ}{N}{M}{v}{w} dn dm = sub-z-ok (S x) = var ``` + + +这个结果是同时代换引理的推论。要使用该引理，我们只需要证明 `subst-zero M` +会将变量映射到某个项，该项产生的值与 `γ , v` 中产生的值相同。令 `y` +为任意变量（即 de Bruijn 索引）： + +* 若索引为 `Z`，则 `(subst-zero M) y = M` 且 `(γ , v) y = v`， + 根据前提可得 `γ ⊢ M ↓ v`。 + +* 若索引为 `S x`，则 `(subst-zero M) (S x) = x` 且 `(γ , v) (S x) = γ x`， + 根据规则 `var` 可得 `γ ⊢ x ↓ γ x`。 + +有了代换引理，就能直接证明归约保持指称不变： ```agda preserve : ∀ {Γ} {γ : Env Γ} {M N v} @@ -237,6 +310,7 @@ preserve (⊔-intro d d₁) r = ⊔-intro (preserve d r) (preserve d₁ r) preserve (sub d lt) r = sub (preserve d r) lt ``` + + +我们通过对 `M` 的语义进行归纳，并对归约进行情况分析来证明： + +* 若 `M` 为变量，则无需归约。 + +* 若 `M` 为应用，则归约要么满足合同性（ξ₁ 或 ξ₂），要么是 β-归约。 + 对于每一种合同性，我们使用归纳假设。对于 β-归约，我们使用代换引理和 `sub` 规则。 + +* 其余的情况都很直接。 -## 归约反射了指称 +## 归约反映了指称不变 + +本节中将证明归约反映了项的指称不变，换言之，若 `N` 的结果是 `v`，且若 `M` +可归约为 `N`，则 `M` 的结果也是 `v`。虽然此证明和前面的语义保持不变的证明 +之间存在一些广泛的相似之处，但我们仍需更多的技术引理才能得到这个结果。 + + + +最主要挑战是处理 β-归约中的代换： (ƛ N) · M —→ N [ M ] + + +我们有 `γ ⊢ N [ M ] ↓ v` 且需要证明 `γ ⊢ (ƛ N) · M ↓ v`。现在考虑 +`γ ⊢ N [ M ] ↓ v` 的推导过程。项 `M` 在 `N [ M ]` 中可能会出现 0、1 或多次。 +对于它可能出现的任意次数，`M` 都可能产生不同的值。不过为了构建出 `(ƛ N) · M` +的推导过程，我们需要单个的 `M` 值。若 `M` 出现了超过 1 次，那么我们就能将不同的值用 +`⊔` 连接到一起。若 `M` 出现了 0 次，那么我们就无需任何关于 `M` 的信息， +并直接使用 `⊥` 作为 `M` 的值。 -### Renaming reflects meaning +### 重命名反映了含义不变 + + +前面我们证明了重命名变量会保持含义不变。现在我们证明它的反面，即重命名反映了含义不变。 +也就是说，若 `δ ⊢ rename ρ M ↓ v` 则 `γ ⊢ M ↓ v`，其中 ``(δ ∘ ρ) `⊑ γ``. + + +首先，我们需要一个前面给出的引理的变体： + ```agda ext-`⊑ : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} → (ρ : Rename Γ Δ) @@ -296,7 +409,12 @@ ext-`⊑ ρ lt Z = ⊑-refl ext-`⊑ ρ lt (S x) = lt x ``` + + +然后证明如下： + ```agda rename-reflect : ∀ {Γ Δ v} {γ : Env Γ} {δ : Env Δ} { M : Γ ⊢ ★} → {ρ : Rename Γ Δ} @@ -322,6 +440,7 @@ rename-reflect {M = L · M} all-n (sub d₁ lt) = sub (rename-reflect all-n d₁) lt ``` + + +我们无法通过对 `δ ⊢ rename ρ M ↓ v` 的推导过程进行归纳来证明此引理， +因此，我们转而通过对 `M` 进行归纳来证明： +* 若它是一个变量，我们可通过对它应用反演引理得到 `v ⊑ δ (ρ x)`。 + 将前提实例化为 `x`，我们有 `δ (ρ x) ⊑ γ x`，于是我们可通过 `var` 规则证明。 + +* 若它是一个 λ-抽象 `ƛ N`，我们有重命名 `ρ (ƛ N) = ƛ (rename (ext ρ) N)`。 + 可通过对 `δ ⊢ ƛ (rename (ext ρ) N) ↓ v` 进行情况分析来论证： + + * 规则 `↦-intro`：为了满足归纳假设的前提，我们证明了重命名可扩展为从 + `γ , v` 到 `δ , v` 的映射。 + + * 规则 `⊥-intro`：直接应用 `⊥-intro`。 + + * 规则 `⊔-intro`：应用归纳假设和 `⊔-intro`。 + + * 规则 `sub`：应用归纳假设和 `sub`。 + +* 若它是一个应用 `L · M`，我们有 `rename ρ (L · M) = (rename ρ L) · (rename ρ M)`， + 于是可通过对 `δ ⊢ (rename ρ L) · (rename ρ M) ↓ v` 进行情况分析来论证， + 而所有的情况都很直白。 + + + +在以后使用 `rename-reflect` 的情况中，重命名始终都是增量函数， +于是我们先在这里为这些特殊情况证明以下推论。 ```agda rename-inc-reflect : ∀ {Γ v′ v} {γ : Env Γ} { M : Γ ⊢ ★} @@ -360,8 +507,13 @@ rename-inc-reflect d = rename-reflect `⊑-refl d ``` + + +### 代换反映了指称不变：变量的情况 + + +我们基本上准备好证明同时代换反映指称不变了，也就是说，若 +`γ ⊢ (subst σ M) ↓ v`，则对于任意 `k` 和某些 `δ`，有 `γ ⊢ σ k ↓ δ k` +且 `δ ⊢ M ↓ v`。我们首先从 `M` 是一个变量 `x` 的情况开始， +已知前提是 `γ ⊢ σ x ↓ v`，我们需要证明对于某个 `δ`，有 `` δ ⊢ ` x ↓ v ``。 +我们选择的环境 `δ` 应当将 `x` 映射到 `v`，将任何其他变量映射到 `⊥`。 + + +接下来我们定义将 `x` 映射到 `v`，将其他变量映射到 `⊥` 的环境，即 +`const-env x v`。为了区分变量，我们定义以下函数来确定变量的相等性： ```agda _var≟_ : ∀ {Γ} → (x y : Γ ∋ ★) → Dec (x ≡ y) @@ -388,7 +552,11 @@ var≟-refl Z = refl var≟-refl (S x) rewrite var≟-refl x = refl ``` + + +接着我们用 `var≟` 来定义 `const-env`： ```agda const-env : ∀{Γ} → (x : Γ ∋ ★) → Value → Env Γ @@ -397,14 +565,21 @@ const-env x v y with x var≟ y ... | no _ = ⊥ ``` + +当然，`const-env x v` 将 `x` 映射到值 `v`： ```agda same-const-env : ∀{Γ} {x : Γ ∋ ★} {v} → (const-env x v) x ≡ v same-const-env {x = x} rewrite var≟-refl x = refl ``` + + +以及 `const-env x v` 将 `y` 映射到 `⊥`，且 `x ≢ y`。 ```agda diff-const-env : ∀{Γ} {x y : Γ ∋ ★} {v} @@ -416,23 +591,45 @@ diff-const-env {Γ} {x} {y} neq with x var≟ y ... | no _ = refl ``` + + +于是我们为 `δ` 选择 `const-env x v` 并通过 `var` 规则得到了 `` δ ⊢ ` x ↓ v ``。 + + +剩下的就是证明 `` γ `⊢ σ ↓ δ ``，以及对于任意 `k` 有 `δ ⊢ M ↓ v`，据此我们 +就能为 `δ` 选择 `const-env x v`。我们有两种情况需要考虑：`x ≡ y` 或 `x ≢ y`。 + + +现在完成该证明的两种情况： + +* 对于 `x ≡ y` 的情况，我们需要证明 `γ ⊢ σ y ↓ v`，不过这就是我们的前提。 +* 对于 `x ≢ y,` 的情况， we need to show + that `γ ⊢ σ y ↓ ⊥`, which we do via rule `⊥-intro`. + + +这样，我们就完成了同时代换反映指称不变的证明中变量的情况。 +以下是正式的证明： ```agda subst-reflect-var : ∀ {Γ Δ} {γ : Env Δ} {x : Γ ∋ ★} {v} {σ : Subst Γ Δ} @@ -450,9 +647,17 @@ subst-reflect-var {Γ}{Δ}{γ}{x}{v}{σ} xv ``` + + +### 代换与环境的构造 + + +每一个代换都能产生可求值为 `⊥` 的项。 ```agda subst-⊥ : ∀{Γ Δ}{γ : Env Δ}{σ : Subst Γ Δ} @@ -461,9 +666,14 @@ subst-⊥ : ∀{Γ Δ}{γ : Env Δ}{σ : Subst Γ Δ} subst-⊥ x = ⊥-intro ``` + + +若代换产生的项的求值结果为 `γ₁` 或 `γ₂` 中的值，那么这些项的求值结果也是 +`γ₁ ⊔ γ₂` 中的值。 ```agda subst-⊔ : ∀{Γ Δ}{γ : Env Δ}{γ₁ γ₂ : Env Γ}{σ : Subst Γ Δ} @@ -474,7 +684,11 @@ subst-⊔ : ∀{Γ Δ}{γ : Env Δ}{γ₁ γ₂ : Env Γ}{σ : Subst Γ Δ} subst-⊔ γ₁-ok γ₂-ok x = ⊔-intro (γ₁-ok x) (γ₂-ok x) ``` + + +### λ 构造子是单射的 ```agda lambda-inj : ∀ {Γ} {M N : Γ , ★ ⊢ ★ } @@ -484,14 +698,25 @@ lambda-inj : ∀ {Γ} {M N : Γ , ★ ⊢ ★ } lambda-inj refl = refl ``` + +### 同时代换反映了指称相等 + + + +本节中我们要证明一个核心引理，即代换反映了指称不变。也就是说，若 +`γ ⊢ subst σ M ↓ v`，则 `δ ⊢ M ↓ v` 且对于某个 `δ` 有 `` γ `⊢ σ ↓ δ ``。 +我们通过对 `γ ⊢ subst σ M ↓ v` 的推导过程进行归纳来证明， +为此需要稍微重述一下该引理，将前提更改为 `γ ⊢ L ↓ v` 和 `L ≡ subst σ M`。 ```agda split : ∀ {Γ} {M : Γ , ★ ⊢ ★} {δ : Env (Γ , ★)} {v} @@ -549,9 +774,15 @@ subst-reflect (sub d lt) eq ... | ⟨ δ , ⟨ subst-δ , m ⟩ ⟩ = ⟨ δ , ⟨ subst-δ , sub m lt ⟩ ⟩ ``` + +* 情况 `var`：我们有 `subst σ M ≡ y`，因此 `M` 也必须是一个变量，称为 `x`。 + 我们应用引理 `subst-reflect-var` 得出结论。 + + + +* 情况 `↦-elim`：我们有 `subst σ M ≡ L₁ · L₂`，需要对 `M` 进行情况分析： + * 情况 `` M ≡ ` x ``：我们再次应用 `subst-reflect-var` 得出结论。 + + * 情况 `M ≡ M₁ · M₂`：根据归纳假设，我们有某个 `δ₁` 和 `δ₂` 使得 + `δ₁ ⊢ M₁ ↓ v₁ ↦ v₃` 和 `` γ `⊢ σ ↓ δ₁ ``，以及 `δ₂ ⊢ M₂ ↓ v₁` + 和 `` γ `⊢ σ ↓ δ₂ ``。 + 根据 `⊑-env` 我们有 `δ₁ ⊔ δ₂ ⊢ M₁ ↓ v₁ ↦ v₃` 和 `δ₁ ⊔ δ₂ ⊢ M₂ ↓ v₁` + （使用 `⊑-env-conj-R1` 和 `⊑-env-conj-R2` 得出），因此 `δ₁ ⊔ δ₂ ⊢ M₁ · M₂ ↓ v₃`。 + 我们通过 `subst-⊔` 引理得出 `` γ `⊢ σ ↓ δ₁ ⊔ δ₂ `` 从而证明此情况。 + + +* 情况 `↦-intro`：我们有 `subst σ M ≡ ƛ L′`，需要对 `M` 进行情况分析： + * 情况 `M ≡ x`：我们应用 `subst-reflect-var` 引理。 + * 情况 `M ≡ ƛ M′`：根据归纳假设，我们有 `(δ′ , v′) ⊢ M′ ↓ v₂` 和 + `(δ , v₁) ⊢ exts σ ↓ (δ′ , v′)`。根据后者可得 `(δ , v₁) ⊢ # 0 ↓ v′`。 + 根据引理 `var-inv` 我们有 `v′ ⊑ v₁`，于是根据 `up-env` 引理我们有 + `(δ′ , v₁) ⊢ M′ ↓ v₂`，因此 `δ′ ⊢ ƛ M′ ↓ v₁ → v₂`。我们还需要证明 + `δ ⊢ σ ↓ δ′`。固定 `k`，我们有 `(δ , v₁) ⊢ rename S_ σ k ↓ δ k′`， + 接着应用引理 `rename-inc-reflect` 可得 `δ ⊢ σ k ↓ δ k′`，于是此情况证明完毕。 + + +* 情况 `⊥-intro`：我们为 `δ` 选择`⊥`。 + 根据 `⊥-intro` 我们有 `⊥ ⊢ M ↓ ⊥`。 + 根据 `subst-⊥` 引理有 `` δ `⊢ σ ↓ `⊥ ``。 + + +* 情况 `⊔-intro`：根据归纳假设我们有 `δ₁ ⊢ M ↓ v₁`、`δ₂ ⊢ M ↓ v₂`、 + `` δ `⊢ σ ↓ δ₁ `` 和 `` δ `⊢ σ ↓ δ₂ ``。 + 根据 `⊑-env`、`⊑-env-conj-R1` 和 `⊑-env-conj-R2` 我们有 `δ₁ ⊔ δ₂ ⊢ M ↓ v₁` + 和 `δ₁ ⊔ δ₂ ⊢ M ↓ v₂`，因此根据 `⊔-intro` 可得 `δ₁ ⊔ δ₂ ⊢ M ↓ v₁ ⊔ v₂`。 + 根据 `subst-⊔` 可得 `` δ `⊢ σ ↓ δ₁ ⊔ δ₂ ``。 + + + +### 单一代换反映了指称不变 + + +现在大部分工作已经完成，我们已经证明了同时代换反映了指称不变。当然，β-归约使用单一代换， +因此我们需要一个推论来证明单一代换反映了指称不变。也就是说，给定项 +`N : (Γ , ★ ⊢ ★)` 和 `M : (Γ ⊢ ★)`，若 `γ ⊢ N [ M ] ↓ w`，则对于某个值 `v` +有 `γ ⊢ M ↓ v` 且 `( γ , v) ⊢ N ↓ w` 。于是我们有 `N [ M ] = subst (subst-zero M) N`。 + + +我们首先证明一个关于 `subst-zero` 的引理，即若 `δ ⊢ subst-zero M ↓ γ`，则对某个值 +`w`，有 `` γ `⊑ (δ , w) × δ ⊢ M ↓ w ``。 ```agda subst-zero-reflect : ∀ {Δ} {δ : Env Δ} {γ : Env (Δ , ★)} {M : Δ ⊢ ★} @@ -615,6 +899,7 @@ subst-zero-reflect {δ = δ} {γ = γ} δσγ = ⟨ last γ , ⟨ lemma , δσγ lemma (S x) = var-inv (δσγ (S x)) ``` + + +我们选择 `w` 作为 `γ` 中的最后一个值，通过将前提应用到 `Z` 可得 `δ ⊢ M ↓ w`。 +最后，要证明 `` γ `⊑ (δ , w) ``，我们需要在输入项中通过归纳来证明一个引理。 +由于我们选择了 `w`，因此基本的情况是平凡的。在归纳的情况中 `S x` 中， +前提 `δ ⊢ subst-zero M ↓ γ` 给出了 `δ ⊢ x ↓ γ (S x)`，接着使用 `var-inv` +可得 `` γ (S x) ⊑ (δ `, w) (S x) ``。 + + +现在证明代换反映了指称不变： ```agda substitution-reflect : ∀ {Δ} {δ : Env Δ} {N : Δ , ★ ⊢ ★} {M : Δ ⊢ ★} {v} @@ -635,18 +931,33 @@ substitution-reflect d with subst-reflect d refl ... | ⟨ w , ⟨ ineq , δMw ⟩ ⟩ = ⟨ w , ⟨ δMw , ⊑-env γNv ineq ⟩ ⟩ ``` + + +我们应用 `subst-reflect` 引理可得对于某个 `γ` 有 `δ ⊢ subst-zero M ↓ γ` +和 `γ ⊢ N ↓ v`。通过使用前者，`subst-zero-reflect` 给出了 `` γ `⊑ (δ , w) `` +和 `δ ⊢ M ↓ w`。我们通过应用 `⊑-env` 引理，使用 `γ ⊢ N ↓ v` 和 `` γ `⊑ (δ , w) `` +可得 `δ , w ⊢ N ↓ v`。 + + +### 归约反映了指称不变 + + +现在我们已经证明了代换反映了指称不变，可以很容易地证明归约也拥有此性质： ```agda reflect-beta : ∀{Γ}{γ : Env Γ}{M N}{v} @@ -685,10 +996,18 @@ reflect (⊔-intro d₁ d₂) r mn rewrite sym mn = reflect (sub d lt) r mn = sub (reflect d r mn) lt ``` + +## 归约蕴含指称等价 + + + +我们已经证明了归约保持并反映了指称不变，因此归约蕴含指称等价： ```agda reduce-equal : ∀ {Γ} {M : Γ ⊢ ★} {N : Γ ⊢ ★} @@ -699,9 +1018,14 @@ reduce-equal {Γ}{M}{N} r γ v = ⟨ (λ m → preserve m r) , (λ n → reflect n r refl) ⟩ ``` + + +最终我们就得到了**可靠性（Soundness Property）**，即多步归约到一个 +λ-抽象蕴含指称等价于该 λ-抽象。 ```agda soundness : ∀{Γ} {M : Γ ⊢ ★} {N : Γ , ★ ⊢ ★}