Haskell Lambda Alpha 等价答案

【问题标题】：Haskell Lambda Alpha EquivalenceHaskell Lambda Alpha 等价
【发布时间】：2017-12-07 22:32:47
【问题描述】：

我正在尝试在 Haskell 中为 lambda 写一个 alpha 等价函数。

data Expr = App Expr Expr | Lam Int Expr | Var Int deriving (Show,Eq)

我已经阅读了一些在线资源，但无法将它们转换为代码。谢谢

【问题讨论】：

实现。如果有人可以在 haskell 中给我一些代码，以便在此数据类型上实现 alpha 等价
你能告诉我们你的尝试吗？
Implementing Alpha-Equivalence in haskell的可能重复

标签： haskell lambda-calculus

【解决方案1】：

因此，如果您可以通过重命名变量将一个表达式转换为另一个表达式，则两个表达式是 alpha 等价的。那么我们如何才能捕捉到这一点呢？主要有两种方式：

跟踪两个表达式中哪些变量名必须相互对应。
（显式或隐式）转换为使用封闭范围编号而不是变量名的形式。

我们去第一个

-- helper functions for association lists
type Alist a = [(a,a)]
assoc, rassoc :: Eq a => a -> Alist a -> a
assoc x ((a,b):ps) = if x == a then b else assoc x ps
rassoc x = assoc x . map (\(a,b) -> (b,a))
acons a b l = (a,b):l

(=*=) :: Expr -> Expr -> Bool
a =*= b = eq [] a b where
  eq l (Lam n x) (Lam m y) = eq (acons n m l) x y
  eq l (Var n) (Var m) = assoc n l == m && n == rassoc m l
  eq l (App f u) (App g v) = eq l f g && eq l u v
  eq l _ _ = False

这里唯一真正的微妙之处是比较变量的情况。要检查x 和y 是否是alpha 等价的，我们需要检查x 的绑定是否对应于y 的绑定并且y 的绑定对应于x 的绑定。否则我们可能会说 \x.\y.x 是 alpha 等价于 \y.\y.y。

另外值得注意的是，格式错误的表达式会导致匹配失败。

下面是隐式执行第二个选项的方法：

varN :: Eq a => a -> [a] -> Int
varN a xs = v 0 xs where
  v n (x:xs) = if a == x then n else v (n+1) xs

a =*= b = eq [] [] a b in where
  eq k l (Lam n x) (Lam m y) = eq (n:k) (m:l) x y
  eq k l (Var n) (Var m) = varN n k == varN m l
  eq k l (App f u) (App g v) = eq k l f g && eq k l u v
  eq k l _ _ = False

希望你能看到它们是等价的

【讨论】：

【解决方案2】：

type SymToSym = Map String String

alphaEqHelper :: Lexp -> Lexp -> SymToSym -> SymToSym -> Bool
alphaEqHelper (Lambda lname lfunc) (Lambda rname rfunc) ltor rtol =
  alphaEqHelper lfunc rfunc (Map.insert lname rname ltor) (Map.insert rname lname rtol)
alphaEqHelper (Apply lfunc largs) (Apply rfunc rargs) ltor rtol =
  alphaEqHelper lfunc rfunc ltor rtol && alphaEqHelper largs rargs ltor rtol
alphaEqHelper (Atom lname) (Atom rname) ltor rtol
  | Map.member lname ltor && Map.member rname rtol =
    fromJust (Map.lookup lname ltor) == rname
      && fromJust (Map.lookup rname rtol) == lname
  | Map.member lname ltor || Map.member rname rtol = False
  | otherwise = lname == rname
alphaEqHelper _ _ _ _ = False

alphaEq :: Lexp -> Lexp -> Bool
alphaEq llexp rlexp =
  alphaEqHelper
    llexp
    rlexp
    Map.empty
    Map.empty

【讨论】：