Unification

3. Unification (단일화)

 

  1차 술어 논리의 문장 P와 Q가 있다고 해보자. 이 두개의 문장에 있는 각 변수들을 서로 match 시키는 작업을 Unification이라고 한다. 예를들어, ∃X friend(maxim,X) 라는 predicate sentence가 있을때, 이를 unification을 하게되면 friend(maxim,jim) 이 된다. 이때에 도메인에는 maxim의 친구 목록중에 jim이 존재 해야한다. 그리고 이를 {jm/X} 로 표시할 수 있다. 이것은 X를 jim으로 바꿔 주었다는 뜻을 가진다. 좀더 예제를 들어보자. plus(X,Y,Z) 라는 sentence가 있다고 해보자. 여기에 {5/X,3/Y,2/Z}를 적용 시키면 plus(5,3,2)가 되고, 결과값은 10이 된다. 여기에서 숫자(5,3,2)들은 각각 X,Y,Z의 substitute라고 하고, X,Y,Z는 original expression 이라고 한다. 이처럼 단일화를 할때에는 아래의 룰을 따른다.

 

1. Constant (상수) 는 Variable(변수) 의 substitute(대리자)가 될 수 있다.

2. Constant는 다른 것으로 바뀔 수 없다. (대리자를 통한 치환을 할 수 없다.)

3. Variable은 해당 variable을 포함하는 대리자와  unify 될 수 없다. (ex. unify(X, p(X)) is wrong) 

4. match를 하려는 predicate sentence에는 unify를 통한 변화를 모두 적용 시켜 줘야 한다.

   (ex. plus(X,Y,Z)  와 minus(X,R,T) 가 있을때 {5/X} 를 통해 plus(5,Y,Z)로 바꿔주었다면, minus(5,R,T) 로 역시 변환 해야한다.)

 

 

그리고 unify 룰을 서로 합성 시키는 것이 있는데, 이를 composition(합성) 이라고 한다. 각 단계별로 나오는 unification method 를 합성시키는 것이다. 예를들어 단계별로 나오는 method가 

 

 

{X/Y, W/Z}, {V/X}, {a/V, f(b)/W} 

 

라면   {a/Y, f(b)/Z} 로 composition결과를 만들어 낼 수 있다.

 

그렇다면 이제 위에서 알아본 모든 방법을 가지고 실제 예제를 unification 해보겠다. 아래의 예제를 통해, unify method를 알아내는 방법을 익히도록 하자.

 

unify( (parents X(father X)(mother tom), (parents tom(father tom) Y) )는 차례대로 천천히 unify해 나간다. 2개의 sentence를 앞에서부터 비교하여, 서로 같은 부분을 떼어내어 따로 unify를 하고, 다른 부분은 서로 같게 고칠 수 있으면, 고치고 그렇지 않으면 한쪽에 모두 몰아 넣는다.

 

(1)

 

(parents X(father X)(mother tom)

(parents tom(father tom) Y)           의 첫번째 공통점은 parents 이다. 그러므로 이를 따로 unify를 진행한다.

 

unify(parents, parents) 을 아무러 method없이 떼어내는데 성공했다.

 

 

 

(2)

 

X(father X)(mother tom)

tom(father tom) Y            을 다시 unify하려고 보니, X와 tom이 서로 매치가 된다. 상수는 바꿀 수 없음로 X를 변환한다.

 

 unify(x,tom)이 분리 되었고, 이를 통해 

{tom/X} method가 도출되었다.

 

메서드가 구해졌으니, 이를 남은식에 모두 적용 시킨다. X 는 tom으로 치환된다.

 

(3)

 

(father tom)(mother tom)

(father tom) Y                 을 unify 하니, father 와 뒤의 상수 가 같은 형태 이다. 그러므로 이를 분리 하는데 먼저

 

unify(father tom, father tom) 으로 분리 되고, 다시 한번 분리 되어

 

unify(father, father) 과 unify(tom,tom) 이 된다.  역시, 메서드의 사용 없이 분리가 완료 되었다.

 

 

(4)

 

mother tom

Y                마지막이다. Y와 mother tom은 match 되어야 하므로,

 

unify(mother tom, Y) 로 unify되고,

{mother tom/Y} method가 도출된다.