笔记:无名表示

传统的有名 CoC 项语法:

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

对应的替换实现:

{x[xt]} {=} {t}
{y[xt]} {=} {x}
{(t{1}t{2})[xt]} {=} {t{1}[xt]t{2}[xt]}
{(λx.s)[xt]} {=} {λx.s}
{(λy.s)[xt]} {=} {λy.s[yy][xt]} {yFVt}
{(λy.s)[xt]} {=} {λx.s[xt]} {yFVt}
{((x:t{1})t{2})[xt]} {=} {(x:t{1}[xt])t{2}}
{((y:t{1})t{2})[xt]} {=} {(y:t{1}[xt])t{2}[yy][xt]} {yFVt}
{((y:t{1})t{2})[xt]} {=} {(y:t{1}[xt])t{2}[xt]} {yFVt}
{{n}[xt]} {=} {{n}}

其中 FVt 用以获取自由变量表,定义如下:

{FVx} {=} {{x}}
{FV(λx.e)} {=} {FVe{x}}
{FV(t{1}t{2})} {=} {FVt{1}FVt{2}}
{FV((x:t{1})t{2})} {=} {FVt{1}(FVt{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[ks]

使得对任意的项 t 满足

t[xs]{Γ}=t{Γ}[xs{Γ}]

第一次尝试(只考虑 变量,λ 和 App):

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

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

第二次尝试:

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

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

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

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

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

{{c}(k)} {=} {k+1} {ifkc}
{{c}(k)} {=} {k} {ifk<c}
{{c}(λ.d)} {=} {λ.{c+1}(d)}
{{c}(d{1}d{2})} {=} {{c}(d{1}){c}(d{2})}
{} {} {}
{j[js]} {=} {s}
{k[js]} {=} {k}
{(λ.d)[js]} {=} {λ.d[j+1{0}(s)]}
{(d{1}d{2})[js]} {=} {d{1}[js]d{2}[js]}

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

{Applyφd} {:} {(Term)Term}
{Applyφk} {=} {φk}
{Applyφ(λ.d)} {=} {λ.Apply(Ident(Weak1φ))d}
{Applyφ(d{1}d{2})} {=} {(Applyφd{1})(Applyφd{2})}
{Applyφ(d{1}d{2})} {=} {(Applyφd{1})(Apply(Ident(Weak1φ))d{2})}
{Applyφ{n}} {=} {{n}}

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

{(φσ)0} {=} {φ0}
{(φσ)n} {=} {σ(n1)}
{Identk} {=} {k}
{Weaknk} {=} {k+n}
{Subst0d} {=} {(kd)ident}

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