루프 불변성

Sep 23, 2021

루프 불변성(Loop Invariant)

Introduction to Algorithm, 3rd, Cormen을 토대로 정리한 내용입니다.

루프 불변성의 정의

알고리즘이 타당한지 확인하기 위해 사용되는 성질로, 루프 불변성을 정의하고 루프가 제대로 돌아가는 동안 루프 불변성이 변하지 않음을 확인함으로써, 구현 알고리즘이 옳은지 점검하는 데 도움을 줄 수 있다.

루프 불변성이 만족하는 지는 총 3가지를 증명해야한다.

• 초기화(Initialization) 조건 : 첫번째 루프에 들어가기 전에 루프 불변성이 참이다.

• 유지 (Maintenance) 조건 : 루프에 들어가기 전에 참이였다면, 다음 루프의 이전에도 루프 불변성은 참이다.

• 종료 (Termination) 조건 : 루프가 종료되었을 때, 루프 불변성이 참이다.

루프 불변성 유용성의 근거: 수학적 귀납법

위 세 가지의 경우가 증명을 통해 알고리즘의 옮음을 증명할 수 있다. 이는 마치 수학적 귀납법 증명 과정과 비슷하다.

🔵 수학적 귀납법

어떠한 자연수가 특정 조건을 만족하고, 다음 자연수 또한 만족한다는 것을 증명하면, 모든 자연수가 해당 조건을 만족한다는 증명.

예를 들어 초기화와 유지 단계가 참이면, 우리는 언제나 루프에 진입하기 전에 루프 불변성이 참이라는 것을 증명할 수 있다.

초기화는 귀납법에서 전제(Base case)에 해당하고, 유지는 귀납적 단계에 해당한다.

세번째 종료 단계는 알고리즘 증명에 있어서 가장 중요한데, 루프의 종료 조건에 관련되어 사용되며, 유한한 루프 이후에 루프가 종료되기 때문에, 무한한 자연수에 적용되는 수학적 귀납법과의 차이를 보인다.

루프 불변성의 예시 : 삽입 정렬

//의사 코드는 숫자가 1부터 시작함
for j = 2 to A.length
    key = A[j]
    // 정렬된 배열 A[1..j-1]에 A[j]를 삽입.
    i = j - 1
    while i > 0 and A[i] > key
        A[i+1] = A[i]
        i = i - 1
    A[i+1] = key

루프 불멸성 : 부분 배열 A[1...j-1]은 입력 배열의 A[1...j-1]까지의 원소들이며, 언제나 정렬되어 있다.

초기화 조건 성립 증명

• 첫 루프 진입 전에, j = 2이며, 부분 배열 A[1..j-1]은 A[1]로 하나만 존재하므로, 정렬되어 있으며, 이는 루프 불멸성을 참으로 만든다.

유지 조건 성립 증명

• 상기 의사 코드의 while부터 끝 부분은 A[j] = key가 올바른 순서에 위치할 때까지 i가 1씩 줄어들다가, 올바른 위치에 A[j]를 집어넣게 된다.
• A[1...j]까지의 모든 원소는 입력 배열 A[0...j]의 원소이며, 모두 정렬되게 된다. 따라서 루프 불멸성은 언제나 참이다.

종료 조건 성립 증명

• j는 for loop에 의해 언제나 1씩 증가하므로 결국엔 A의 길이를 넘게 되고, 종료 조건이 성립되어 루프가 종료되게 된다.
• 이때의 부분 배열 A[1...A.lenght]는 입력 배열 A[1...A.length]와 같고, 모두 정렬되어 있으며, 이는 모든 배열이 정렬되어 있음을 의미하며, 루프 불멸성이 참이 된다.

이를 통해 세 단계 모두 참이므로 해당 알고리즘의 루프의 결과는 옳다.