实例化与抽象化
实例化（Instantiation）指的是用合适的参数替换掉表达式中的绑定变量的过程。 抽象化（Abstraction）则相反，指的是在重新绑定时，用合适的绑定变量替换表达式中的自由变量。
Lean 内核采用：
- deBruijn 索引 来表示绑定变量；
- 唯一标识符（unique identifiers）来表示自由变量。
在这里，自由变量 指的是表达式中原本引用某个绑定变量，但该绑定变量所处的绑定器已被“打开”，不再立即可用。因此，我们用自由变量来临时替代这个绑定变量，并记录一些与原绑定器相关的信息。
假设我们有如下 λ 表达式：
(fun (x : A) => <body>)
我们需要对这个表达式进行类型推断时，必须遍历到其中的 <body> 部分，而该部分可能包含引用到绑定变量 x 的子表达式。
当我们进入 <body> 时，有两种方式：
- 将绑定变量
x添加到某个上下文（context）中，并带着整个状态化的上下文进入<body>。 - 临时用 自由变量 替换掉所有引用
x的绑定变量，这样我们无需携带额外的上下文即可进入<body>。
如果随后我们回到最初“打开”绑定器之前的位置，抽象化 的过程将允许我们再次用绑定变量（并赋予正确的 deBruijn 索引）替换掉那些临时的自由变量，从而重新构造出正确的闭合表达式。
自由变量的抽象化实现细节
对于 deBruijn 表示法中的“自由变量”，我们用 deBruijn 层级来记录：
- 自由变量自身记录的信息是：“我是一个表示 从望远镜顶部开始数的第 n 个绑定变量 的自由变量”。
这种方法正好与 deBruijn 索引相反：它表示的是从望远镜的 底部 往上数的第 n 个绑定变量。
在这里，“顶部”和“底部”指的是将表达式中的绑定器序列看作一棵树时的上下位置：
fun
/ \
a fun
/ \
b ...
\
fun
/ \
e bvar(0)
例如，表达式：
fun (a b c d e) => bvar(0)
这里的 bvar(0) 是从底部数的第 0 个绑定变量，即引用的是 e。
再例如：
fun (a b c d e) => fvar(4)
这里的 fvar(4) 是从顶部数的第 4 个绑定变量，同样引用的是 e，但这次表达方式不同，是从 顶部往下计数。
为什么要区分这两种表示法？
在强归约（strong reduction）过程中，当我们创建自由变量时，我们能知道一些信息：
- 我们知道要替换进来的自由变量可能会因为后续的归约而被重新移动位置；
- 我们明确知道目前 在我们之上的绑定器数量（因为我们进入当前表达式时访问过它们）；
- 我们知道稍后可能需要抽象化这个表达式，以便重新闭合开放的绑定器，这时我们必须重新绑定自由变量。
但在创建自由变量的那个时刻，我们却 无法得知当前下方还剩余多少绑定器。也就是说，我们暂时无法预见这个自由变量在最后抽象化后具体会处于“自底部起的第几个”绑定变量的位置上。
因此，用 deBruijn 层级标记自由变量（即自顶部计数）更为便捷。
如何具体实现抽象化？
如果具体实现中使用唯一标识符为自由变量标记位置，那么在抽象化过程中，只需具备以下信息即可：
- 被还原的表达式；
- 唯一标记的自由变量列表；
即可完成抽象化。因为 自由变量在列表中的位置 正好明确表明了这些自由变量对应的绑定变量位置。