최적의 "가장 일반적인 통합제"알고리즘은 무엇입니까?

Question

질문

가장 효율적인 MGU 알고리즘은 무엇입니까? 시간 복잡성은 얼마입니까? 스택 오버 플로우 답변으로 설명하기에 충분히 간단합니까?

Google에서 답을 찾으려고 노력했지만 ACM 구독을 통해서만 액세스 할 수있는 개인 .pdfs를 계속 찾고 있습니다.

SICP에서 한 번의 토론을 찾았습니다. 여기

"가장 일반적인 통일 알고리즘"이 무엇인지 설명 : "자유 변수"와 "상수"를 포함하는 두 개의 표현 나무를 가져 가십시오 ...

 e1 = (+ x? (* y? 3) 5)
 e2 = (+ z? q? r?)

그런 다음 가장 일반적인 통합 알고리즘은 두 표현식을 동일하게 만드는 가장 일반적인 바인딩 세트를 반환합니다.

즉

mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5

"대부분의 일반"에 의해 대신 (x = 1)과 (z = 1)을 바인딩 할 수 있으며 E1과 E2도 동등하게 만들 수 있지만 더 구체적입니다.

SICP 기사는 합리적으로 비싸다는 것을 암시하는 것으로 보입니다.

정보를 위해, 내가 묻는 이유는 유형의 추론 이이 "통일"알고리즘과 관련이 있다는 것을 알고 있기 때문입니다.

Answer 1

실제로 사용되는 간단한 알고리즘 (예 : Prolog)은 병리학 적 사례의 경우 지수입니다.

Martelli와 Montanari의 이론적으로보다 효율적인 알고리즘이 있지만 (IIRC는 선형입니다) 실제로 발생하는 간단한 경우에는 훨씬 느리므로 많이 사용되지 않습니다.

Answer 2

바이더와 스나이더 구문 통일 및 정식 통일을 위해 여러 통일 알고리즘을 발표했습니다.

그들은 그들의 세 번째 구문 통일 알고리즘 (섹션 2.3)이 O (n alpha (n))에서 실행된다고 말합니다. 여기서 알파 (n)는 역 Ackermann 기능입니다. 실제 상황에서는 작은 상수와 동일합니다.