수학적 귀납법 ↔ 루프 불변식

요약

반복문이 맞다는 증명은 도미노처럼 넘어가는 수학적 귀납법을 “몇 바퀴 돌았나”에 쓴 것이다. 처음에 참이라는 것이 첫 도미노이고, 한 바퀴 돌아도 참으로 남는다는 것이 다음 도미노를 넘어뜨리는 규칙이다. 그래서 이 둘만 보이면 몇 바퀴 뒤든 참이다. 다만 바퀴 수에 대한 귀납은 반복문이 언젠가 멈춘다는 것까지는 알려 주지 않아서, 매 바퀴 줄어드는 0 이상의 정수를 따로 찾아야 한다.

먼저 비교해 보기

표를 펼치기 전에 두 사례의 공통 구조와 대응 관계를 먼저 적어 본다.

이산수학: 수학적 귀납법의 홀수 합	알고리즘: 이분 탐색의 lower_bound
증명할 것: \(P(k)\): \(1 + 3 + \cdots + (2k - 1) = k^2\)	증명할 것: 바퀴를 시작할 때마다 \(I\): \(a[0..lo-1]\)은 모두 \(x\) 미만, \(a[hi..n-1]\)은 모두 \(x\) 이상, \(0 \le lo \le hi \le n\)
첫 경우: \(k = 1\)이면 \(1 = 1^2\)	첫 바퀴 전: \(lo = 0\), \(hi = n\)이면 두 구간이 비어 참
한 걸음: \(k^2 + (2k + 1) = (k + 1)^2\)	한 바퀴: \(lo < hi\)일 때 \(a[mid] < x\)면 \(lo = mid + 1\), 아니면 \(hi = mid\). 어느 쪽이든 \(I\)가 남는다
세는 것: 더한 홀수의 개수 \(k\)	세는 것: 돈 바퀴 수. 코드에는 없다
멈춤: 없다. 모든 \(k \ge 1\)을 다룬다	멈춤: \(hi - lo\)가 매 바퀴 1 이상 줄어 언젠가 \(lo = hi\)
예: \(k = 4\)이면 \(1 + 3 + 5 + 7 = 16 = 4^2\)	예: \(a = [2, 4, 4, 7, 9, 12, 15, 20]\), \(x = 7\)이면 \((lo, hi)\)가 \((0, 8) \to (0, 4) \to (3, 4) \to (3, 3)\)이고 답은 3

대응 관계

알고리즘	수학	공통 구조
불변식 \(I\): \(lo\), \(hi\)의 상태에 대한 진술	명제 \(P(t)\): “\(t\)바퀴 이상 돈다면, \(t\)바퀴 뒤의 상태가 \(I\)를 만족한다”¹	증명할 성질
지금까지 돈 바퀴 수 \(t\)	귀납 변수	무엇에 대한 귀납인가
초기화: \(lo = 0\), \(hi = n\)이면 두 구간이 비고 \(0 \le 0 \le n \le n\)	기저 \(P(0)\)²	첫 경우
이번 바퀴 시작에서 \(I\)가 참이라고 둔다	귀납 가정 \(P(t)\)	이미 넘어진 도미노
유지: \(I\)와 반복 조건 \(lo < hi\)가 참이면 한 바퀴 뒤에도 \(I\)	귀납 단계 \(P(t) \Rightarrow P(t + 1)\)²	한 걸음 넘어가기
몇 바퀴 뒤든 \(I\)가 참	\(\forall t \ge 0,\ P(t)\)	결론
끝난다: \(hi - lo\)는 0 이상의 정수이고 매 바퀴 1 이상 준다	정렬 원리³	0 이상의 정수는 끝없이 줄 수 없다
종료: 멈춘 바퀴 수 \(T\)에서 \(I\)와 \(lo \ge hi\)를 합치면 \(lo = hi\), 답은 \(lo\)	\(\forall t,\ P(t)\)를 \(t = T\)에 쓰기	결론을 원하는 꼴로 읽기
재귀로 쓴 이분 탐색: 남은 칸 수 \(hi - lo\)에 대한 증명	강한 귀납법³	더 작은 모든 경우를 가정

어디까지 같은가

