实现alpha等价 - Haskell

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'].但我再次对Haskell很恐怖.你能不能给我一个如何实现它的线索？

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 = ???