3, 4 & 5

Author: subfish-zhou

src/SUMMARY.md

@@ -7,13 +7,13 @@
 - [信任](./trust/trust.md)
     - [非安全声明](./trust/unsafe_declarations.md)
     - [对抗性输入](./trust/adversarial_inputs.md)
-- [Export format](./export_format.md)
-- [Kernel concepts](./kernel_concepts/kernel_concepts.md)
-    - [The big picture](./kernel_concepts/the_big_picture.md)
-    - [Clarifying language](./kernel_concepts/clarifying_language.md)
-    - [Instantiation and abstraction](./kernel_concepts/instantiation_and_abstraction.md)
-    - [Weak and strong reduction](./kernel_concepts/weak_and_strong_reduction.md)
-- [Names](./names.md)
+- [导出格式](./export_format.md)
+- [内核的基本概念](./kernel_concepts/kernel_concepts.md)
+    - [概览](./kernel_concepts/the_big_picture.md)
+    - [术语解释](./kernel_concepts/clarifying_language.md)
+    - [实例化与抽象化](./kernel_concepts/instantiation_and_abstraction.md)
+    - [弱归约与强归约](./kernel_concepts/weak_and_strong_reduction.md)
+- [名称](./names.md)
 - [Levels](./levels.md)
 - [Expressions](./expressions/expressions.md)
     - [Notes on Implementing Expressions](./expressions/implementing_expressions.md)
@@ -23,4 +23,4 @@
 - [Definitional Equality](./type_checking/definitional_equality.md)
 - [Reduction](./type_checking/reduction.md)
 - [Open issues & future work](./future_work.md)
-- [Further reading](./further_reading.md)
+- [延伸阅读](./further_reading.md)

src/export_format.md

@@ -1,27 +1,27 @@
-# Export format
+# 导出格式
 
-An exporter is a program which emits Lean declarations using the kernel language, for consumption by external type checkers. Producing an export file is a complete exit from the Lean ecosystem; the data in the file can be checked with entirely external software, and the exporter itself is not a trusted component. Rather than inspecting the export file itself to see whether the declarations were exported as the developer intended, the exported declarations are checked by the external checker, and are displayed back to the user by a pretty printer, which produces output far more readable than the export file. Readers can (and are encouraged to) write their own external checkers for Lean export files.
+导出器（exporter）是一种程序，它以内核语言导出 Lean 中的声明，以便外部的类型检查器使用。生成一个导出文件即意味着完全脱离了 Lean 生态系统；文件中的数据可由完全外部的软件进行检查，且导出器自身并不是一个可信组件。用户无需直接查看导出文件，以确认导出的声明是否符合开发者的原意；相反，导出的声明将由外部检查器检查，再通过美观打印器（pretty printer）以更易读的形式展示给用户。读者可以（且被鼓励）自行编写外部检查器来处理 Lean 的导出文件。
 
