비교 구문 트리가 모듈로 알파 변환

Question

예를 들어, 내가 컴파일러/증명 검사 일하고, 나는 구문 트리가 있다면 내가 이와 같은, 궁금 해서요 :

data Expr 
    = Lambdas (Set String) Expr 
    | Var String 
    | ... 

할 수있는 방법이 있다면 Expr의 alpha-equivalence (등가 모듈로 이름 바꾸기)를 확인하십시오. 그러나이 Expr은 람다의 변수 집합이 교환 가능하다는 점에서 람다 계산법과 다릅니다. 즉 매개 변수의 순서는 검사에 영향을 미치지 않습니다.

(간단히하기 위해 Lambda ["x","y"] ...은 Lambda ["x"] (Lambda ["y"] ...)과 구별되며이 경우 순서가 중요합니다.)

다른 말로 표현하면 두 개의 Exprs이 주어지면 하나의 이름에서 어떻게 효율적으로 이름 바꾸기를 찾을 수 있습니까? 이러한 종류의 조합 문제는 NP 완성의 냄새를 풍깁니다.

Answer 1

매개 변수의 commutativity는 지수 비교를 암시합니다 (true).

하지만 매개 변수 목록을 정규화하여 단일 순서로 비교하면됩니다. 그러면 이름 바꾸기와 비교되는 나무는 본질적으로 나무의 크기가 선형 일 것입니다.

내가 제안하는 것은 각 매개 변수 목록에 대해 하위 트리를 (순차적으로, 포스트 오더는 일관성있는 한 중요하지 않습니다.) 방문하고 매개 변수를 첫 번째 매개 변수 사용을 방문하십시오. 당신이 B 먼저 다음 두 번째가 발생하기 때문에

lambda(b,a) 

,와 b의 추가 만남은 중요하지 않습니다 : 그래서 당신은

lambda(a,b): .... b ..... a ... b .... 

이있는 경우 당신은 매개 변수의 목록을 정렬 할 것입니다. 트리를 정규화 된 매개 변수 목록과 비교하십시오.

람다 (lambda) 절의 연산자가 교환 가능하다고 주장하면 수명이 더 복잡해진다. 제 생각에 당신은 여전히 ​​그것을 정상화 할 수 있습니다.

Answer 2

Daan Leijen의 HMF에게 약간의 아이디어가 있습니다. (그는 또한 교환 법칙이 성립 건너 'foralls'에 대한 바인더 처리. 특히

을, 그는 신체의 발생 순서에 변수를 바인딩합니다.

가 그런 다음 용어의 비교는 같은 방법으로 모두 skolemizing 포함

그 결과를 비교.

우리는 그 skolemization가 locally nameless representation로 통과 대체하여보다 더 잘 할 수

.

data Bound t a = Bound {-# UNPACK #-} !Int t | Unbound a 

instance Functor (Bound t) where ... 
instance Bifunctor Bound where ... 

data Expr a 
    = Lambdas {-# UNPACK #-} !Int (Expr (Bound() a)) 
    | Var a 

는 이제 람다에서 바운드의 발생이 변수는 직접 바인딩 당신이 그 사건에 넣고 싶은 어떤 유형의 정보와 함께, 람다에 의해, 여기에서 나는 방금()을 사용했습니다.

닫힌 용어는 'a'에서 다형성을 가지며 사용 사이트별로 람다 요소를 정렬하면 (사용하지 않는 용어를 제거하여 람다를 항상 정규화 할 수 있습니다.) 알파 등가 용어는 간단히 (= =), 열려있는 용어가 필요한 경우에는 Expr String 또는 다른 표현으로 작업 할 수 있습니다.

Expr 및 Bound에 대한 더 자세한 아날 리 티브 버전은 실존 유형 및 유형 레벨을 사용하여 바인딩되는 변수의 수를 식별하고 Bound 생성자에서 'Fin'을 사용하지만, 불변량을 유지하기 위해 람다에서 발생하는 변수보다 더 많은 변수를 바인딩하지 않고 유형 정보가 Var (Bound n _)과 일치하여 n인데, 다른 유형을 유지하는 데 너무 많은 부담이 없습니다.

업데이트 : 내 bound 패키지를 사용하여 완전히 자체적으로 개선 된 버전을 사용할 수 있습니다!