ASPP - 5. 알고리즘 정당성 증명

9 minute read

알고리즘 정당성 증명
- 수학적 귀납법과 반복문 불변식
  - 수학적 귀납법
    - 수학적 귀납법의 세 단계
  - 반복문 불변식(loop invariant)
- 증명 기법들

알고리즘 정당성 증명

문제가 복잡해지면 알고리즘이 문제를 해결할 수 있는지 어떻게 알 수 있을까? 단위 테스트?

단위 테스트는 알고리즘에 문제가 있음을 증명할 수는 있지만, 알고리즘에 문제가 없음을 증명할 수는 없다

예전엔 이 말이 잘 이해가 안 됐다. 그런데 어려운 문제를 풀려고 이렇게 저렇게 코드를 짜다 보면
이 코드가 문제를 해결할 수 있을까?라거나
‘내가 짜는 알고리즘에 문제가 없어서 모든 테스트 케이스를 통과할 수 있다는 것을 어떻게 보장하지? 같은 의문이 들었다.

그러니, 내가 짜는 알고리즘이 1. 무엇을 목표로, 2. 어떻게, 3. 왜 그렇게 짜는지도 모른 채 되는대로 풀었던 셈이다.
풀면 다행이고, 못 풀면 그냥 그 시간 허탕친 셈이었고 남는 게 적었다.

고등학교 수학처럼 알고리즘을 유형에 따라 그냥 외우면 편할 수도 있고, 사실 선 암기 후 이해도 좋은 학습 방법이라 생각하지만, 머리가 굵어졌는지 이제는 그게 잘 안 된다.
코드를 짜면서도 ‘난 왜 이렇게 코드를 짜지?’ 같은 생각이 들면 잘 알지도 못하면서 푸는 척 하는 모습에 그냥 더이상 풀고 싶지가 않아진다.

결국 제대로 풀려면 증명에 대해 이해를 해야 하고, 그 과정에서 각종 수학적 기법이 동원되어야 한다고 한다.
당장 이해가 안 가더라도 정리를 할 필요성을 새삼 느낀다.

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

수학적 귀납법

증명 대상? 반복적인 구조를 갖는 명제들
알고리즘 정당성 증명 시 가장 유용하게 사용되는 기법

수학적 귀납법의 세 단계

단계 나누기

증명하고 싶은 사실을 여러 단계로 나눈다
귀납이라 함은 반복되는 사실로 일반화 하는 추리 방법이다
- 흔히 아는 잘못된 일반화인 백조는 희다, 왜냐하면 이제까지 관측된 백조는 모두 흰색이었으니까가 대표적이다
- 그럼 여기서 백조는 희다가 증명하고 싶은 사실이면, 백조 하나하나의 색을 확인하는 것이 단계 나누기다
반복문을 돌든, 재귀적으로 호출하든 어떤 식으로든 답을 찾아가는 단위가 있을 것이다. 즉 알고리즘 내에서 같은 패턴으로 반복되는, 시작과 끝이 있는 한 싸이클이 있을 것이다. 그 한 싸이클을 찾아서 정의하는 것으로 이해가 된다.

첫 단계 증명

증명하고 싶은 내용이 성립함을 처음 증명하는 것
백조를 하나 찾아서 흰 색임을 보이면 된다

귀납 증명

한 백조가 흰 색이었고, 다음 백조가 흰 색임을 보이는 것. 즉 반복적으로 발생함을 보이는 과정
어느 순간 검은 백조가 나올 것이고, 그러면 증명은 실패한다.

반복문 불변식(loop invariant)

반복문의 내용이 한 번 실행될 때마다 중간 결과가 답으로 가는 길 위에 잘 있는지를 명시하는 조건
반복문이 마지막에 정답을 계산하기 위해서는 항상 이 식이 변하지 않고 성립되어야 한다

반복문 불변식 증명

반복문 진입시에 불변식 성립함을 보인다
반복문 내용이 불변식을 깨뜨리지 않음을 보인다
- 반복문 내용 시작 시 불변식 성립
- 반복문 내용 끝날 때 불변식 성립
반복문 종료 시 불변식 성립하면, 정답 구했음을 보인다

/* 불변식은 여기에서 성립 */
while(comeCondition){
  /* 반복문 내용 시작 시 */
            ...
  /* 반복문 내용 끝날 때 */
  /* 불변식은 여기에서도 성립 */
}

이진 탐색과 반복문 불변식

