問題タブ [decidable]

文脈自由文法を使用して、有限言語または無限言語の解決策を考え出そうとしています。

私はこれらの文法を持っており、それが有限または無限の言語の解であるかどうかを見つけます

だから私はするだろう

だから私はここでこのような単語を生成する方法を知っていますが、それが有限言語か無限言語かをどのように見つけるのでしょうか?

私は言語 {4^(w⋅g)34^(g)|w,g∈NAT} をアルファベット {0,1} で持っています。

この言語が認識可能か、決定可能か、文脈自由か、規則的か、またはこれらのいずれでもないかを調べる必要があります。

どうすればそれを行うか、知ることができますか？

ありがとう

私はこれらのことに非常に慣れていません。これが非常に素朴な質問ではないことを願っています。

Prologで次の式を試しました：A⇒B

Bが真であるとすると、A を評価するとFALSE となります。

私の質問は、なぜ FALSE なのですか? (TRUE ではないのはなぜですか?) 現在の情報では、 Bについて何もわかりません。Prolog は、未知のものに対して FALSE を出力するという仮定に基づいて機能しますか?

これが仮定である場合、これはどのくらい一般的ですか?

もう1つ頭に浮かぶのは、入力クエリと公理の結合への割り当てを見つけることです（基本的にSAT解決）。結果の出力は TRUE であるため、A の値に関係なく、ランダムに 1 つを選択します (デフォルトではゼロですか?)。

1次論理の性質に基づき、半決定可能です。文Aが文Bを論理的に意味する場合、これは発見できますが、その逆はできません。では、真実の証拠がない場合、後者のケースは実際にはどのように扱われるのでしょうか?

PS1。Prolog がどのように機能するかについての簡単な説明も役に立つかもしれません。SAT ソルバーをブラック ボックスとして使用しますか? それとも貪欲な検索アルゴリズムですか?

マシン L(M) の文字列が決定可能かどうかを証明しようとしていますが、そのための適切な結果を見つけることができません。これに関するいくつかの例を説明するのを手伝ってくれる人はいますか。

私が試しているシナリオは、2 つの文字列があり、S1 が S2 のサブセットであり、show machine L(M) が決定可能であることです。

この型を使用して、決定可能な解析を実行できる文字列について推論しています。

たとえば、数字 [0-9] を次のように定義します。

次に、次の関数を使用できます。

このs2n関数はコンパイル時に問題なく動作するようになりましたが、それ自体はあまり役に立ちません。Every Digit (unpack s)実行時にそれを使用するには、関数を使用する前に証明を構築する必要があります。

だから私は今、この関数のようなものを書きたいと思います:

それか、メンバーシップの証明または非メンバーシップの証明のいずれかを返したいのですが、これらのいずれかを一般的な方法で行う方法が完全にはわかりません。代わりに、Maybe文字だけのバージョンを試してみました:

しかし、その後、次の統合エラーが発生します。

しかし、タイプp ですChar -> Type。この統合の失敗の原因はわかりませんが、問題は以前の質問に関連している可能性があると思います。

これは私がやろうとしていることに対する賢明なアプローチですか? 現時点では少し多すぎるように感じますが、これらの関数のより一般的なバージョンが可能になるはずです。クラスがどのように機能するかと同様の方法で、キーワードを使用して aまたはautoを与える関数を記述できるとよいでしょう。Maybe proofEither proof proofThatItIsNotDecEq

L が任意の言語の場合。言語 perms(L) は、L からの単語のすべての順列の言語です。

正誤問題: L が再帰的に列挙可能 (計算可能) である場合、perms(L) も再帰的に列挙可能です。

これは以前の決勝戦で、L が決定可能であれば perms(L) も決定可能であるという質問とともにありました。これは真実であることがわかりました。

私は間違っていると思いますが、この主張を裏付ける証拠はありません。