정지 문제

이 문서에는 일반적인 참조 목록이 포함되어 있지만 대응하는 충분한 인라인 인용이 없습니다. 좀 더 정밀한 인용문을 도입하여 이 글의 개선에 도움을 주시기 바랍니다.(2018년 9월) (이 템플릿메시지 삭제 방법 및 삭제 시기 확인)

계산 가능성 이론에서 정지 문제는 임의의 컴퓨터 프로그램과 입력에 대한 설명에서 프로그램이 실행을 마칠지 아니면 영원히 계속 실행될지를 결정하는 문제이다.앨런 튜링은 1936년에 가능한 모든 프로그램-입력 쌍에 대해 정지 문제를 해결하기 위한 일반 알고리즘은 존재할 수 없다는 것을 증명했다.

모든 프로그램f'병리학적' 프로그램인 프로그램이 중단되는지 여부를 판단할 수 있습니다.g는 어떤 입력과 함께 호출되며, 자신의 소스와 f에 대한 입력을 전달할 수 있으며, f가 예측한 g의 동작과는 특히 반대입니다.이 경우를 처리하는 f는 존재할 수 없습니다.그 증거의 핵심 부분은 튜링 기계로 알려진 컴퓨터와 프로그램의 수학적 정의이다; 정지 문제는 튜링 기계에서 결정할 수 없다.그것은 해결할 수 없는 것으로 증명된 결정 문제의 첫 번째 사례 중 하나이다.이 증거는 어떤 프로그래밍 발명도 완벽하게 수행할 수 없는 응용 프로그램의 클래스를 정의하는 실용적인 컴퓨팅 작업에 있어 중요합니다.

Jack Copeland는 정지라는 용어의 도입이 1950년대에 ^[1]Martin Davis의 연구 덕분이라고 말한다.

배경

정지 문제는 고정된 튜링-완전 계산 모델, 즉 튜링 기계와 동등할 정도로 충분히 일반적인 프로그래밍 언어로 작성될 수 있는 모든 프로그램에 대한 결정 문제입니다.문제는 프로그램 및 프로그램에 대한 입력이 주어졌을 때 해당 입력으로 실행되었을 때 프로그램이 최종적으로 중지되는지 여부를 결정하는 것입니다.이 추상 프레임워크에서는 프로그램 실행에 필요한 메모리 용량이나 시간에 대한 리소스 제한이 없습니다. 중단되기 전에 임의로 시간이 오래 걸리고 임의 저장 공간을 사용할 수 있습니다.문제는 단순히 주어진 프로그램이 특정 입력에서 정지될지 여부입니다.

예를 들어 의사 코드에서 프로그램은

while (true) continue

정지하지 않고 무한 루프 상태로 계속됩니다.반면 프로그램은

print "Hello, world!"

정지합니다.

이러한 프로그램의 정지 여부를 결정하는 것은 간단하지만, 보다 복잡한 프로그램은 문제가 있습니다.이 문제에 대한 한 가지 접근법은 프로그램을 몇 가지 단계 동안 실행하고 프로그램이 중지되는지 확인하는 것입니다.그러나 프로그램이 중단되지 않으면 프로그램이 결국 중단될지 아니면 영원히 실행될지는 알 수 없다.튜링은 주어진 임의의 프로그램과 입력에 대해 프로그램이 그 입력과 함께 실행될 때 정지되는지 여부를 항상 정확하게 결정하는 알고리즘이 없음을 증명했다.튜링의 증명의 본질은 그러한 알고리즘이 모순된 결과를 만들어 낼 수 있고 따라서 정확할 수 없다는 것이다.

프로그래밍 결과

일부 무한 루프는 매우 유용할 수 있습니다.예를 들어 이벤트 루프는 일반적으로 무한 ^[2]루프로서 코드화됩니다.다만, 대부분의 서브루틴은 ^[3]종료하는 것을 목적으로 하고 있습니다.특히, 하드 실시간 컴퓨팅에서 프로그래머들은 종료가 보장될 뿐만 아니라 주어진^[4] 마감일 전에 종료가 보장되는 서브루틴을 쓰려고 시도한다.

때때로 이러한 프로그래머는 범용(튜링 완료) 프로그래밍 언어를 사용하지만 MISRA C나 SPARK와 같은 제한된 스타일로 쓰려고 시도합니다.이렇게 하면 결과 서브루틴이 지정된 기한 ^{[citation needed]}전에 완료됨을 쉽게 증명할 수 있습니다.

이들 프로그래머는 최소전력 규칙을 적용하는 경우도 있습니다.이들은 의도적으로 튜링 완전하지 않은 컴퓨터 언어를 사용합니다.대부분의 ^{[citation needed]}경우 Coq와 같이 모든 서브루틴의 종료를 보증하는 언어입니다.

일반적인 함정

중단 문제의 어려움은 의사결정 절차가 모든 프로그램 및 입력에 대해 작동해야 한다는 요건에 있습니다.특정 프로그램은 특정 입력으로 정지하거나 정지하지 않습니다.항상 "halts"에 응답하는 알고리즘과 항상 "does not stop"에 응답하는 알고리즘 중 하나를 고려합니다.특정 프로그램 및 입력에 대해 이들 2개의 알고리즘 중 하나가 올바르게 응답합니다.다만, 어느 것이 어느 쪽인지 모르는 경우가 있습니다.그러나 두 알고리즘 모두 정지 문제를 일반적으로 해결하지는 않습니다.

