알고리즘의 정당성 증명

• 이번 글에서는 알고리즘 증명에 자주 사용되는 기법들, 또 그 증명의 일반적인 패턴들을 다뤄볼까 합니다!

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

• 수학적 귀납법은 반복적 구조를 가진 명제들을 증명하는 데 유용한 방법으로, 단계별로 문제를 나누어 각 단계에서의 성립을 증명합니다.
• 예를 들어, 도미노가 하나씩 쓰러지는 것처럼, 첫 단계가 성립하고, 한 단계가 성립하면 다음 단계도 성립한다는 것을 보임으로써 전체가 성립함을 증명합니다.

 

• 추가적으로 반복문 불변식 또한 알고리즘의 정당성을 증명하는 데 유용합니다.
• 알고리즘 내의 반복문이 올바른 결과를 내기 위해 각 단계에서 특정 조건이 계속해서 유지되어야 함을 의미합니다.
• 이를 증명하기 위해 반복문 시작 시, 반복문 내에서, 그리고 반복문 종료 시에 불변식이 성립함을 보여야 합니다.
• 예로써 이진 탐색 알고리즘에서는 while문이 실행될 때마다 특정 조건이 유지되는 것을 보임으로써, 알고리즘이 정확한 결과를 낸다는 것을 증명할 수 있습니다.

# 이진 탐색

# 필수 조건: A는 오름차순으로 정렬되어 있습니다.
# 결과: A[i-1] < x <= A[i]인 i를 반환합니다.
# 이때 A[-1] = 음의 무한대, A[n] = 양의 무한대라고 가정합니다.
def bin_search(A: list, x: int) -> int:
    n = len(A)
    lo, hi = -1, n
    # 반복문 불변식 1: lo < hi
    # 반복문 불변식 2: A[lo] < x <= A[hi]
    # (*) 불변식은 여기서 성립해야 합니다.
    while lo + 1 < hi:
        mid = (lo + hi) // 2
        if A[mid] < x:
            lo = mid
        else:
            hi = mid
        # (**) 불변식은 여기서도 성립해야 합니다.
    return hi

• 삽입 정렬에서도 유사한 방식으로, 반복문 내에서 배열의 일부분이 항상 정렬되어 있음을 보여주는 불변식을 통해 알고리즘의 정확성을 증명합니다.

# 불변식이 추가된 삽입 정렬 알고리즘

def insertion_sort(A: list) -> None:
    for i in range(len(A)):
        # 불변식 a: A[0..i-1]은 이미 정렬되어 있습니다.
        # A[0..i-1]에 A[i]를 끼워넣습니다.
        j = i
        while j > 0 and A[j-1] > A[j]:
            # 불변식 b: A[j+1..i]의 모든 원소는 A[j]보다 큽니다.
            # 불변식 c: A[0..i] 구간은 A[j]를 제외하면 정렬되어 있습니다.
            A[j-1], A[j] = A[j], A[j-1]
            j -= 1

• 또한, 단정문을 사용해 반복문 내에서 불변식이 항상 성립하도록 강제함으로써 알고리즘의 오류를 빠르게 발견할 수 있습니다.

 

귀류법

• 귀류법은 잘못된 결론을 가정하고 그로부터 모순을 이끌어내는 증명 방식입니다.
• 이 방법은 알고리즘의 최적성을 증명하는 데 효과적으로 사용됩니다.
• 예를 들어, 열차에 과다한 승객이 있을 경우 가장 멀리 가는 승객을 먼저 내리게 하는 것이 최선임을 증명하는 데 귀류법을 사용할 수 있습니다.
• 만약 더 짧은 거리를 가는 승객을 내렸을 때 그것이 더 좋은 선택이라고 가정하면, 실제로는 그런 상황이 불가능함을 증명함으로써 가장 멀리 가는 승객을 내리는 것이 최적의 선택임을 보일 수 있습니다.

 

• 이와 비슷하게, 책장을 쌓는 문제에서는 귀류법을 사용하여 특정 순서대로 책장을 쌓는 것이 최적임을 증명할 수 있습니다.
• 예를 들어, 각 책장의 최대 견딜 수 있는 무게와 자신의 무게의 합($M_i + W_i$)이 큰 책장을 아래에 놓는 것이 최적임을 증명하고자 할 때, 그 반대의 순서로 쌓았을 때 최적의 결과를 얻을 수 없음을 보임으로써 최적의 순서를 입증할 수 있습니다.

 

다른 기술들

비둘기집의 원리

• 비둘기집의 원리는 한정된 자원 또는 공간에 대해 더 많은 요소들이 존재하면 반드시 중복이 생긴다는 것을 말합니다.
• 예를 들어, 서울에 천만 명의 사람이 있고, 사람의 머리카락 수가 최대 백만 개라고 할 때, 비둘기집의 원리에 따라 머리카락 수가 같은 두 사람이 서울에 반드시 존재함을 증명할 수 있습니다.
• 순환 소수를 찾는 문제에서 이 비둘기집의 원리를 이용할 수 있습니다.
• 나눗셈을 시뮬레이션할 때, 나머지의 가능한 값의 범위가 제한되어 있기 때문에 결국에는 반복되는 나머지가 나타날 수밖에 없고, 이는 순환 소수임을 의미합니다.

# 분수 a/b의 소수 표현을 출력합니다.
# a >= 0, b > 0이라고 가정합니다.
def print_decimal(a: int, b: int) -> None:
    iter = 0
    while a > 0:
        # 첫 번째와 두 번째 사이에 소수점을 찍습니다.
        if iter == 1:
            print('.', end='')
        print(a // b, end='')
        a = (a % b) * 10
        iter += 1

 

구성적 증명

• 구성적 증명은 문제의 해결책을 직접 만들어내거나 실제 예시를 제시함으로써 어떤 문제에 대한 답이 존재한다는 것을 증명하는 방법입니다.
• 이 방식은 이론적인 논증보다는 실제적인 해결책을 제시하는데 초점을 맞춥니다. 예를 들어, 하늘을 나는 교통 수단의 가능성을 증명할 때, 이론적인 분석 대신 실제 비행기를 만들거나 그 제작 방법을 제시하는 것이 구성적 증명의 예가 됩니다.
• 안정적 결혼 문제는 구성적 증명을 사용하는 대표적인 예입니다. 이 문제에서는 각 남녀가 서로 선호하는 순서에 따라 짝을 찾는 방법을 알고리즘으로 제시합니다.
• 이 알고리즘은 여성이 가장 선호하는 남성에게 프로포즈하고, 남성은 받은 프로포즈 중 가장 마음에 드는 여성과 짝을 이룹니다.
• 이 과정은 모든 사람이 짝을 찾을 때까지 반복되며, 최종적으로 모든 짝이 '안정적'임을 증명합니다. 여기서 안정적이란 어떤 남녀도 현재의 파트너보다 서로를 더 선호하지 않는 상태를 의미합니다.