Coq와 같은 비 튜링 완전한 언어의 실질적인 한계는 무엇입니까?

Coq와 같은 비 튜링 완전한 언어의 실질적인 한계는 무엇입니까?

---

튜링이 아닌 완전한 언어가 있고 내가 대학에서 Comp Sci를 공부하지 않았기 때문에 누군가 튜링 불완전한 언어 (예 : Coq )가 할 수없는 것을 설명 할 수 있습니까?

아니면 완전성 / 불완전 성이 실질적인 실질적인 관심 이 없는가 (즉, 실제적으로 큰 차이가 없는가)?

편집 -나는 X 또는 그와 비슷한 것으로 인해 비 튜링 완전한 언어로 해시 테이블을 만들 수 없다는 줄을 따라 대답을 찾고 있습니다 !

---

먼저, 우리가 "계산"이라고 부르는 것은 무엇이든 Turing 기계 (또는 다른 많은 동등한 모델)로 수행 할 수 있다고 말하는 Church-Turing 논문에 대해 이미 들어 보셨을 것입니다. 따라서 Turing-complete 언어는 모든 계산을 표현할 수있는 언어입니다. 반대로 튜링 불완전 언어는 표현할 수없는 계산이있는 언어입니다.

네, 그다지 유익하지 않았습니다. 예를 들어 보겠습니다. Turing 불완전한 언어로는 할 수없는 한 가지가 있습니다. Turing 머신 시뮬레이터를 작성할 수 없습니다 (그렇지 않으면 시뮬레이션 된 Turing 머신에서 모든 계산을 인코딩 할 수 있습니다).

좋아, 그것은 여전히 매우 유익하지 않았다. 진짜 질문은 튜링 불완전한 언어로 작성할 수없는 유용한 프로그램은 무엇 입니까? 글쎄요, 누군가 어딘가에서 유용한 목적으로 작성한 모든 프로그램을 포함하는 "유용한 프로그램"의 정의를 내놓은 사람은 아무도 없으며 모든 튜링 머신 계산을 포함하지는 않습니다. 따라서 모든 유용한 프로그램을 작성할 수있는 튜링 불완전한 언어를 설계하는 것은 여전히 ​​매우 장기적인 연구 목표입니다.

이제 매우 다른 종류의 튜링 불완전 언어가 몇 가지 있으며 할 수없는 부분이 다릅니다. 그러나 공통된 주제가 있습니다. 언어를 디자인하는 경우 언어가 Turing-complete가되도록하는 두 가지 주요 방법이 있습니다.

• 언어에 임의의 루프 ( while) 및 동적 메모리 할당 ( malloc) 이 있어야합니다.

• 언어가 임의의 재귀 함수를 지원해야 함

그럼에도 불구하고 일부 사람들이 프로그래밍 언어를 호출 할 수있는 비 튜링 완전 언어의 몇 가지 예를 살펴 보겠습니다.

• FORTRAN의 초기 버전에는 동적 메모리 할당이 없습니다. 계산에 필요한 메모리 양을 미리 파악하고 할당해야했습니다. 그럼에도 불구하고 FORTRAN은 한때 가장 널리 사용되는 프로그래밍 언어였습니다.

  명백한 실제 제한은 프로그램을 실행하기 전에 프로그램의 메모리 요구 사항을 예측해야한다는 것입니다. 그것은 어려울 수 있으며 입력 데이터의 크기가 미리 제한되지 않으면 불가능할 수 있습니다. 당시 입력 데이터를 제공하는 사람은 프로그램을 작성한 사람이 많았 기 때문에 그렇게 큰 문제는 아니 었습니다. 그러나 그것은 오늘날 작성된 대부분의 프로그램에서 사실이 아닙니다.

• Coq는 정리 를 증명 하기 위해 고안된 언어입니다 . 이제 정리를 증명하고 프로그램을 실행하는 것은 매우 밀접하게 관련 되어 있으므로 정리를 증명하는 것처럼 Coq로 프로그램을 작성할 수 있습니다. 직관적으로 "A는 B를 의미한다"정리의 증명은 정리 A의 증명을 인수로 취하고 정리 B의 증명을 반환하는 함수입니다.

  시스템의 목표는 정리를 증명하는 것이므로 프로그래머가 임의의 함수를 작성하도록 할 수 없습니다. 그 언어로 방금 자신을 호출하는 어리석은 재귀 함수를 작성할 수 있다고 상상해보십시오 (좋아하는 언어를 사용하는 줄 선택).

  theorem_B boom (theorem_A a) { return boom(a); }
  let rec boom (a : theorem_A) : theorem_B = boom (a)
  def boom(a): boom(a)
  (define (boom a) (boom a))
  

  그런 함수의 존재가 A가 B를 의미한다고 확신하게 할 수는 없습니다. 그렇지 않으면 진정한 정리가 아닌 모든 것을 증명할 수있을 것입니다! 따라서 Coq (및 유사한 정리 증명)는 임의의 재귀를 금지합니다. 재귀 함수를 작성할 때 항상 종료됨을 증명 해야합니다 . 그래야 정리 A의 증명에서 실행할 때마다 정리 B의 증명이 생성된다는 것을 알 수 있습니다.

  Coq의 즉각적인 실질적인 제한은 임의의 재귀 함수를 작성할 수 없다는 것입니다. 시스템은 종료되지 않는 모든 함수를 거부 할 수 있어야하므로 중지 문제 (또는보다 일반적으로 Rice의 정리 ) 의 결정 불가능 성은 거부 된 종료 함수도 있음을 보장합니다. 추가 된 실질적인 어려움은 기능이 종료되었음을 증명하기 위해 시스템을 도와야한다는 것입니다.

  A에서 B까지의 함수가 있다면 A가 B를 의미한다는 수학적 증명만큼이나 좋다는 보장을 훼손하지 않으면 서 증명 시스템을 프로그래밍 언어와 비슷하게 만들기위한 많은 연구가 진행되고 있습니다. 더 많은 것을 받아들이도록 시스템을 확장합니다. 종료 기능은 연구 주제 중 하나입니다. 다른 확장 방향에는 입력 / 출력 및 동시성과 같은 "실제"문제에 대한 대처가 포함됩니다. 또 다른 도전은 이러한 시스템을 단순한 필사자가 액세스 할 수 있도록 만드는 것입니다 (또는 단순한 필사자가 실제로 액세스 할 수 있음을 확신).

