엔스키둥슈프로블루 문제

Entscheidungsproblem

수학과 컴퓨터 과학에서 엔트쉐이둥스프로블럼(Entscheidungsproblem, 독일어로 [ [ntˈaaɪaaddspspspspspspbleble, "결정문제"로 발음함)은 1928년 데이비드 힐베르트와 빌헬름 애커만이 제기한 도전이다.[1] 문제는 문구를 입력으로 간주하고 문장이 보편적으로 유효한지, 즉 공리를 만족하는 모든 구조에서 유효한지에 따라 "예" 또는 "아니오"라고 대답하는 알고리즘을 요구한다.

완전성 정리

1차 논리학의 완전성 정리에 의해, 진술은 공리로부터 추론할 수 있는 경우에만 보편적으로 유효하므로, Entscheidungsprobroblem은 또한 주어진 진술이 논리 규칙을 이용하여 공리로부터 증명할 수 있는지를 결정하기 위한 알고리즘을 요구하는 것으로도 볼 수 있다.

1936년 알론조 교회와 앨런 튜링은 "효과적으로 계산할 수 있다"는 직관적인 개념이 튜링 기계(또는 람다 미적분학에서 표현 가능한 것)에 의해 계산 가능한 기능에 의해 포착된다고 가정할 때 엔치등스프로 문제에 대한 일반적인 해결이 불가능하다는 것을 보여주는 독립된 논문을[2] 발표했다. 이 가정은 현재 Church-Turing 논문으로 알려져 있다.

문제의 역사

엔트쉐이둥스프로 문제의 기원은 17세기에 성공적인 기계 계산 기계를 건설한 후 수학적인 진술의 진실 가치를 결정하기 위해 기호를 조작할 수 있는 기계를 만드는 꿈을 꾸었던 고트프리드 라이프니즈로 거슬러 올라간다.[3] 그는 첫걸음이 깨끗한 격식어여야 한다는 것을 깨달았고, 후속 작업의 상당 부분은 그 목표를 향해 있었다. 1928년 데이비드 힐버트와 빌헬름 애커먼은 위에서 설명한 형태로 질문을 던졌다.

힐버트는 "프로그램"을 계속하면서 1928년 국제회의에서 세 가지 질문을 던졌는데, 그 중 세 번째 질문은 "힐버트의 엔체이둥스프로 문제"[4]로 알려지게 되었다. 1929년 모세 쇤핀켈은 폴 버네이즈가 작성한 결정문제의 특수한 사례에 관한 논문 하나를 발표했다.[5]

1930년 말, 힐버트는 해결할 수 없는 문제 같은 것은 없을 것이라고 믿었다.[6]

부정적인 대답

그 질문에 대답하기 전에, "알고리즘"의 개념은 공식적으로 정의되어야 했다. 이것은 1935년 알론조 교회가 그의 λ-미적분을 바탕으로 한 "유효한 계산력"이라는 개념으로, 이듬해 알란 튜링이 튜링 기계라는 개념으로 한 것이다. 튜링은 이러한 모델들이 계산의 동등한 모델이라는 것을 즉시 인식했다.

엔치둥스프로 문제에 대한 부정적 답변은 그 후 1935-36년 알론조 교회(처치의 정리)가, 그 직후 1936년 알란 튜링(튜링의 증명)이 독자적으로 제시하였다. Church는 두 개의 주어진 λ-미적분표현을 등가인지 아닌지를 결정하는 계산 가능한 함수가 없다는 것을 증명했다. 그는 Stephen Kleene의 초기 작품에 크게 의존했다. 튜링은 주어진 튜링 머신이 정지하는지(정지 문제)를 결정하는 '일반적인 방법'의 존재에 대한 문제를 엔치등스프로 문제를 해결할 수 있는 '알고리즘'이나 '일반적인 방법'의 존재 문제로 줄였다. '알고리즘'이 튜링 기계와 동등한 것으로 이해되고, 후자의 질문에 대한 대답이 음(일반적으로)인 경우, Entscheidungsproblem에 대한 알고리즘의 존재에 대한 질문도 음(일반적으로)이어야 한다. 튜링은 1936년 논문에서 "각 컴퓨팅 머신 'it'에 대응하여 'Un(it)'이라는 공식을 만들고, 'Un(it)'이 검증 가능한지 여부를 판단하는 일반적인 방법이 있다면, 'It'가 0을 출력하는지 여부를 판단하는 일반적인 방법이 있음을 보여준다"고 밝혔다.

Church와 Turing 양쪽의 작업은 그의 불완전성 정리에 관한 Kurt Gödel의 초기 연구, 특히 논리학을 산술로 줄이기 위해 논리 공식에 숫자를 할당하는 방법(Gödel 번호 매기기)에 의해 많은 영향을 받았다.

엔트쉐이둥스프로 문제는 힐베르트의 10번째 문제와 관련이 있는데, 힐베르트는 디오판틴 방정식에 해결책이 있는지 여부를 결정하기 위한 알고리즘을 요구한다. 그러한 알고리즘의 비존재도 1970년 증명서의 마지막 부분을 가지고 유리 마티야세비치, 줄리아 로빈슨, 마틴 데이비스, 힐러리 푸트남의 저작에 의해 성립된 것으로 엔체이둥스프로 문제에 대한 부정적인 답을 내포하고 있다.

일부 1차 이론은 알고리즘적으로 해독할 수 있다; 이것의 예로는 프레스버거 산술, 실제 폐쇄 필드 및 많은 프로그래밍 언어의 정적 유형 시스템이 있다. 그러나 페이노의 공리에 표현된 자연수의 일반적 1차 이론은 알고리즘으로 결정할 수 없다.

실질적인 의사결정 절차

논리 공식의 클래스에 대한 실질적인 의사결정 절차를 갖는 것은 프로그램 검증과 회로 검증에 상당한 관심이 있다. 순수 부울 논리 공식은 대개 DPLL 알고리즘에 기초한 SAT 해결 기법을 사용하여 결정된다. 선형 현실 또는 이성적 산술에 대한 결합 공식은 심플렉스 알고리즘을 사용하여 결정할 수 있으며, 선형 정수 산술(프레즈버거 산술)의 공식은 쿠퍼의 알고리즘이나 윌리엄 푸그의 오메가 테스트를 사용하여 결정할 수 있다. 부정, 접속사 및 분리가 있는 공식은 만족도 시험의 어려움과 접속사 결정의 어려움을 결합한다. 이들은 일반적으로 SAT 해결 방법과 접속사 및 전파 기술에 대한 의사결정 절차를 결합한 시만텍 해결 기법을 사용하여 오늘날 결정된다. 실제 폐쇄장 이론으로도 알려진 실제 다항식 산술은 해독이 가능하다. 이것이 타르스키-세이덴버그 정리로서 원통형 대수분해를 이용하여 컴퓨터에서 실행되어 왔다.

참고 항목

메모들

  1. ^ 데이비드 힐베르트와 빌헬름 애커만. Grundzüge der Orgistischen Logik. 1928년 독일 베를린 스프링거 영어 번역: 데이비드 힐베르트와 빌헬름 애커만. 수학 논리의 원리. AMS Chelsea 출판사, Providence, Providence, 미국 로드아일랜드, 1950년
  2. ^ Church의 논문은 1935년 4월 19일 미국수학회에 제출되어 1936년 4월 15일에 발표되었다. 자신의 결과물을 작성하는 데 상당한 진전을 이루었던 튜링은 출판 당시 교회의 증거를 알고 실망했다(알론조 교회 논문에서 맥스 뉴먼과 처치 사이의 통신 참조). 튜링은 재빨리 논문을 완성하고 서둘러 출판했다; 그것은 1936년 5월 28일 런던수학협회 회보에 의해 접수되었고, 1936년 11월 12일에 읽혀졌고, 시리즈 2의 제42권(1936–7)에 출판되었다; 1936년 11월 30일에 발행된 제3부(230–240쪽)와 12월 23일에 발행된 제4부(241–265)에 나타났다. 1936; 튜링은 제43권(1937), 페이지 544–546에 수정을 추가했다. 1996년 소어 끝에 있는 각주를 참조하십시오.
  3. ^ 데이비스 2000: 페이지 3-20
  4. ^ 호지스 페이지 91
  5. ^ Kline, G. L.; Anovskaa, S. A. (1951), "Review of Foundations of mathematics and mathematical logic by S. A. Yanovskaya", Journal of Symbolic Logic, 16 (1): 46–48, doi:10.2307/2268665, JSTOR 2268665
  6. ^ 힐베르트 인용 호지스 페이지 92

참조

외부 링크