정지 문제(Halting problem)
임의의 프로그램과 입력을 받아 그 프로그램이 언젠가 멈출지를 언제나 옳게 판정하는 알고리즘(algorithm)은 없다. 대각선 논법(diagonal argument)의 계산 버전.
프로그램 하나와 입력 하나를 받아, 그 프로그램이 그 입력에서 언젠가 멈출지 아니면 영원히 돌지를 언제나 옳게 답하는 프로그램 H가 있을까요? 그냥 돌려 보는 것으로는 부족합니다. 백만 걸음 뒤에도 멈추지 않았다면, 영원히 도는 것인지 백만한 걸음째에 멈출 것인지 알 수 없기 때문입니다. 1936년 튜링은 그런 H가 있을 수 없음을 증명했습니다. 튜링이 다룬 것은 '기계가 숫자를 끝없이 찍어 내는가'를 가리는 문제였고, 오늘날의 '멈추는가' 형태와 이름은 1950년대에 자리 잡았지만, 논증은 같습니다. 여기서 프로그램은 튜링 기계(Turing machine)든 파이썬 같은 범용 프로그래밍 언어든 상관없습니다. 메모리에 한계가 없다고 치면 둘은 서로를 흉내 낼 수 있기 때문입니다. 나아가 '어떤 기계적 방법으로도 안 된다'고 읽는 것은 처치–튜링 논제(Church–Turing thesis)에 기댑니다.
증명은 표 한 장입니다. 프로그램은 유한한 기호열이니 번호를 붙여 모두 늘어놓을 수 있습니다(가산). 행은 프로그램, 열은 입력으로 준 프로그램의 코드
H가 있다고 해 봅시다. 그러면 H를 부품으로 써서 새 프로그램 D를 만들 수 있습니다. D는 입력 x를 받으면 H(x, x)를 물어, 'x가 자기 코드를 받으면 멈춘다'는 답이면 일부러 무한 반복에 빠지고, '영원히 돈다'는 답이면 곧바로 멈춥니다. D의 줄은 대각선을 한 칸씩 뒤집은 것입니다. D가
칸토어의 대각선 논법(Cantor's diagonal argument)에서 뒤집은 대각선이 목록에 없는 실수(real number)를 만들었듯, 여기서는 목록에 없는 프로그램을 만듭니다. 러셀의 역설(Russell's paradox)의 '자기 자신을 원소(element)로 갖지 않는 집합(set)'과도 같은 모양입니다. 비슷한 시기에 미국 논리학자 알론조 처치도 람다 계산(lambda calculus)으로 판정할 수 없는 문제가 있음을 보였습니다. 정지 문제에서 곧바로 여러 결과가 나옵니다. 미국 논리학자 헨리 고든 라이스가 1953년에 증명한 라이스 정리(Rice's theorem)는, 프로그램이 '무엇을 계산하는가'에 관한 자명하지 않은 성질은 모두 판정할 수 없다고 말합니다. '이 프로그램은 어떤 입력에도 0을 출력하는가', '이 프로그램은 적어도 한 입력에서 멈추는가' 같은 질문이 그런 성질입니다. '자명하지 않다'는 그 성질을 가진 프로그램도, 갖지 않은 프로그램도 있다는 뜻입니다. 코드의 길이처럼 계산 결과가 아니라 코드 자체의 모양에 관한 성질은 여기에 들지 않습니다. 또 참인 산술 문장을 모두, 그리고 참인 것만 증명하는 형식 체계(formal system)가 있다면 정지 문제를 풀 수 있으므로, 여기서 불완전성 정리(incompleteness theorem)도 다시 얻어집니다.
판정할 수 없다는 것이 막연한 말이 아님을 보여 주는 예가 있습니다. 4 이상의 짝수를 차례로 보며 두 소수(prime number)의 합으로 쓸 수 없는 수를 찾으면 멈추는 짧은 프로그램은, 골드바흐 추측(Goldbach's conjecture)이 거짓이면 멈추고 참이면 영원히 돕니다. 골드바흐 추측은 '4 이상의 짝수는 모두 두 소수의 합이다'(예: 10 = 3 + 7)라는 추측으로, 1742년 프로이센의 수학자 크리스티안 골드바흐와 오일러가 주고받은 편지에서 나왔습니다. 이 프로그램 하나가 멈출지를 아는 것이 280년 넘게 풀리지 않은 난제를 푸는 일입니다.
이어지는 곳. 정지 문제가 불가능한 것은 '모든' 프로그램에 대해 판정하는 일입니다. 특정한 프로그램이 멈춘다는 것은 증명할 수 있는 경우가 많고, 입력을 한 번만 훑고 끝나는 유한 오토마톤(finite automaton)은 언제나 멈춥니다. 단순 타입 람다 계산(simply typed lambda calculus)의 프로그램도 언제나 멈추지만, 그 대가로 계산 가능한 함수(function)를 모두 적을 수는 없습니다. 끝나지 않음을 ⊥라는 자리로 수학 안에 적는 영역 이론(domain theory)에서는 '끝나지 않으면 참, 끝나면 거짓'인 함수가 정보의 순서를 거스르므로 처음부터 연속 함수가 될 수 없는데, 이것은 같은 불가능을 순서의 말로 다시 본 것입니다. 프로그램이 명세를 지키는지 증명하는 호어 논리(Hoare logic)도 이 벽에 부딪힙니다. '끝난다면 이 조건이 성립한다'는 부분 정확성(partial correctness)으로 읽으면 {참} C {거짓}은 'C는 어디서 시작해도 끝나지 않는다'는 뜻이라, 모든 삼중을 판정하는 알고리즘은 정지 문제를 풀어 버리기 때문입니다. 풀 수 있는 문제 안에서 '얼마나 빨리' 풀 수 있는지를 묻는 것이 P 대 NP 문제(P versus NP problem)입니다. 어떤 문자열을 출력하는 가장 짧은 프로그램의 길이, 곧 콜모고로프 복잡도(Kolmogorov complexity)도 계산할 수 없습니다. 짧은 프로그램부터 차례로 돌려 보는 방법은 영원히 도는 프로그램에서 막히고, 다른 어떤 방법으로도 안 된다는 것이 비슷한 자기 참조(self-reference) 논증으로 증명되어 있습니다.
이 개념이 나오는 긴 글
이 개념 위에 세워진 것
이 개념을 언급하는 페이지
- 칸토어의 대각선 논법
… 답을 읽고 그것을 뒤집는 대상을 만드는 방식입니다. 모든 프로그램이 멈추는지 판정하는 알고리즘이 없다는정지 문제는 "판정기가 자기에 대해 멈춘다고 답하면 영원히 돌고, 멈추지 않는다고 답하면 멈추는" 프로그램을 …
- 러셀의 역설
… 논리학의 큰 결과마다 다시 나타납니다. 괴델의 불완전성 정리에서는 '나는 증명할 수 없다'는 문장이,정지 문제에서는 자기 코드를 입력받으면 반대로 행동하는 프로그램이 같은 역할을 합니다. 미국 논리학자 ⟦알론조 …
- 괴델의 불완전성 정리
… 바탕인 집합론 공리 체계 ZFC에서 증명도 반증도 할 수 없습니다. 이어지는 곳. 1936년 튜링은정지 문제를 풀 수 없음을 보였는데, 이것에서도 불완전성이 나옵니다. 참인 산술 문장을 모두, 그리고 참인 것만 …
- 튜링 기계
… 않으면 영원히 돈다고 판정할 수 있게 됩니다. 멈추는 기계와 영원히 도는 기계를 이렇게 가려내는 일은정지 문제때문에 불가능합니다. 다섯 상태의 경우 가장 오래 달리는 기계가 47,176,870걸음 만에 멈춘다는 …
- 람다 계산
… 항도 있고, 주어진 항이 정규형에 닿는지 판정하는 일반적인 방법은 없습니다. 처치는 1936년 이것으로정지 문제와 같은 종류의 불가능성을 보였습니다. 처치와 그의 제자 J. 바클리 로서가 증명한 처치–로서 …
- 처치–튜링 논제
… 그래서 오늘날 "그것을 하는 알고리즘은 없다"는 말은 "그것을 하는 튜링 기계는 없다"는 뜻으로 쓰이고,정지 문제가 대표적인 예입니다. 기계는 가산개뿐인데 자연수에서 자연수로 가는 함수는 셀 수 없이 많으니, 계산할 …
- P 대 NP 문제
… 달러의 밀레니엄 문제 가운데 하나로 꼽았습니다. 대부분의 연구자는 P ≠ NP라고 믿지만 증명은 없습니다.정지 문제는 아무리 오래 걸려도 풀 수 없는 문제이고, P 대 NP는 풀 수 있는 문제 안에서 빠르기를 묻는 …
- 유한 오토마톤
… 아래층입니다. 이어지는 곳. 유한 오토마톤은 입력을 한 번 훑으면 반드시 멈추므로, 튜링 기계와 달리정지 문제가 생기지 않습니다. 전이마다 확률을 붙이면 마르코프 연쇄가 되고, 상태는 숨어 있고 상태가 내놓는 …
- 촘스키 위계
… 받아들이는' 튜링 기계가 있는 언어이고, 제한 없는 문법이 적는 언어와 정확히 같습니다. 구체적인 예가정지 문제에서 나옵니다. 멈추는 프로그램들의 코드를 모은 언어는 재귀 열거이지만(돌려 보다가 멈추면 받아들이면 …
- 알고리즘
… 있다는 것까지 증명할 수 있습니다. 대표가 프로그램과 입력을 받아 그 프로그램이 언젠가 멈추는지 판정하는정지 문제입니다. 이어지는 곳. 알고리즘을 설계하는 대표적인 틀이 몇 가지 있습니다. 문제를 같은 모양의 더 작은 …
- 콜모고로프 복잡도
… 모양입니다. 러셀이 옥스퍼드 도서관 사서 G. G. 베리에게서 들었다며 소개한 역설입니다). 이것은정지 문제와 이어져 있습니다. 짧은 프로그램들을 모두 돌려 보면 되지 않느냐고 할 수 있지만, 어떤 프로그램이 끝내 …
- 공리와 공준
… 수학 기초론 논쟁에서, 증명을 기계로 검사할 수 있는 형식 체계의 한계는 괴델의 불완전성 정리와정지 문제에서 이어집니다. 그런 체계에서 쓴 증명을 컴퓨터가 공리와 추론 규칙까지 내려가 한 단계씩 검사하게 하는 …
- 수학 기초론 논쟁
… 쌍둥이 소수가 끝없이 많은지는 아직 아무도 모릅니다. 끝없이 찾아야만 하는 이런 명제의 모양은 뒤에정지 문제에서 다시 나타납니다. 프로그램이 멈추면 멈춘 것을 볼 수 있지만, 멈추지 않는다는 것은 기다려서는 알 수 …
- 기술 집합론
… 너머로 넓힌 것이 위상수학입니다. 논리의 '어떤'과 '모든'이 집합의 층이 되는 모습은 튜링 기계와정지 문제에서 계산 가능성의 층을 세는 방식과도 닮았으며, 둘 다 자기 참조와 대각선과 무한을 다루는 법으로 …
- 정수론
… 퍼트넘, 줄리아 로빈슨의 작업을 이어받아 그런 절차가 있을 수 없음을 증명했습니다. 이 판정 불가능성은정지 문제와 뿌리가 같습니다. 작은 예: 두 제곱수의 합 세 기둥이 한꺼번에 움직이는 예를 봅시다. 어떤 수가 두 …
- 인공지능
… 계산할 수 있는가. 기계가 원리적으로 무엇을 계산할 수 있고 없는지라는 더 밑바닥의 질문은 튜링 기계,정지 문제, 처치–튜링 논제에 있습니다. 이 위키의 AI 페이지들. 표에서 배우는 고전적인 방법. 점들에 가장 …
- 단순 타입 람다 계산
… 곳이 없습니다. 대가도 분명합니다. 모든 계산이 끝나는 언어는 튜링 기계만큼 강할 수 없습니다. 이유는정지 문제와 같은 대각선 논법입니다. 프로그램이 모두 끝나고, 프로그램을 수로 적어 입력으로 줄 수 있으며, 그 …
- 직관주의 논리
… 멈추지 않는다'의 증명이 있다면, 그 증명은 M을 받아 어느 쪽인지를 알려 주는 방법이어야 합니다. 그것은정지 문제를 푸는 프로그램이고, 그런 프로그램은 없습니다. 이 논증은 1945년 미국 논리학자 스티븐 클리니가 …
- 의존 타입
… 검사 자체가 끝나지 않을 수 있습니다. 의존 타입 언어가 모든 함수가 끝나기를 요구하는 이유입니다. 그런데정지 문제때문에 '끝나는 함수'를 빠짐없이 알아볼 수는 없으니, 구조적 되부름처럼 끝남이 눈에 보이는 모양만 …
- 증명 보조기
… 논리의 문장이 증명 가능한지 판정하는 일반적인 방법이 없다는 것이 1936년 처치와 튜링의 결과입니다(정지 문제와 같은 종류의 불가능성). 증명이 있다면 기호열을 짧은 것부터 차례로 검사해 언젠가 찾을 수는 있지만, …
- 데카르트 닫힌 범주
… A에서 A의 부분집합 전체로 가는 전사는 없습니다. 칸토어의 대각선 논법입니다. 러셀의 역설,정지 문제, 괴델의 불완전성 정리의 논증도 같은 틀의 변형으로 읽을 수 있습니다. 반대로 타입이 없는 람다 …
- 선형 논리와 선형 타입
… 정의에서 바로 나오며, 선형 논리 전체의 증명 가능성이 결정 불가능하다는 사실은 카운터 기계의정지 문제를 선형 논리로 옮겨 증명합니다.
- 영역 이론: 스콧과 재귀의 의미
… n에서 끝나면 1'처럼 무한히 많은 값을 봐야 하는 변환은 연속이 아니고, 프로그램으로 쓸 수도 없습니다.정지 문제의 벽도 같은 모양으로 보입니다. 정지 문제 자체는 프로그램의 코드를 입력으로 받는 문제라 아래 논증과 …
- 호어 논리와 프로그램 검증
… 없습니다. {참} C {거짓}은 'C는 어떤 상태에서 시작해도 끝나지 않는다'는 뜻이라, 그런 알고리즘은정지 문제를 풀어 버리기 때문입니다. 그래서 불변식을 기계가 늘 알아서 찾아 줄 수는 없고, 1978년 스티븐 쿡이 …
- 최소 기술 길이
… 모든 프로그램으로 가설의 범위를 넓히면 콜모고로프 복잡도와 솔로모노프의 보편 예측이 되는데, 그 대가는정지 문제때문에 계산할 수 없게 된다는 것입니다. 개수를 적고 배치를 적는 부호의 뼈대는 이항계수입니다. n이 …