Haskell 中的 Alpha 等价（Lambda 术语）

Question

我正在尝试在 Haskell 中实现一个函数，该函数检查两个 Lambda 项是否等价于 alpha。

alphaEq :: LExp -> LExp -> Bool
alphaEq (ID x) (ID y) = x == y
alphaEq (LAMBDA x1 e1) (LAMBDA x2 e2) = alphaEq e1 (substitute x2 (ID x1) e2)
alphaEq (APP e1 f1) (APP e2 f2) = alphaEq e1 e2 && alphaEq f1 f2
alphaEq _ _ = False

substitute :: Var -> LExp -> LExp -> LExp
substitute v k (ID x) = if v == x then k else (ID x)
substitute v k (LAMBDA x e) = if v == x then (LAMBDA x e) else (LAMBDA x (substitute v k e))
substitute v k (APP e1 e2) = APP (substitute v k e1) (substitute v k e2)

但这并不能完全满足我的需要，例如，这个输入：

alphaEq (LAMBDA "w" (LAMBDA "z" (APP (ID "z") (ID "w")))) (LAMBDA "x" (LAMBDA "y" (APP (ID "y") (ID "x"))))

当然是 alpha 等价物，计算结果为 False。你能看出我做错了什么并纠正我吗？

Answer 1

正如评论中所讨论的那样，使用您尝试过的替换来定义和测试 alpha 等价性比乍看起来要难。也许您可以通过关注已经可见的特定问题来修复您的代码，但我建议采用另一种方法：

将两个表达式翻译成一个新的规范形式，可以从字面上进行比较。

对于新表格应该是什么，您有一些选择。我的直觉是使用一种新的 AST 数据类型来表达您在 De Bruijn indecies 中的 lambda 微积分。