알고리즘의 정당성 증명
수학적 귀납법
수학적 귀납법은 반복적인 구조를 갖는 명제들을 증명하는 데 유용하게 사용되는 증명 기법입니다. 귀납법 증명은 크게 세 단계로 나누어집니다.
- 단계 나누기: 증명하고 싶은 사실을 여러 단계로 나눕니다.
- 첫 단계 증명: 첫 단계에서 증명하고 싶은 내용이 성립합을 보입니다.
- 귀납 증명: 어떤 한 단계에서 증명하고 싶은 내용이 성립한다면, 다음 단계에서도 성립하는지 보입니다.
반복문 불변식
귀납법을 이용해 알고리즘의 정당성을 증명할 때는 반복문 불변식이라는 개념이 유용하게 쓰입니다. 반복문 불변식이란 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건입니다.
불변식을 이용하면 반복문의 정당성을 다음과 같이 증명할 수 있습니다.
- 반복문 진입시에 불변식이 성립함을 보인다.
- 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. 다르게 말하면, 반복문 내용이 시작할 때 불변식이 성립했다면 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
- 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.
이진 탐색과 반복문 불변식
// 필수 조건: A는 오름차순으로 정렬되어 있다.
// 결과: A[i - 1] < x <= A[i]인 i를 반환한다.
// 이때 A[-1] = 음의 무한대, A[n] = 양의 무한대라고 가정한다.
int binsearch(const vector<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;
}
이 코드가 실행될 때 반복문 불변식인 lo < hi와 A[lo] < x <= A[hi]를 만족하는지 확인해야 합니다. 까다로운 코드를 짤 때 해당 코드가 가져야 할 불변식을 파악하고 작성하면 좀더 오류가 적은 코드를 작성할 수 있습니다.
귀류법
귀류법이란 증명해야할 명제와 반대되는 명제를 참이라고 가정하고 논리를 전개해서 모순을 찾아서 증명하는 기법을 귀류법이라고 합니다. 귀류법은 대게 어떤 선택이 항상 최선임을 증명하고자 할 때 많이 이용됩니다. 우리가 선택한 답보다 좋은 답이 있다고 가정한 후에, 사실은 그런 일이 있을 수 없음을 보이면 우리가 최선의 답을 선택했음을 보일 수 있기 때문입니다.
다른 기술들
비둘기집의 원리
101마리의 비둘기가 100개의 비둘기집에 모두 들어갔다면, 2마리 이상이 들어간 비둘기집이 반드시 하나는 있게 마련이다.
101마리의 비둘기가 100개의 비둘기집에 모두 들어갔다면, 2마리 이상이 들어간 비둘기집이 반드시 하나는 있게 마련이다.
위 글만 보고도 알 수 있을만큼 쉬운 이론입니다.
구성적 증명
구성적 증명이란 답의 실제 예를 들거나 답을 만드는 방법을 실제로 제시하는 증명입니다. 이 증명은 우리가 원하는 어떤 답이 존재한다는 사실을 증명하기 위해서 사용됩니다.
참고문헌: 구종만, 프로그래밍 대회에서 배우는 알고리즘 문제해결전략, 인사이트, (2012)
Author And Source
이 문제에 관하여(알고리즘의 정당성 증명), 우리는 이곳에서 더 많은 자료를 발견하고 링크를 클릭하여 보았다 https://velog.io/@qwe910205/알고리즘의-정당성-증명저자 귀속: 원작자 정보가 원작자 URL에 포함되어 있으며 저작권은 원작자 소유입니다.
우수한 개발자 콘텐츠 발견에 전념 (Collection and Share based on the CC Protocol.)