Quick Sort Partitioning 의 Loop Invariant 증명

Loop Invariant 는 프로그램 구동시 알고리즘내의 반복문의 정확성을 증명하기 위해서 사용된다. 그 조건으로 초기조건, 유지조건, 종료조건이 존재한다. 각각 아래와 같은 의미를 갖는다

• 초기조건(Initialization) : Loop 가 첫 번째 반복을 시작하기 전에 루프 불변성이 참이여야 함.
• 유지조건(Maintenance) : 반복 시작전 불변성이 참이었다면, 다음 반복 시작 전에도 계속 참이여야 함.
• 종료조건(Termination) : 루프가 종료될 때 그 불변식이 알고리즘의 타당성을 보이는데 도움이 될 유용한 특성을 가져야 함.

추가로 Quick Sort 의 동작원리상 partitioning이 발생한다. 이는 Quick Sort 내에서 Pivot 을 선택하고 재정렬 하는 과정을 의미하며. Pivot 과정에서 한쪽에는 피봇보다 작은 요소들이 위치하고, 다른쪽에는 피봇보다 큰 요소들이 위치하게 된다.

# Python

def partition(arr, start, end):
    pivot = arr[end]
    low = start - 1
    for high in range(start, end):
        if arr[high] <= pivot:
            low += 1 
            arr[low], arr[high] = arr[high], arr[low] # swap
    arr[low + 1], arr[end] = arr[end], arr[low + 1]
    return low + 1

def quickSort(arr, start, end):
    if start < end:
        pivot = partition(arr, start, end)
        quickSort(arr, start, pivot - 1)
        quickSort(arr, pivot + 1, end)

arr = [12, 9, 3, 7, 14, 11]
n = len(arr) - 1

print("원본 배열:", arr)

quickSort(arr, 0, n)

print("정렬된 배열:", arr)

partitioning을 구현하는 함수인 partition()의 정확성을 평가하려면 이 역시 Loop invariant 를 증명하면 된다.

• 초기조건 : Loop 시작전에 pivot 기준으로 나뉘어진 두 배열이 모두 비어있기 때문에 루프 불변성은 참이다. (여기서 비어있다는 의미는 실제로 arr이 비어있다기 보다는 '논리적' 으로 분할된 SubArray 가 비어있다고 이해하면 된다.)
• 유지조건 :
  • high 인덱스 값은 지속적으로 오른쪽으로 이동하면서 low 인덱스 값과 비교한다. 이는 high 가 pivot보다 작거나 같은 요소를 발견할 때까지 계속된다.
  • arr[high] ≤ pivot 일 때 : 만약 pivot 보다 작거나 같은 arr[high] 값을 찾았을 경우, arr[low+1] 값과 arr[high] 값을 swap 함으로서, 추후 pivot 보다 작은 수가 pivot 왼쪽에 위치하도록 조정 한다.
  • arr[high] ≥ pivot 일 때 : high 인덱스 값을 증가시킨다.
  유지조건을 통해 추후 pivot 왼쪽에는 pivot 보다 작은 원소들만 존재하고, pivot 오른쪽에는 pivot보다 큰 원소들만 존재할 수 있게 조정 되므로, 루프 불변성은 참이다.
• 종료조건 : Loop는 high 가 end에 도달하면 종료되며, 결론적으로 배열은 다음과 같은 상태가 된다
  
  • arr[start] ~ arr[low] ≤ pivot
  • arr[low+1] ~ arr[end-1] > pivot
  • arr[end] = pivot

따라서 QuickSort의 partitioning이 Loop invariant 함을 증명 하였다.

+ 추가적으로 이는 Loop Invariant 에 관한 내용임을 명심해라. 즉, partition function 내부에 위치한 ‘Loop’ 가 불변한지 묻는 과정이다. 때문에 마지막 정렬(swap(arr[low + 1], arr[end])) 가 이뤄지지 않은 상태에서 종료조건을 바라봐야 한다. 일련의 Loop 과정을 거치고 난 뒤에 arr[end] 는 Pivot 값이 위치하게 되고, arr[low + 1] 값 부터 arr[end - 1] 까지는 pivot 보다 큰 값이 위치해 있다. 때문에 Pivot 오른쪽에 큰 값을 위치하게 하기 위해서 Pivot이 위치한 arr[end] 값과, Pivot 대비 큰값이 있는 arr[low + 1] 값을 swap 하는 것이다.

이러한 과정은 Loop Invariant 를 계산하는 과정에서 불필요한 것이다.(말했듯이 어디까지나 Loop가 불변한지만 확인하면 된다. 마지막 swap 과정은 Loop 외의 문제이다)