本文介绍了在haskell中实现Alpha等价性的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我想用这个数据定义来定义Alpha-Equivalence
I want to define Alpha-Equivalence using this data definition
type Sym = Char
data Exp = Var Sym | App Term Exp | Lam Sym Exp
deriving (Eq, Read, Show)
这样做吗?
What is the best way to do this?
推荐答案
一种方法是将名称转换为De Bruijn索引,例如 0
引用最内层lambda绑定的变量, 1
下一个封闭lambda,依此类推。因此,您可以使用相对索引而不是绝对名称,从而为您提供alpha等价和避免捕获的替换:
One way is to convert names to De Bruijn indices, where e.g. 0
refers to the variable bound by the innermost enclosing lambda, 1
the next enclosing lambda, and so on. So instead of absolute names, you use relative indices, giving you alpha-equivalence and capture-avoiding substitution for free:
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)
您只需在名称范围内保留名称的 :
To do the conversion, you just keep an environment of the names in scope:
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等价性很简单:
Now, alpha equivalence is simple:
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
这篇关于在haskell中实现Alpha等价性的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!