주어진 소스 코드의 실행을 시뮬레이트하는 프로그램(인터프리터)이 있습니다.이러한 프로그램들은 이 경우 프로그램이 중지됨을 보여줄 수 있습니다. 즉, 인터프리터 자체가 결국 시뮬레이션을 중지하게 되며, 이는 원래 프로그램이 중지되었음을 나타냅니다.그러나 인터프리터는 입력 프로그램이 정지하지 않으면 정지하지 않기 때문에 이 방법으로는 정지 문제를 해결할 수 없습니다.정지하지 않는 프로그램에 대해서는 정상적으로 "정지하지 않음"이라고 대답할 수 없습니다.

정지 문제는 이론적으로 유한 메모리를 가진 LBA(Linear Bounded Automata) 또는 결정론적 기계에 대해 결정 가능합니다.메모리가 유한한 머신의 설정은 한정되어 있기 때문에, 그 머신의 결정론적 프로그램은 최종적으로 이전의 ^[5]설정을 정지하거나 반복할 필요가 있습니다.

...어떤 유한 상태 기계라도 완전히 방치하면, 결국 완벽하게 주기적인 반복 패턴에 빠지게 됩니다.이 반복 패턴의 지속 시간은 시스템의 내부 상태 수를 초과할 수 없습니다.

단, 백만 개의 작은 부품이 있고 각각 2개의 상태가 있는 컴퓨터는 적어도^1,000,000 2개의 상태를 ^[6]가질 수 있습니다.

이것은 1 뒤에 약 30만 개의 0이 이어지는 것입니다.그러한 기계가 우주선의 주파수로 작동한다고 해도, 은하 진화의 연속은 그러한 사이클을 통과하는 여행 시간에 비하면 아무것도 아닐 것입니다.

기계는 유한할 수 있지만, 오토마타는 "여러 가지 이론적인 한계가 있다":^[6]

...관련된 규모는 주로 국가 다이어그램의 최종성에 기초한 이론과 논거가 큰 의미를 지니지 않을 수 있다는 의심을 불러일으킬 것이다.

또한 각각의 가능한 결정 후에 상태를 열거함으로써 유한한 메모리를 가진 비결정론적 기계가 비결정론적 결정의 가능한 시퀀스 중 하나, 일부 또는 전부를 정지시킬지 여부를 자동으로 결정할 수 있다.

역사

정지하는 문제는 역사적으로 중요한데, 그 이유는 그것이 가장 먼저 입증될 수 없는 문제 중 하나였기 때문이다.1936년 4월, Alonzo Church는 람다 미적분 문제의 결정 불가능성에 대한 그의 증거를 발표했다.튜링의 증거는 1937년 1월에 출판되었다.그 이후로, 다른 많은 결정 불가능한 문제들이 설명되었다.

타임라인

• 1900(표준):데이비드 힐베르트는 파리에서 열린 제2차 국제 수학자 대회에서 "23개의 질문" (현재는 힐베르트의 문제로 알려져 있음)을 제출했습니다. "이들 중 두 번째는 '페아노 공리'의 일관성을 증명하는 것으로, 그가 보여줬듯이, 수학의 엄격함에 의존했습니다."^[7]
• 1920년(1992년) ~ 1921년(1921년) :Emil Post는 태그 시스템의 정지 문제를 해결 ^[8]불가능한 후보로 보고 있습니다. 이것의 해결 불가능성은 훨씬 후에 Marvin Minsky에 ^[9]의해 확립되었습니다.
• 1928(표준):힐베르트는 볼로냐 ^[10]국제회의에서 그의 '제2의 문제'를 다시 한 번 말한다. 그는 세 가지 질문을 던졌다. 즉, #1: 수학은 완료되었는가? #2: 수학은 일관성이 있습니까? #3: 수학은 어려운가?^[11] 세 번째 질문은 "결정 문제"^[12]로 알려져 있습니다.
• 1930(표준):Kurt Gödel은 힐베르트의 1928년 질문 ^[13]중 처음 두 가지에 대한 답으로 증거를 발표한다. "처음에는 힐버트가 화를 내고 좌절했을 뿐이었지만, 그 후 그는 문제를 건설적으로 다루려고 하기 시작했습니다. 괴델은 자신의 작품이 힐베르트의 형식주의적 관점과 모순되지 않는다고 느꼈고, 그의 논문에 그 생각을 표현했다.^[14]
• 1931(표준):Gödel은 "공식적으로 결정할 수 없는 수학 원리 및 관련 시스템 I"을 출판합니다.^[15]
• 1935년 4월 19일(1935-04-19):Alonzo Church는 효과적으로 계산할 수 있는 함수의 직관적인 개념은 일반 재귀 함수에 의해 또는 람다 정의 가능한 함수에 의해 동등하게 공식화될 수 있다고 제안하는 "소수 이론의 해결할 수 없는 문제"를 출판한다. 그는 람다 미적분의 정지 문제(즉, 주어진 람다 식이 정규 형태를 갖는지 여부)를 효과적으로 계산할 수 없다는 것을 증명한다.^[16]
• 1936년(표준):Church는 "Entscheidungsproblem"이 해결할 수 없다는 첫 번째 증거를 발표했다.^[17]
• 1936년 10월 7일(1936-10-07) :Emil Post의 논문 "무한 조합 프로세스" 공식 I"가 수신됩니다. Post는 "프로세스"에 "(C) Stop" 명령을 추가합니다. 그는 이러한 프로세스를 "각 특정 문제에 대해 프로세스가 종료되는 경우 유형 1..."이라고 불렀습니다.^[18]
• 1936년 5월(1936-05) ~ 1937년 1월(1937-01) :앨런 튜링의 "계산 가능한 숫자에 관한 문제"는 1936년 5월에 출판되었고 1937년 ^[19]1월에 인쇄되었다. 튜링의 증명은 재귀 함수에 의한 계산에서 벗어나 기계에 의한 계산 개념을 도입한다. 이는 "해결 불가능한 것으로 판명된 의사결정 문제의 첫 번째 예"^{[20][page needed]} 중 하나이다.
• 1939년(1939년): J. 바클리 로서는 괴델, 처치 및 튜링에 의해 정의된 "유효한 방법"의 본질적 등가성을 관찰한다.^[21]
• 1943년(1943년):한 논문에서 스티븐 클린은 다음과 같이 말한다. "완전한 알고리즘 이론을 세울 때, 우리가 하는 것은 절차를 설명하는 것이다... 어떤 절차가 필연적으로 종료되며, 그 결과로부터 '예' 또는 '아니오'라는 질문에 대한 확답을 읽을 수 있는 방식으로 '술어 값이 참인가?'라는 질문에 대한 것이다."
• 1952년(표준):클린은 튜링 기계의 정지 문제에 대한 해결 불가능성에 대한 논의를 포함하고 "결국 정지"하는 기계의 관점에서 그것을 재구성한다. 즉, 정지: "... 주어진 상황에서 시작되었을 때, 주어진 기계가 결국 정지하는지를 결정하는 알고리즘은 없다."^[22]
• 1952년(표준):마틴 데이비스는 1952년 일리노이 대학 제어 시스템 연구소의 일련의 강의에서 '해열 문제'라는 용어를 사용했다. 이러한 용어의 사용은 이번이 처음일 가능성이 높다.^[23]

