알고리즘의 정당성 증명

1. 도입

해결해야 할 문제가 간단할 때는 직관적으로 알고리즘을 설계할 수 있지만, 무제가 복잡해지면 이 알고리즘이 과연 문제를 제대로 해결하는지를 파악하기 조차 까다롭다. 단위 테스트를 이용해 여러 개의 입력에 대해 프로그램을 실행해 보고 그 답을 점검해 볼 수도 있지만, 이런ㅅ 기으로는 이 알고리즘이 존재 가능한 모든 입력에 대해 정확하게 동작한다는 사실을 증명할 수 없다.단위 테스트는 알고리즘에 문제가 있음을 증명할 수는 있어도 문제가 없음을 증명할 수는 없기 때문이다. 따라서 알고리즘의 정확한 증명을 위해서는 각종 수학적인 기법이 동원되어야 한다.

알고리즘의 증명을 공부해야 하는 가장 큰 이유는 많은 경우 증명이 알고리즘을 유도하는 데 결정적인 통찰을 담고 있기 때문이다. 모든 알고리즘은 사실 치열한 고민과 개선 과정을 거쳐 태어난다. 이과정에서 결정적으로 필요한 깨달음이 증명에 담겨 있는 경우가 많다. 그러므로 sudo코드를 외우기만 해서는 알고리즘에 담겨 있는 깨달음을 제대로 흡수했다고 볼 수 없으며, 증명을 이해하는 편이 알고리즘을 사용하는 입장에서도 더 큰 공부가 된다.
이번 장에서는 알고리즘의 정당성 증명에서 흔히 나타나는 패턴들을 알아보고 몇 가지의 예제 증명들을 다뤄 볼 것이다.

2. 수학적 귀납법과 분복문 불변식

100개의 도미노가 순서대로 놓여 있는 광경을 상상해 본다. 그리고 다음 두 가지 사실을 안다고 가정한다.

• 첫번째 도미노는 직접 손으로 밀어서 쓰러뜨린다.
• 한 도미노가 쓰러지면 다음 도미노 역시 반드시 쓰러진다.

그러면 마지막 도미노 또한 당연히 쓰러진다는 것을 직관적으로 알 수 있다. 수학적 귀납법은 이와 같이 반복적인 구조를 갖는 명제들을 증명하는 데 유용하게 사용되는 증명 기법이다. 이 귀납적 증명은 크게 세 단계로 나누어진다.

• 단계 나누기 : 증명하고 싶은 사실을 여러 단계로 나눈다. 도미노 문제에서는 100개의 도미노를 각각 하나의 도미노로 나누었던 것이 해당된다.
• 첫 단계 증명 : 그 중 첫 단계에서 증명하고 싶은 내용이 성립함을 보인다. 도미노 문제에서는 도미노가 쓰러짐을 의미한다.
• 귀납 증명 : 한 단계에서 증명하고 싶은 내뇽이 성립한다면, 다음 단계에서도 성립함을 보인다. 앞의 예에세는 한 도미노가 쓰러지면 다음 도미노도 반드시 쓰러짐을 보이는 과정이다.
  

위의 개념을 이용하여 '사다리 타기 게임'을 생각해보자.

• 단계 나누기 : 텅빈 N개의 세로줄에서부터 시작해서 원하는 사다리가 될 때까지 가로줄을 그러 간다고 한다. 이때 가로줄을 하나 긋는 것을 한 단계라고 한다.
• 첫 단계 증명 : 텅빈 N개의 세로줄에서는 항상 맨 위 선택지와 맨 아래 선택지가 1:1 대응이 된다.
• 귀납 증명 : 가로줄을 그러서 두 개의 세로줄을 연결했다고 하자. 이때 두 세로줄의 결과는 서로 뒤바뀐다. 하지만 여전히 1:1대응을 이룬다.
  

반복문 불변식

귀납법은 알고리즘의 정당성을 증명할 때 가장 유용하게 사용되는 기법이다. 왜나면 대부분의 알고리즘은 어떠한 형태로든 반복적인 요소를 가지고 있기 때문이다. 귀납법은 이런 알고리즘들이 옳은 답을 계산함을 보이기 위해서 알고리즘의 각 단계가 정답으로 가는 길 위에 있음을 보이고, 결과적으로는 알고리즘의 답이 옳음을 보인다.
귀납법을 이용해 알고리즘의 정당성을 증명할 때는 반복문 불변식이라는 개념이 유용하게 쓰인다. 이것은 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건이다. 불변식을 이용하면 반복문의 정당성을 다음과 같이 증명할 수 있다.

• 반복문 진입시에 불변식이 성립함을 보인다.
• 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. 다르게 말하면, 반복문 내용이 시작할 때 불변식이 성립했다면 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
• 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.
  불변식을 이용해 반복문의 정당성을 증명하는 과정은 귀납법과 다를 것이 없다. 전체 작업을 각 단계로 나누는 과정이 이미 반복문으로 나타나 있으니 더 간단하다. 반복문이 처음 시작 될 때 해당 불변식이 만족함을 보이고, 반복문 내용이 한 번 지나가도 이 조건이 다시 유지됨을 보여주면 된다.
  
  

단정문을 이용해 반복문 불변식 강제하기

단정문은 불변식과 아주 잘 어울린다. 불변식을 주석으로만 달아 놓을 것이 아니라 단정문으로 강제해 버리면 해당 불변식이 깨졌을 때 프로그램이 강제 종료되기 때문에 불변식의 유지에 문제가 있다는 사실을 아주 쉽게 알 수 있다. 물론 단정문도 속도에 어느 정도 영향을 주기 때문에 엄청나게 많이 실행되는 반복문 안에 단정문을 배치하는 것은 삼가는게 좋다.

3. 귀류법

우리가 원하는 바와 반대되는 상황을 가정하고 논리를 전개해서 결론이 잘못됐음을 찾아내는 증명 기법을 귀류법이라고 한다. 보통 귀류법은 대개 어떤 선택이 항상 최선임을 증명하고자 할 때 많이 이용된다. 우리가 선택한 답보다 좋은 답이 있다고 가정한 후에, 사실은 그런 일이 있을 수 없음을 보이면 우리가 최선의 답을 선택했음을 보일 수 있기 때문이다.

귀류법을 이용한 증명들

문제를 풀기위해 귀납법과 귀류법을 모두 이용한 증명들을 많이 볼 수 있다. 알고리즘의 결과가 최선임을 보이기 위해 각 단계에서 최선의 선택을 함을 귀류법으로 증명하고, 각 단계에서 최선의 선택을 한다면 다음 단계에서도 최선의 선택을 할 수 있음을 귀납법으로 증명하는 것이다.