/**
  * A[-1]은 음의 무한대, A[n]은 양의 무한대 가정
  * @param A 오름차순으로 정렬되어 있다
  * @param x 찾고자 하는 값
  * @return A[i-1] < x <= A[i]인 i를 반환
  */
public int binarySearch(List<Integer> A, int x) {
    int low = 0, high = A.size();
    /* 1. 반복문 불변식: low < high */
    /* 2. 반복문 불변식: A[low] < x <= A[high] */
    while (low < high) { /* 3. 반복문 종료 시: low >= high */
        int mid = low + (high - low) / 2;
        System.out.printf("mid: %d, (%d - %d) / 2: %d\n", mid, high, low, (high - low) / 2);
        if (A.get(mid) < x) {
            low = mid + 1; /* 책과 다른 부분. 책은 low를 -1로 초기화 */
        } else {
            high = mid;
        }
    }

    return high;
}

이진 탐색 내부의 while문은 총 두 개의 반복문 불변식 유지

$low \lt high$

작은 값은 큰 값보다 항상 작다
반복문 종료 시?
- $low \ge high$가 된다. 이때 $low \lt high$ 반복문 불변식과 조합을 하면,
- $high \le low \lt high$가 되며, low는 high일 수밖에 없다

$A[low] \lt x \le A[high]$

x는 작은 인덱스보다 크고 큰 인덱스보다 작거나 같은 인덱스에 위치한다

애초에 불변식이 성립한다고 가정했으니 이것은 당연히 성립

x라는 값이 리스트 A의 low 인덱스와 high 인덱스 사이에 존재함을 가정했으니 당연히 성립한다는 게 무슨 말일까?
만약 x에 해당하는 값이 A에 존재하지 않는다면 어떻게 될까? 불변식이 깨진다.
불변식에 대해 다시 상기해보자면,

불변식은 반복문이 마지막에 정답을 계산하기 위해서는 항상 이 식이 변하지 않고 성립해야 하는 것이다

따라서 불변식이 성립하는 한, x는 A[log]와 A[high] 사이에 존재한다

삽입정렬과 반복문 불변식

삽입정렬?
- 각 원소를 순서대로 고려하면서
- 이 원소를 앞에 있는 정렬된 부분 수열에
- 끼워넣는 작업을 반복

public void insertionSort(List<Integer> A) {
    /* 1. 반복문 불변식: A[0..i-1]은 이미 정렬되어 있다. */
    for (int i = 0; i < A.size(); i++) {
        /* 그렇다면 A[0..i-1]에 A[i]를 끼워넣는다. */
        int j = i;
        /* 2. 반복문 불변식: A[j + 1..i]의 모든 원소는 A[j]보다 크다 */
        while (j > 0 && A.get(j - 1) > A.get(j)) { /* 불변식이 맞지 않는 데이터가 있다면? */
            /* 불변식에 맞게 바꾼다 */
            /* 3. 반복문 불변식: A[0..i] 구간은 A[j]를 제외하면 정렬되어 있다 */
            Collections.swap(A, j - 1, j);
            j--;
        }
    }
}

1. 반복문 불변식: A[0..i-1]은 이미 정렬되어 있다

0부터 i-1이면 배열 내 전체 인덱스다. 즉, 정렬 작업 전에 이미 A가 정렬되어 있다고 가정하고 시작한다.
귀류법 같은 느낌인데,
- 정렬되었다고 가정하고
- 모순되는 데이터를 찾아서
- 모순을 해소함으로써 가정이 맞았음을 증명한다

2. 반복문 불변식: A[j + 1..i]의 모든 원소는 A[j]보다 크다

이 경우는 일종의 답정너다. 이 불변식을 지키기 위해 데이터를 바꿈으로써 정렬이 이뤄진다.
while (j > 0 && A.get(j - 1) > A.get(j)) 통해 모순되는 데이터를 찾는다

3. 반복문 불변식: A[0..i] 구간은 A[j]를 제외하면 정렬되어 있다

