問題タブ [decidable]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
turing-machines - 2 つのスタックを持つ PDA は RE 言語を受け入れることができますか?
そのため、チューリング マシンが停止しない文字列が正確に何を意味するのかを理解するのに少し苦労しました。チューリング マシンは 2 つのスタックを持つ決定論的オートマトンに相当するとどこかで読みました。しかし、2つのスタックを持つ決定論的オートマトンは、有限の文字列が停止すると判断されたときに、停止しない文字列をどのように受け入れるのでしょうか...何か不足していますか??
types - Agdaで帰納的に定義された型の部分式を定義する方法は?
式が単純な帰納的に定義された構文上の特定の形式の部分式であるかどうかを判断する単純な述語を定義しようとしています。おそらく単純な問題がいくつか発生しています。
(i) 与えられた型 A を持つパラメータ化されたモジュールを使用したい. A が決定可能な等値を持つという意味で、A がセットであるという情報をどのようにインポートできますか? これができない場合、いくつかの回避策はありますか? これが私が代わりにナットを持っている理由です。
(ii) t1 ≡ (t2 // t3)(および同様に定義された) 述語isSubFormulaは、等しい部分式を処理する適切な方法ですか? そうでない場合、他にどのように簡単にこれを行うことができますか? equalFmlaまた、 for の述語を作成してから、 with でグローバルな部分式の述語を作成することも検討しましisSubFormula ⊎ equalFmlaたが、これがそれほどきれいかどうかはわかりません。
(iii) 最初の行の内部でパターン マッチを行うと、最後の 3 行が青色で強調表示されるのはなぜですか? どうすればこれを修正できますか
(iv){!Data.Nat._≟_ n1 n2 !}以下の絞り込みを行わないのはなぜですか?