2021-11-27-TIL
Today I Learned
무한루프의 검증이 가능한가?
코딩테스트 문제를 풀다보면 가끔씩 무한루프가 발생할 수 있는 문제가 있다. 그런 경우, 대부분 문제에서 특정 조건으로 무한루프를 돌지 않도록 제한할 수 있다. 하지만 만약 정확한 조건을 제한할 수 없다면 어떠한 근거로 무한루프라고 판단할 수 있는가?
- https://en.wikipedia.org/wiki/Loop_invariant
일반적으로는 판단할 수 없다
임의의 프로그램과 입력이 주어졌을 때 그 프로그램이 언젠가 멈출지, 영원히 돌지를 판정하는 문제를 정지 문제(halting problem)라고 한다. 앨런 튜링은 모든 프로그램에 대해 이것을 판정하는 일반적인 알고리즘이 존재할 수 없음을 증명했다. 그래서 “아무 루프나 넣으면 무한루프인지 알려 주는 방법”은 없다.
하지만 이것은 모든 프로그램을 한 번에 다루는 방법이 없다는 뜻이다. 내가 짠 특정 루프가 끝난다는 것은 증명할 수 있고, 특정 조건에서는 무한루프를 확실히 감지할 수도 있다.
끝난다는 근거: 루프 변형식
링크한 루프 불변식(loop invariant)은 매 반복 전후에 항상 참인 조건이다. 불변식은 “루프가 끝난다면 결과가 맞다”는 부분 정확성(partial correctness)을 보여 줄 뿐, 루프가 끝난다는 것 자체는 보장하지 않는다.
종료를 보이는 도구는 루프 변형식(loop variant)이다. 반복할 때마다 엄격하게 줄어들고, 무한히 줄어들 수 없는 값(예를 들어 0 이상의 정수)을 하나 찾으면 된다. 그런 값이 있으면 루프는 반드시 끝난다. 불변식과 변형식을 함께 보이면 결과가 맞고 루프도 끝난다는 완전 정확성(total correctness)이 된다.
1
2
3
4
5
6
int lo = 0, hi = n - 1;
while (lo <= hi) { // 변형식: hi - lo + 1 (남은 구간의 크기)
int mid = (lo + hi) >>> 1;
if (a[mid] < target) lo = mid + 1; // 구간이 최소 1 줄어든다
else hi = mid - 1; // 구간이 최소 1 줄어든다
}
이분 탐색에서 남은 구간의 크기는 매번 1 이상 줄어들고 음수가 될 수 없으므로 루프는 끝난다. 반대로 lo = mid처럼 구간이 줄지 않는 경우가 생기면 변형식이 깨지고, 그 지점이 무한루프의 원인이다.
무한루프라는 근거: 상태의 반복
코딩테스트의 시뮬레이션 문제에서는 반대 방향의 근거를 쓸 수 있다. 다음 상태가 현재 상태만으로 결정되고(결정적), 가능한 상태의 수가 유한하다면, 같은 상태가 두 번 나타나는 순간 그 뒤의 과정은 똑같이 반복된다. 따라서 방문한 상태를 집합에 기록해 두고, 이미 본 상태가 다시 나오면 무한루프라고 판정할 수 있다.
1
2
3
4
5
6
7
8
Set<State> visited = new HashSet<>();
State s = start;
while (!s.isGoal()) {
if (!visited.add(s)) {
return -1; // 같은 상태가 다시 나왔다: 무한루프
}
s = s.next();
}
상태는 위치, 방향, 남은 값처럼 다음 상태를 결정하는 정보를 빠짐없이 담아야 한다. 하나라도 빠지면 다른 상태를 같은 상태로 잘못 판단한다. 또한 이 방법은 상태 수가 유한해야 성립하고, 상태 수만큼의 메모리가 필요하다.
댓글
아직 댓글이 없습니다