我正在尝试在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。你能看出我做错了什么并纠正我吗？
1条答案
按热度按时间tp5buhyn1#
正如评论中所讨论的，像你尝试的那样使用替换来定义和测试alpha等价性比看起来要困难得多。也许你可以通过专注于已经可见的特定问题来修复你的代码，但我建议使用另一种方法：
将这两个表达式翻译成一个新的规范形式，可以从字面上进行比较。
你可以选择新的形式，我的直觉是一个新的AST数据类型，用De Bruijn indecies来表达lambda caculus。