問題タブ [decidable]

計算理論では、ProvableとDecidableという用語は交換可能ですか？それらは同じことを意味しますか？

たとえば、決定問題（Das Entscheidungsproblem）と呼ばれる何かが証明可能かどうかという質問をよく目にします。

TMが言語を認識し、受け入れ状態または拒否状態になった場合、言語は決定可能です。開発者として これは、プログラムにバッファオーバーフローまたはデッドロックが含まれているかどうかを判断できることを意味するため、重要だと思います。また、次の問題は決定不可能です。

• プログラムが初期化されていない変数にアクセスすることはありますか？
• 2つの文脈自由文法が同じ言語を記述していますか。
• サブルーチンへのパラメーターが参照またはコピー結果によって渡される場合、違いはありますか？

決定可能性の観点から、決定可能性の重要なポイントは何と言いますか。また、決定可能性が（特に開発者にとって）重要である理由は何ですか。

注：箇条書きは回答に問題はありません。トピックは自分で調べることができます。要点を知りたいだけです。

私は関連する決定可能性/認識可能な問題に取り組んでおり、それを解決するには、チューリングマシンのエンコード/表現について明確にする必要があります。

チューリングマシンは正式には7タプルとして定義されていることを私は知っています。Uチューリングマシンと別のチューリングマシンを持っている場合、その一部（アルファベット、入力記号、受け入れ状態のセットなど） を認識Mするように設計するのは簡単ですか？UMM

M私の一部は、これらは有限集合であるため、それらを数えるのは簡単だと思いますが、無限にループする可能性なしに、定義の一部を列挙できるかどうか疑問に思います。

アーサー・デントは、地球上でまだ利用できない宇宙時代の技術を使用して、TM M1 が空のテープで開始されたときに停止するかどうかを判断するアルゴリズムを開発しました。しかしその後、彼は人生、宇宙、そしてすべての意味が42であることを発見しました.

(a) [5] 与えられた TM M2 に対して、Arthur が既に開発したプログラムを使用して、入力 42 で M2 が停止するかどうかを判断できることを証明してください。プルーフで新しい TM を作成する場合は、そのマシン スキーマを指定します。

(b) [5] Arthur のプログラムよりも高速であるが、TM M2 が入力 42 で停止するかどうかという質問に答えるプログラムがあるとします。Arthur がこのアルゴリズムを使用して、空白で開始したときに一部の TM M1 が停止するかどうかを判断する方法を説明してください。テープ。プルーフで新しい TM を作成する場合は、そのマシン スキーマを指定します。

(c) [5] 私たちはクラスで、TM M が空のテープで開始されたときに停止するかどうかを判断する問題は決定できないことを証明しました。TM M が入力 42 で停止するかどうかを判断することも決定不能であることを証明するために使用できるのは、部分 (a) または部分 (b) ですか?

私の教授がここで話していることを解読するのを手伝ってくれる人はいますか?

G の言語が nil であるような文脈自由文法 G がある場合、G は決定可能ですか?

答えがイエスであることはわかっていますが、これを証明するのに苦労しています。私が最初に考えたのは、q1 という 1 つの状態しかないということです。これは、G に相当するチューリング マシンの開始状態と受け入れ状態です。このマシンは、入力を受け入れず、受け入れに達したため、すぐに停止して受け入れます。州。これは受け入れられる答えですか、それとも私はここから離れていますか?

編集：

Joel が以下で述べたように、私が説明した言語はすべての文字列を受け入れます。これに対抗するために、私は 2 番目のマシン G' を提案します。G' には、開始状態 q1、受け入れ状態 q2、拒否状態 q3 の 3 つの状態があります。q1 は G' のアルファベットのすべてのシンボルで q3 に遷移し、q2 も同様です。q1 から q2 へのイプシロン遷移があります。したがって、G' に供給される文字列に記号が存在する場合、G' は拒否します。シンボルがない場合、唯一のオプションはイプシロン遷移を受け入れ状態にすることです。それはどのように聞こえますか？

編集：

上記の解は、言語 L(G') = {""} を受け入れることが証明されました。

これが決定可能かどうかに苦しんでいます：

A = {x は自然数の集合の要素 | x より大きいすべての y に対して、2y は 2 つの素数の和です}

チューリング マシンに供給されると、受け入れ状態に達することはなく、拒否しない限り無限にループするという事実を考えると、これは決定可能であると考える傾向があります。ただし、言語が決定可能であるためには、それを決定するためのアルゴリズムのみが存在する必要があることも知っています。必ずしもそれがどのように行われるかを知る必要はありません。これで、私の一部は決定可能だと思いますか？どちらかを証明する方法を知っている人はいますか？

リニアと呼ばれるNumのスーパークラスを作りたい

エラーが発生します：

私が理解していることから、線についての何かinstance (Num a) => Linear a whereが間違っています。（フラグを使用するとコンパイルされます-XFlexibleInstances -XUndecidableInstances:)

それらの恐ろしい旗を使わずにこれを達成する方法はありますか？（そして、上記のコードについて決定不可能なのは世界で何ですか??）

更新：線形に多項式タイプを追加しました。

多項式を追加した後、それらのフラグでさえコンパイルされず、エラーが発生します。

L = {<T> | T は {00, 01}} を認識するチューリング マシンです。

L が決定不能であることを証明します。

ここで使用する削減を理解することさえ本当に困難です。

私は無料の昼食を求めているのではなく、正しい方向へのプッシュを求めているだけです.

コンパイルするために-XUndecidableInstancesを必要とするHaskellコードをいくつか書きました。私はそれがなぜ起こるのか、違反されている特定の条件があり、したがってGHCが叫ぶことを理解しています。

しかし、タイプチェッカーが実際にハングしたり、無限ループに陥ったりするような状況に遭遇したことはありません。

非終了インスタンス定義はどのように見えますか？例を挙げていただけますか？