"halting problem"이라는 말의 어원

튜링은 그의 어떤 작품에서도 "해부"나 "종료"라는 단어를 사용하지 않았다.튜링의 전기 작가 호지스는 그의 색인에 "halting" 또는 "halting problem"이라는 단어를 가지고 있지 않다.1958년 ^[24]데이비스가 증명한 "halting problem"이라는 단어의 최초 사용 기록은 다음과 같다.

"이론 2.2 정지 문제를 반복적으로 해결할 수 없는 튜링 기계가 존재합니다.
이와 관련된 문제는 심볼_i S"에 대한 단순한 튜링 기계 Z의 인쇄 문제다.

데이비스는 그의 증거에 대해 아무런 설명도 덧붙이지 않기 때문에, 사람들은 그것이 그가 독창적이라고 추측한다.그러나 데이비스는 클린이 비공식적으로 ^[22]증거를 진술했다고 말했다.Copeland는 다음과 같이 말한다.^[1]

마틴 데이비스가 (처음 ^[23]말한 것처럼) 멈춘 문제는 그렇게 명명했다.('계산 가능한 숫자에 대하여'에서 튜링이 정지정리를 진술하고 증명했다고 종종 말하지만, 엄밀히 말하면 이는 사실이 아니다.)

형식화

그의 원본 증명에서 튜링은 튜링 기계를 도입함으로써 알고리즘의 개념을 공식화했다.그러나 결과는 그들에게 특정한 것이 아니다; 그것은 마르코프 알고리즘, 람다 미적분, 포스트 시스템, 레지스터 머신 또는 태그 시스템과 같이 튜링 기계에 대한 계산 능력에 동등한 다른 계산 모델에 동등하게 적용된다.

중요한 것은 형식화를 통해 알고리즘이 동작할 수 있는 데이터 유형에 알고리즘을 쉽게 매핑할 수 있다는 것입니다.예를 들어, 형식주의가 알고리즘이 문자열(튜링 기계 등) 위에 함수를 정의하도록 허용한다면, 이러한 알고리즘의 문자열에 대한 매핑이 있어야 하며, 형식주의가 알고리즘이 자연수 위에 함수를 정의하도록 허용한다면 알고리즘과 자연수의 매핑이 있어야 한다.문자열에 대한 매핑은 보통 가장 간단하지만 n개의 문자를 가진 알파벳 위의 문자열을 n개의 숫자 시스템에서 숫자로 해석하여 숫자에 매핑할 수도 있습니다.

세트로서의 표현

의사결정 문제의 일반적인 표현은 문제의 속성을 소유하는 객체 집합이다.정지 세트

K = {(i, x) 프로그램 i가 입력 x}에서 실행될 때 중지됨

정지 문제를 나타냅니다.

이 집합은 반복적으로 열거할 수 있습니다. 즉, 포함된 모든 쌍(i, x)을 나열하는 계산 가능한 함수가 있음을 의미합니다.그러나 이 집합의 보수는 반복적으로 열거할 ^[25]수 없습니다.

정지 문제에는 많은 동등한 공식들이 있다; 튜링 정도가 정지 문제의 그것과 같은 집합은 그러한 공식이다.이러한 집합의 예는 다음과 같습니다.

