實施阿爾法等價 - 哈斯克爾

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。