초기화와 유지가 모든 바퀴를 덮는 것까지는 귀납법 그대로다². 다만 귀납 변수가 코드에 없다. \(I\)는 바퀴 수를 말하지 않고 \(lo\), \(hi\)의 상태만 말한다. 그래서 “\(t\)바퀴 뒤의 상태가 \(I\)를 만족한다”로 바꿔 읽어야 귀납법이 된다. 수학적 귀납법 문서의 s += 2*k - 1 예에서는 반복 변수 \(k\)가 곧 바퀴 수라서 이 차이가 드러나지 않는다.
유지는 반복 조건을 하나 더 가정한다. 보통 귀납 단계의 가정은 \(P(t)\) 하나다. 유지는 \(I\)에 더해 \(lo < hi\)를 쓴다⁴. 이 조건이 “\(t + 1\)번째 바퀴가 실제로 돈다”에 해당한다. 바퀴가 돌지 않으면 \(P(t + 1)\)은 “돈다면”이 거짓이라 저절로 참이다¹. 반복 조건을 빼면 유지가 깨진다. \(lo = hi = n\)은 \(I\)를 만족하지만 \(mid = n\)이라 \(a[n]\)을 읽어 범위를 넘는다.
바퀴 수에 대한 귀납은 멈춤을 주지 않는다. 이 귀납은 “몇 바퀴 뒤든 \(I\)“까지만 준다. 언젠가 멈춘다는 것은 두 번째 논증으로 보인다. 매 바퀴 1 이상 줄어드는 0 이상의 정수 \(hi - lo\)를 잡고 정렬 원리를 쓴다. 그래서 유지는 통과하고 멈춤에서만 깨지는 코드가 있다. 이분 탐색 문서의 오해인 lo = mid가 그렇다. “멈춘다면 맞다”까지만 보인 것을 부분 정확성(partial correctness)이라 한다⁴.
바퀴 수 대신 남은 칸 수로 귀납하면 멈춤도 함께 나온다. 명제를 “\(I\)가 참이고 \(hi - lo = m\)인 상태에서 출발하면 반복문이 멈추고 \(x\) 이상인 첫 칸을 돌려준다”로 잡는다. 한 바퀴 뒤 남은 칸 수는 \(\lfloor m/2 \rfloor\)(\(\lfloor\ \rfloor\)는 소수점 아래를 버린 정수) 이하로 뛰므로 강한 귀납법을 쓴다. 재귀와 백트래킹의 “재귀 함수가 맞다는 것” 정리와 같은 모양이다. 멈춤을 따로 보여야 했던 것은 귀납법의 한계가 아니라, 귀납 변수로 바퀴 수를 고른 결과다.
불변식은 직접 고르고, 종료에서 답이 나올 만큼 강하게 고른다. 귀납법 연습 문제는 증명할 \(P\)가 주어진다. 반복문에서는 불변식을 스스로 정하고, 멈췄을 때 답을 읽을 만큼 강하게 잡아야 한다. lower_bound에서 왼쪽 조건(\(a[0..lo-1]\)은 모두 \(x\) 미만)과 범위 조건(\(0 \le lo \le hi \le n\))만 지켜도 유지는 된다. 하지만 이것만으로는 멈췄을 때 \(lo\)가 “\(x\) 이상인 첫 칸”인지 모른다. 예를 들어 \(a = [1, 5]\), \(x = 3\)에서 \(lo = hi = 0\)은 두 조건을 만족하지만 답은 1이다. 오른쪽 조건(\(a[hi..n-1]\)은 모두 \(x\) 이상)이 필요한 곳은 유지가 아니라 종료다.

이 연결로 얻는 것

수학에서 알고리즘으로.

기저를 빠뜨리면 틀린다. 매개변수 탐색의 최소형 틀도 같은 네 단계로 증명한다. 거기서 초기화는 입력 조건 “\(ok(hi)\)는 참”에 기댄다. 범위 안에 참인 값이 하나도 없으면 기저가 거짓이고, 틀은 답이 아닌 \(hi\)를 돌려준다. 귀납법에서 기저를 빼면 거짓 명제도 “증명”되는 것과 같다.
멈춤은 줄어드는 정수 하나로 보인다. 정렬 원리 덕분에 매 바퀴 줄어드는 0 이상의 정수 하나만 찾으면 멈춤이 증명된다. 이분 탐색은 \(hi - lo\), 유클리드 호제법은 나머지 \(r_1\), 아래 전이 문제의 빠른 거듭제곱은 지수 \(e\)다.
알고리즘 증명을 세 모양으로 읽는다. 알고리즘 문서들의 정확성 증명은 귀납법 계열의 세 모양으로 나뉜다⁵. 초기화·유지·끝난다·종료 틀은 그중 첫째 모양에 속한다.

모양	무엇에 대한 귀납인가	쓰는 곳
보통 귀납법	바퀴 수	이분 탐색, 매개변수 탐색
강한 귀납법	입력 크기, 거리 \(0\)부터 \(k\)까지의 층 전부, 금액 \(x\)	재귀 함수, BFS, 동적 계획법
가장 작은 반례(정렬 원리)	처음으로 틀린 것	다익스트라의 “처음으로 틀리게 확정된 점”