• {i 프로그램이 입력 0으로 실행되면 중지됨}
• {i 입력 x}로 실행하면 프로그램이 중지되는 입력 x가 있습니다.

실증 개념

Christopher Stracey는 중단 문제가 해결될 ^[26][27]수 없다는 모순을 통해 증거를 개략적으로 설명했다.증명은 다음과 같이 진행됩니다.서브루틴 f가 정지하면 true를 반환하고, 그렇지 않으면 false를 반환하는 합계 계산 가능 함수가 있다고 가정합니다.다음 서브루틴에 대해 생각해 보겠습니다.

방어하다 g():     한다면 정지하다(g):         loop_module() 

halts(g)는 true 또는 false를 반환해야 합니다.halts는 합계로 간주되었기 때문입니다.halts(g)가 true를 반환하면 g는 loop_forever를 호출하고 정지하지 않습니다.이것은 모순입니다.halts(g)가 false를 반환하면 g는 정지합니다.이는 loop_forever를 호출하지 않기 때문입니다.이것도 모순입니다.전체적으로 g는 g가 해야 한다고 말하는 것과 반대이기 때문에 halts(g)는 g가 halt되는지 여부와 일치하는 참 값을 반환할 수 없습니다.따라서 halts가 전체 계산 가능 함수라는 초기 가정은 거짓이어야 합니다.

엄밀한 증거의 스케치

위의 개념은 증명의 일반적인 방법을 보여주지만, 계산 가능한 함수는 서브루틴을 인수로 직접 사용하지 않고 프로그램의 소스 코드를 취합니다.게다가, g의 정의는 자기 참조적이다.엄밀한 증거가 이러한 문제를 해결합니다.전체적인 목표는 임의의 프로그램 i가 임의의 입력 x에서 정지하는지 여부를 결정하는 완전한 계산 가능 함수가 없음을 보여주는 것이다. 즉, 다음 함수 h("halts"의 경우)는 계산할 ^[28]수 없다.

${\displaystyle h(i,x)=syslog{case}1&{\text{if}}}{\text{program }}}ix,\0&{\text{cases}}} 입력이 중지됩니다.}}\end {case}}$

여기서 프로그램 i는 고정 튜링 완전 계산 모델의 모든 프로그램의 열거에서 i번째 프로그램을 참조한다.

증명은 두 개의 인수를 가진 모든 계산 가능 함수가 필수 함수 h가 될 수 없다는 것을 직접 입증함으로써 진행된다.개념의 개요와 같이, 모든 계산 가능한 이진 함수 f가 주어졌을 때, 다음과 같은 부분 함수 g도 일부 프로그램 e에 의해 계산 가능하다.

${\displaystyle g(i)=cases}0&{\text{if}}}f(i,i)=0,\{\text{cases}&{\text{cases}}.}}\end {case}}$

g가 계산 가능하다는 검증은 다음 구성체(또는 이에 상당하는 구성체)에 의존한다.

• 계산 가능한 하위 프로그램(f를 계산하는 프로그램은 프로그램 e의 하위 프로그램),
• 값의 중복(프로그램 e는 g의 입력 i에서 f의 입력 i, i를 계산한다),
• 조건부 분기(프로그램 e는 f(i,i)에 대해 계산하는 값에 따라 두 결과 중 선택),
• 정의된 결과를 생성하지 않음(영구적인 루프 등),
• 값 0을 반환합니다.

e의 다음 의사 코드는 g를 계산하는 간단한 방법을 나타냅니다.

절차. e(i):     한다면 f(i, i) == 0 그리고나서         돌아가다 0     또 다른         고리 영원히. 

g는 부분 계산 가능하기 때문에, 계산 모델이 튜링 완전이라는 가정에 의해 g를 계산하는 프로그램 e가 있어야 한다.이 프로그램은 정지 함수 h가 정의되어 있는 모든 프로그램 중 하나입니다.증명의 다음 단계는 h(e, e)가 f(e, e)와 같은 값을 가지지 않음을 나타냅니다.

g의 정의에 따라 다음 두 가지 경우 중 하나가 충족되어야 합니다.

• f(e,e) = 0 정도 g(e) = 0. 이 경우 프로그램 e는 입력 e에서 정지하므로 h(e,e) = 1입니다.
• f(e, e) 0 0이므로 g(e)는 정의되어 있지 않습니다.이 경우 프로그램 e는 입력 e에서 중지되지 않으므로 h(e, e) = 0입니다.

어느 경우든 f는 h와 같은 함수가 될 수 없습니다.f는 두 개의 인수를 가진 임의의 합계 계산 가능 함수였기 때문에, 그러한 모든 함수는 h와 달라야 한다.

이 증거는 칸토어의 대각선 주장과 유사하다.위의 표와 같이 각 자연수에 대해 하나의 열과 하나의 행으로 2차원 배열을 시각화할 수 있습니다.f(i,j) 값은 i행 j에 배치됩니다.f는 전체 계산 가능 함수로 간주되기 때문에 어레이의 모든 요소는 f를 사용하여 계산할 수 있습니다.함수 g의 구성은 이 배열의 주 대각선을 사용하여 시각화할 수 있습니다.배열의 위치(i,i)에 0이 있으면 g(i)는 0입니다.그렇지 않으면 g(i)는 정의되지 않습니다.이 모순은 배열에 g 자체에 대응하는 열 e가 있다는 사실에서 비롯됩니다.이제 f가 정지 함수 h라고 가정하고, g(e)가 정의되면(이 경우 g(e) = 0), g(e)는 f(e, e) = 1로 정지한다. 그러나 g(e) = 0일 때만 g(e) = 0, 모순되는 f(e) = 1. 마찬가지로 g(e)가 정의되지 않으면, f(e) = 1로 정지 함수 f(e)가 정의되지 않는다.이는 g(e)가 정의되지 않는다는 가정과 모순된다.두 경우 모두 모순이 발생합니다.따라서 임의의 계산 가능 함수 f는 정지 함수 h가 될 수 없습니다.

