X->x->xα等于\x->\y->x？

Question

所以我知道，在\x->\y->x中，第二个x被绑定到第一个(请告诉我我错了)，在\x->\x->x中最后一个x被绑定到中间一个。但是，当涉及到α等价时，这会有什么区别吗？

\x->\x->xα与\x->\y->x等价吗？

Answer 1

如果t1和t2这两个术语是alpha等价的，那么对于任何上下文E[.]、E[t1]和E[t2]都是相同的术语。

因此，如果您有两个术语，并且您找到了一个使它们简化为两个不同术语的上下文，那么您就知道它们不是alpha等效的。

在这里，您有t1 = \x.\x.x和t2 = \x.\y.x，使用应用两个不同术语的上下文，例如v1和v2，您有：

t1 v1 v2 = (\x.\x.x) v1 v2 --> (\x.x) v2 --> v2

和

t2 v1 v2 = (\x.\y.x) v1 v2 --> (\y.v1) v2 --> v1

因此，您可以推断它们不是alpha等效的。

也就是说，如果你真的想使用α等价，你应该花时间去理解什么是自由的，有界的变量，并问问自己，在变量绑定方面，α等价意味着什么。