Haskell 和 Lambda 微积分 : Implementing Alpha-Congruence (Alpha-Equivalence)

Question

我正在 Haskell 中实现一个不纯的非类型 lambda 演算解释器。

我目前坚持实现“alpha-congruence”(在某些教科书中也称为“alpha-equivalence”或“alpha-equality”)。我希望能够检查两个 lambda 表达式是否相等或不相等。例如，如果我在解释器中输入以下表达式，它应该产生 True(\ 用于指示 lambda 符号):

>\x.x == \y.y
True

问题在于理解以下 lambda 表达式是否被视为 alpha 等价:

>\x.xy == \y.yx
???

>\x.yxy == \z.wzw
???

在\x.xy ==\y.yx的情况下，我猜测答案是True。这是因为 \x.xy =>\z.zy 和 \y.yx =>\z.zy 以及两者的右侧相等(其中符号 => 用于表示 alpha 缩减)。

在\x.yxy ==\z.wzw的情况下，我同样猜测答案是True。这是因为 \x.yxy =>\a.yay 和 \z.wzw =>\a.waw (我认为)是相等的。

问题在于，我的所有教科书定义都规定，只需更改绑定(bind)变量的名称即可将两个 lambda 表达式视为相等。它没有提到表达式中的自由变量也需要统一重命名。因此，即使 y 和 w 都位于 lambda 表达式中的正确位置，程序如何“知道”第一个 y代表第一个 w，第二个 y 代表第二个 w。我需要在实现中保持一致。

简而言之，我将如何实现函数 isAlphaCongruent 的无错误版本？为了使其发挥作用，我需要遵循哪些确切规则？

我更愿意在不使用 de Bruijn 指数的情况下执行此操作。

Answer 1

您误解了:不同的自由变量并不等价。所以 y/= x 和 \w.wy/=\w.wx 和 \x.xy/=\y.yx 。同样，\x.yxy/=\z.wzw 因为 y/= w。

你的书没有提到自由变量可以统一重命名，因为它们不允许统一重命名。

(这样想:如果我还没有告诉你 not 和 id 的定义，你会期望 \x.not x 和 \x.id x 是等价的吗？我当然希望不是!)