-The official exporter is [lean4export](https://github.com/leanprover/lean4export).
+官方的导出器为：[lean4export](https://github.com/leanprover/lean4export)。
 
+官方导出器的 master 分支沿用了 Lean 3 的基本格式（参见 [此处](https://github.com/leanprover/lean3/blob/master/doc/export_format.md)），但增加了 Lean 4 新增的内容，包括 **投影（projections）** 、 **字面量（literals）** 和显式的 let 表达式（let expressions）支持。这些新增内容已在 lean4export 的 readme 中详细描述。
 
-The master branch of the official exporter uses the same base format as lean 3 [here](https://github.com/leanprover/lean3/blob/master/doc/export_format.md), with the addition of the new-to-lean4 items, which are projections, literals, and explicitly support for let expressions. The new stuff is outlined in the lean4export readme.
+另外，[此 lean4export 的 fork 版本](https://github.com/ammkrn/lean4export/tree/format2024)对导出格式进行了轻微修改，具体说明如下：该版本新增了对 **可约性提示（reducibility hints）** 、 **商类型声明（quotient declarations）** 、递归器（recursors）**以及** ι-化简规则（rec rules）的导出支持。这些新增导出特性旨在提供更大的实现灵活性与更好的性能表现，同时也便于开发更为简洁的软件，以便于试验；并能简化类型检查器的自举（bootstrapping）及测试过程。
 
-A slightly modified version of the export format supported by [this fork](https://github.com/ammkrn/lean4export/tree/format2024) of lean4export is described below. These modifications export reducibility hints, quotient declarations, recursors, and iota reduction rules (rec rules). These additional exports were added to give more flexibility in implementation and for performance, but they also allow for the development of more minimized software used for experimentation, and can make bootstrapping and testing a checker easier for developers.
-
-There are also [ongoing discussions](https://github.com/leanprover/lean4export/issues/3) about how best to evolve the export format.
+此外，社区也在[持续讨论](https://github.com/leanprover/lean4export/issues/3)如何更好地优化导出格式。
 
 ## (ver 0.1.2)
 
-For clarity, some of the compound items are decorated here with a name, for example `(name : T)`, but they appear in the export file as just an element of `T`.
+为了清晰起见，下述复合元素标记了名称，例如 `(name : T)`，但在实际导出文件中，它们仅表现为类型 `T` 的元素，不包含额外标记。
 
-The export scheme for mutual and nested inductives is as follows: 
-+ `Inductive.inductiveNames` contains the names of all types in the `mutual .. end` block. The names of any other inductive types used in a nested (but not mutual) construction will not be included.
-+ `Inductive.constructorNames` contains the names of all constructors for THAT inductive type, and no others (no constructors of the other types in a mutual block, and no constructors from any nested construction).
+互递归（mutual）与嵌套（nested）归纳类型的导出方案如下：
 
-**NOTE:** readers writing their own parsers and/or checkers should initialize names[0] as the anonymous name, and levels[0] as universe zero, as they are not emitted by the exporter, but are expected to occupy the name and level indices for 0.
+* `Inductive.inductiveNames` 包含 `mutual ... end` 区块中所有归纳类型的名称。不包括任何其他嵌套（但非互递归）构造中的归纳类型名称。
+* `Inductive.constructorNames` 仅包含对应归纳类型自身的所有构造子（constructor）名称，不含其他类型的构造子（即不含互递归区块中其他类型的构造子，也不含嵌套构造中的构造子）。
 
-```
+**注意**：自己编写解析器和检查器的读者应注意初始化 `names[0]` 为匿名名称（anonymous name），并初始化 `levels[0]` 为宇宙层级零（universe zero），因为导出器不会显式导出它们，但会假定它们分别占据索引 0 的名称和层级位置。
+
+```lean
 File ::= ExportFormatVersion Item*
 
 ExportFormatVersion ::= nat '.' nat '.' nat

src/further_reading.md

@@ -1,4 +1,4 @@
-# Further reading
+# 延伸阅读
 
 + Mario Carneiro's [thesis on Lean's type theory](https://github.com/digama0/lean-type-theory)
 

src/kernel_concepts/clarifying_language.md

@@ -1,39 +1,66 @@
-# Clarifying language
+# 术语解释
 
+## Type、Sort 与 Prop
 
-## Type, Sort, Prop
+* `Prop` 即为 `Sort 0`。
+* `Type n` 即为 `Sort (n+1)`。
+* 内核中实际表示这些概念的是统一的 `Sort n`，用户始终可以直接使用它。
 
-`Prop` refers to `Sort 0`
+之所以有时使用 `Type <N>` 或者 `Prop` 而非统一使用 `Sort n`，是因为 `Type <N>` 中的元素具有一些重要的性质与行为，是 `Prop` 中元素所不具备的，反之亦然。
 
-`Type n` refers to `Sort (n+1)`
+例如：`Prop` 中元素具有 **定义性的证明无关性（definitional proof irrelevance）** ，而 `Type _` 中的元素可直接使用 **大消去（large elimination）** ，无需满足其他额外条件。
 
-`Sort n` is how these are actually represented in the kernel, and can always be used.
+## Level/universe 与 Sort
 
-The reason why `Type <N>` and `Prop` are sometimes used instead of always adhering to `Sort n` is that elements of `Type <N>` have certain important qualities and behaviors that are not observed by those of `Prop` and vice versa.
+* 术语“level”（层级）和“universe”（宇宙）实际上是同义的，指的都是内核中同一种对象。
 
-Example: elements of `Prop` can be considered for definitional proof irrelevance, while elements of `Type _` can use large elimination without needing to satisfy other tests.
+偶尔有一种细微的区别，即“宇宙参数”（universe parameter）通常暗含着特指变量形式的层级。这是因为：
 
+* “宇宙参数”特指在 Lean 声明中用作参数化的层级集合，而这些只能是变量名（identifiers）。
+* 例如，一个 Lean 声明可以写成：
 
-## Level/universe and Sort
+  ```lean
+  def Foo.{u} ..
+  ```
 
-The terms "level" and "universe" are basically synonymous; they refer to the same kind of kernel object.
+  这里的含义是「定义 Foo，以宇宙变量 u 为参数化」。
 
-A small distinction that's sometimes made is that "universe parameter" may be implicitly restricted to levels that are variables/parameters. This is because "universe parameters" refers to the set of levels that parameterize a Lean declaration, which can only be identifiers, and are therefore restricted to identifiers. If this doesn't mean anything to you, don't worry about it for now. As an example, a Lean declaration may begin with `def Foo.{u} ..` meaning "a definition parameterized by the universe variable `u`", but it may not begin with `def Foo.{1} ..`, because `1` is an explicit level, and not a parameter.
+  但不能直接写成：
 
-On the other hand, `Sort _` is an expression that represents a level.
+  ```lean
+  def Foo.{1} ..
+  ```
 
-## Value vs. type
+  因为 `1` 是一个明确的宇宙层级，而非参数（parameter）。
 
-Expressions can be either values or types. Readers are probably familiar with the idea that `Nat.zero` is a value, while `Nat` is a type. An expression `e` is a value or "value level expression" if `infer e != Sort _`. An expression `e` is a type or "type level expression" if `infer(e) = Sort _`.
+另一方面，`Sort _` 则是表示某个宇宙层级的表达式。
 
+## 值与类型
 
-## Parameters vs. indices
+Lean 中的表达式可以是 **值** 或者 **类型**。
 
-The distinction between a parameter and index comes into play when dealing with inductive types. Roughly speaking, elements of a telescope that come before the colon in a declaration are parameters, and elements that come after the colon are indices:
+* 用户可能熟悉的例子：
 
-```
-      parameter ----v         v---- index
+  * `Nat.zero` 是一个 **值**；
+  * `Nat` 是一个 **类型**。
+
+具体而言，对于表达式 `e`：
+
+* 若 `infer e ≠ Sort _`，则称为 **值表达式**。
+* 若 `infer e = Sort _`，则称为 **类型表达式**。
+
+## 参数与指标
+
+参数（parameter）与指标（index）的区别在处理归纳类型时尤为重要。
+
+简单来说，在 Lean 中的归纳类型声明里，「冒号之前」的参数列表为 **参数**，「冒号之后」为 **指标**：
+
+```lean
+         -- 参数 ----v         v---- 指标
 inductive Nat.le (n : Nat) : Nat → Prop
 ```
 
-The distinction is non-negligible within the kernel, because parameters are fixed within a declaration, while indices are not.
+这一差别在内核中至关重要：
+
+* 参数在单个归纳声明的定义中是固定不变的；
+* 而指标则在具体构造中并不固定。

src/kernel_concepts/instantiation_and_abstraction.md

@@ -1,38 +1,85 @@
-# Instantiation and abstraction
+# 实例化与抽象化
 
-Instantiation refers to substitution of bound variables for the appropriate arguments. Abstraction refers to replacement of free variables with the appropriate bound variable when replacing binders. Lean's kernel uses deBruijn indices for bound variables and unique identifiers for free variables.
+实例化（Instantiation）指的是用合适的参数替换掉表达式中的绑定变量的过程。
+抽象化（Abstraction）则相反，指的是在重新绑定时，用合适的绑定变量替换表达式中的自由变量。
 
-For our purposes, a free variable is a variable in an expression that refers to a binder which has been "opened", and is no longer immediately available to us, so we replace the corresponding bound variable with a free variable that has some information about the binder we're leaving behind.
+Lean 内核采用：
 
-To illustrate, let's say we have some lambda expression `(fun (x : A) => <body>)` and we're doing type inference. Type inference has to traverse into the `<body>` part of the expression, which may contain a bound variable that refers to `x`. When we traverse into the body, we can either add `x` to some stateful context of binders and take the whole stateful context into the body with us, or we can temporarily replace all of the bound variables that refer to `x` with a free variable, allowing us to traverse into the body without having to carry any additional context.
+* **deBruijn 索引** 来表示绑定变量；
+* **唯一标识符**（unique identifiers）来表示自由变量。
 
-If we eventually come back to where we were before we opened the binder, abstraction allows us to replace all of the free variables that were once bound variables referring to `x` with new bound variables that again refer to `x`, with the correct deBruijn indices.
+在这里，**自由变量** 指的是表达式中原本引用某个绑定变量，但该绑定变量所处的绑定器已被“打开”，不再立即可用。因此，我们用自由变量来临时替代这个绑定变量，并记录一些与原绑定器相关的信息。
 
-## Implementing free variable abstraction
+假设我们有如下 λ 表达式：
 
-For deBruijn levels, the free variables keep track of a number that says "I am a free variable representing the nth bound variable *from the top of the telescope*". 
+```lean
+(fun (x : A) => <body>)
+```
+
+我们需要对这个表达式进行类型推断时，必须遍历到其中的 `<body>` 部分，而该部分可能包含引用到绑定变量 `x` 的子表达式。
+
+当我们进入 `<body>` 时，有两种方式：
+
+1. 将绑定变量 `x` 添加到某个上下文（context）中，并带着整个状态化的上下文进入 `<body>`。
+2. 临时用 **自由变量** 替换掉所有引用 `x` 的绑定变量，这样我们无需携带额外的上下文即可进入 `<body>`。
+
+如果随后我们回到最初“打开”绑定器之前的位置，**抽象化** 的过程将允许我们再次用绑定变量（并赋予正确的 deBruijn 索引）替换掉那些临时的自由变量，从而重新构造出正确的闭合表达式。
 
-This is the opposite of a deBruijn index, which is a number indicating "the nth bound variable from the bottom of the telescope".
+## 自由变量的抽象化实现细节
 
-Top and bottom here refer to visualizing the expression's telescope as a tree:
+对于 deBruijn 表示法中的“自由变量”，我们用 deBruijn 层级来记录：
 
+* 自由变量自身记录的信息是：“我是一个表示 **从望远镜顶部开始数的第 n 个绑定变量** 的自由变量”。
+
+这种方法正好与 deBruijn 索引相反：它表示的是从望远镜的 **底部** 往上数的第 n 个绑定变量。
+
+在这里，“顶部”和“底部”指的是将表达式中的绑定器序列看作一棵树时的上下位置：
+
+```lean
+        fun
+       /   \
+      a    fun
+           /  \
+          b   ...
+                \
+                 fun
+                 /  \
+                e   bvar(0)
 ```
-      fun
-      /  \
-    a    fun
-        /   \
-      b      ...
-              \
-              fun
-             /   \
-            e    bvar(0)
+
+例如，表达式：
+
+```lean
+fun (a b c d e) => bvar(0)
 ```
 
-For example, with a lambda `fun (a b c d e) => bvar(0)`, the bound variable refers to `e`, by referencing "the 0th from the bottom".
+这里的 `bvar(0)` 是从底部数的第 0 个绑定变量，即引用的是 `e`。
+
+再例如：
+
+```lean
+fun (a b c d e) => fvar(4)
+```
+
+这里的 `fvar(4)` 是从顶部数的第 4 个绑定变量，同样引用的是 `e`，但这次表达方式不同，是从 **顶部往下计数**。
+
+## 为什么要区分这两种表示法？
+
+在强归约（strong reduction）过程中，当我们创建自由变量时，我们能知道一些信息：
+
+* 我们知道要替换进来的自由变量可能会因为后续的归约而被重新移动位置；
+* 我们明确知道目前 **在我们之上的绑定器数量**（因为我们进入当前表达式时访问过它们）；
+* 我们知道稍后可能需要抽象化这个表达式，以便重新闭合开放的绑定器，这时我们必须重新绑定自由变量。
+
+但在创建自由变量的那个时刻，我们却 **无法得知当前下方还剩余多少绑定器**。也就是说，我们暂时无法预见这个自由变量在最后抽象化后具体会处于“自底部起的第几个”绑定变量的位置上。
+
+因此，用 deBruijn 层级标记自由变量（即自顶部计数）更为便捷。
 
-In the lambda expression `fun (a b c d e) => fvar(4)`, the free variable is a deBruijn level representing `e` again, but this time as "the 4th from the top of the telescope".
+## 如何具体实现抽象化？
 
-Why the distinction? When we create a free variable during strong reduction, we know a couple of things: we know that the free variable we're about to sub in might get moved around by further reduction, we know how many open binder are *ABOVE* us (because we had to visit them to get here), and we know we might need to quote/abstract this expression to replace the binders, meaning we need to re-bind the free variable. However, in that moment, we do NOT know how many binders remain below us, so we cannot say how many variables from the bottom that variable might be when it's eventually abstracted/quoted.
+如果具体实现中使用唯一标识符为自由变量标记位置，那么在抽象化过程中，只需具备以下信息即可：
 
-For implementations using unique identifiers to tag free variables, this problem is solved by having the actual telescope that's being reconstructed during abstraction. As long as you have the expression and a list of the uniquely-tagged free variables, you can abstract, because the position of the free variables within the list indicates their binder position.
+* 被还原的表达式；
+* 唯一标记的自由变量列表；
 
+即可完成抽象化。因为 **自由变量在列表中的位置** 正好明确表明了这些自由变量对应的绑定变量位置。

src/kernel_concepts/kernel_concepts.md

@@ -1,4 +1,3 @@
+# 内核的基本概念
 
-# Kernel concepts
-
-This chapter begins with a high level road map, which everyone should read, then covers some ideas needed to understand the kernel's nuts and bolts, and is less focused on theory. The ideas in the later sections do not need to be completely understood up-front, so readers should feel free to skim them and come back as needed.
+本章开头会给出一个高层次的路线图（建议所有人都认真阅读），接下来会介绍一些理解内核实现细节所必需的概念，本章的侧重点并不在理论本身。后面几节的内容无需一开始就彻底理解，读者可放心地先粗略浏览，日后再根据需要回顾即可。