| 수학기초론 Foundations of Mathematics | |||
| {{{#!wiki style="margin: 0 -10px -5px; min-height: calc(1.5em + 5px)" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px" | 다루는 대상과 주요 토픽 | ||
| 수리논리학 | 논리 · 논증{귀납논증 · 연역논증 · 귀추 · 유추} · 공리 및 공준 · 증명{증명보조기 · 자동정리증명 · 귀류법 · 수학적 귀납법 · 반증 · 더블 카운팅 · PWW} · 논리함수 · 논리 연산 · 잘 정의됨 · 조건문(조각적 정의) · 명제 논리(명제 · 아이버슨 괄호 · 역 · 이 · 대우) · 양상논리 · 술어 논리(존재성과 유일성) · 형식문법 · 유형 이론 · 모형 이론 | ||
| 집합론 | 집합(원소 · 공집합 · 집합족 · 곱집합 · 멱집합) · 관계(동치관계 · 순서 관계) · 순서쌍(튜플) · 서수(하세 다이어그램 · 큰 가산서수) · 수 체계 · ZFC(선택공리) · 기수(초한기수) · 절대적 무한 · 모임 | ||
| 범주론 | 범주 · 함자 · 수반 · 자연 변환 · 모나드 · 쌍대성 | ||
| 계산가능성 이론 | 계산 · 오토마타 · 튜링 기계 · 바쁜 비버 · 정지 문제 · 재귀함수 | ||
| 정리 | |||
| 드모르간 법칙 · 대각선 논법 · 러셀의 역설 · 거짓말쟁이의 역설 · 뢰벤하임-스콜렘 정리 · 슈뢰더-베른슈타인 정리 · 집합-부분합 정리 · 퍼스의 항진명제 · 굿스타인 정리 · 완전성 정리 · 불완전성 정리(괴델 부호화) · 힐베르트의 호텔 · 연속체 가설 · 퍼지 논리 | |||
| 기타 | |||
| 예비사항(약어 및 기호) · 추상화 · 벤 다이어그램 · 수학철학 | |||
| 틀:논리학 · 틀:이산수학 · 틀:이론 컴퓨터 과학 · 철학 관련 정보 · 논리학 관련 정보 · 수학 관련 정보 | }}}}}}}}} | ||
| '''이론 컴퓨터 과학 {{{#!wiki style="display: inline-block; font-family:Times New Roman, serif;font-style:italic"''' | |||||
| {{{#!wiki style="margin: 0 -10px -5px; min-height: calc(1.5em + 5px)" {{{#!folding [ 펼치기 · 접기 ] {{{#!wiki style="margin: -5px -1px -11px" | <colbgcolor=#a36> 이론 | ||||
| 기본 대상 | 수학기초론{수리논리학(논리 연산) · 계산 가능성 이론 · 범주론 · 집합론} · 이산수학(그래프 이론) · 수치해석학 · 확률론 및 통계학 · 선형대수학 | ||||
| 다루는 대상과 주요 토픽 | |||||
| 계산 가능성 이론 | 재귀함수 · 튜링 머신 · 람다대수 · 처치-튜링 명제 · 바쁜 비버 | ||||
| 오토마타 이론 | FSM · 푸시다운 · 튜링 머신(폰노이만 구조) · 정규 표현식 · 콘웨이의 생명 게임 · 형식언어 | ||||
| 계산 복잡도 이론 | 점근 표기법 · 튜링 기계^고전, 양자, 비결정론적, 병렬 임의접근 기계^ · 알고리즘 · 자료구조 · 알고리즘 패러다임(그리디 알고리즘, 동적 계획법) | ||||
| 정보이론 | 데이터 압축(무손실 압축 포맷 · 손실 압축 포맷) · 채널 코딩(채널 용량) · 알고리즘 정보 이론(AIT) · 양자정보과학 | ||||
| 프로그래밍 언어이론 | 프로그래밍 언어(함수형 언어 · 객체 지향 프로그래밍 · 증명보조기) · 메타 프로그래밍 · 유형 이론 · 프로그래밍 언어 의미론 · 파싱 · 컴파일러 이론 | ||||
| 주요 알고리즘 및 자료구조 | |||||
| 기초 | 정렬 알고리즘 · 순서도 · 탐색 알고리즘 | ||||
| 추상적 자료형 및 구현 | 배열^벡터^ · 리스트^연결 리스트^ · 셋(set)^레드-블랙 트리, B-트리^ · 우선순위 큐^힙, 피보나치 힙^ | ||||
| 수학적 최적화 | 조합 최적화 | 외판원 순회 문제 · 담금질 기법 · 유전 알고리즘 · 기계학습 | |||
| 볼록 최적화 | 내부점 방법 · 경사하강법 | ||||
| 선형계획법 | 심플렉스법 | ||||
| 계산 수론 및 암호학 | 밀러-라빈 소수판별법 · Pollard-rho 알고리즘 · 쇼어 알고리즘 · LLL 알고리즘 · 해시(MD5 · 암호화폐 · 사전 공격(레인보우 테이블) · SHA) · 양자 암호 | ||||
| 대칭키 암호화 방식 | 블록 암호 알고리즘(AES · ARIA · LEA · Camellia) · 스트림 암호 알고리즘(RC4) | ||||
| 공개키 암호화 방식 | 공개키 암호 알고리즘(타원 곡선 암호 · RSA) · 신원 기반 암호 알고리즘(SM9) | ||||
| 계산기하학 | 볼록 껍질 · 들로네 삼각분할 및 보로노이 도형^Fortune의 line-sweeping 알고리즘^ · 범위 탐색^vp-tree, R-tree^ · k-NN | ||||
| 그래프 이론 | 탐색^BFS, DFS, 다익스트라 알고리즘, A* 알고리즘^ · 에드몬드-카프 · 크루스칼 알고리즘 · 위상 정렬 · 네트워크 이론 | ||||
| 정리 | |||||
| 정지 문제대각선 논법 · 암달의 법칙 · P-NP 문제미해결 · 콜라츠 추측미해결 | |||||
| 틀:이산수학 · 틀:수학기초론 · 틀:컴퓨터공학 | }}}}}}}}} | ||||
1. 개요
停止 問題 / Halting problem정지 문제는 판정 문제(decision problem)의 한 갈래로, "주어진 프로그램이 해결하고자 하는 문제가 해결 가능한지 말해줄 수 있는 일반화된 알고리즘이 존재하는가?" 라는 질문이다.
2. 의의
1936년 앨런 튜링은 이것을 해결할 수 있는 일반화된 방법은 없다라는 결론을 내렸으며[1], 이는 논리학적으로 결정불가능함(undecidable)이 증명된 최초의 문제다. 고로, 현대에 어떠한 문제가 결정 불가능인지를 증명할 때 가장 전형적인 방법은 이 문제가 정지문제로 환원될 수 있다는 것을 보여주는 방법이다.[2] 여기서 조금 더 확장해보면 '알고리즘에서 함수에 대한 non-trivial한 문장은 결정불가능이다'라는 라이스의 정리로 이어진다. 라이스의 정리는 어떠한 튜링 머신이 받아들이는 내용이 자명한가, 자명하지 않은가에 대한 판단은 불가능하다 라고 정의한다.정지 문제를 포함한 어떠한 문제라도 단 한 번의 동작으로 풀 수 있는 가상의 장치인 신탁(oracle) 장치를 튜링 머신에 달아놓은 신탁 기계(oracle machine)라는 가상의 시스템을 가정하더라도 이 신탁 기계는 자기 자신의 정지 문제를 풀 수가 없다.[3] 아래의 귀류법을 통한 증명에서 따라나오는 결론은 "어떤 시스템이 자기 자신에 대한 정지 문제를 풀 수 있다면 그 시스템은 튜링 머신을 모사(simulate)할 능력이 없다."이다.
3. 증명
엄밀한 증명은 앨런 튜링의 증명의 경우 튜링 머신 및 그 입력 스트링을, 알론조 처치의 증명의 경우 람다 함수의 정의를 통해 증명하나, 아래에서는 프로그래밍 경험자 입장에서 쉽게 이해하도록 문제를 실제 프로그래밍 의사코드에 비유하고 있다. 아래 코드의 각 요소들은 충분히 쉽게 튜링 머신이나 람다 함수꼴로 인코드할 수 있다.대락적인 증명법을 보자면, 귀류법을 이용한 증명방법이 있다. 즉, 해결방법이 있다라는 가정에서 모순이 발생한다는 것을 보임으로써 증명한다. 즉 증명하고자 하는 것은 "정지 문제를 판별하는 알고리즘이 없다"라는 명제이므로, 귀류법을 위해 "정지문제를 판별하는 알고리즘이 있다"고 전제함으로서 시작한다.
정지 문제 판별 알고리즘이 있다고 가정했으니, 이에 따라
exit(a, i)라는 함수를 구현할 수 있다.- a: 사용될 임의의 프로그램
- i: 사용될 임의의 input
a가 함수이고 a(i) 함수 콜이 무한 루프에 빠진다면, exit(a, i) == false가 성립한다.이제 여기서 exit을 모순시키는 함수를 정의한다.
function subroutine(s) {
if exit(s,s) == false
return true
else
loop forever
}
여기서 주의할 점은 다음과 같다.
- 프로그램의 입력으로 프로그램을 받을 수 있다! 가장 간단한 예로 컴파일러의 경우 프로그램(의 소스)을 받아 프로그램(의 바이너리)을 만드는 프로그램이다. 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이 존재하게 하는 가정, 즉 정지 문제를 해결할 알고리즘이 존재한다는 대전제가 붕괴하면서 증명이 종결된다.4. 같이 보기
정지 문제의 설명과 증명을 요약한 애니메이션. 영어 음성으로 한글 자막을 지원한다. 영상에서 말하는 Stuck은 Halt와 동의어가 아님에 유의해야한다! Stuck했다면 (프로그램이 뻗어서) Halt가 발생하지 않고, Not Stuck이라면 프로그램이 정상 종료되어 Halt가 발생하는 것이다. 그런데 한글 자막에서는 이를 고려하지 않고 단순히 '멈춘다'라고 번역하여 완전히 반대로 설명이 되어 있으므로 시청 시 이에 유의해야 한다.
들어가서 댓글을 최신순으로 정렬해보면 잘못 이해한 사람들이 상당히 많음을 알 수 있다. 컴퓨터과학이나 수학과는 별로 접점이 없는 시청자 중 일부가 설명을 잘못 이해해서 일어난 참사인 듯하다. 어찌나 반발이 심한지 업로더가 FAQ까지 만들 정도. 심지어 한때는 싫어요 비중이 절반을 넘어가던 시절도 있었다.
잘못 이해한 사람의 대부분은 이 영상이 설명하는 논리 전개의 목적이 '귀류법을 통해, 즉 정지 문제 판별 알고리즘이 존재 가능하다고 가정할 때 모순이 생김을 통해 정지 문제 판별 알고리즘이 존재 불가함을 증명하는' 것임을 간과한다. 이에 따라 대개는 'H가 단순히 무한 루프에 빠지면서 끝나는 것 아니냐', 'N이라는 기계만 없으면 H는 멀쩡하게 작동하는 것 아니냐' 등의 질문을 던진다. 전자의 경우 'H는 증명의 목적상 모든 정지 문제를 풀 수 있다고 전제되었다. H가 올바른 입력을 받았음에도 무한 루프에 걸린다면, 무한 루프에 걸리는 것은 문제를 영영 못 푸는 것이므로 H가 모든 정지 문제를 풀 수 있다는 전제에 모순이 되는 것이다. 따라서 H는 존재하지 않는 게 맞다.'
5. 관련 문서
[1] 비슷한 시기에 튜링보다 조금 빨리 알론소 처치가 다른 방법으로 증명하였으나, 추후에 튜링과 처치는 공동으로 두 증명방식이 본질적으로는 같은 내용이라는것을 보였다.[2] 정지 문제로 환원해볼 수 있는 몇 가지 실세계의 사례로는 교통체증이나 골드버그 장치 등이 있다. 루프에 계속 갇혀있을지, 아니면 교착상태가 해결되고 종료될지 확실하게 결정할 수 없기 때문이다.[3] 바쁜 비버 문서 참고. 고차 바쁜 비버 함수가 바로 이것과 관련이 있다.[4] 한편 이 증명 방식은 전지전능한 존재가 있다는 것을 논파할 때 가장 먼저 나오는 논리 중 하나인데 이 논리가 신이 아니라 기술에도 적용된다는 것에 인지부조화가 온 것일지도.