계산가능성 이론

문제를 결정할 수 없음을 증명하는 일반적인 방법은 문제를 정지 문제로 줄이는 것입니다.예를 들어, 자연수에 대한 특정 문장이 참인지 거짓인지를 결정하는 일반 알고리즘은 있을 수 없습니다.그 이유는 특정 입력이 주어지면 특정 프로그램이 정지한다는 명제는 자연수에 대한 동등한 문장으로 변환될 수 있기 때문이다.알고리즘이 자연수에 대한 모든 문장의 진실 값을 찾을 수 있다면, 이 문장의 진실 값을 찾을 수 있을 것입니다. 그러나 원래 프로그램이 중지되는지 여부를 결정합니다.

라이스의 정리는 정지 문제는 풀 수 없다는 정리를 일반화한다.그것은 모든 비사소한 속성에 대해, 모든 프로그램에 대해, 입력 프로그램에 의해 구현된 부분 함수가 그 속성을 가지고 있는지 여부를 결정하는 일반적인 결정 절차는 없다고 명시하고 있다. (부분 함수는 항상 결과를 생성하지 않을 수 있는 함수이며, 따라서 결과를 생성하거나 h를 실패시킬 수 있는 프로그램을 모델링하는 데 사용된다.)예를 들어, alt.) "입력 0에 대한 halt" 속성은 판별할 수 없습니다.여기서 "non-trival"은 속성을 충족하는 부분 함수의 집합이 빈 집합도 아니고 모든 부분 함수의 집합도 아님을 의미합니다.예를 들어, "halts or failed to stop on input 0"은 모든 부분 함수에 대해 명백하게 참이기 때문에 사소한 속성이며 단순히 "true"를 보고하는 알고리즘에 의해 판별할 수 있습니다.또한, 이 정리는 프로그램에 의해 구현된 부분 함수의 속성에만 적용됩니다. 라이스 정리는 프로그램 자체의 속성에는 적용되지 않습니다.예를 들어, "100단계 내 입력 0에 대한 중단"은 프로그램에 의해 구현되는 부분 함수의 속성이 아니라 부분 함수를 구현하는 프로그램의 속성으로 매우 결정 가능합니다.

그레고리 차이틴은 무작위로 생성된 프로그램이 정지할 확률을 비공식적으로 나타내는 실수의 일종인 기호 δ로 나타나는 정지 확률을 정의했습니다.이 숫자들은 정지 문제와 같은 튜링 정도를 가지고 있다.이는 정의할 수 있지만 완전히 계산할 수는 없는 정규적이고 초월적인 숫자입니다.즉, δ의 숫자를 생성하는 알고리즘이 없다는 것을 증명할 수 있습니다.단, 처음 몇 자리 숫자는 간단한 경우로 계산할 수 있습니다.

튜링의 증거는 알고리즘이 멈추는지 여부를 결정하는 일반적인 방법이나 알고리즘이 있을 수 없다는 것을 보여주는 반면, 그 문제의 개별 인스턴스는 공격에 매우 민감할 수 있다.특정 알고리즘을 지정하면 입력에 대해 정지해야 한다는 것을 나타내는 경우가 많습니다.사실 컴퓨터 과학자는 정확성 증명의 일환으로 정지하는 경우가 많습니다.그러나 각각의 증명은 특별히 가까운 알고리즘에 대해 개발되어야 한다; 튜링 기계상의 알고리즘이 멈추는지 여부를 결정하는 기계적이고 일반적인 방법은 없다.그러나 일반적인 프로그램에서 자주 성공하는 증명 작성을 위해 자동화된 방법으로 사용할 수 있는 휴리스틱스가 몇 가지 있습니다.이 연구 분야를 자동 종료 분석이라고 합니다.

정지하는 문제에 대한 부정적인 답변이 튜링 기계로 해결할 수 없는 문제들이 있다는 것을 보여주기 때문에, 처치-튜링 논문은 효과적인 방법을 구현하는 기계에 의해 성취될 수 있는 것을 제한한다.그러나 인간의 상상으로 상상할 수 있는 모든 기계가 처치-튜링 논문(예: 오라클 기계)의 대상이 되는 것은 아니다.장기적으로 튜링 기계에 의한 시뮬레이션을 회피하는 실제 결정론적 물리적 과정이 있을 수 있는가, 그리고 특히 그러한 가설적 과정이 튜링 기계를 위한 정지 문제를 해결할 수 있는 계산 기계(하이퍼 컴퓨터)의 형태로 유용하게 이용될 수 있는가 하는 것은 열린 질문이다.다른 것들이요.이와 같이 알려지지 않은 물리적 과정이 인간의 두뇌의 작용에 관여하고 있는지, 그리고 인간이 정지된 ^[29]문제를 해결할 수 있는지 여부도 미해결의 문제이다.

