チューリング完全でない言語が世の中にあり、私が大学でComp Sciを勉強していなかったとすると、チューリング不完全言語(Coqなど)ではできないことを誰かが説明できますか?
それとも、実際の利害関係がない(つまり、実際にはあまり違いがない)完全性/不完全性ですか?
編集-私はあなたの線に沿って答えを探していますX、またはそのようなもののために非チューリング完全言語でハッシュテーブルを構築することはできません!
チューリング完全でない言語が世の中にあり、私が大学でComp Sciを勉強していなかったとすると、チューリング不完全言語(Coqなど)ではできないことを誰かが説明できますか?
それとも、実際の利害関係がない(つまり、実際にはあまり違いがない)完全性/不完全性ですか?
編集-私はあなたの線に沿って答えを探していますX、またはそのようなもののために非チューリング完全言語でハッシュテーブルを構築することはできません!
まず、チャーチチューリングの論文について聞いたことがあると思います。この論文では、「計算」と呼ばれるものはすべて、チューリングマシン(または他の多くの同等モデルのいずれか)で実行できるものであると述べています。したがって、チューリング完全言語は、任意の計算を表現できる言語です。逆に、チューリング不完全言語は、表現できない計算が存在する言語です。
わかりました、それはあまり有益ではありませんでした。例を挙げましょう。チューリングの不完全な言語ではできないことが1つあります。それは、チューリングマシンのシミュレーターを作成できないことです(そうしないと、シミュレートされたチューリングマシンで計算をエンコードできます)。
わかりました、それはまだあまり有益ではありませんでした。本当の問題は、チューリングの不完全な言語で書くことができない有用なプログラムは何かということです。さて、誰かが有用な目的のために書いたすべてのプログラムを含み、すべてのチューリングマシンの計算を含まない「有用なプログラム」の定義を思いついた人は誰もいません。したがって、すべての有用なプログラムを記述できるチューリング不完全言語を設計することは、依然として非常に長期的な研究目標です。
現在、いくつかの非常に異なる種類のTuring-不完全な言語があり、それらは実行できないことで異なります。ただし、共通のテーマがあります。言語を設計している場合、その言語がチューリング完全であることを確認するための2つの主要な方法があります。
言語に任意のループ(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の直接の実際的な制限は、任意の再帰関数を記述できないことです。システムはすべての非終了関数を拒否できる必要があるため、停止問題(またはより一般的にはライスの定理)の決定不能性により、拒否される終了関数も確実に存在します。追加の実際的な難しさは、関数が終了することを証明するためにシステムを支援しなければならないことです。
AからBまでの関数がある場合、AがBを意味する数学的証明と同じくらい良いという保証を損なうことなく、証明システムをよりプログラミング言語のようにすることについて、多くの継続的な研究があります。機能の終了は、研究トピックの1つです。他の拡張の方向性には、入出力や並行性などの「現実の」懸念への対処が含まれます。もう1つの課題は、これらのシステムを単なる人間がアクセスできるようにすることです(または、実際にアクセスできることを単なる人間に納得させることもできます)。
同期プログラミング言語は、リアルタイムシステム、つまり、プログラムがnクロックサイクル未満で応答する必要があるシステムをプログラミングするために設計された言語です。これらは主に、車両制御や信号などのミッションクリティカルなシステムに使用されます。これらの言語は、プログラムの実行にかかる時間と、プログラムが割り当てる可能性のあるメモリの量を強力に保証します。
もちろん、このような強力な保証に対応するのは、メモリ消費量と実行時間を事前に予測できないプログラムを作成できないことです。特に、メモリ消費量や実行時間が入力データに依存するプログラムを作成することはできません。
プログラミング言語になろうとさえしない特殊な言語がたくさんあるので、チューリング完全性から遠く離れて快適にとどまることができます:正規表現、データ言語、ほとんどのマークアップ言語、...
ちなみに、ダグラス・ホフスタッターは、計算に関する非常に興味深い人気の科学書をいくつか書いています。特に、ゲーデル、エッシャー、バッハ:永遠の黄金の編組です。彼がチューリング完全性の限界について明確に論じているかどうかは覚えていませんが、彼の本を読むことは、より技術的な資料を理解するのに間違いなく役立ちます。
最も直接的な答えは次のとおりです。チューリング完全ではないマシン/言語を使用して、チューリングマシンを実装/シミュレーションすることはできません。これは、チューリング完全性の基本的な定義に由来します。チューリングマシンを実装/シミュレートできる場合、マシン/言語はチューリング完全です。
それで、実際的な意味は何ですか?まあ、完全にチューリングしていることを示すことができるものはすべて、計算可能なすべての問題を解決できるという証拠があります。これは、定義上、完全にチューリングされていないものには、解決できない計算可能な問題があるというハンディキャップがあることを意味します。これらの問題が何であるかは、システムを非チューリング完全にするために欠落している機能によって異なります。
たとえば、言語がループや再帰をサポートしていない場合、または暗黙的にループをチューリング完全にすることはできません。これは、チューリングマシンを永久に実行するようにプログラムできるためです。その結果、その言語はループを必要とする問題を解決できません。
別の例は、言語がリストまたは配列をサポートしていない場合(または、たとえばファイルシステムを使用してそれらをエミュレートできる場合)、チューリングマシンはメモリへの任意のランダムアクセスを必要とするため、チューリングマシンを実装できません。その結果、その言語は、メモリへの任意のランダムアクセスを必要とする問題を解決できません。
したがって、言語を非チューリング完全であると分類する欠落している機能は、言語の有用性を実際に制限するものそのものです。つまり、答えは次のとおりです。言語が非チューリング完全になる理由は何ですか。
Coqなどの言語に適さない重要なクラスの問題は、終了が推測されているか、証明するのが難しい問題です。数論にはたくさんの例がありますが、おそらく最も有名なのはコラッツの予想です
function collatz(n)
while n > 1
if n is odd then
set n = 3n + 1
else
set n = n / 2
endif
endwhile
この制限により、Coqではそのような問題をあまり自然ではない方法で表現する必要があります。
チューリングマシンをシミュレートする関数を作成することはできません。チューリングマシンをシミュレートする関数2^128
(または2^2^2^2^128
ステップ)を記述して、チューリングマシンが受け入れられたか、拒否されたか、または許可されたステップ数より長く実行されたかを報告できます。
「実際には」、コンピューターがチューリングマシンのステップをシミュレートできるようになるまでには長い時間がかかるため2^128
、チューリングの不完全性は「実際には」大きな違いをもたらさないと言っても過言ではありません。