알고리즘의 정당성 증명 (귀류법 / 반복문 불변식)

수학적 귀납법 이용하기

 

- 문제 단계 나누기

- 첫번째 내용 증명 

- 귀납 증명

첫번째 내용의 증명이 성립하며, 그 다음단계에서도 그 문제가 성립한다는 것을 보이면 해당 내용이 귀납적으로 마지막까지 성립함을 알 수 있습니다.

 

EX ) 100개의 도미노의 예시
 알고있는 내용
1. 첫번째 도미노는 사람이 밀어 넘어뜨린다.
2. 한 도미노가 넘어지면, 그 다음 도미노도 반드시 넘어진다.

Q . 마지막 도미노가 넘어지는가?

A : 1개의 도미노를 한계의 단계로 생각 (문제 단계 나누기)
B : 첫번째 도미노가 넘어짐을 증명(첫번째 내용 증명)
C : 한 도미노가 넘어질 때 다음 도미노가 넘어짐을 보임(귀납 증명)

알고있는 사실을 기반으로 위의 내용을 증명하면, 귀납적으로 마지막 도미노 또한 넘어짐을 증명할 수 있습니다.

EX ) 사다리 게임

Q . 맨 위 선택지와 맨 아래 선택지는 반드시 1 : 1 대응하는가?

A : 사다리에 원하는 가로줄을 1개를 추가하는 과정을 하나의 단계로 생각
B : 초기 상태에서 맨 위 선택지와 맨 아래 선택지는 1 : 1 대응함
C : 가로 줄이 하나 그어지면, 연결된 두 새로줄의 위쪽 선택지에 대한 아래 선택지는 서로 뒤바뀌지만,
두 세로줄이 1 : 1 대응임은 변하지 않음

위의 과정을 통해, 귀납적으로 가로줄을 몇번 긋더라도 사다리 타기는 항상 1 : 1 대응임을 귀납적으로
증명할 수 있습니다.

 

반복문 불변식(Loop Invariant)

대부분의 알고리즘은 반복적인 요소를 가지고 있는데, 그러한 반복 과정에서도 해당 식이 만족함을 보임으로써 올바른 답을 향해 가고있음을 보일 수 있습니다.

 

반복문 불변식을 이용한 정당성 증명

1. 반복문 진입 시 불변식이 성립함을 보인다.
2. 반복문이 진행하며 불변식의 내용을 깨트리지 않음을 보인다.
3. 반복문 종료시에 불변식이 성립하면, 항상 정답을 구했음을 보인다.

# * 반복문 진입 전 불변식을 만족함을 보이기
"""
while 조건:
    //반복문 작업
    반복문 내부애서도 불변식을 만족함을 보이기
//반복문이 끝나고 나서도 불변식을 만족함을 보이기
"""    

 

반복문 불변식을 통해 이진탐색(Binary Search)의 정당성 증명하기

def binarySearch(x,A):
    left,right = -1,len(A)

    while left + 1 < right:
        mid = (left + right) // 2

        if A[mid] < x:  left = mid
        else: right = mid
    return right

 

다음의 이진탐색 알고리즘의 정당성을 반복문 불변식을 이용해 증명할 수 있습니다.

#기본 조건 : 주어진 리스트 A는 반드시 오름차순으로 정렬되어있어야 한다.
#해당 알고라즘은 결과로서 A[i-1] < 주어진 숫자 X <= A[i]인 i를 반환한다.

def binarySearch(x,A):
    #불변식
    # left < right
    # A[left] < x <= A[right]

    left,right = -1,len(A)
    #left,right값은 초기값으로 각각 -1, len(A)값을 가진다
    #A[-1],A[len(A)]를 -inf,inf로 가정한다.

    #-1 < len(A)이고, 입력으로 주어진 실수 x에 대해 -inf < x < inf를 만족한다.
    #|x| < inf이므로 초기 상태에서만 x < A[right]형태를 가짐

    while left + 1 < right:
        # left + 1 < right, 즉 left + 2 <= right인 경우에만 동작하므로, mid값은 반드시 left와 right 사이의 값
        #i ) A[mid] > x : left = mid
        #ii ) A[mid] <= x : right = mid
        #위의 케이스에 따라 left, right를 변경하더라도
        #조간 A[left] < x <= A[right]는 유지되며,
        #left < mid < right이므로, left < right또한 유지됨을 알 수 있다.

        mid = (left + right) // 2

        if A[mid] < x:  left = mid
        else: right = mid

    return right
    #다음의 사실을 알 수 있음.
    # 1. #left + 1 = right
    # 반복문이 종료되었다는 것은 left + 1 >= right임을 의미하고, left < right이므로, left + 1 = right임을 알 수 있다.
    # 2. A[left] < x <= A[right]
    # 반복문 불변식이 유지되므로 당연히 성립
    # 3. 우리가 원하는 값 i == right