de Bruijn 索引

Posted on June 6, 2021 
module posts.deBruijn where
open import Data.Nat
open import Data.Fin -- using (Fin; raise; zero; suc)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

众所周知，含有名字的 Lambda 演算中比较麻烦的一件事就是替换，比如对于替换 (λx. y)[y := x]，由于替换进来的 lambda 项含有自由变量 x， 如果直接将 y 变成 x，那么会得到 λx. x，自由变量 x 被绑定了，显然这是一个不正确的结果。 一般的解决方式是对 λx. y 进行α-变换，即对绑定变量进行重命名， 这里我们把 x 变成 z，那么可以得到 (λz. y)[y := x]，此时可以直接得到结果 λz. x。 按照这种方式我们可以写出如下的替换定义：

(1a) x[x := N] ≡ N,
(1b) y[x := N] ≡ y if x ̸≡ y,
(2) (PQ)[x := N] ≡ (P[x := N])(Q[x := N]),
(3) (λy. P)[x := N] ≡ λz. (P[y := z][x := N]), 其中 z ∉ FV(N)，即 z 不为 N 的自由变量

定义(3)说明，我们必须得创建一个新名字，这种定义并不优雅，如果用代码实现可能需要维护一些额外的状态， 为了解决这个问题，我们使用数字来表示变量，数字 k 表示由内向外第 k 个封闭 λ 所绑定的变量，k 被称为 de Bruijn 索引，用这种方式表示的项叫做 de Bruijn 项。

比如，我们用 λ. 0 表示 λx. x，因为这里的 x 被第 0 个 λ 所绑定。 又比如，我们用 λ. λ. 0 1 表示 λx. λy. x y，这里的 x 和 y 分别是由内向外第 0 个和第 1 个 λ 所绑定的变量。 上面的两个例子都不含自由变量，对于含有自由变量的项，例如 λ x. x y，我们不知道应该怎样表示 y， 需要引入一个命名上下文对所有自由变量分配一个初始索引， 对于上面的例子，我们假设有命名上下文 Γ = y, a, b, c, d, e，那么我们能得到 Γ 下 λ x. x y 的 de Bruijn 项表示为 λ. 0 6，y 在 Γ 下的索引为 5，在项中变成 6 是因为引入了内层 λ，所以由内向往数 λ 要 +1。

由于我们的项包含自由变量，必须给定一个能绑定所有自由变量的上下文才能使项有意义。 例如要为一个 de Bruijn 项赋型，那么上下文必须给项中的每一个自由变量都绑定一个类型。 如果对一个 de Bruijn 项求值，那么上下文必须给相中的每一个自由变量都绑定一个值。 项中的每一个自由变量在上下文中都对应一个唯一的索引，叫做上下文索引，项 1 中自由变量 1 对应的上下文索引是 1，项 λ. 0 1 2 中自由变量 1 和 2 对应的上下文索引是 0 和 1。 项的上下文索引和 de Bruijn 索引有以下关系：

项的上下文索引 + λ 层数 = de Bruijn 索引

为了处理方便，我们用一个自然数 n 约束上下文，表示上下文为 [0, n) 范围内的上下文索引都提供了绑定，例如对于项 0 1，我们可以取 n = 2，也可以取 n = 3。

下面开始在 Agda 中定义 de Bruijn 项。

infix  5 ƛ_
infixl 7 _·_
infix  9 `_

data Term : ℕ → Set where
  `_ : ∀{n} → Fin n → Term n
  _·_ : ∀{n} → Term n → Term n → Term n
  ƛ_ : ∀{n} → Term (suc n) → Term n

我们使用了自然数 n 索引项的类型，表示项中自由变量的上下文索引的上界。

一些测试用例，其中 # i 为 Fin n 类型下自然数的表示：

