Реализация Альфа-Эквивалентность в Haskell

Question

Я хочу, чтобы определить альфа-эквивалентностью с использованием этого определения данных

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

Что такое лучший способ сделать это?

Answer 1

Один из способов - преобразовать имена в индексы De Bruijn, где, например, 0 относится к переменной, связанной с самой внутренней охватывающей лямбдой, 1 следующей охватывающей лямбдой и т. Д. Таким образом, вместо абсолютных имен, вы используете относительные индексов, что дает вам альфа-эквивалентность и замену захвата избегающих бесплатно:

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) 

Теперь, альфа-эквивалентность проста:

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