수학적 귀납법과 반복문 불변식

100개의 도미노가 있을 때 두 가지 사실을 안다고 가정해보자.

첫 번째 도미노는 직접 손으로 밀어서 쓰러뜨린다.

한 도미노가 쓰러지면 다음 도미노 역시 반드시 쓰러진다.

그러면 마지막 도미노 또한 당연히 쓰러진다는 것을 직관적으로 알 수 있다.

수학적 귀납법은 이와 같이 반복적인 구조를 갖는 명제들을 증명하는데 사용된다.

귀납법 증명 3 Step

단계 나누기 : 증명하고 싶은 사실을 여러 단계로 나눈다.

첫 단계 증명 : 그 중 첫 단계에서 증명하고 싶은 내용이 성립함을 보인다.

귀납 증명 : 한 단계에서 증명하고 싶은 내용이 성립하면, 다음 단계에서도 성립함을 보인다.

귀납법은 알고리즘의 정당성 증명 시 가장 유용하게 사용되는 기법인데,

왜냐하면 대부분의 알고리즘은 어떠한 형태로든 반복적인 요소를 갖고 있기 때문이다.

귀납법을 이용해 알고리즘의 정당성을 증명할 때는 반복문 불변식 이라는 개념이 유용하게 쓰인다.

반복문 불변식 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건

불변식을 이용하면 반복문의 정당성을 다음과 같이 증명할 수 있다.

1. 반복문 진입시에 불변식이 성립함을 보인다.

2. 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. 다르게 말하면, 반복문 내용이 시작할 때 불변식이 성립했다면, 내용이 끝날 때에도 불변식이 항상 성립함을 보인다.

3. 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.

예 1) 이진 탐색과 반복문 불변식

//필수 조건: A는 오름차순으로 정렬되어 있다.
//결과: A[i-1] < x <= A[i]인 i를 반환한다.
//이때 A[-1]=음의 무한대, A[n]=양의 무한대라고 가정한다.
int binsearch(const vector<int>& A, int x){
int n=A.size();
int lo=-1, hi=n;
//반복문 불변식 1: lo<hi
//반복문 불변식 2: A[lo] < x <= A[hi]
//(*)불변식은 여기서 성립해야 한다.
while(lo+1<hi){
int mid=(lo+hi)/2;
if(A[mid]<x)
lo = mid;
else
hi = mid;
//(**) 불변식은 여기서도 성립해야 한다.
}
return hi;
}

초기 조건 while문이 시작할 때 lo와 hi는 초기값 -1과 n으로 초기화된 상태이다. 만약 n=0 이라면 while문을 아예 건너뛰기 때문에 불변식 1은 항상 성립한다. A[-1]은 음의 무한대, A[n]은 양의 무한대로 가정하므로 불변식 2 또한 성립한다.

유지 조건 while문 내부가 불변식을 깨뜨리지 않음을 보이면 된다.

불변식 1 : while문 내부로 들어왔다는 말을 hi와 lo의 차이가 2 이상이라는 의미이므로 mid 는 항상 두 값의 사이에 위치하게 된다. 따라서 mid를 lo에 대입하건 hi에 대입하건 항상 불변식 1은 계속 유지된다.

불변식 2 :

-A[mid]<x인 경우 : 반복문을 시작할 때 x<=A[hi]는 이미 알고 있었다. 따라서 A[mid]<x<=A[hi] 가 되므로, lo에 mid를 대입해도 불변식은 성립한다.

-x<A[mid]인 경우 : 반복문을 시작할 때 알고 있었던 A[lo]<x과 합쳐 보면 A[lo]<x<A[mid]를 얻을 수 있다. 따라서 hi에 mid를 대입해도 불변식 2는 성립한다.

알고리즘 정당성 증명