Deploying to gh-pages from @ 2846fa7 🚀

axioms_and_computation.html

@@ -195,8 +195,8 @@ <h1 id="公理与计算"><a class="header" href="#公理与计算">公理与计
 computation. This also blocks evaluation in the kernel, but it is
 compatible with compilation to bytecode.
 -->
-<p>Lean 的标准库定义了一个公理：<strong>命题外延性（Propositional Extensionality）</strong>。
-以及一个**商（Qoutient）**结构，它蕴含了函数外延性的公理。
+<p>Lean 的标准库定义了一个公理： <strong>命题外延性（Propositional Extensionality）</strong> 。
+以及一个 <strong>商（Qoutient）</strong> 结构，它蕴含了函数外延性的公理。
 这些扩展被用来发展如集合与有限集这些理论。我们在后面会看到，
 这些定理的使用会阻碍 Lean 内核中的求值，因此 <code>Nat</code> 类型的封闭项不再求值为数值。
 但是 Lean 在对其虚拟机器求值器进行字节码编译时会擦除类型和命题信息，
@@ -285,7 +285,7 @@ <h2 id="历史与哲学背景"><a class="header" href="#历史与哲学背景">
 <p>然而在 19 世纪，数学论证复杂性的提升推动了数学家发展新的推理风格，
 抑制算法信息并调用数学对象，从而抽象掉了对象被表征的细节。
 目标是在不陷入繁重的计算细节的情况下获得强大的「概念」理解，
-但这可能导致数学定理在直接计算的解读上干脆就是 <strong>错误</strong> 的。</p>
+但这可能导致数学定理在直接计算的解读上干脆就是  <strong>错误</strong>  的。</p>
 <!--
 There is still fairly uniform agreement today that computation is
 important to mathematics. But there are different views as to how best
@@ -303,9 +303,9 @@ <h2 id="历史与哲学背景"><a class="header" href="#历史与哲学背景">
 -->
 <p>今天数学界仍在相当普遍地同意计算对于数学很重要。
 但对于如何以最佳方式解决计算问题有不同的看法。
-从<strong>构造性</strong>的角度来看，将数学与其计算根源分开是一个错误；
+从 <strong>构造性</strong> 的角度来看，将数学与其计算根源分开是一个错误；
 每条有意义的数学定理都应具有直接的计算解释。
-从<strong>经典的</strong>角度来看，保持关注点的分离更有成效：
+从 <strong>经典的</strong> 角度来看，保持关注点的分离更有成效：
 我们可以使用一种语言和方法体系编写计算机程序，
 同时保持使用非构造性理论和方法对其进行推理的自由。
 Lean 旨在支持这两种方法。库的核心部分以构造性方式开发，
@@ -590,8 +590,8 @@ <h2 id="函数外延性"><a class="header" href="#函数外延性">函数外延
 quotients, and more. But the solutions are not so clear cut, and the
 rules of Lean's underlying calculus do not sanction such reductions.
 -->
-<p>当前的研究计划包括关于<strong>观测类型论（Observational Type Theory）</strong>
-和**立方类型论（Cubical Type Theory）**的研究，旨在扩展类型理论，
+<p>当前的研究计划包括关于 <strong>观测类型论（Observational Type Theory）</strong>
+和 <strong>立方类型论（Cubical Type Theory）</strong> 的研究，旨在扩展类型理论，
 以便允许对涉及函数外延、商，等等的强制转换进行归约。
 但解决方案并不明朗，而 Lean 的底层演算法则对此类归约也不支持。</p>
 <!--
@@ -770,7 +770,7 @@ <h2 id="商"><a class="header" href="#商">商</a></h2>
 <p>当然，当 <code>r</code> 是等价关系时，商集的结构是最常用的。给定上面的 <code>r</code>，
 如果我们根据法则 <code>r' a b</code> 当且仅当 <code>Quot.mk r a = Quot.mk r b</code> 定义 <code>r'</code>，
 那么显然 <code>r'</code> 就是一个等价关系。事实上，<code>r'</code> 是函数 <code>a ↦ quot.mk r a</code>
-的<strong>核（Kernel）</strong>。公理 <code>Quot.sound</code> 表明 <code>r a b</code> 蕴含 <code>r' a b</code>。
+的 <strong>核（Kernel）</strong> 。公理 <code>Quot.sound</code> 表明 <code>r a b</code> 蕴含 <code>r' a b</code>。
 使用 <code>Quot.lift</code> 和 <code>Quot.ind</code>，我们可以证明 <code>r'</code> 是包含 <code>r</code> 的最小的等价关系，
 意思就是，如果 <code>r''</code> 是包含 <code>r</code> 的任意等价关系，则 <code>r' a b</code> 蕴含 <code>r'' a b</code>。
 特别地，如果 <code>r</code> 开始就是一个等价关系，那么对任意 <code>a</code> 和 <code>b</code>，我们都有