알고리즘에서 수학으로.

귀납 단계를 코드로 실험한다. 실제로 돌리면서 바퀴마다 불변식을 assert하면 결론, 곧 “도달한 상태마다 \(I\)“를 확인한다. \(I\)를 만족하는 모든 상태에서 한 바퀴씩 돌려 보면 실제 실행이 닿지 않는 상태까지 보므로 귀납 단계 자체를 확인한다. 둘 다 증명하기 전에 명제가 믿을 만한지 싸게 확인하는 방법이다. 실험 통과가 증명은 아니다. 유클리드 호제법 구현은 앞의 방식으로 매 바퀴 불변식의 일부를 확인한다. 이 문서의 검증 코드는 두 방식을 모두 쓴다.
수학 쪽 반복 계산도 같은 틀로 읽는다. 가우스 소거법은 “해 집합이 같고 앞 열들의 피벗 아래가 0”을 바퀴마다 넘긴다. 경사 하강법은 걸음 크기를 그 문서의 조건대로 잡을 때 “함숫값이 지나온 기울기 크기의 제곱합에 비례하는 만큼 이상 줄었다”를 바퀴마다 넘긴다.

전이 문제

정수론의 빠른 거듭제곱에 같은 틀을 쓴다. 0 이상의 정수 \(a\), \(E\)에 대해 아래 반복문이 끝나면 r == a ** E임을 보여라. 불변식과 매 바퀴 줄어드는 양을 직접 고르고, 초기화·유지·끝난다·종료를 쓰라. 또 \(e\)가 홀수인 바퀴에서 r *= b만 하고 멈추면 불변식은 어떻게 되는가?

r, b, e = 1, a, E
while e > 0:
    if e & 1:
        r *= b
    b *= b
    e >>= 1

답

불변식은 \(r \cdot b^e = a^E\)이고, 줄어드는 양은 \(e\)다¹.

초기화: \(1 \cdot a^E = a^E\).
유지: \(e > 0\)일 때. \(e\)가 짝수면 \(r\)은 그대로이고 \((b^2)^{e/2} = b^e\)다. 홀수면 \((rb)(b^2)^{(e-1)/2} = r b^e\)다. 어느 쪽이든 \(r \cdot b^e\)가 바뀌지 않는다.
끝난다: \(e \ge 1\)이면 \(\lfloor e/2 \rfloor < e\)이고, \(e\)는 0 이상의 정수라 끝없이 줄 수 없다. 바퀴 수는 \(E\)의 2진 자릿수와 같다.
종료: \(e = 0\)이면 \(r \cdot b^0 = r = a^E\).

r *= b만 한 순간에는 \(r \cdot b^e\)가 \(a^E \cdot b\)가 된다. \(a \ge 2\)이면 이 값은 \(a^E\)와 달라 불변식이 깨진다. 바퀴의 나머지 두 줄이 이를 되돌린다. 불변식은 바퀴 경계에서만 참이면 되고, 바퀴 안에서는 잠시 깨져도 된다. 이분 탐색은 한 바퀴에 변수 하나만 바꿔서 이런 순간이 없다.

확인 문제

C1 lower_bound의 유지 단계는 \(I\) 말고 반복 조건 \(lo < hi\)도 가정한다. 이 가정은 귀납법의 어디에 해당하고, 빼면 어떤 상태에서 무엇이 깨지는가?

답: \(P(t)\)를 “\(t\)바퀴 이상 돈다면 \(t\)바퀴 뒤 상태가 \(I\)를 만족한다”로 두면, 반복 조건은 “\(t + 1\)번째 바퀴가 실제로 돈다”에 해당한다. 돌지 않으면 \(P(t + 1)\)은 저절로 참이라 도는 경우만 따지면 된다. 조건을 빼면 \(lo = hi = n\)인 상태에서 \(I\)는 참인데 \(mid = n\)이라 \(a[n]\)을 읽어 범위를 넘는다. “반복 조건은 종료에만 쓴다”가 흔한 오답이다. 유지에서도 \(lo \le mid < hi\)를 얻는 데 쓴다.

C2 이분 탐색의 lo = mid + 1을 lo = mid로 바꾸면 초기화·유지·끝난다·종료 중 어느 단계가 깨지는가? 깨지는 입력도 들어라.

답: 끝난다가 깨진다. \(a[mid] < x\)면 \(a[0..mid-1]\)도 모두 \(x\) 미만이라 \(lo = mid\)로 옮겨도 \(I\)는 지켜진다. 그러나 \(hi = lo + 1\)이면 \(mid = lo\)라서 \(hi - lo\)가 줄지 않는다. 예를 들어 \(a = [2]\), \(x = 5\)이면 \((lo, hi) = (0, 1)\)에서 \(mid = 0\), \(a[0] = 2 < 5\)라 \(lo = 0\)이 되어 영원히 돈다. “유지가 깨진다”가 흔한 오답이다.

