알고리즘의 정당성 증명
해결해야 할 문제가 간단할 때는 직관적으로 알고리즘을 설계할 수 있지만, 문제가 복잡해지면 알고리즘이 과연 문제를 제대로 해결하는지 파악하는 것이 힘들다. 물론 단위테스트를 통해서 해결할 수도 있겠지만, 이 방법으로는 턱없이 모자라다.
따라서, 알고리즘의 정확한 증명을 위해서는 각종 수학적인 기법이 동원되어야 한다.
알고리즘에 대한 증명은, 알고리즘을 유도하는 데 결정적인 통찰을 담고 있다. 모든 알고리즘은 치열한 고민과 개선 과정을 거쳐 태어나고 이 과정에서 결정적으로 필요한 깨달음이 증명에 담겨있는 경우가 많다. 또한, 증명을 아는 편이 사용하는 입장에서도 큰 공부가 된다.
1. 반복문 불변식
귀납법은 알고리즘의 정당성을 증명할 때 가장 유용하게 사용되는 기법이다. 대부분의 알고리즘은 어떠한 형태로든 반복적인 요소를 가지고 있기 때문이다. 귀납법은 이런 알고리즘이 옳은 답을 계산함을 보이기 위해서 각 단계가 정답으로 가는 길 위에 있음을 보이고, 결과적으로는 알고리즘의 답이 옳음을 보인다.
귀납법을 이용해 알고리즘의 정당성을 증명할 때는 반복문 불변식(loop in-variant)이라는 개념이 유용하게 쓰인다. 반복문 불변식이란, 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건이다. 반복문이 마지막에 정답을 계산하기 위해서는 항상 이 식이 변하지 않고 성립해야 한다.
⭐️ 불변식을 이용하여 반복문의 정당성을 증명하는 방법
- 반복문 진입시에 불변식이 성립함을 보인다.
- 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. 반복문 내용이 시작할 때 불변식이 성립했다면 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
- 반복문 종료시에 불변식이 성립했다면 그 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
2. 귀류법
원하는 바와 반대되는 상황을 가정하고 논리를 전개해서 결론이 잘못됐음을 찾아내는 증명 기법을 귀류법이라고 한다.
