Unification

단일화(Unification) : 이재규 외 : 긍정식 (Modus Ponens) 와 같은 추론규칙 (Inference Rule) 을 적용하기 위해서는 두 개의 문장이 문법적으로 서로 동일한 형태를 갖는지를 평가하는 매칭 (Matching) 기능이 있어야 한다. 명제계산 (Propositional Calculus) 에서는 매칭이 간단하게 이루어질 수 있지만, 술어계산 (Predicate Calculus) 에서는 변수부호가 있으므로 매칭과정이 복잡하게 된다. 이러한 문장간의 매칭을 효과적으로 처리해주는 과정을 단일화 라고 한다.

Wikipedia : Unification : 단일화는 Prolog 의 주요 개념중의 하나이다. 그것은 변수의 내용을 bind 하는 메카니즘을 나타내며 일종의 한번의 할당 (one-time assignment) 으로 보여질 수 있다. Prolog 에서 이 동작은 기호 "=" 으로 표기한다.

1. uninstantiated 변수 X (예를들면 이전에 어떤 단일화도 수행되지 않았던 변수) 는 uninstantiated variable (그리고 효율적으로 그 alias 가 된다) 이나 atom 또는 term 과 단일화 될수있다.
2. 하나의 atom 은 같은 atom 과만 단일화 할수있다.
3. 만일 terms 의 heads 와 arities 가 같은 문장이고 인수들이 단일화된다면, 하나의 term 은 또다른 term 과 단일화된다 (이것은 재귀 행동이라는 것을 주목).

그 선언적 성격 때문에, 단일화의 순서에서 그 명령은 (보통) 어떤 역할도 가지지 않는다.

단일화의 예

A=A

Succeeds (항진명제 (Tautology))

A=B, B=abc

Both A and B are unified with the atom abc

xyz=C, C=D

Unification is symmetric

abc=abc

Unification succeeds

abc=xyz

Fails to unify, atoms are different

f(A)=f(B)

A is unified with B

f(A)=g(B)

Fails, the heads of terms are different

f(A)=f(B,C)

Fails to unify, because terms have different arity

f(g(A))=f(B)

Unifies B with the term g(A)

f(g(A), A)=f(B, xyz)

Unifies A with the atom xyz and B with the term g(xyz)

A=f(A)

Infinite unification, A is unified with f(f(f(f(...)))).

A=abc, xyz=X, A=X

Fails to unify; effectively abc=xyz

Visual Prolog : Matching Things Up: Unification : goal 을 만족시키기 위해 각자의 subgoal 을 만족시켜야 하고 또한 각 인수와 match 되는 clause 를 찾기위해 프로그램의 위에서 아래로 search 하게 된다. goal 과 match 되는 clause 를 찾으면 goal 과 clause 가 identical 해지도록 free variable 에 값이 bind 된다. 이때 goal 은 clause 에 unify 되었다고 말해지고 이러한 matching 과정을 unification 이라 한다.

단일화 알고리즘 (Unification Algorithm) : Elaine Rich