問題タブ [decidable]

私は集合を関係として符号化し、集合に対する操作を普遍的に定量化された含意として符号化しています。単項述語 p (例: v<4, v>4, ..) を満たす要素を選択することによって新しいセットを生成するセットに対する選択演算子があります。この演算子のおかげで、数式に単純な算術述語が含まれています。このような式の Z3 エンコーディングの例を以下に示します。

予想どおり、Z3 は上記の式に対して UNSAT を返します。しかし、私の質問は -

1. 数式を前置正規形で記述できるとすれば、それはまだ EPR クラスですか?
2. そのような式は決定可能ですか？z3 はそのような式の決定手順ですか? 式が決定可能になるように述語を制約するにはどうすればよいですか?

更新 - 前述の式のセットは、リレーショナル代数の結合クエリとして表現できますが、不等式があります。

私は、すべての正規言語が決定可能であることを証明しようとしています。

したがって、決定論的有限オートマトン (DFA) からチューリング決定可能マシンに移行できることを証明しようとしているのです。

そのため、元の自動化 (DFA) をシミュレートするチューリング マシンを構築する方法がわかりません。

状態 (自動化とチューリング マシン) はもちろん似ていますが、続行する方法がわかりません..

前もって感謝します。しらん

Total問題が再帰的でない (決定可能)ことを証明する助けが必要です。

Halting問題の対角化証明は知っていますが、 Total問題についても同じ種類の証明が必要です。参照用にHalting Problem Proof を投稿しています。

問題の証明の停止

停止問題を決定できると仮定します。次に、次のようないくつかの合計関数 Halt が存在します。

ここでは、すべてのプログラムに番号を付けており、[x] はこの順序で x 番目のプログラムを指します。入力を one-one 関数を介して 2 つの数値のペアを表す単一の数値として扱うことにより、Halt を ℵ から ℵ へのマッピングと見なすことができます。

Halt が存在する場合、Disgree も存在します。

Disagree は ℵ から ℵ へのプログラムであるため、Disagree は Halt によって推論できます。d を Disagree = Φd とします。

Disagree(d) が定義されている ⇔ Halt(d,d) = 0 ⇔ Φd (d) が定義されていない ⇔ Disagree(d) が定義されていない

しかし、これは、不一致がそれ自体の存在に矛盾することを意味します。元の仮定を除いて、私たちが取ったすべてのステップは建設的だったので、元の仮定が間違っていたと推測しなければなりません. したがって、停止問題は解決できません。

私のクラスでは、次の言語が有限であるかどうかについて質問があります

{w : w は {a ^m b ⁿ :m+n≤k}} の正規表現で、k は特定の自然数です。

言語には多くても単語が存在する可能性があるため、有限だと思います(K+1)*k/2が、参照の答えは w は無限です

誰でも説明できますか

ps: 特定の正規言語に対して正規表現は 1 つしかありませんか?

Math exchange から次の説明を見つけました

その言語の文字列のみを停止して受け入れるチューリング マシンが存在する場合、その言語は認識可能であり、その言語にない文字列の場合、TM は拒否するか、まったく停止しません。注: チューリング マシンが言語に含まれていない文字列に対して停止する必要はありません。

その言語に含まれる文字列を受け入れ、その言語に含まれない文字列を拒否するチューリング マシンが存在する場合、その言語は決定可能です。」

2つの違いがよくわかりません。ある言語の文字列のみを受け入れるチューリング マシンと、ある言語の文字列を受け入れるチューリング マシンの違いは何ですか? チューリングマシンは何でも受け入れることができるということですか？

受け入れ状態がマークされていないときに Turing Machine T, ACCEPTS がマークされ、受け入れ状態がマークされているときに拒否する理由がわかりません。

E(dfa) = {| A は DFA であり、L(A) = 空集合 (記号を持たない)}

E(dfa) は決定可能な言語です。

証明: DFA は、DFA の矢印に沿って移動することによって、開始状態から受け入れ状態に到達する場合、何らかの文字列を受け入れます。この条件をテストするために、例 3.23 で使用したものと同様のマーキング アルゴリズムを使用する >TM T を設計できます。

T= "入力時、ここで A は DFA です: 1. A の開始状態をマークします。 2. 新しい状態がマークされなくなるまで繰り返します: 3. 既にマークされている状態から移行する状態をマークします。 . 4. 承認状態がマークされていない場合は承認し、それ以外の場合は拒否します。

これは私には逆に思えます。誰でもこれを説明できますか？

ありがとうございました。

私は Agda を初めて使用し、Decidable関数とDec型を理解するために助けが必要です。

私は一次論理述語を定義しようとしていますが、ある種のブール値を証明してエンコードしたいと考えています。これを行う方法は Dec タイプを使用することです..

今、私が知る限り、これを行うには、すべての論理演算子をセット型ではなく決定可能な型に再定義する必要があります。そうするために、私はそれを新しい型に埋め込んだのです。これは、and 演算子に対して行った方法です。

それはそれを行う方法ですか、それとも別の方法がありますか？

次に、この演算子を使用して Nat 値の関係を定義したいので、次のようにしました。

しかし、これは型エラーを与えます..

論理ステートメントを証明するためにそれを使用するチュートリアルまたは例に誰かが私Decを案内してくれれば幸いです..

C++ が決定可能でないことはわかっています。しかし、それは再帰的に列挙可能ですか?

有効な C++ プログラムのセットを、現在の C++ 標準の下で適切に定義されたプログラムと定義しましょう。

有効な C++ プログラムを常に有限時間で識別できるコンパイラを構築することは可能ですか?

それとも再帰的に列挙可能ですか？

有限時間内に無効なC++ プログラムを常に識別できるコンパイラを構築することは可能ですか?

それともどちらでもない？