알고리즘의 정당성 증명

알고리즘 문제 해결 전략 Chap5

• 수학적 귀납법과 반복문 불변식
  • 수학적 귀납법
    • 반복적인 구조를 갖는 명제들을 증명하는 데 유용하게 사용되는 증명 기법
      • 단계 나누기
      • 첫 단계 증명
      • 귀납 증명
  • 반복문 불변식
    • 귀납법: 알고리즘의 정당성을 증명할 때 가장 유용하게 사용되는 기법
    • 반복문 불변식(loop invariant)
      • 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건
      • 불변식을 이용하면 반복문의 정당성을 다음과 같이 증명
        • 반복문 진입시에 불변식이 성립함을 보인다.
        • 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. 
          • 반복문 내용이 시작할 때 불변식이 성립했다면 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
        • 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.
      • 증명 방법
        • 초기 조건
        • 유지 조건
          • 불변식
      • 예시) 삽입 정렬과 반복문 불변식
        • 초기 조건: 반복문이 시작할 때, i=0이면 해당 구간은 비어있으니 항상 정렬되어 있음
          • 불변식 유지: for문의 내요잉 종료할 때 이 불변식이 깨지지 않고 유지됨을 보이기 위해서는 while문의 정당성을 증명해야 함
  • 귀류법
    • 어떤 명제가 참이라고 가정한 후, 모순을 이끌어내 그 가정이 거짓임을, 즉 처음의 명제가 거짓임을 증명하는 방법
    • 각 단계에서 최선의 선택을 한다면 다음 단계에서도 최선의 선택을 할 수 있음을 귀납적으로 증명
  • 다른 기술들
    • 비둘기집의 원리
      • 얼핏 보면 대답하기 힘든 질문을 대답하는 데 유용하게 쓰이는 원리
    • 동전 뒤집기
    • 순환 소수 찾기
    • 구성적 증명
      • 다른 관점을 취하는 증명방식으로 구성적 증명
      • 원하는 어떤 답이 존재한다는 사실을 증명하기 위해 사용
      • 실제 예를 들거나 답을 만드는 방법을 실제로 제시하는 증명
    • 안정적 결혼 문제
      • 구성적 증명으로 해결되는 대표적인 문제
      • 답의 존재성을 보이는 대신 답을 만드는 알고리즘을 제시함으로써 답이 존재함을 보임
      • 예) 남/여 사이의 짝을 만들어주기
        • 여성들이 모두 자신이 가장 선호하는 남성의 앞에 가서 프로포즈를 함, 남성이 맘에 드는 여성을 고르면 나머지 퇴짜 맞기
        • 여성들이 다음으로 맘에 드는 남성들에게 고백 -> 자기 짝보다 더 맘에 드는 여성이 다가오면 새로운 여성에게 넘어감
        • 더 프로포즈를 할 여성이 없을 때까지 2번 항목 반복
      • 항상 종료한다는 증명
        • 종료 증명
          • 각 여성은 퇴짜 맞을때마다 지금까지 프로포즈를 했던 남성들보다 우선순위가 낮은 남성에게 프로포즈를 한다. 
          • 각 여성이 최대 n명의 남성들에게 순서대로 프로포즈한 이후에는 더 이상 프로포즈할 남성이 없으므로, 해당 과정은 언젠가 반드시 종료
        • 모든 사람들이 짝을 찾는지 증명
          • 귀류법을 적용하여 남녀 한사람씩 짝을 찾지 못하고 남았다고 가정한다면, 여성은 우선순위가 높은 순서대로 모두에게 한 번씩 프로포즈하기 때문에, 이 남성에게도 한 번은 프로포즈함.
          • 해당 남성은 프로포즈를 받아들였어야 하고, 따라서 짝을 찾지 못하는 사람은 있을 수가 없음
        • 짝들의 안정성
          • 귀류법으로 증명
          • ..