• 동기식 프로그래밍 언어 는 실시간 시스템, 즉 프로그램이 n 클럭주기 미만으로 응답해야하는 시스템을 프로그래밍하기 위해 설계된 언어입니다 . 주로 차량 제어 또는 신호와 같은 미션 크리티컬 시스템에 사용됩니다. 이러한 언어는 프로그램 실행에 걸리는 시간과 할당 할 수있는 메모리 양에 대한 강력한 보증을 제공합니다.

  물론, 이러한 강력한 보장의 대응은 메모리 소비와 실행 시간을 미리 예측할 수없는 프로그램을 작성할 수 없다는 것입니다. 특히 입력 데이터에 따라 메모리 사용량이나 실행 시간이 달라지는 프로그램은 작성할 수 없습니다.

• 프로그래밍 언어가 되려고하지도 않기 때문에 튜링 완전성에서 편안하게 멀어 질 수있는 많은 전문 언어가 있습니다. 정규식, 데이터 언어, 대부분의 마크 업 언어 등 ...

그건 그렇고, Douglas Hofstadter 는 계산에 관한 매우 흥미로운 여러 과학 서적, 특히 Gödel, Escher, Bach : an Eternal Golden Braid를 썼습니다 . 그가 튜링 불완전 성의 한계를 명시 적으로 논의했는지는 기억 나지 않지만 그의 책을 읽으면 더 많은 기술 자료를 이해하는 데 확실히 도움이 될 것입니다.

---

가장 직접적인 대답은 다음과 같습니다. Turing이 완전하지 않은 기계 / 언어는 Turing 기계를 구현 / 시뮬레이션하는 데 사용할 수 없습니다. 이는 튜링 완성도의 기본 정의에서 비롯됩니다. 튜링 기계를 구현 / 시뮬레이션 할 수 있다면 기계 / 언어는 튜링 완성입니다.

그렇다면 실제적인 의미는 무엇입니까? 글쎄요, 튜링이 완료된 것으로 보일 수있는 모든 것이 계산 가능한 모든 문제를 해결할 수 있다는 증거가 있습니다. 정의에 따르면 튜링이 완료되지 않은 것은 해결할 수없는 계산 가능한 문제가 있다는 핸디캡이 있음을 의미합니다. 이러한 문제는 시스템이 튜링을 완전하게 만드는 기능이 누락되었는지에 따라 다릅니다.

예를 들어 언어가 루핑이나 재귀를 지원하지 않거나 암시 적으로 루프가 Turing 기계가 영원히 실행되도록 프로그래밍 될 수 있기 때문에 Turing이 완료 될 수없는 경우입니다. 따라서 해당 언어는 루프가 필요한 문제를 해결할 수 없습니다.

또 다른 예는 언어가 목록이나 배열을 지원하지 않는 경우 (또는 파일 시스템을 사용하여 에뮬레이션 할 수있는 경우) Turing 머신은 메모리에 임의의 임의 액세스가 필요하기 때문에 Turing 머신을 구현할 수 없습니다. 따라서 해당 언어는 메모리에 대한 임의의 임의 액세스가 필요한 문제를 해결할 수 없습니다.

따라서 언어를 비 튜링 완전성으로 분류하는 누락 된 기능은 언어의 유용성을 실질적으로 제한하는 바로 그 기능입니다. 그래서 대답은 다릅니다. 무엇이 비 튜링 언어를 완전하게 만드는가?

---

An important class of problems that are a bad fit for languages such as Coq is those whose termination is conjectured or hard to prove. You can find plenty of examples in number theory, maybe the most famous is the Collatz conjecture

function collatz(n)
  while n > 1
    if n is odd then
      set n = 3n + 1
    else
      set n = n / 2
    endif
 endwhile

This limitation leads to have to express such problems in a less natural way in Coq.

---

You can't write a function that simulates a Turing machine. You can write a function that simulates a Turing machine for 2^128 (or 2^2^2^2^128 steps) and reports whether the Turing machine accepted, rejected, or ran for longer than the allowed number of steps.

Since "in practice" you will be long gone before your computer can simulate a Turing machine for 2^128 steps, it's fair to say that Turing incompleteness does not make much of a difference "in practice".

참고URL : https://stackoverflow.com/questions/3492188/what-are-the-practical-limitations-of-a-non-turing-complete-language-like-coq