괴델의 불완전성 이론

이 섹션은 어떠한 출처도 인용하지 않습니다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 섹션의 개선에 도움을 주십시오. 조달되지 않은 자재는 제거될 수 있습니다.(2019년 8월) (이 템플릿메시지 삭제 방법 및 삭제 시기 확인)

괴델의 불완전성 정리에 의해 제기된 개념은 정지된 문제에서 제기된 개념과 매우 유사하며, 증명도 상당히 유사합니다.사실, 첫 번째 불완전성 정리의 더 약한 형태는 정지 문제의 결정 불가능성의 쉬운 결과이다.이 약한 형태는 완전하고 소리나는 자연수의 공리화가 불가능하다고 주장함으로써 불완전성 정리의 표준 진술과는 다르다."소리" 부분은 약해지는 것입니다: 그것은 우리가 자연수에 대한 진실된 진술만을 증명하기 위해 문제의 공리적인 시스템을 필요로 한다는 것을 의미합니다.건전성은 일관성을 의미하기 때문에 이 약한 형태는 강한 형태의 결과로 볼 수 있다.괴델의 제1불완전성정리의 표준형태의 진술은 진술의 진실값과는 전혀 무관하지만 수학적 증거를 통해 그것을 찾을 수 있는가 하는 문제에만 관계된다는 것을 관찰하는 것이 중요하다.

정리의 더 약한 형태는 정지 문제의 결정 불가능에서 다음과 같이 증명될 수 있다.자연수에 관한 모든 진실된 1차 논리 스테이트먼트의 건전한(따라서 일관된) 완전한 공리화가 있다고 가정합니다.그런 다음 이 모든 문장을 열거하는 알고리즘을 구축할 수 있습니다.이것은 자연수 n이 주어졌을 때 자연수에 대한 진정한 1차 논리문을 계산하는 알고리즘 N(n)이 있다는 것을 의미하며, 모든 참 문장에 대해 N(n)이 그 문을 생성하도록 적어도 1개의 n이 있다는 것을 의미한다.이제 a를 나타내는 알고리즘이 입력 i에서 정지하는지 여부를 결정한다고 가정합니다.이 문장은 1차 논리문(예를 들어 H(a, i))으로 표현될 수 있습니다.공리화가 완료되었으므로 N(n) = H(a, i)인 n이 존재하거나 N(n') = h H(a, i)인 n'이 존재하게 된다.따라서 H(a, i) 또는 그 부정을 찾을 때까지 모든 n을 반복하면 우리는 항상 중단하고 더 나아가 그것이 제공하는 답은 (건전성에 의해) 참이 됩니다.이는 정지 문제를 결정하는 알고리즘을 제공한다는 것을 의미합니다.우리는 그러한 알고리즘이 있을 수 없다는 것을 알고 있기 때문에 자연수에 관한 모든 진실된 1차 논리 스테이트먼트의 일관되고 완전한 공리화가 존재한다는 가정은 거짓이어야 한다.

일반화

정지 문제의 많은 변형은 계산 가능성 ^[30]교과서에서 찾을 수 있습니다.일반적으로 이러한 문제는 재완성되며 표준 정지 문제와 마찬가지로 산술적 계층 내 복잡도 ${\displaystyle {\delta \mathrm{}}_{}^{}}$ 1$$(\$displaystyle \Sigma$ _${1}^0})$을 나타냅니다.따라서 변형을 결정할 수 없으며, 표준 정지 문제는 각 변종으로 감소하며, 그 반대도 마찬가지입니다.단, 일부 변형은 높은 수준의 용해성을 가지며 표준 정지 문제로 환원할 수 없습니다.다음 두 가지 예는 일반적입니다.

모든 입력에서 정지

(재귀 이론에서) 전체성이라고도 알려진 보편적 정지 문제는 주어진 컴퓨터 프로그램이 모든 입력에 대해 정지할 것인지 결정하는 문제입니다(전체라는 이름은 계산된 함수가 전체인지 여부에 대한 동등한 질문에서 유래합니다).이 문제는 정지 문제로서 결정할 수 없을 뿐만 아니라 매우 결정할 수 없습니다.산술적 계층구조로 $보면{\displaystyle {\mathrm{}}_{}^{}}$ ${\displaystyle {\mathrm{}}_{}^{}}$0(\$displaystyle \Pi$ _$$${2}^{0})$ ^[31]-complete이다.

이는 특히 정지된 문제에 대해 오라클을 사용해도 결정할 수 없다는 것을 의미합니다.

부분 솔루션 인식

일부 입력의 경우 정지된 문제에 대한 정답을 반환하고 다른 입력의 경우 정답을 반환하지 않는 프로그램이 많이 있습니다.단, "프로그램 p가 주어졌을 때 부분 정지 솔버인가"라는 문제는 적어도 정지 문제만큼 어렵다.이를 확인하려면 이를 위한 알고리즘 PHSR(부분 정지 솔버 인식자)이 있다고 가정합니다.그런 다음 다음과 같이 정지 문제를 해결할 수 있습니다.입력 프로그램 x가 y로 정지하는지 여부를 테스트하려면 입력(x,y)에서 true를 보고하고 다른 모든 입력에서 분기하는 프로그램 p를 구성합니다.다음으로 PHSR을 사용하여 p를 테스트합니다.

