我在 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.zyand\y.yx => \z.zy和 两者的右侧相等（符号=>用于表示 alpha 减少）。
\x.yxy == \z.wzw我也猜想答案是True。这是因为\x.yxy => \a.yay和\z.wzw => \a.wawwhich（我认为）是平等的。
问题是我所有教科书的定义都指出，只有绑定变量的名称需要更改，两个 lambda 表达式才能被视为相等。它没有说明表达式中的自由变量也需要统一重命名。因此，即使y和w都在 lambda 表达式中的正确位置，程序如何“知道”第一个y代表第一个w，第二个y代表第二个w。我需要在实现中对此保持一致。
简而言之，我将如何实现函数的无错误版本isAlphaCongruent？为了使它起作用，我需要遵循哪些确切的规则？
我宁愿在不使用 de Bruijn 指数的情况下这样做。