lambda演算中变量之间的Alpha等价

Question

只是一个相当简单的问题(所以在我看来).如果两个变量(x)(x)是alpha等价的.是(x1x2)(x2x1)阿尔法相同呢？

Answer 1

如果一个术语可以通过重命名绑定变量纯粹转换为另一个术语,则两个术语是等效的.

如果变量与某些封闭的lambda的参数名称匹配,则认为该变量是绑定变量.否则它是一个自由变量.这里有一些例子:

?x. x          -- x is bound
?x. y          -- y is free
?f. ?x. f x y  -- f and x are bound, y is free
f (?f. f x)    -- the first f is free; the second is bound. x is free
z              -- z is free

基本上,"绑定"和"自由"大致对应于程序语言中"范围"和"范围外"的概念.

如果你还修复了对该变量的所有引用,那么Alpha等价基本上捕获了在程序中重命名变量是安全的想法.也就是说,当您更改lambda术语的参数时,您还必须进入lambda的主体并更改该变量的用法.(如果名称由第一个lambda中的另一个lambda重新绑定,则最好确保不在内部lambda中执行重命名.)

以下是alpha等效术语的一些示例:

?x. x   <->   ?y. y   <->   ?berp. berp
?x. ?f. f x   <->   ?x. ?g. g x   <->   ?f. ?x. x f   <->  ?x1. ?x2. x2 x1
?f. ?f. f f   <->   ?g. ?f. f f   <->   ?f. ?g. g g

那么x xalpha等价于x1x2 x1x2？没有! 在第一个任期内x是免费的,因为它不受封闭的lambda的约束.(也许它是对全局变量的引用.)因此将其重命名为不安全x1x2.

我怀疑你的导师真的应该说这?x. x x是α等同于?x1x2. x1x2 x1x2.这里x由lambda绑定,因此您可以安全地重命名它.

是x1 x2阿尔法-相当于x2 x1？出于同样的原因,没有.

而?x1. ?x2. x1 x2等同于?x1. ?x2. x2 x1？同样,不,因为这不仅仅是一个重命名 - 变量x1和x2变量四处移动.

然而,?x1. ?x2. x1 x2 是的α-相当于?x2. ?x1. x2 x1:

1. 重命名x1为一些临时名称,如z:?z. ?x2. z x2
2. 重命名x2为x1:?z. ?x1. z x1
3. 重命名z为x2:?x2. ?x1. x2 x1

在语言实现中正确地重命名是一个非常麻烦的问题,许多编译器编写者选择称为de Bruijn索引的无名表示.变量不是使用文本,而是表示一个数字,用于衡量变量绑定的lambdas数量.一个无名的代表就像.请注意,这与de Bruijn表示完全相同.de Bruijn指数彻底解决了α等价问题(尽管它们很难阅读).?x2. ?x1. x2 x1?. ?. 2 1?x1. ?x2. x1 x2