问题标签 [decidable]

令 L(G) 是由上下文无关文法 G 生成的语言。以下决策问题是可判定的吗？
L(G) 是否是确定性上下文无关语言？

我从这个链接中理解了为什么上述问题无法确定，但我有一个疑问。
我们知道 CFL 和 PDA 是等价的（参考），即对于每个 CFL G，都有一个 PDA M 使得 L(G) = L(M)，反之亦然。
如果 DPDA 可以接受上下文无关语言，则它是确定性的。
确定性 PDA 是一种基于当前输入的任何状态至多有一次可能的转换。

既然我们可以为每个 CFL 创建一个 PDA 并区分 PDA 是否是确定性的，我们是否可以说 L(G) 是否是确定性上下文无关语言的问题是可判定的？还是我错过了什么？

考虑语言

考虑语言 Aabb = {< M > | M 是 TM，M 接受 abb} a) Aabb 代表的计算问题是什么？b) 证明 Aabb 是不可判定的。

我试图证明这一点，但不知道该怎么做。

我需要证明语言L(EVEN) = { M : |L(M)| is even }是不可判定的。

换句话说，语言L(EVEN)是所有接受某种偶数基数语言的图灵机的集合。

这里，M是某个图灵机的编码，如果存在L(EVEN).

我已经使用 Turing Reductions 完成了与此类似的其他问题，可以在此处看到一个示例：

我的问题是我无法想出一些以前证明的不可判定的语言来展示有用L <= L(EVEN)。

到目前为止，我们在课堂上涵盖的不确定语言如下：

我也可以使用这些语言的补语，因为可判定性在补语下是封闭的。我如何使用这些不可判定的语言之一来证明 L(EVEN) 也是不可判定的，使用与我包含的示例问题类似的设置？

我知道在组合 SWRL 和 OWL2 时推理通常不起作用，因为组合是不可判定的。然而，当仅使用某些事物/规则时是可判定的。因此，假设我只想使用SWRL 数学内置函数，是否给出了可分性？

我试图找到 L={⟨M⟩ | 的前缀 M 是 TM，它接受其字母表上的每个回文 }，但我不知道该怎么做，因为它涉及到一个图灵机。有没有人有任何想法？谢谢！

我在使用字符串可判定性时遇到问题。首先，我很困惑为什么在 Agda 中处理可判定性如此困难，而在 Coq 中它看起来像黄油一样光滑。当我试图证明这个关于字符串的简单定理时，Agda 展开了这个混乱的定义，除非你确切地知道你要做什么，否则几乎不可能使用它。如何通过保持定义完整的模式匹配来处理字符串可判定性？

我正在使用 Stump 的保持功能而不是 Agda 的检查。

这是 Agda 的输出：

如果我现在应用重写，目标会被简化，但我们的假设列表仍然一团糟。当我尝试按 ctrl-a 时，我收到以下错误，尽管目标似乎无法推断：

尽管如此，我还是能够继续进行，就好像 snd 术语明显更清晰，然后只需应用基本规则即可得出最终证明。

最后一行是完整的证明。任何的意见都将会有帮助！

所以，我很难弄清楚图灵机不会停止的字符串到底是什么意思。我在某处读到图灵机相当于具有 2 个堆栈的确定性自动机。但是，具有 2 个堆栈的确定性自动机将如何接受一个不会停止的字符串，而对于任何有限的字符串，它决定停止......我错过了什么吗？

已知存在可判定问题、半可判定问题和不可判定问题。TM（图灵机）接受的语言是一个 re set（递归可枚举），并且在某些情况下也是一个递归集。re（但不是递归）集合的一个例子是接受某个（固定）字符串“x”的 TM 集合。解释是这样的：“这个问题是半可判定的（即集合是 re），因为如果某个 TM_i（i 是它在哥德尔枚举中的索引）属于集合，那么通过算法（过程， TM, ecc.) 列出所有接受“x”的 TM，并继续这样做，在某个点我将能够找到 TM_i。但是，如果 TM_i 不属于该集合，那么我无法得出任何结论：列出所有接受“x”的 TM 的算法将永远持续下去。

现在我试着从不同的角度思考同样的问题。假设我有一个随机图灵机 TM_j，我想确定它是否属于上述集合。我可以将字符串“x”作为输入给 TM_j，如果它在“接受”状态（最终状态）停止，那么我知道 TM_j 接受“x”，因此是集合的一部分。另一方面，如果 TM_j 不接受“x”，它可能会停止在某个非最终状态（因此我知道 TM_j 拒绝“x”），或者它可能会永远循环下去。在第二种情况下，我不能通过观察两个相同的配置来列出 TM 在执行期间的所有配置并得出结论它永远循环（因此拒绝“x”）吗？如果“c1, c2, c3, c4, . . . , c21, c3, . . 。” 是 TM_j 的配置列表，我观察到 c3 是重复的，并且由于机器是确定性的，c3 后面会跟着 c4，c4 依次给出 c5，依此类推，直到 c21，然后又是 c3。. . 因此，我可以得出结论，TM_j 循环，因此“x”不能被它接受，因为它永远不会达到最终（接受）状态。然而，这意味着给定一个通用的 TM，我可以确定它是否属于该集合，因此该集合是递归的而不是递归可枚举的！

有人可以帮助我了解我的错误在哪里吗？

我试图定义一个简单的谓词来确定一个公式是否是一个给定形式的子公式，而不是一个简单的归纳定义的语法。我遇到了一些可能很简单的问题。

(i) 我宁愿使用具有给定类型 A 的参数化模块。在 A 具有可判定相等性的意义上，如何导入 A 是一个集合的信息？如果无法做到这一点，有什么解决方法？这就是我使用 Nat 的原因。

(ii)t1 ≡ (t2 // t3)谓词（并且定义类似）isSubFormula是处理相等子公式的正确方法吗？如果没有，还有什么方法可以轻松做到这一点？我也考虑过编写一个谓词equalFmla，然后用它制作一个全局子公式谓词，isSubFormula ⊎ equalFmla但我不确定这是否如此干净。

(iii) 当我在第一行内部进行模式匹配时，为什么最后三行会突出显示蓝色？我怎样才能解决这个问题

(iv) 为什么{!Data.Nat._≟_ n1 n2 !}下面的细化不行？

我试图理解为什么这个 Etm 不可判定性的“证明”是错误的。

ALLtm={ < M >|M是一个TM，L(M)=∑*}

ETM={< M >|M是一个TM，L(M)=∅}

我们知道 ALLTM 是不可判定的，假设 ETM 是可判定的（T 是决定 ETM 的 TM）并得到一个矛盾。

为什么这种减少并不能证明 Etm 是不可判定的？

（如果 w∈L(M) M1 拒绝它，那么如果 L(M)=∑*，L(M1)=∅。

如果 w∉L(M)（M 不在 w 上停止或拒绝）M1 接受 w，所以如果 L(M)≠∑*，L(M1)≠∅)。