티스토리 뷰
정지 문제, 또는 Halting Problem으로 불리는 판정 문제의 한 갈래로 "유한한 수의 단계 후에 주어진 프로그램이 해결하고자 하는 문제가 해결되는지 우리에게 미리 말해줄 수 있는 어떠한 알고리즘이 존재하는가?" 라는 질문이다. 다르게 말 하지면 튜링머신에 1개의 프로그램과 Input자료 1개를 넣으면서 "야 너 이게 유한한 단계 후에 답이 나올지 나에게 풀어보기 전에 미리 알려줄 수 있어?" 라는 질문을 할 때 이를 해결해줄 수 있는 특정한 단일 프로그램이 있는가가 정지 문제이다.
2. 의의[편집]
결론부터 말하자면, 그런 거 없다. 정지를 정지합니다
1936년 앨런 튜링은 이것을 해결할 수 있는 일반화된 방법은 없다라는 결론을 내렸으며[1], 이는 논리학적으로 결정불가능함(undecidable)이 증명한 최초의 문제다. 고로, 현대에 어떠한 문제가 결정불가능인지를 증명할 때 가장 전형적인 방법은 이 문제가 정지문제로 변형될 수 있다는것을 보여주는 방법이다.
여기서 조금 더 확장해보면 알고리즘에서 함수에 대한 non-trivial한 문장은 결정불가능이다라는 라이스의 정리로 이어진다. 라이스의 정리는 어떠한 튜링머신이 받아들이는 내용이 자명한가, 자명하지 않은가에 대한 판단은 불가능하다 라고 정의한다.
3. 증명[편집]
엄밀한 증명은 (앨런 튜링의 증명의 경우) 튜링 머신 및 그 입력 스트링을, (알론조 처치의 증명의 경우) 람다 함수의 정의를 통해 증명한다. 아래 증명은 프로그래밍 경험자 입장에서 쉽게 이해하도록 문제를 실제 프로그래밍 의사코드에 비유하고 있으나, 아래 코드의 각 요소들은 충분히 쉽게 튜링 머신이나 람다 함수꼴로 인코드할 수 있다.
대락적인 증명법을 보자면, 귀류법을 이용한 증명방법이 있다. 즉, 해결방법이 있다라는 가정에서 모순이 발생한다는것을 보임으로써 증명한다. 즉 증명하고자 하는 것은 "정지 문제를 판별하는 알고리즘이 없다"라는 명제이므로, 귀류법을 위해 "정지문제를 판별하는 알고리즘이 있다"고 전제함으로서 시작한다.
정지 문제 판별 알고리즘이 있다고 가정했으니, 이에 따라 exit(a, i)라는 함수를 구현할 수 있다.
a : 사용될 임의의 프로그램
i : 사용될 임의의 input
이 함수는 a가 i 입력에 대해 정지하고 결과를 반환하면 참을, 아니면 거짓을 반환한다. 즉 a 프로그램에 i 입력을 먹이면 알고리즘이 끝날 것인가 무한루프에 빠질것인가를 판별하는 함수가 된다. 쉽게 생각해 a가 함수이고 a(i) 함수 콜이 무한루프에 빠진다면, exit(a, i) == false가 성립한다.
이제 여기서 exit을 모순시키는 함수를 정의한다.
function subroutine(s){
if exit(s,s) == false
return true
else
infinite loop
}
여기서 주의할 점은 다음과 같다.
프로그램의 입력으로 프로그램을 받을 수 있다! 가장 간단한 예로 컴파일러의 경우 프로그램(의 소스)을 받아 프로그램(의 바이너리)을 만드는 프로그램이다. subroutine은 프로그램을 받아 그 프로그램의 입력으로 자기 자신을 되먹인다. 예를 들어 s가 컴파일러일 경우, exit(s, s)는 자기 자신을 컴파일하는 중 무한루프에 빠지는지 여부를 검사한다.
자세히 보면 이 subroutine은 결과를 뒤집는다. 즉 s(s)가 무한루프에 빠질 경우 subroutine는 정상적으로 종료하고, s(s)가 정상적으로 종료할 경우 subroutine은 무한루프에 빠진다.
그리고 나서 마지막 단계로 질문을 던진다.
exit(subroutine, subroutine)은 참인가? 거짓인가?
참일 경우: exit의 정의에 의해 subroutine(subroutine)이 정상적으로 종료해야 한다. 근데 exit(subroutine, subroutine)이 참이라고 가정했으므로 subroutine의 조건문에 의해 무한루프를 한다. 즉 참일 수가 없다.
거짓일 경우: exit의 정의에 의해 subroutine(subroutine)이 무한 루프를 돌아야 한다. 근데 exit(subroutine, subroutine)이 거짓이라고 가정했으므로 subroutine의 조건문에 의해 true를 리턴하고 끝난다. 즉 거짓일 수가 없다.
즉 exit(subroutine, subroutine)이 참도 거짓도 될 수 없다는 것이므로, 모순이 발생한 것이다. 따라서 exit 따위는 존재하지 않는다라는 결론에 이르게 된다. 그렇다면 증명의 시작부로 쭈욱 거슬러 올라가서 exit이 존재하게 하는 가정, 즉 정지 문제를 해결할 알고리즘이 존재한다는 대전제가 붕괴하면서 증명이 종결된다.
여담이지만 어떤 절대적인 법칙이 존재하지 않는다는 것을 증명하기 위해, 귀류법으로 자기모순적인 예제를 만들어 되먹이는 과정이 불완전성 정리의 증명과 매우 유사하다. 다른 문제의 결정불가능성 증명의 상당수가 이러한 구조를 따르거나, 혹은 정지 문제로 환원하여 풀어버린다.