_ : Term 1
_ = `(# 0)

_ : Term 2
_ = `(# 0)

_ : Term 0
_ = ƛ `(# 0) -- λx. x

_ : Term 1
_ = ƛ `(# 0) · `(# 1) -- λx. x y

_ : Term 6
_ = ƛ `(# 0) · `(# 5) -- λx. x y

由上面的例子可以看出，项定义中出现的 n 可以大于等于项实际的自由变量上下文索引，这与我们对 n 的定义是一致的。

下面开始研究 de Bruijn 项的替换。

根据需求，我们只需要处理 (λ. M) V 的规约结果 M [0 := V]， 即只需要替换第 0 个自由变量，但如果 M 是 λ. M' 的形式， 那么我们需要递归地对 M' 进行替换，在 M 索引为 0 的自由变量在 M' 中索引会变成 1， 因此我们必须实现一个更加通用的函数来表示替换——能对任意变量进行替换。

最朴素的想法是定义下面的函数：

naive-subst : ∀{n m} → Fin n -> Term m → Term n → Term m

naive-subst 只对一个变量进行替换，而实际上我们对项进行规约时可能需要多次替换。

例如， 对 (λ. 1 0 2) (λ. 0) 进行规约， 结果是 naive-subst 0 (λ. 0) (1 0 2)， 然而这个结果并不正确，因为我们去掉了一层 λ，项中自由变量的索引需要 -1 （可视为将索引为suc i的变量替换为项 ``i）， 与此同时，我们也需要将绑定变量（即索引为 0 的变量）替换为目标项， 因此这是一个批量替换，我们用下面的函数表示：

subst : ∀{n m} → (Fin n → Term m) → Term n → Term m

使用这种方式，(λx. t) v 的下一步规约 t[x := v] 可以表示为下列函数：

_[_] : ∀{n} → Term (suc n) → Term n → Term n
_[_] {n} t v = subst subst-zero t
  where
    subst-zero : Fin (suc n) → Term n
    subst-zero zero = v
    subst-zero (suc n) = ` n

subst-zero 表示一个批量替换：将 t 第 0 个自由变量（即原绑定变量 x）替换成 v ，其他变量则索引 -1。

最后一步是实现 subst，在实现 subst 之前，我们首先需要实现一个移位函数：

rename : ∀{n m} → (Fin n → Fin m) → Term n → Term m
rename f (` x) = `(f x)
rename f (t₁ · t₂) = rename f t₁ · rename f t₂
rename {n} {m} f (ƛ t) = ƛ rename f' t
  where
    f' : Fin (suc n) → Fin (suc m)
    f' zero = zero
    f' (suc i) = suc (f i)

rename 表示将项 t : Term n 中的自由变量整体移位，移位方式由函数 f : Fin n → Fin m 决定，表示将项中上下文索引为 i : Fin n 的自由变量变成上下文索引为 j : Fin m 的自由变量。 考虑项 t：

有了 rename，我们就可以实现 subst 了：

subst : ∀{n m} → (Fin n → Term m) → Term n → Term m
subst f (` x) = f x
subst f (t₁ · t₂) = subst f t₁ · subst f t₂
subst {n} {m} f (ƛ t) = ƛ subst f' t
  where
    f' : Fin (suc n) → Term (suc m)
    f' zero = ` zero
    f' (suc n) = rename (raise 1) (f n)
加上 _[_]，便完成了所有工作： 
_[_] : ∀{n} → Term (suc n) → Term n → Term n
_[_] {n} t v = subst subst-zero t
  where
    subst-zero : Fin (suc n) → Term n
    subst-zero zero = v
    subst-zero (suc n) = ` n

下面的例子验证了 (λ. 1 0 2) (λ. 0) 的结果：

t1 : Term 2
t1 = (`(# 1) · `(# 0) · `(# 2))[ ƛ `(# 0) ]

t2 : Term 2
t2 = `(# 0) · (ƛ `(# 0)) · `(# 1)

_ : t1 ≡ t2
_ = refl