정당성 증명

용어
어떤 - 상황에 따라 a가 되기도 any가 되기도 한다.

간단한 문제의 경우에는 직관적으로 알고리즘을 설계할 수 있지만, 문제가 복잡해지면 알고리즘이 과연 문제를 제대로 해결하는지를 파악하기 어려워집니다.

테스트 케이스를 이용해 단위 테스트를 해서 프로그램을 실행하고 답을 점검해 볼 수 있지만, 이런 방식은 잘못된 예외 케이스를 찾았을 때, 알고리즘에 문제가 있음은 증명할 수 있어도 알고리즘이 문제가 없음을 증명하기는 어렵습니다.

모든 입력에대해서 문제가 없음을 정확하게 증명하기 위해서는 다양한 수학적 기법을 사용해야합니다.

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

수학적 귀납법은 반복적인 구조를 갖는 명제들을 증명하는데 사용되는 증명 기법입니다.
수학적 귀납법은 다음 3단계로 나눠서 증명이 진행됩니다.

1. 단계 나누기
   증명하고 싶은 것을 여러 단계로 나눕니다. (수학적 귀납법을 이용한 수열의 증명에서 1번째항, 2번째항,…k번째항,… n번째항으로 나누는 것이 단계 나누기 입니다.)
2. 첫 단계 증명
   나눈 단계 중 첫번째 단계에서 증명하고싶은 내용이 성립함을 보입니다.
3. 귀납 증명
   k번째 단계에서 증명하고 싶은 내용이 성립한다면, k+1번재 단계에서도 증명하고 싶은 내용이 성립함을 보이면 됩니다.

수학적 귀납법을 소개할 때 가장 많이 나오는 예시가 도미노입니다.
도미노는 첫번째 도미노를 손으로 밀어서 쓰러뜨리면, 다음 도미노도 넘어집니다.
즉, 한 도미노가 스러지면 다음 도미노 역시 쓰러지기 때문에, 중간에 k번째 도미노가 쓰러지면 k+1번째 도미노 역시 쓰러질 것이고 이 과정이 반복되면 마지막 도미노까지 쓰러질 것입니다.

이처럼 도미노가 쓰러지는 것으로부터 얻은 직관으로 이진 탐색을 수학적 귀납법으로 증명해보겠습니다.

이진 탐색과 반복문 불변식

반복문 불변식

이진 탐색의 알고리즘 정당성을 증명하기 전에 반복문 불변식이라는 개념을 먼저 알아보겠습니다.

대부분의 알고리즘은 어떤 형태로든 반복적인 요소를 가지게 됩니다.
이 반복적인 요소를 귀납법을 이용할 때 사용하는 것이 바로 반복문 불변식입니다.
반복문 불변식은 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 있는지를 명시하는 조건 입니다.

반복문의 마지막에 정답을 계산하기 위해서는 중간 단계에서 항상 식이 변하지않고 성립해야합니다.

불변식을 이용해서 반복문의 정당성을 증명하면 다음과 같습니다.
1. 반복문 진입시 불변식이 성립함을 증명
2. 반복문 내용이 불변식을 깨뜨리지 않음을 증명
3. 반복문 종료시 불변식이 성립하는지 확인(확인되면 정답을 찾은 것)

이진 탐색 알고리즘의 정당성 증명

//필수 조건 : arr은 오름차순으로 정렬되어 있다.
public int binsearch(int[] arr,int target){
	int n = arr.length;
	int left = -1, right = n;
	//반복문 불변식 1: left<right
	//반복문 불변식 2: arr[left]<target<=arr[right] 
	while(left + 1 < right){
		int mid = (left + right)/2;
		if(arr[mid]<target) left = mid;
		else right = mid;
	}
	return right;
}

반복문 불변식 1: left<right
while 문의 조건에 걸려서 종료됐다면 반드시 left+1 >= right 입니다.
불변식에 의하면 left < right 이므로 left + 1 = right 가 됩니다.
반복문 불변식 2: arr[left]<target<=arr[right]
이 불변식에 의해서 종료조건을 만난 후에 우리가 구하려 했던 값은 right가 됨을 알 수 있습니다.
이처럼 불변식이 while문 종료시에 항상 성립한다는 것을 보였기 때문에 이 알고리즘의 정당성은 증명되었습니다.

불변식을 이용해서 정당성을 증명하는 과정은 귀납법과 다를 것이 없어보이지만 전체 작업을 각 단계로 나누는 과정이 이미 반복문으로 만들어져있기 때문에 더 간단합니다. 반복문이 처음 시작될 때 불변식이 만족함을 보이고, 반복문 내용이 한 번 지나가도 이 조건이 다시 유지됨을 보여주면 쉽게 증명할 수 있습니다.

귀류법

우리가 원하는 결론과 반대되는 상황을 가정하고 논리를 전개해서 결론이 잘못됐음을 찾아내는 증명 기법입니다.
귀류법은 보통 최선의 선택인지를 증명해야하는 그리디 알고리즘의 정당성을 증명할 때 많이 사용합니다.

귀류법을 이용한 증명

홀수 + 짝수는 홀수 임을 증명해보겠습니다.
1. 홀수 + 짝수는 짝수라고 가정
2. 홀수는 2n-1, 짝수는 2m(n,m은 자연수)
3. 2n-1 + 2m = 2(n-m)-1
4. 2(n-m)-1은 홀수(2의 배수는 짝수)
5. 이는 1에서의 홀수+짝수 = 짝수 가정과 모순
6. 따라서 홀수 + 짝수 = 홀수

귀류법의 활용

