笔记:无名表示
传统的有名 CoC 项语法:
{t} | {=} | {x} | { } | {Variable} |
{} | {|} | {λx | { } | {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 | {=} | {λx | |
{(λy | {=} | {λy′ | { y ∈ FV t} |
{(λy | {=} | {λx | { 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 | {=} | {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} |
{} | {|} | {λ | { } | {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 | {=} | {λ |
{⟦(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{1} d{2})[j ↦ s]} | {=} | {d{1}[j ↦ s] d{2}[j ↦ s]} |
……结果并不正确,反例为 (x (λy
第二次尝试:
{j[j ↦ s]} | {=} | {s} |
{k[j ↦ s]} | {=} | {k} |
{(λ | {=} | {λ |
{(d{1} d{2})[j ↦ s]} | {=} | {d{1}[j ↦ s] d{2}[j ↦ s]} |
……仍不正确,反例为 (λz
第三次尝试,引入一个「弱化」算符,修订错误的引用:
{↑ (k)} | {=} | {k + 1} |
{↑ (λ | {=} | {λ |
{↑ (d{1} d{2})} | {=} | {↑ (d{1}) ↑ (d{2})} |
{ } | { } | { } |
{j[j ↦ s]} | {=} | {s} |
{k[j ↦ s]} | {=} | {k} |
{(λ | {=} | {λ |
{(d{1} d{2})[j ↦ s]} | {=} | {d{1}[j ↦ s] d{2}[j ↦ s]} |
……仍不正确,反例是 (λz
{↑{c}(k)} | {=} | {k + 1} | {if k ≥ c} |
{↑{c}(k)} | {=} | {k} | {if k < c} |
{↑{c}(λ | {=} | {λ | |
{↑{c}(d{1} d{2})} | {=} | {↑{c}(d{1}) ↑{c}(d{2})} | |
{ } | { } | { } | |
{j[j ↦ s]} | {=} | {s} | |
{k[j ↦ s]} | {=} | {k} | |
{(λ | {=} | {λ | |
{(d{1} d{2})[j ↦ s]} | {=} | {d{1}[j ↦ s] d{2}[j ↦ s]} |
在实际实现的时候可以把「替换」过程中的替换项改为一个态射(Morphism):
{Apply φ d} | {:} | {( |
{Apply φ k} | {=} | {φ k} |
{Apply φ (λ | {=} | {λ |
{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 等价性也就是简单的结构相等了,避免了比对复杂的问题。