알고리즘문제해결전략 - 알고리즘 정당성의 증명

5장 알고리즘의 정당성 증명

• 증명을 소홀히 하지 마라
• 알고리즘 외우지 말고 증명을 이해해라

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

• 100개의 도미노가 존재할 때 다음 두 가지 사실을 알고 있다.
• 첫 번째 도미노는 직접 손으로 쓰러트려야 한다.
• 한 도미노가 쓰러지면 다음 도미노는 반드시 쓰러진다.
  귀납법의 증명은 크게 3가지로 나뉜다.
• 단계 나누기 : 증명하고 싶은 사실을 여러 단계로 나눈다.
  • 여기선 100개의 도미노를 하나의 도미노에 대한 규칙으로 나눴다. 당연한 소리지만 단계로 나누는 것이 가장 중요하다.
• 첫 단계 증명 : 그중 첫 단계에서 증명하고 싶은 내용이 성립함을 보인다.
• 귀납 증명 : 한 단계에서 증명하고 싶은 내용이 성립하면, 다음 단계에서도 성립함을 보인다. 앞의 예에서 한 도미노가 쓰러지만 다음 도미노는 반드시 쓰러짐을 보이는 것이 이 과정이다.

예제 - 사다리 게임

사다리 게임은 맨 위의 선택지와 맨 아래 선택지가 언제나 1:1 대응이 되는 것을 알 수 있다. 귀납법을 통해서 증명 해 보자.

• 단계 나누기 : 텅 빈 N개의 세로줄에서부터 시작해서 원하는 사다리가 될 때 까지 하나씩 가로 줄을 그어 간다고 가정한다. 이 때 가로 줄을 하나 긋는 것을 한 단계 라고 정의한다.
• 첫 단계 증명 : 텅 빈 N개의 세로줄에는 항상 맨 위 선택지와 맨 아래 선택지가 1:1 대응이 된다.
• 귀납 증명 : 가로줄을 그어서 두 개의 세로줄을 연결했다고 가정했을 때, 두 세로줄의 결과는 서로 뒤바뀐다. 두 세로줄의 결과가 바뀌더라도 1:1 대응은 변함이 없기 때문에 그 어떤 다음 가로줄이 추가되어도 1:1 대응이 유지됨은 변화하지 않는다.

반복문 불변식(loop in-variant)

귀납법이 알고리즘의 정당성을 증명할 때 가장 유용하게 사용되는 기법이다.
반복문안에 들어가 있는 코드는 실행 환경에서 절대 바뀌지 않기 때문에 똑같은 논리로 계속 반복 될 것이다.

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

1. 반복문 진입시에 불변식이 성립함을 보인다.
2. 반복문 내용이 불변식을 깨트리지 않음을 보인다. 다른게 말하면, 반복문 내용이 시작할 때 불변식이 성립했다면 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
3. 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.

1번과 2번 항목이 증명됐다면 수학적 귀납법을 이용해 이들은 반복문이 종료 할 때까지 항상 이 불변식이 성립함을 보일 수 있다. 예를 들어 while문을 짠다고 하면 이렇게 한다.

//(*) 불변식은 여기서 성립해야 한다.
while(어떤 조건){
    //반복문 내용의 시작
    ..
    //반복문 내용의 끝
    //(**)불변식은 여기서도 성립해야 한다. 
}

이진 탐색과 반복문 불변식

//필수 조건: A는 오름차순으로 정렬되어 있다.
//결과: A[i-1] < x <= A[i]인 i를 반환한다.
//이때 A[-1] = 음의 무한대, A[n] = 양의 무한대라고 가정한다.

int binsearch(const vetor<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이고, 두 번째는 A[lo] <x <=A[hi]이다. 이 불변식이 while문이 완전히 종료하고 함수의 마지막 줄에 올 때까지 계속 성립했다고 가정해 보자.

• lo +1 = hi : while문이 종료했으니 lo+1 >= hi 인데, 불변식에 의하면 lo < hi 이므로 lo+1 = hi일 수 밖에 없다.
• A[lo] < x <= A[hi] 이건 애초에 불변식이라고 가정했으니 당연히 성립한다.

엄밀하게 말하면 다음과 같이 증명된다.

• 초기 조건 : 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 <= [mid]인 경우 : 반복문을 시작할 때 알고 있었던 A[lo] < x와 합쳐보면 A[lo] < x <= A[mid]임을 알 수 있다. 그러므로 hi에 mid를 대입해도 불변식 2는 성립한다.

 

이러한 과정을 거처 while문이 종료되면 우리가 원하는 값이 A[hi]에 저장되어 있음을 알 수 있다. 까다로운 코드를 짤 때 해당 코드가 가져야 할 불변식을 파악하고 작성하면 좀더 오류가 적은 코드를 작성 할 수 있다.