귀류법은 알고리즘의 결과가 최선(최단 경로, 최소 비용 등등)임을 보이기 위한 절차는 다음과 같습니다.
1. 각 단계에서 최선의 선택을 함을 귀류법으로 증명
2. 귀류법으로 최선의 선택함이 증명된다면 다음 단계에서도 최선의 선택을 함을 귀납법으로 증명

비둘기집의 원리

n마리 비둘기 n-1개의 비둘기 집에 넣으면 비둘기가 2마리 이상의 비둘기 집이 적어도 하나 존재한다

구성적 증명

우리가 원하는 어떤 답이 존재한다는 사실을 증명하기위해 사용하는 증명법입니다. 귀류법과 귀납법이 답이 존재한다는 사실을 논증하는 것이라면, 구성적 증명은 답의 실제 예를 들어서 보여주거나 답을 만드는 방법을 실제로 제시하는 증명법입니다.
ex) 코드의 정당성 증명없이 온라인 저지 사이트에 올려서 채점해서 맞으면 그 문제에 한해서는 이상없이 작동하는 코드임을 생각해봅시다.

안정적 결혼 문제

안정적 결혼 문제는 다음과 같은 상황을 이야기합니다.
n명의 남성과 여성이 단체 미팅에서 만났습니다. 여러 게임을 진행하는 동안 모든 사람은 자신이 원하는 상대방의 우선쉰위를 맘 속에 정했고, 이제 시간이 되어 남자 1호와 여자 1호가, 남자 2호와 여자 2호가 각각 짝이 되었습니다. 그런데 남자 1호와 여자 2호는 자신들의 짝보다, 서로를 더 선호한다는 사실을 알게되었습니다. 이런 일이 일어나지않도록 짝을 지어줄 수 있는 방법이 항상 있을까요? 아니면 불가능한 경우가 있을까요?

이 알고리즘은 실제로 어느 대학의 석사 과정 신입생의 지도 교수 배정 과정에 도입된 알고리즘이기도 합니다.

그렇다면 이 알고리즘은 어떻게 해결할 수 있을까요??

1. 처음에는 남성들이 모두 자신이 가장 선호하는 여성의 앞에가서 프로포즈를 합니다. 여성이 그 중 제일 마음에드는 남성을 고르면 나머지는 거절을 당하고 자기 자리로 돌아갑니다.
2. 거절당한 남자들은 상대에게 짝이 있는지 없는지와 관계없이 다음으로 마음에 드는 여성에게 다가가 프로포즈합니다. 여성들은 현재 자신의 짝보다 더 마음에 드는 남성이 다가왔다면, 지금의 짝 대신 새로운 남성을 선택합니다.
3. 짝이 없는 남성이 없을 때까지 2번 항목을 반복합니다.

위와 같이 진행한다면 안정적으로 모든 쌍을 구할 수 있습니다.
모든 여성이 1번씩 알고리즘에 참여하기 때문에 O(N)만큼의 시간이 소모되고 각각의 여성은 자신 선호도를 확인해야하기 때문에 이 과정에서 O(N), 프로포즈한 남성이 선호도 순서를 확인해 여성을 선택하는데 걸리는 시간 O(1)이 소모 됩니다.
그렇기 때문에 이 알고리즘의 시간복잡도는 O(N^2)입니다.

그렇다면 이 알고리즘이 항상 종료된다는 것은 어떻게 알 수 있을까요? 그리고 모든 사람이 짝을 찾고 그 짝이 항상 안정적인 것은 어떻게 알 수 있을까요?

• 종료 증명
  각 남성은 거절당할 때마다 지금까지 프로포즈했던 여성들보다 우선순위가 낮은 여성에게 프로포즈합니다. 따라서 각 남성이 최대 n명의 여성들에게 순서대로 프로포즈한 이후에는 더 이상 프로포즈할 수 있는 여성이 없으므로 반드시 종료됩니다.
• 모든 사람이 짝을 찾음 증명
  프로포즈 받은 여성은 프로포즈한 남성들 중 한 명을 반드시 선택하고, 더 우선순위가 높은 남성이 프로포즈해야지만 짝을 바꾸기 때문에, 한 번이라도 프로포즈를 받은 여성은 항상 작이 있습니다.
  이에 귀류법을 적용해보겠습니다.

1. 남녀 한 사람씩 짝을 찾지 못하고 남았다고 가정
2. 모든 남성은 우선순위가 높은 순서대로 모두에게 한 번씩 프로포즈하기 대문에, 지금 짝을 찾지 못한 여성에게도 한 번은 프로포즈를 했습니다.
3. 우선순위에 따라서 남은 여성은 지금 받은 프로포즈를 받아들여야하기 때문에 짝을 찾지 못하는 사람이 존재할 수 없습니다.

• 짝의 안정성 증명
  귀류법을 사용하면 증명할 수 있습니다.

1. 짝을 지었는데 결과적으로 짝이 아닌 두 념녀가 서로 자신의 짝보다 상대방을 더 선호한다고 가정합니다.
2. 더 선호하는 여성이 있다면 남성은 지금 자신의 짝 이전에 그 여성에게 반드시 프로포즈를 했어야합니다.
3. 여성은 더 마음에 드는 남성이 나타났을 대만 짝을 바꾸기 때문에, 둘이 짝이 아니라는 것은 지금 프로포즈한 남성보다 더 선호하는 남성과 짝이 됐다는 뜻입니다.
4. 그러므로 프로포즈 받았던 남성보다 마음에 들지않는 남성과 최종적으로 짝이 될 수 없습니다.

이처럼 귀류법과 귀납법 그리고 구성적 증명을 이용하면 복잡해보이는 알고리즘의 정당성을 확인하는데 도움이 됩니다.