루프 불변성

루프 불변성이란?

루프 불변성(loop invariant)은 어떤 알고리즘이 잘 동작하는지 증명하기 위해 사용된다.

루프 불변성의 단계

루프 불변성은 세가지 단계로 이루어진다.

1. 초기조건(Initialization)
첫 번째 루프가 시작하기 전 루프 불변성이 참이어야 한다.

2. 유지조건(Maintenance)
루프의 시작 전 루프 불변성이 참이었다면, 그다음 반복에서도 참이 유지되어야 한다.

3. 종료조건(Termination)
루프가 종료되면 불변량은 알고리즘이 옳다는 것을 보여주는 데 도움이 되는 유용한 속성을 제공해야 한다.

한번 예시로 알아보자

삽입 정렬

_list = [4, 7, 1, 5, 2, 8, 3, 6]

def INSERTION_SORT(A):
    for j in range(1, len(A)):
        key = A[j]

        i = j - 1
        while i >= 0 and A[i] > key:
            A[i + 1] = A[i]
            i -= 1
        A[i + 1] = key
    return A

sorted_list = INSERTION_SORT(_list)
print(*sorted_list)

>>> 1 2 3 4 5 6 7 8

루프 불변성
매 반복의 시작에 A[0, ...,j-1]은 정렬된 상태이다.

초기조건
j=1 일 때 배열 A[0, ...,j-1]은 하나의 요소만 가지고 있고 이는 정렬된 상태를 의미한다.

유지조건
A[j]가 올바른 자리를 찾을 때까지 A[j-1], A[j-2], A[j-3] ... 을 이동시킨다. 그리고 해당 반복이 끝나면 배열 A[0, ...,j]은 정렬된 상태가 된다. 그러므로 j가 증가하며 매 반복이 진행되어도 루프 불변성이 유지된다.

종료조건
n번째의 반복이 끝나면 배열 A[0..n]은 정렬된 상태이고 해당 배열은 전체 배열을 의미하기 때문에 전체 배열이 모두 정렬되었다 할 수 있다.