하스켈 람다 알파 동등한

Question

나는 람다에 대해 하스켈에서 알파 등가 함수를 적어 내려고했다.

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

좀 온라인 리소스를 읽은하지만 난 코드로 변환 할 수 없습니다. 감사합니다.

Answer 1

두 개의 표현식은 변수 이름을 변경하여 다른 표현식으로 바꿀 수 있습니다. 그럼 어떻게 잡을 수 있니? 두 가지 주요 방법이 있습니다.

1. 두 표현식에서 어느 변수 이름이 서로 일치해야하는지 추적하십시오.
2. (명시 적으로 또는 암시 적으로) 변수 이름 대신 범위를 포함하는 숫자가 사용되는 양식으로 변환합니다.

하는의이 첫 번째

-- 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이 알파 등가인지 확인하려면 x에 대한 바인딩이 y의 바인딩에 해당하고 y에 대한 바인딩이 x에 대한 바인딩에 해당하는지 확인해야합니다. 그렇지 않으면 \x.\y.x은 \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 

바라건대 당신은 이러한