위의 인수는 정지 문제를 PHS 인식으로 환원하는 것이며, 마찬가지로 모든 입력에 대한 정지 등의 어려운 문제도 줄일 수 있습니다.이는 PHS 인식이 결정되지 않을 뿐만 아니라 산술적 계층, 특히 ${\displaystyle {\mathrm{}}_{}^{}}$ 0$($ 스타일 $\Pi$ _${2}^0})$에서 더 높다는 것을 의미합니다.

손실계산

손실 튜링 기계는 테이프의 일부가 비결정적으로 사라질 수 있는 튜링 기계이다.정지 문제는 손실 튜링 머신에 대해 결정 가능하지만 비원발성 ^[32]재귀적입니다.

오라클 머신

정지 문제에 대한 오라클이 있는 기계는 특정 튜링 기계가 특정 입력에 대해 정지할지 여부를 결정할 수 있지만, 일반적으로 그들은 자신과 동등한 기계가 정지할지를 결정할 수 없다.

「 」를 참조해 주세요.

• 바쁜 비버
• 괴델의 불완전성 정리
• 브루어-힐베르트 논쟁
• 콜모고로프 복잡도
• P 대 NP 문제
• 종료 분석
• 최악의 경우 실행 시간

메모들

레퍼런스

• Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (2): 345–363. doi:10.2307/2371045. JSTOR 2371045.
• Copeland, B. Jack, ed. (2004). The essential Turing : seminal writings in computing, logic, philosophy, artificial intelligence, and artificial life, plus the secrets of Enigma. Oxford: Clarendon Press. ISBN 0-19-825079-7.
• 튜링의 논문은 이 책에서 3번이다Davis, Martin (1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. New York: Raven Press..Godel, Church, Rosser, Kleene, Post의 논문을 포함합니다.
• 를 클릭합니다Davis, Martin (1958). Computability and Unsolvability. New York: McGraw-Hill..
• 제13장('계산 가능한 함수')에서는 튜링 기계의 정지 문제의 해결 불가능성에 대해 설명합니다Kleene, Stephen Cole (1952). Introduction to metamathematics. North-Holland. ISBN 0923891579..튜링의 용어인 원 없는 비할로팅 기계에서 벗어나 클린은 대신 멈추는 기계, 즉 멈추는 기계를 말합니다.
• Minsky, Marvin (1967). Computation: finite and infinite machines. Englewood Cliffs, NJ: Prentice-Hall. ISBN 0131655639.. 제8장 섹션 8.2 "정지 문제의 해결 불가능"을 참조하십시오.
• Moore, Cristopher; Mertens, Stephan (2011). The Nature of Computation. Oxford University Press. doi:10.1093/acprof:oso/9780199233212.001.0001. ISBN 978-0-19-923321-2.
• 1970년에 처음 출판된 이 책은 1880년대부터 1930년대까지 독일의 수학과 물리학의 흥미로운 역사이다Reid, Constance (1996). Hilbert. New York: Copernicus. ISBN 0387946748..수학자, 물리학자, 엔지니어들에게 친숙한 수백 개의 이름이 그 페이지에 등장한다.아마도 명확한 언급이 없고 각주가 거의 없어 손상되었을 것이다.리드는 힐버트를 개인적으로 아는 사람들과의 수많은 인터뷰와 힐버트의 편지와 논문들이 그녀의 정보원이었다고 말했다.
• Sipser, Michael (2006). "Section 4.2: The Halting Problem". Introduction to the Theory of Computation (Second ed.). PWS Publishing. pp. 173–182. ISBN 0-534-94728-X.
• 튜링, A.M.(1937년)."연산 번호는 Entscheidungsproblem에 대한 적용으로".런던 수학 학회 회보.Wiley도.s2-42(1):230–265. doi:10.1112/plms/s2-42.1.230.ISSN 0024-6115., 튜링, A.M.(1938년)."에 계산 가능한 숫자를 적용하는 Entscheidungsproblem.ACorrection".런던 수학 학회 회보.Wiley도.s2-43(1):544–546. doi:10.1112/plms/s2-43.6.544.ISSN 0024-6115.어디 이제 중단 문제를 입안하면서 그것이(또한 Entscheidungsproblem로)해결이 불가능하다는 것을 보여 주튜링 기계들을 정의합니다 이것은 획기적인 종이다.
• Penrose, Roger (1989). The emperor's new mind: concerning computers, minds, and the laws of physics (1990 corrected reprint ed.). Oxford: Oxford University Press. ISBN 0192861980.. 2장 "알고리즘과 튜링 기계" 참조.지나치게 복잡한 프레젠테이션(더 나은 모델을 위해 데이비스의 논문 참조), 튜링 기계와 정지하는 문제에 대한 철저한 프레젠테이션, 처치의 람다 미적분.
• Hopcroft, John E.; Ullman, Jeffrey D. (1979). Introduction to Automata Theory, Languages, and Computation (1st ed.). Addison-Wesley. ISBN 81-7808-347-7.. 7장 "기계 조작"을 참조하십시오.「언어」, 「NP-완전성」등의 기계 해석을 중심으로 한 책.
• 참고: 그의 증거로 이어지는 역사와 그에 대한 논의를 위한 "진실의 정신" 장Hodges, Andrew (1983). Alan Turing: the enigma. New York: Simon and Schuster. ISBN 0-671-49207-1..
• Börger, Egon (1989). Computability, complexity, logic. Amsterdam: North-Holland. ISBN 008088704X.
• Abdulla, Parosh Aziz; Jonsson, Bengt (1996). "Verifying Programs with Unreliable Channels". Information and Computation. 127 (2): 91–101. doi:10.1006/inco.1996.0053.

추가 정보

• c2: Halting Problem(중지 문제)
• Alfred North Whitehead와 Bertrand Russell, 프린키피아 매스매티카에서 *56까지, 케임브리지 대학 출판부에서 1962년.Re: 역설의 문제, 저자들은 집합의 어떤 "결정함수"에서도 객체가 되지 않는 문제에 대해 논의한다. 특히 "서론, 1장 24절"과 "형식 논리에서 발생하는 어려움"과 2.I장 "악의-원칙" 페이지 37ff, 2장.VII. "The Contractions"
• 마틴 데이비스, "컴퓨팅이란 무엇인가", 수학 투데이의 린 아서 스틴, 빈티지 북스(랜덤 하우스), 1980.비전문가를 위한 튜링 머신에 대해 쓰여진 것 중 가장 훌륭한 작은 논문입니다.데이비스는 튜링 머신을 Post의 계산 모델에 기초한 원심플러 모델로 축소합니다.Chaitin 증명에 대해 논의합니다.에밀 포스트, 줄리아 로빈슨의 전기도 포함되어 있습니다.
• 에드워드 벨트라미, 랜덤이 뭐죠? 수학과 삶에 있어서의 기회와 질서, 코페르니쿠스: Springer-Verlag, New York, 1999.수학적인 성향이 있는 비전문가를 위한 읽기 쉽고, 마지막에는 더 어려운 것을 넣을 수 있습니다.튜링 기계 모델이 들어 있습니다.Chaitin의 공헌에 대해 설명합니다.
• 어니스트 나겔과 제임스 R. 뉴먼, 고델스프루프, 뉴욕대학교 출판부, 1958년아주 어려운 주제에 대한 훌륭한 글쓰기가군요.수학적인 성향이 있는 비전문가용.Gentzen의 증명(96~97페이지)과 각주에 대해 설명합니다.부록에서는 Peano Axioms에 대해 간략하게 설명하고 독자들에게 형식 논리를 부드럽게 소개합니다.
• Daras, 니콜라스 J.;Rassias, Themistocles M.(2018년).현대 이산 수학, 암호, 정보 체계와 모델링에서 어플리케이션과 분석:.사장 스위스.아이 에스비엔 978-3319743240..장 제3절 1중단 문제에 대한 품질 설명, 상의 모순에 증거를, 그리고 Halting의 문제 도움이 되는 그래픽 표현이 들어 있다.
• Taylor Booth, Sequential Machines and Automata Theory, 뉴욕, Wiley, 1967년제9장 튜링 머신 튜링전기 엔지니어 및 기술 전문가용 어려운 책입니다.튜링 기계와 관련된 재귀, 부분 재귀, 문제 중단에 대해 설명합니다.튜링 머신 모델이 들어 있습니다.9장의 끝에 있는 참고 자료에는 대부분의 오래된 책(1952년부터 1967년까지 작가 마틴 데이비스, F. C. 헤니, H. 에르메스, S. C. 클린, M. 민스키, T. Rado 포함)과 다양한 기술 논문이 수록되어 있다.비지 비버 프로그램의 메모를 참조하십시오.
• 바쁜 비버 프로그램은 Scientific American, 1984년 8월, 1985년 3월 23페이지에 설명되어 있습니다.Booth의 참고 자료에는 Rado, T.(1962)의 Bell Systems Tech, J. 41의 계산 불가능한 함수에 대한 설명이 나와 있습니다.Booth는 또한 9장 396쪽의 3, 4, 5, 6번 문제에서 Rado의 바쁜 비버 문제를 정의합니다.
• 데이비드 볼터, 튜링의 남자: 컴퓨터 시대의 서양 문화, 노스캐롤라이나 대학 출판부, 채플 힐, 1984.일반 독자를 위해.날짜일 수 있습니다.또 다른 (매우 심플)가 있다튜링 머신 모델입니다.
• Sven Köhler, Christian Schindelhauer, Martin Ziegler, 현실 세계의 정지 문제에 대해, 컴퓨터 사이언스 volume 3623의 ISBN 3540281932 Springer 강의 노트: "정지 문제의 불변성"은 모든 경우에 대해 올바르게 대답할 수 없다는 것을 의미합니다.한편으로, "예"라는 끊임없는 대답은 무한히 정확하고, 틀린 대답 또한 무한히 자주 틀립니다.질문을 합리적으로 하기 위해 해결할 수 있는 인스턴스의 밀도를 고려합니다.이는 고려 중인 프로그래밍 시스템에 따라 크게 달라지는 것으로 나타났습니다.
• 기계 윤리에 대한 논리적 한계, 치명적인 자율 무기에 대한 결과 - 논술된 논문: 정지 문제는 도덕적인 로봇이 없다는 것을 의미합니까?

외부 링크

• 루프 스누퍼 스쿠핑 - 정지 문제의 판별 불능의 시적 증거
• 애니메이션 영화 - 정지 문제의 판별 불가능성의 증거를 설명하는 애니메이션
• 제2천년의 두 번째 가장 중요한 정리에 대한 2분간의 증명 - 단 13줄의 증명