实施阿尔法等价 - 哈斯克尔

Question

所以让我定义的几件事情：

type Name = String 

data Exp = Var Name 
     | App Exp Exp 
     | Lam Name Exp 
    deriving (Eq,Show,Read) 

我想定义alpha-equivalence，这是

alpha_eq :: Exp -> Exp -> Bool 
-- The terms x and y are not alpha-equivalent, because they are not bound in a lambda abstraction 
alpha_eq (Var x) (Var y) = False 
alpha_eq (Lam x e1) (Lam y e2) = False 
alpha_eq (App e1 e2) (App e3 e4) = False 

例如Lam "x" (Var "x")和Lam "y" (Var "y")都是等价的。不过，我在Haskell上既新鲜又可怕。有人可以提供关于如何实施alpha_eq的线索吗？有一件事我想过在这种情况下使用Map Name Int所以我会：

['x' -> 0] ['y' -> 0] 

所以在这种情况下Map['x'] == Map['y']。但是，我在哈斯克尔又一次很可怕。你能否给我一个线索如何实现它？

Answer 1

是的，使用Map一个正确的想法（尽管考虑关键和值类型应该是什么;与Map Name Int你需要两个额外的参数，而不是一个）。您需要将其添加为辅助函数的说法，我不会给全面实施既然你问了只有线索：

alpha_eq e1 e2 = alpha_eq' e1 e2 env0 where 
    env0 = ??? 
    alpha_eq' (Var x) (Var y) env = ??? 
    alpha_eq' (Lambda x e1) (Lambda y e2) env = ??? 
    alpha_eq' (App e1 e2) (App e3 e4) env = ??? 
    -- you don't want to throw an error in all other cases 
    alpha_eq' _ _ env = ??? 

Answer 2

你也可以将单独的函数subst :: Name -> Exp -> Exp -> Exp。然后，alpha_eq林情况变得

alpha_eq :: Exp -> Exp -> Bool 
... 
alpha_eq (Lam x xb) (Lam y yb) = xb `alpha_eq` subst y (Var x) yb 
... 

Excersise：找出其他alpha_eq案件和实施subst。