笔记：无名表示

传统的有名 CoC 项语法：

{t}	{=}	{x}	{  }	{Variable}
{}	{|}	{λx. t}	{  }	{Abstraction}
{}	{|}	{t{1} t{2}}	{  }	{Application}
{}	{|}	{(x : t{1}) → t{2}}	{  }	{Function Space}
{}	{|}	{⋆{n}}	{  }	{Universes}

对应的替换实现：

{x[x ↦ t]}	{=}	{t}
{y[x ↦ t]}	{=}	{x}
{(t{1} t{2})[x ↦ t]}	{=}	{t{1}[x ↦ t] t{2}[x ↦ t]}
{(λx. s)[x ↦ t]}	{=}	{λx. s}
{(λy. s)[x ↦ t]}	{=}	{λy′. s[y ↦ y′][x ↦ t]}	{ y ∈ FV t}
{(λy. s)[x ↦ t]}	{=}	{λx. s[x ↦ t]}	{ y ∉ FV t}
{((x : t{1}) → t{2})[x ↦ t]}	{=}	{(x : t{1}[x ↦ t]) → t{2}}
{((y : t{1}) → t{2})[x ↦ t]}	{=}	{(y′ : t{1}[x ↦ t]) → t{2}[y ↦ y′][x ↦ t]}	{ y ∈ FV t}
{((y : t{1}) → t{2})[x ↦ t]}	{=}	{(y : t{1}[x ↦ t]) → t{2}[x ↦ t]}	{ y ∉ FV t}
{⋆{n}[x ↦ t]}	{=}	{⋆{n}}

其中 FV t 用以获取自由变量表，定义如下：

{FV x}	{=}	{{x}}
{FV (λx. e)}	{=}	{FV e − {x}}
{FV (t{1}t{2})}	{=}	{FV t{1} ∪ FV t{2}}
{FV ((x : t{1}) → t{2})}	{=}	{FV t{1} ∪ (FV t{2} − {x})}
{FV ⋆{n}}	{=}	{{}}

可以看到，传统有名表示的问题在于：

• 需要在替换的时候小心处理自由变量和同名绑定。
• α-等价性判定的实现相对繁琐，性能也不好。

---

Dr Bruijn 编码：变量没有名字而是引用「这个变量是离这儿第几个 λ/Π 引入的」：

{d}	{=}	{k}	{  }	{Bounded Variable}
{}	{|}	{λ. d}	{  }	{Abstraction}
{}	{|}	{d{1} d{2}}	{  }	{Application}
{}	{|}	{d{1} → d{2}}	{  }	{Function Space}
{}	{|}	{⋆{n}}	{  }	{Universes}

传统项转换到 De Bruijn 编码项，其中 Γ 为一个名字列表：

{⟦x⟧{Γ}}	{=}	{Lookup Γ x}
{⟦t{1} t{2}⟧{Γ}}	{=}	{⟦d{1}⟧{Γ} ⟦d{2}⟧{Γ}}
{⟦λx.t⟧{Γ}}	{=}	{λ.⟦d{1}⟧{x, Γ}}
{⟦(x : t{1}) → t{2}⟧{Γ}}	{=}	{⟦t{1}⟧{Γ} → ⟦t{2}⟧{x, Γ}}
{⟦⋆{n}⟧{Γ}}	{=}	{⋆{n}}

那么 De Bruijn 项的替换要怎么实现呢？换言之，我们希望实现

d[k ↦ s]

使得对任意的项 t 满足

⟦t[x ↦ s]⟧{Γ} = ⟦t⟧{Γ}[⟦x⟧ ↦ ⟦s⟧{Γ}]

第一次尝试（只考虑 变量，λ 和 App）：

{j[j ↦ s]}	{=}	{s}
{k[j ↦ s]}	{=}	{k}
{(λ. d)[j ↦ s]}	{=}	{λ. d[j ↦ s]}
{(d{1} d{2})[j ↦ s]}	{=}	{d{1}[j ↦ s] d{2}[j ↦ s]}

……结果并不正确，反例为 (x (λy. y))[x ↦ λz. z]。原因在于，每次「深入」一个 λ 的时候，要被替换的变量编号就变掉啦！

第二次尝试：

{j[j ↦ s]}	{=}	{s}
{k[j ↦ s]}	{=}	{k}
{(λ. d)[j ↦ s]}	{=}	{λ. d[j + 1 ↦ s]}
{(d{1} d{2})[j ↦ s]}	{=}	{d{1}[j ↦ s] d{2}[j ↦ s]}

……仍不正确，反例为 (λz. x)[x ↦ λy. w]，我们忘记去处理 s 里面「外面的」变量了，因此当它被塞进 λ 里面后，引用差了一位。

第三次尝试，引入一个「弱化」算符，修订错误的引用：

{↑ (k)}	{=}	{k + 1}
{↑ (λ. d)}	{=}	{λ. ↑ (d)}
{↑ (d{1} d{2})}	{=}	{↑ (d{1}) ↑ (d{2})}
{ }	{ }	{ }
{j[j ↦ s]}	{=}	{s}
{k[j ↦ s]}	{=}	{k}
{(λ. d)[j ↦ s]}	{=}	{λ. d[j + 1 ↦ ↑ (s)]}
{(d{1} d{2})[j ↦ s]}	{=}	{d{1}[j ↦ s] d{2}[j ↦ s]}

……仍不正确，反例是 (λz. x)[x ↦ λy. w y]，这次问题出在我们错误地弱化了 s 中的「内部」变量。因此，「弱化」是需要有 Cut-off 的：

{↑{c}(k)}	{=}	{k + 1}	{if k ≥ c}
{↑{c}(k)}	{=}	{k}	{if k < c}
{↑{c}(λ. d)}	{=}	{λ. ↑{c + 1}(d)}
{↑{c}(d{1} d{2})}	{=}	{↑{c}(d{1}) ↑{c}(d{2})}
{ }	{ }	{ }
{j[j ↦ s]}	{=}	{s}
{k[j ↦ s]}	{=}	{k}
{(λ. d)[j ↦ s]}	{=}	{λ. d[j + 1 ↦ ↑{0}(s)]}
{(d{1} d{2})[j ↦ s]}	{=}	{d{1}[j ↦ s] d{2}[j ↦ s]}

在实际实现的时候可以把「替换」过程中的替换项改为一个态射（Morphism）：

{Apply φ d}	{:}	{(ℕ → Term) → Term}
{Apply φ k}	{=}	{φ k}
{Apply φ (λ. d)}	{=}	{λ. Apply (Ident ⋉ (Weak 1 ⋅ φ)) d}
{Apply φ (d{1} d{2})}	{=}	{(Apply φ d{1}) (Apply φ d{2})}
{Apply φ (d{1} → d{2})}	{=}	{(Apply φ d{1}) → (Apply (Ident ⋉ (Weak 1 ⋅ φ)) d{2})}
{Apply φ ⋆{n}}	{=}	{⋆{n}}

其中使用了一些辅助函数：

{(φ ⋉ σ) 0}	{=}	{φ 0}
{(φ ⋉ σ) n}	{=}	{σ (n − 1)}
{Ident k}	{=}	{k}
{Weak n k}	{=}	{k + n}
{Subst0 d}	{=}	{(k ⇒ d) ⋉ ident}

使用此种方法表示项的话，Alpha 等价性也就是简单的结构相等了，避免了比对复杂的问题。