왜 j와 j-1만 비교할까? j와 j-1만 바꾸면 되나? j와 j-2, j-3 … j-i은 비교할 필요 없나? 필요없다
- 왜 필요없을까? 2. 반복문 불변식: A[j + 1..i]의 모든 원소는 A[j]보다 크다가 유지되고 있기 때문
- 앞선 반복문에서 만약 A[j + 1..i]보다 A[j]가 큰 경우, 즉 A.get(j - 1) > A.get(j)인 경우가 있다면 while문 안에서 스왑이 이뤄지고 2번 불변식이 유지된다
- 따라서 각 int j = i; 후 while문에서는 앞서 이미 검증된 j-2, j-3 등은 고려할 필요가 없다.
A[j]를 제외하면 정렬 되어 있다는 것은 무얼 의미할까?
- Collections.swap이 다른 원소들의 정렬 상태를 건드리지 않음을 의미한다
- 다른 원소들의 정렬 상태를 건드리지 않기 때문에, 앞서 이미 검증된 j-2, j-3 등은 정렬된 상태를 유지한다
증명
- j = 0? A[0]은 정렬되어 있다
- j > 0? A[j-1] > A[j]인 경우 A[j-1]과 A[j]만 바꾸면 나머지 정렬된 것들은 변하지 않는다

삽입정렬의 반복문 불변식 정리

처음에 정렬하려는 대상이 이미 정렬되었음을 가정하고, 불변식으로 설정한다.
정렬 조건을 불변식으로 만든다.
- 귀납적으로 정렬은 다음과 같다
  - $A[0] \le A[1]$
  - $A[1] \le A[2]$
  - $A[2] \le A[3]$
  - …
  - $A[i-2] \le A[i-1]$
  - 따라서 $A[j] \le A[j + 1..i]$가 된다
- $A[j] \le A[j + 1..i]$ 불변식이 유지되도록 Collections.swap을 한다.
이때 이미 정렬된 다른 원소들을 변경시키지 않음 역시 불변식으로 설정한다. 이를 통해 Collections.swap으로 인해 이미 정렬된 것이 변경되면, 전체 정렬이 무효화 되도록 설정한다

반복문 불변식: 결론

지금도 헷갈리지만, 처음보다는 조금 이해가 되는 거 같다.
처음에는 왜 혼자 가정하고 그게 성립하다고 하지?라고 생각했었다.
근데 이진 탐색 코드는 예제일 뿐이다. 실제로는 알고리즘을 푸는 사람이 반복문 불변식을 가정해야 한다.
즉,

데이터는 재귀적이든 반복문이든 어떤 반복적인 작업에 전달이 되고
알고리즘 조건과 데이터를 통해 귀납적으로 규칙을 발견하여 반복문 불변식을 가정하고
가정된 불변식에 따라 반복문 마지막에 정답을 계산해내는지 확인해야 한다

따라서 정당성 검증에도 마법은 없다. 만약 귀납적인 추론이 잘못되어 잘못된 불변식을 가정하면 어떻게 될까?
불변식에 맞지 않는 데이터를 확인하게 되고, 불변식과 귀납 추론은 깨지게 되며, 불변식은 더이상 불변식이 아니게 된다.

따라서 어느 반복문에서 어떤 데이터가 어떻게 유지되어야 하는지가 이미 머릿속에 있어야 한다

그렇다면 불변식을 가정할 수 있다는 것 자체가 애초에 어느 정도 문제를 풀 능력이 된다는 것…으로 이해가 된다.
결국 귀납 추론을 잘해서 정확한 규칙을 찾고, 규칙에 따라 불변식을 만드는 연습을 해야 할 것 같다.

증명 기법들

원하는 바와 반대되는 상황을 가정하고 논리를 전개해서 결론이 잘못됐음을 찾아내느 증명 기법
대개 어떤 선택이 항상 최선임을 증명하고자 할 때 많이 이용

귀류법: 책장 쌓기

조건
- $M_{i}$: 각 책장마다 버틸 수 있는 최대 무게
- $W_{i}$: 각 책장 자신의 무게
- above(i): i번째 책장 위에 쌓인 모든 책장의 집합
$\text{책장 위에 올라간 다른 책장들의 무게의 합} \le \text{견딜 수 있는 최대 무게}$.

\[\sum_{j \in above(i)}W_{j} \quad \le \;\; M_{i}\]

정렬 순서는 $M_{i}$와 $W_{i}$ 합이 가장 큰 것부터 아래에 놓는다

정렬 순서의 증명

가령 아래와 같은 책장 4개가 있다고 해보자

    [ C ]
[     A     ]
  [   B   ]

이 경우 앞서 원하는 정렬 순서인 A, B, C와는 반대가 된다. 그럼 이 반대가 되는 사실이 잘못되었음을 찾아내면 정렬 순서가 증명된다.