C3 바퀴 수 대신 남은 칸 수 \(m = hi - lo\)로 귀납하면 왜 멈춤을 따로 보일 필요가 없고, 왜 보통 귀납법이 아니라 강한 귀납법을 쓰는가?

답: 명제를 “\(I\)가 참이고 \(hi - lo = m\)인 상태에서 출발하면 반복문이 멈추고 \(x\) 이상인 첫 칸을 돌려준다”로 잡으면 “멈춘다”가 명제 안에 들어 있다. \(m = 0\)이면 바로 멈추고 종료 단계로 답이 나온다. \(m \ge 1\)이면 한 바퀴 뒤 \(I\)가 남고 남은 칸 수가 \(\lfloor m/2 \rfloor\) 이하가 된다. \(m \ge 3\)이면 이 값은 어느 쪽으로 가든 \(m - 1\)보다 작다. 그래서 바로 앞 경우만 가정하는 보통 귀납법으로는 부족하고, \(m\)보다 작은 모든 경우를 가정해야 한다.

검증: 값 0~5, 길이 0~8인 정렬 리스트 3,003개와 \(x = -1, \dots, 6\)(무작위 입력 3,000개 더)에서 바퀴마다 불변식, \(hi - lo\)가 매 바퀴 1 이상 줄어듦, 답이 bisect_left와 같음. 모든 상태에서 유지(반복 조건이 있을 때, 실제 실행이 닿지 않는 상태 포함)와 종료, 반복 조건 없이 \(a[n]\)을 읽는 상태, 약한 불변식의 유지와 \([1, 5]\) 반례, lo = mid가 유지는 지키고 \([2]\), \(x = 5\)에서 멈추지 않음, 남은 칸 수 \(\le \lfloor m/2 \rfloor\)(\(m \le 2000\)), 남은 칸 수에 대한 명제(반복문과 재귀판), 매개변수 탐색 최소형의 불변식과 참인 값이 없을 때 답이 아닌 \(hi\)를 돌려줌, 홀수 합 표, 전이 문제의 불변식·바퀴 수·중간 값 \(a^E \cdot b\). 모두 실험으로 확인한 것이고, 증명은 본문에 있다 — 38_induction-loop-invariant_verify.py

\(P(t)\)를 “\(t\)바퀴 이상 돈다면”으로 잡는 방식, 반복 조건과 “다음 바퀴가 돈다”의 대응, 남은 칸 수에 대한 강한 귀납, 약한 불변식의 예, 빠른 거듭제곱의 불변식 \(r \cdot b^e = a^E\)는 위 출처의 틀을 이분 탐색과 빠른 거듭제곱에 적용한 것이다. 근거: 38_induction-loop-invariant_verify.py의 전수·무작위 확인. ↩ ↩² ↩³
Cormen·Leiserson·Rivest·Stein, Introduction to Algorithms 3판, 2.1절. 초기화를 귀납법의 기저에, 유지를 귀납 단계에 견준다. 귀납 단계를 끝없이 쓰는 보통의 귀납법과 달리, 반복이 멈추면 “귀납”도 멈추고 종료 단계에서 불변식과 멈춘 조건을 함께 쓴다고 적는다. ↩ ↩² ↩³
Lehman·Leighton·Meyer, Mathematics for Computer Science, 2장 “The Well Ordering Principle”, 5장 “Induction”(강한 귀납법). ↩ ↩²
Rosen, Discrete Mathematics and Its Applications 7판, 5.5절 “Program Correctness”(부분 정확성, 루프 불변식, while 문의 추론 규칙). 이 규칙도 유지의 가정에 반복 조건을 넣고, 결론에 반복 조건의 부정을 붙인다. ↩ ↩²
분류의 근거는 각 문서의 증명이다. 이분 탐색·매개변수 탐색은 초기화·유지·끝난다·종료를 쓴다. BFS는 층 번호 \(k\)에 대한 귀납인데, 가정에서 거리 \(0\)부터 \(k\)까지의 층을 모두 쓰므로 강한 귀납이다. 수학적 귀납법 문서의 활용도 같게 분류한다. 재귀와 백트래킹은 강한 귀납 정리를, 동적 계획법은 금액 \(x\)에 대한 강한 귀납을 쓴다. 다익스트라는 “처음으로 틀리게 확정된 점”을 잡는 귀류법을 쓴다. ↩