@@ -780,7 +780,7 @@ <h2 id="商"><a class="header" href="#商">商</a></h2>
 notion of a *setoid*, which is simply a type with an associated
 equivalence relation:
 -->
-<p>为支持这种通用使用案例，标准库定义了 <strong>广集（Setoid）</strong> 的概念，
+<p>为支持这种通用使用案例，标准库定义了  <strong>广集（Setoid）</strong>  的概念，
 它只是一个带有与之关联的等价关系的类型：</p>
 <pre><code class="language-lean"><span class="boring">namespace Hidden
 </span>class Setoid (α : Sort u) where
@@ -859,7 +859,7 @@ <h2 id="商"><a class="header" href="#商">商</a></h2>
 the relevant equivalence relation:
 -->
 <p>回顾一下标准库中的 <code>α × β</code> 代表类型 <code>α</code> 和 <code>β</code> 的笛卡尔积。
-为了说明商的用法，让我们将类型为 <code>α</code> 的元素构成的**无序对（Unordered Pair）**的类型定义为
+为了说明商的用法，让我们将类型为 <code>α</code> 的元素构成的 <strong>无序对（Unordered Pair）</strong> 的类型定义为
 <code>α × α</code> 类型的商。首先，我们定义相关的等价关系：</p>
 <pre><code class="language-lean">private def eqv (p₁ p₂ : α × α) : Prop :=
   (p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
@@ -1161,7 +1161,7 @@ <h2 id="选择公理"><a class="header" href="#选择公理">选择公理</a></h
 subtypes as follows:
 -->
 <p>这可以在 <code>Classical</code> 命名空间中找到，所以定理的全名是 <code>Classical.choice</code>。
-选择公理等价于**非限定摹状词（Indefinite Description）**原理，可通过子类型表示如下：</p>
+选择公理等价于 <strong>非限定摹状词（Indefinite Description）</strong> 原理，可通过子类型表示如下：</p>
 <pre><code class="language-lean"><span class="boring">namespace Hidden
 </span><span class="boring">universe u
 </span><span class="boring">axiom choice {α : Sort u} : Nonempty α → α
@@ -1221,7 +1221,7 @@ <h2 id="选择公理"><a class="header" href="#选择公理">选择公理</a></h
 definition is conventionally known as *Hilbert's epsilon function*:
 -->
 <p>假设环境类型 <code>α</code> 非空，<code>strongIndefiniteDescription p</code> 产生一个满足 <code>p</code>
-的元素 <code>α</code>（如果存在的话）。该定义的数据部分通常被称为 <strong>希尔伯特 ε 函数</strong>：</p>
+的元素 <code>α</code>（如果存在的话）。该定义的数据部分通常被称为  <strong>希尔伯特 ε 函数</strong> ：</p>
 <pre><code class="language-lean"><span class="boring">open Classical
 </span><span class="boring">universe u
 </span>#check (@epsilon :

dependent_type_theory.html

@@ -475,7 +475,7 @@ <h2 id="类型作为对象"><a class="header" href="#类型作为对象">类型
 ``α``, no matter which type universe ``α`` lives in. This explains the
 type signature of the function ``List``:
 -->
-<p>然而，有些操作需要在类型宇宙上具有<strong>多态（Polymorphic）</strong>。例如，<code>List α</code> 应该对任何类型的 <code>α</code> 都有意义，无论 <code>α</code> 存在于哪种类型的宇宙中。所以函数 <code>List</code> 有如下的类型：</p>
+<p>然而，有些操作需要在类型宇宙上具有 <strong>多态（Polymorphic）</strong> 。例如，<code>List α</code> 应该对任何类型的 <code>α</code> 都有意义，无论 <code>α</code> 存在于哪种类型的宇宙中。所以函数 <code>List</code> 有如下的类型：</p>
 <pre><code class="language-lean">#check List    -- List.{u} (α : Type u) : Type u
 </code></pre>
 <!--
@@ -540,7 +540,7 @@ <h2 id="函数抽象和求值"><a class="header" href="#函数抽象和求值">
 
 Here are some more examples
 -->
-<p>从另一个表达式创建函数的过程称为<strong>lambda 抽象</strong>。假设你有一个变量 <code>x : α</code> 和一个表达式 <code>t : β</code>，那么表达式 <code>fun (x : α) =&gt; t</code> 或者 <code>λ (x : α) =&gt; t</code> 是一个类型为 <code>α → β</code> 的对象。这个从 <code>α</code> 到 <code>β</code> 的函数把任意 <code>x</code> 映射到 <code>t</code>。</p>
+<p>从另一个表达式创建函数的过程称为 <strong>lambda 抽象</strong> 。假设你有一个变量 <code>x : α</code> 和一个表达式 <code>t : β</code>，那么表达式 <code>fun (x : α) =&gt; t</code> 或者 <code>λ (x : α) =&gt; t</code> 是一个类型为 <code>α → β</code> 的对象。这个从 <code>α</code> 到 <code>β</code> 的函数把任意 <code>x</code> 映射到 <code>t</code>。</p>
 <p>这有些例子：</p>
 <pre><code class="language-lean">#check fun x : Nat =&gt; fun y : Bool =&gt; if not y then x + 1 else x + 2
 #check fun (x : Nat) (y : Bool) =&gt; if not y then x + 1 else x + 2
@@ -611,7 +611,7 @@ <h2 id="函数抽象和求值"><a class="header" href="#函数抽象和求值">
 following expressions:
 -->
 <p>这个表达式表示一个接受三个类型 <code>α</code>，<code>β</code> 和 <code>γ</code> 和两个函数 <code>g : β → γ</code> 和 <code>f : α → β</code>，并返回的 <code>g</code> 和 <code>f</code> 的复合的函数。(理解这个函数的类型需要理解依值积类型，下面将对此进行解释。)</p>
-<p>lambda表达式的一般形式是 <code>fun x : α =&gt; t</code>，其中变量 <code>x</code> 是一个<strong>绑定变量（Bound Variable）</strong>：它实际上是一个占位符，其「作用域」没有扩展到表达式 <code>t</code> 之外。例如，表达式 <code>fun (b : β) (x : α) =&gt; b</code> 中的变量 <code>b</code> 与前面声明的常量 <code>b</code> 没有任何关系。事实上，这个表达式表示的函数与 <code>fun (u : β) (z : α) =&gt; u</code> 是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是<strong>alpha等价</strong>的，也就是被认为是「一样的」。Lean 认识这种等价性。</p>
+<p>lambda表达式的一般形式是 <code>fun x : α =&gt; t</code>，其中变量 <code>x</code> 是一个 <strong>绑定变量（Bound Variable）</strong> ：它实际上是一个占位符，其「作用域」没有扩展到表达式 <code>t</code> 之外。例如，表达式 <code>fun (b : β) (x : α) =&gt; b</code> 中的变量 <code>b</code> 与前面声明的常量 <code>b</code> 没有任何关系。事实上，这个表达式表示的函数与 <code>fun (u : β) (z : α) =&gt; u</code> 是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是 <strong>alpha等价</strong> 的，也就是被认为是「一样的」。Lean 认识这种等价性。</p>
 <p>注意到项 <code>t : α → β</code> 应用到项 <code>s : α</code> 上导出了表达式 <code>t s : β</code>。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型:</p>
 <pre><code class="language-lean">#check (fun x : Nat =&gt; x) 1     -- Nat
 #check (fun x : Nat =&gt; true) 1  -- Bool
@@ -1363,7 +1363,7 @@ <h2 id="隐参数"><a class="header" href="#隐参数">隐参数</a></h2>
 ``List.nil``:
 -->
 <p>此处定义的 <code>ident</code> 和上面那个效果是一样的。</p>
-<p>Lean 有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为<strong>繁饰（Elaboration）</strong>。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 <code>id</code> 或 <code>List.nil</code> 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。</p>
+<p>Lean 有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些「洞」或「占位符」的过程通常被称为 <strong>繁饰（Elaboration）</strong> 。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 <code>id</code> 或 <code>List.nil</code> 这样的表达式被认为是「多态的」，因为它可以在不同的上下文中具有不同的含义。</p>
 <p>可以通过写 <code>(e : T)</code> 来指定表达式 <code>e</code> 的类型 <code>T</code>。这就指导 Lean 的繁饰器在试图解决隐式参数时使用值 <code>T</code> 作为 <code>e</code> 的类型。在下面的第二个例子中，这种机制用于指定表达式 <code>id</code> 和 <code>List.nil</code> 所需的类型:</p>
 <pre><code class="language-lean">#check List.nil               -- List ?m
 #check id                     -- ?m → ?m