在 haskell 中实现 Alpha 等效性答案

【问题标题】：Implementing Alpha-Equivalence in haskell在 haskell 中实现 Alpha 等效性
【发布时间】：2016-10-29 06:16:18
【问题描述】：

我想使用这个数据定义来定义 Alpha-Equivalence

type Sym = Char
data Exp = Var Sym | App Term Exp | Lam Sym Exp 
deriving (Eq, Read, Show)

最好的方法是什么？

【问题讨论】：

收到回复后请不要删除逃跑
请参阅schoolofhaskell.com/user/edwardk/bound，了解让您不必不必进行 alpha 等效的技术说明
仅供参考，您无需进行 alpha 转换即可实现 lambda 演算评估器

标签： haskell lambda-calculus

【解决方案1】：

一种方法是将名称转换为 De Bruijn 索引，例如0 指的是由最里面的封闭 lambda 绑定的变量，1 是下一个封闭的 lambda，依此类推。因此，您可以使用 relative 索引代替 absolute 名称，从而免费为您提供 alpha 等价和避免捕获的替换：

type Sym = Char
data Exp = Var Sym | App Exp Exp | Lam Sym Exp
  deriving (Eq, Read, Show)

type Ind = Int
data Exp' = Var' Ind | App' Exp' Exp' | Lam' Exp'
  deriving (Eq, Read, Show)

要进行转换，您只需在范围内保留名称的环境：

db :: Exp -> Exp'
db = go []
  where

    -- If we see a variable, we look up its index in the environment.
    go env (Var sym) = case findIndex (== sym) env of
      Just ind -> Var' ind
      Nothing -> error "unbound variable"

    -- If we see a lambda, we add its variable to the environment.
    go env (Lam sym exp) = Lam' (go (sym : env) exp)

    -- The other cases are straightforward.
    go env (App e1 e2) = App' (go env e1) (go env e2)

现在，alpha 等价很简单：

alphaEq x y = db x == db y
-- or:
alphaEq = (==) `on` db

例子：

-- λx.x ~ λy.y
Lam 'x' (Var 'x') `alphaEq` Lam 'y' (Var 'y')  ==  True

-- λx.λy.λz.xz(yz)
s1 = Lam 'x' $ Lam 'y' $ Lam 'z'
  $ Var 'x' `App` Var 'z' `App` (Var 'y' `App` Var 'z')

-- λa.λb.λc.ac(bc)
s2 = Lam 'a' $ Lam 'b' $ Lam 'c'
  $ Var 'a' `App` Var 'c' `App` (Var 'b' `App` Var 'c')

-- λa.λb.λc.ab(ac)
s3 = Lam 'a' $ Lam 'b' $ Lam 'c'
  $ Var 'a' `App` Var 'b' `App` (Var 'a' `App` Var 'c')

s1 `alphaEq` s2  ==  True
s1 `alphaEq` s3  ==  False

【讨论】：