1. A와 B의 위치를 항상 바꿀 수 있음

A와 B의 위치는 항상 바꿀 수 있다. 바꾸는 것은 문제가 아니며, 바꾼 후 A가 B의 무게까지 견딜 수 있는지가 문제 된다.

2. A가 B의 무게를 견딜 수 있는지

$(\text{A가 견딜 수 있는 무게} + \text{A 책장의 무게}) \gt (\text{B가 견딜 수 있는 무게} + \text{B 책장의 무게})$가 된다. 이를 부등식으로 표현하면,

\[M_{A} + W_{A} \gt M_{B} + W_{B}\\\]

여기서 A가 버틸 수 있는 무게만 좌변에 남긴다

\[M_{A} \gt M_{B} + W_{B} - W_{A}\]

앞서 처음에 A 책장이 B 책장 위에 올라가 있었다.

    [ C ]
[     A     ]
  [   B   ]

여기서 B가 버틸 수 있는 무게는 $\text{A 책장의 무게} + \text{A 책장 위 책장들의 무게}$가 되며, 이에 따르면 다음 부등식이 성립한다.

\[X = \sum_{j \in above(A)}W_{j}\\ M_{B} \ge W_{A} + X\]

두 부등식을 정리하면

\[M_{A} \gt M_{B} + (W_{B} - W_{A}) \ge W_{A} + X + (W_{B} - W_{A})\\ M_{A} \gt X + W_{B}\]

X는 A 위에 올라가 있는 상자들의 무게의 합이고 $W_{B}$는 B 책장의 무게로, 두 합이 $M_{A}$보다 작으므로 A 책장도 B와 나머지 모든 책장을 지탱할 수 있다
따라서 $M_{i}$와 $W_{i}$ 합이 가장 큰 것부터 아래에 놓는다라는 정렬 순서로 쌓았을 때 가장 높은 탑을 얻지 못하는 경우는 존재하지 않는다.

비둘기집의 원리

나뭇잎이 1,000개에서 10,000개인 나무가 10만 그루 존재할 때, 나뭇잎 수가 같은 나무가 존재할까? 결론부터 말하면 반드시 존재한다.

여기서 중요한 것은 가능한 나뭇잎 수의 경우의 수와 총 나무의 개수다.
나뭇잎 수의 베리에이션은 1,000과 10,000 사이의 숫자가 가능하며, 가능한 나뭇잎 수의 경우는 1,000개, 1,001개, … 10,000개로 9,001가지가 있다.
$\left \{ \text{나뭇잎} \in \mathbb{N}| 1,000 \le \text{나뭇잎} \le 10,000 \right \}$

가능한 나뭇잎 수의 경우는 9,001개인데 10만 그루의 나무가 있다면, 반드시 나뭇잎 수가 같은 나무가 존재할 수밖에 없다.
9,001가지 경우의 수를 100,000개의 나무에 분배해야 하기 때문이다. 이를 비둘기집의 원리(Pigeonhole Principle)이라고 한다.

10마리의 비둘기가 9개의 비둘기집에 모두 들어갔다면, 2마리 이상이 들어간 비둘기 집이 반드시 하나는 있게 마련이다.

처음에 생각했을 때 나뭇잎 수가 같은 나무가 존재할까? 어떻게 알지? 수를 다 세봐야 하나? 같은 생각이 떠올랐다.
우선 1,000, 10,000, 100,000 같은 일일이 세기 어려운 큰 숫자를 어떻게 처리할지가 걱정됐다.
그리고 존재하는지 여부를 어떻게 true 또는 false로 증명할지가 막막했다.
그런데 이를 9,001가지 경우의 수를 100,000개의 나무에 분배라고 표현하니 단번에 이해가 됐다.
4개씩 있는 3종류 사탕 12개를 10명이 먹으면, 두 명 이상은 반드시 같은 사탕을 먹게 된다.

더 적은 종류의 데이터를 더 많은 수의 데이터에 분배할 경우, 같은 데이터를 돌려쓰는 경우가 생길 수밖에 없다.

동전 뒤집기

순환 소수 찾기

구성적 증명

우리가 원하는 어떤 답이 존재한다는 사실을 증명하기 위해 사용
답이 존재한다는 사실을 논증하는 것(X), 답의 실제 사례 제시 또는 답을 만드는 방법을 제시하는 증명(O)

안정적 결혼 문제

Twitter Facebook LinkedIn