루프불변성이란?
루프불변성이란 알고리즘이 타당한 이유를 쉽게 설명하기 위해서 사용된다. 루프 불변성의 세가지 조건은 다음과 같다.
초기 조건
루프가 첫번째 반복을 시작하기 전에 루프 불변성이 참이어야 한다.
말이 좀 어려운데 단순하게 말해서 특정 알고리즘이 첫번째 상태에서 참이어야 한다는 뜻이다.
책에서 예시를 든 삽입 정렬을 살펴보자
for j =2 to A.length:
key = A[j]
// A[j]일 때 정렬된 배열 A[1..j-1]에 삽입한다.
i = j-1
while i>0 and A[i]>key:
A[i+1] = A[i]
i = i-1
A[i+1] =key삽입정렬의 초기 조건
루프가 첫 반복을 하기 전인 j=2일 때 부분 배열인 A[1]은 원래의 A[1]의 값과 달라지지 않았고 값이 하나이기 때문에 정렬되어 있는 상태이다.
초기 조건에서 확인할 수 있는 루프 불변성을 증명할 수 있는 방법은
- 일단 원래의 값에 변조가 없는지 확인하고
- 알고리즘의 목적을 달성했는지 확인한다.
이렇게 2가지를 만족하면 루프 불변성이 성립한다고 할 수 있다.
루프 불변성이 성립하는 2가지 조건은 유지 조건과 종료 조건에서도 성립해야 만한다.
유지 조건
루프의 반복이 시작하기 전에 루프 불변성이 참이었다면 다음 반복이 시작하기 전에도 루프 불변성이 참이어야 한다.
이걸 다시 삽입정렬에 적용해보자
삽입정렬의 유지 조건
일단 A[j-1]의 루프 불변성이 성립한다고 가정한다면 A[j]는 A[1..j-1]의 원소의 변화가 없고 A[j]가 추가된 것이기 때문에 A[1..j]의 원소에는 변화가 없다. 또한 정렬된 A[1..j-1]에서 맞는 위치를 찾아서 A[j]의 값을 적어 넣는 것이기 때문에 A[1..j]는 정렬된 상태이다.
여기서도 아까와 같은 조건이 성립하므로 루프불변성이 성립함을 확인할 수 있다.
종료 조건
루프가 종료될 때 그 불변식이 알고리즘의 타당성을 보이는데 도움이 될 유용한 특성을 가지고 있어야 한다.
앞선 조건들과는 좀 다른데 루프가 끝나고 났을 때에 루프의 결과물이 타당한지 확인하는 조건이라고 할 수 있다.
이렇게 설명을 읽어 보면 알 수 있겠지만 사실상 고등학교 때 배운 수학적 귀납법과 유사한 과정이라고 생각하면 쉬울 것이라고 생각한다.
