update 2024.10.29

lean/main/03_expressions.lean

@@ -52,15 +52,28 @@ end Playground
 
 ## De Bruijn 索引
 
-考虑以下 lambda 表达式 `(λ f x => f x x) (λ x y => x + y) 5`，化简时会在变量 `x` 中遇到冲突。
+考虑以下 lambda 表达式 `(λ x : ℕ => λ y : ℕ => x + y) y`，当我们朴素地用 `y` 替换 lambda 表达式中的 `x` 时，我们得到 `λ y ： ℕ => y + y`。但这是错误的：这个 lambda 表达式是一个有两个参数的函数，它将一个参数加到另一个参数上，而计算出的版本却将自己的参数加到自己身上。问题的根源在于，`y` 这个名字既用于外层 lambda 表达式中的变量，又用于内层 lambda 表达式中绑定的变量。使用相同的变量名意味着，当我们对应用进行求值或 β-归约时，必须小心不要混淆不同的变量。为了解决这个问题，Lean 实际上并不通过名称引用绑定变量。相反，它使用了一个称为 __de Bruijn 索引__ 的巧妙技巧。
 
-为了避免变量名称冲突，`Expr` 使用了一个称为 __de Bruijn 索引__ 的巧妙技巧。在 de Bruijn 索引中，每个由 `lam` 或 `forallE` 绑定的变量都会转换为数字 `#n`。该数字表示我们应该在 `Expr` 树上查找多少个绑定器才能找到绑定此变量的绑定器。因此，我们上面的例子将变成（为了简洁起见，现在在类型参数中放置通配符 `_`）：
+在 de Bruijn 索引中，每个由 `lam` 或 `forallE` 绑定的变量都会转换为数字 `#n`。该数字表示我们应该在 `Expr` 树上越过多少个绑定器才能找到绑定此变量的绑定器。因此，我们上面的例子将变成（为了简洁起见，把不必要的部分用通配符 `_` 替换）：
 
-``app (app (lam `f _ (lam `x _ (app (app #1 #0) #0))) (lam `x _ (lam `y _ (app (app plus #1) #0)))) five``
+```
+app (lam `x _ (lam `y _ (app (app `plus #1) #0) _) _) (fvar _)
+```
 
-现在我们在执行β-规约时不需要重命名变量。我们还可以轻松检查两个包含绑定表达式的 `Expr` 是否相等。这就是为什么 `bvar` 的类型签名是 `Nat → Expr` 而不是 `Name → Expr`。
+`fvar` 代表 `y`，而 lambda 表达式的变量现在用 `#0` 和 `#1` 表示。当我们对这个应用求值时时，我们用 `fvar _` 替换属于 `lam x` (这里是 `#1` )的绑定变量，得到
 
-如果 de Bruijn 指标对于其前面的绑定器数量来说太大，我们说它是一个 __松弛的 `bvar`__；否则我们说它是 __绑定的__。例如，在表达式 ``lam `x _ (app #0 #1)`` 中，`bvar` `#0` 由前面的绑定器绑定，而 `#1` 是松弛的。 Lean 将所有 de Bruijn 索引称为 `bvar`（「绑定变量」），这隐含了一种理念：除了一些非常低级的函数之外，Lean 期望表达式不包含任何松弛的 `bvar`。相反，每当我们想要引入一个松弛的 `bvar` 时，我们都会立即将其转换为 `fvar`（「自由变量」）。下一章将讨论其具体工作原理。
+```
+(lam `y _ (app (app `plus (fvar _)) #0) _)
+```
+
+美观打印出来则是：
+```
+λ y_1 => y + y_1
+```
+
+注意，Lean 已经自动为剩余的绑定变量选择了一个名称 `y_1`，以避免与 `fvar` `y` 的名称冲突。选择的名称基于 `lam` 中的名称建议 `y`。
+
+如果 de Bruijn 指标对于其前面的绑定器数量来说太大，我们说它是一个 __松弛的 `bvar`__；否则我们说它是 __绑定的__。例如，在表达式 ``lam `x _ (app #0 #1)`` 中，`bvar` `#0` 由前面的绑定器绑定，而 `#1` 是松弛的。 Lean 将所有 de Bruijn 索引称为 `bvar`（「绑定变量」），这隐含了一种理念：除了一些非常低级的函数之外，Lean 期望表达式不包含任何松弛的 `bvar`。相反，每当我们想要引入一个松弛的 `bvar` 时，我们都会立即将其转换为 `fvar`（「自由变量」）（因此，Lean 的绑定器表示是「局部无名的」。）。下一章将讨论其具体工作原理。
 
 如果表达式中没有松弛的 `bvar`，我们称该表达式为 __闭的__。用 `Expr` 替换所有松弛的 `bvar` 实例的过程称为 __实例化__（instantiation）。反之称为**抽象化**（abstraction）。
 

lean/main/04_metam.lean

@@ -379,7 +379,7 @@ abbrev             reducibleDef   : Nat      := defaultDef + 1
 如果我们重复上述命令，并让 Lean 打印出隐式参数，我们可以看到 `+` 符号实际上是 `hAdd` 函数的应用，而该函数是 `HAdd` 类型类的一个成员：
 -/
 
-set_option pp.explicit true
+set_option pp.explicit true in
 #eval traceConstWithTransparency .reducible ``reducibleDef
 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) defaultDef 1
 

lean/main/05_syntax.lean

@@ -83,7 +83,7 @@ notation:65 lhs:65 " ~ " rhs:65 => (lhs - rhs)
 notation:65 a:65 " ~ " b:65 " mod " rel:65 => rel a b
 
 /-
-Lean 会优先选择这种符号，而不是先解析为上面定义的 `a ~ b`，然后因为不知道如何处理 `mod` 和等价关系参数而报错。
+Lean 会优先选择这种符号，如果先解析为上面定义的 `a ~ b`，那么它就会因为不知道如何处理 `mod` 和等价关系参数而报错。
 -/
 
 #check 0 ~ 0 mod Eq -- 0 = 0 : Prop