问题标签 [decidable]

首先是上面的问题是否正确？

我认为可判定性是特定问题的属性，例如 1. 给定字符串是否属于特定语言 2. TM 是否会在给定输入上达到特定状态，而不是 TM（或任何其他机器）本身。

如果上述问题是正确的，那么我认为它是不可判定的。

它可能会停留在特定状态并且可能无法达到目标状态。它还可以修改输入并移动到以前的状态，所以我们也不知道它是否会达到目标状态

有什么方法可以证明或反驳它？

我有一个来自理论计算机科学领域的问题。

所谓的通用语言 L_u 是由对 (M, w) 组成的，使得 w \in L(M)。语言 L_ne 由具有非空语言的机器 M（实际上是它们的描述，但我们在这里不要太拘谨）组成。我们都知道 L_u 和 L_ne 都是非递归的，但仍然是 RE（递归可枚举）。另一方面，L_u 的补码（我们称它为 L_nu）甚至在 RE 中也没有，因为如果是，L_u 和 L_nu 都必须是递归的。

如果我们能够将 L_nu 简化为 L_ne，我们将证明 L_ne 也是非 RE。这意味着这种减少应该是不可能的。但是，我不知道为什么会这样。

首先，为了将语言 L 简化为 L'，我们必须构造一个可计算函数 f，它将 L 的每个可能的正实例映射到 L' 的某个正实例，并将 L 的每个可能的负实例映射到 L' 的某个负实例。仅此而已，不是吗？

其次，我认为我们可以有把握地假设通用图灵机 (UTM) 有两个最终状态，一个是状态和一个否状态。当然，如果 w \not\in L(M) 对于给定的输入 (M, w)，UTM 将永远不会到达 NO 状态，但我们仍然可以假设如果 UTM 停止，它将在 YES 状态或 NO 状态下这样做。这也是正确的，不是吗？

现在让我们尝试将 L_nu 简化为 L_ne，如下所示：给定一对 (M, w)，构建一个机器 M'，使用 UTM 的逻辑在 w 上运行 M，如果 UTM 说是，则说否，反之亦然。显然，L_nu 的正实例（w \not\in L(M)）映射到 L_ne 的正实例（L(M') 在这种情况下是非空的，因为 M' 总是说是），而 L_nu 的负实例 ( w \in L(M)) 被转换为 L_ne 的负实例（L(M') 是空的，因为 M' 总是说 NO）。虽然机器 M' 显然对于至少一些正输入永远运行（因为至少有一对 (M, w) 与 w \not\in M 使得 UTM 永远运行），减少本身是可计算的：M' 的代码包括 UTM 的代码（这绝对可以完成）和一个简单的逻辑，用于检查内置 UTM（如果应用于 (M, w)）是否已到达 YES 状态或到 NO 状态。就是这样。

因此，我刚刚“证明”了 L_ne 是非 RE。但是，由于情况并非如此，我一定是在某个地方出错了。这真的让我感到困惑，因为从 L_u 到 L_ne 的标准简化，例如，Hopcroft-Ullman-Motwani 中给出的，采用了非常相似的推理。

如果有人能帮我解开这个谜语，我将不胜感激！

给定两个列表 xs 和 ys，我想获得 Dec(xs ≡ ys) 的值。有谁知道包含这样一个运算符的标准库模块的名称？

我遇到了一个声明，假设 TM 是否会覆盖它自己的任何输入是无法确定的。

什么是直觉以及对此的实际证明？

如果语言L由 TM决定，我们就说它是递归的。

如果L被TM识别，则它是递归可枚举(re) 的。

假设，枚举器( en-r ) 是一个确定性图灵机，其打印机从空白磁带开始，可以打印字符串 s1, s2, s3, s4... sn... 如果语言是无限的，则永远继续。

程序需要生成正在打印的字符串，所以这是一个图灵机，它在磁带上的某个地方生成语言中的所有字符串。我也可以在磁带上存储其他东西。

en-r 的语言是它打印的所有字符串的集合。En-r 是生成器机器，而不是识别器机器。

对于枚举器 EN，我们说 L(EN) = {s| EN 打印 s}。

关于这种情况，我有 3 个问题：

1. 假设 L 是一个重集，那么我们如何使用识别器为 L 创建一个枚举器？

2. 如果 L 是一种语言，并且有一个枚举器按升序枚举 L，那么为什么 L 是递归的？

3. 为什么如果 L 是递归的，那么有一个 en-r 以递增的顺序枚举它？

谢谢

试图自学计算理论，偶然发现了这个问题：

假设我们有两个集合：

1. {T | T 是图灵机，L(T) 至少包含 1001 个字符串}
2. {T | T 是图灵机，L(T) 最多包含 1001 个字符串}

其中一个是可识别的，另一个则不是。

哪个是哪个，为什么？

直觉上，我认为具有“至少 1001 个字符串”的那个是无法识别的，因为它没有字符串数量的上限，所以这个数字可能是无限的，但同样一些无限的语言应该是可识别的。

我对这个问题很困惑。表明一组可识别而另一组不可识别的正确直觉和正式方法是什么？

我正在通过 Sipser 书中的练习，这让我很难过：

如果 CFG G 中的变量 A 是必要的（即，它出现在属于 G 的某个字符串 w 的每个推导中。

NECESSARY_cfg = {<G,A>|A 是 G 中的必要变量}

我们如何证明 NECESSARYcfg 是一个。图灵可识别 B. 无法确定？

问题截图

我很困惑，所以直觉和正式的答案都将不胜感激。

我们知道问题是“<em>这个图灵机在那个输入上是否至少采取了这个有限数量的步骤？” 是可判定的，因为它总是回答是或否，如果机器达到给定的步数，它会说是，如果在此之前停止，它会说否。

现在这是我的疑问：如果它在达到那么多步骤之前就停止了——即输入要么（1）被接受，要么（2）被拒绝，或者（3）如果它没有停止而是进入无限循环——那么，当我们在情况（3）中时，我们如何确定它总是在那个循环中？我的意思是，如果它不是永远运行，而是在某个时间点退出循环，那么它可能会超过所要求的步骤数，现在可以做出决定，这在以前是不可能的。如果是这样，那么当我们知道被困在一个循环中我们将无法对结果发表任何意见时，我们怎么能得出结论是可以判定的呢？

在 Coq 标准库中，“小于”关系对于自然数 ( lt_dec) 和整数 ( Z_lt_dec) 是可判定的。但是，当我搜索 ( Search ({ _ _ _ } + {~ _ _ _ })) 时，我找不到有理数的Q_le_decor Qle_dec，只能Qeq_dec找到可判定的相等性。

这是因为“小于”关系对于 Coq 中的有理数是不可判定的吗？或者它是可决定的，但决策过程没有在标准库中实现？

在 Z3 (Python) 中，我解决了以下问题：

请注意，编码没有意义，只是播放。

关键是结果完全出乎我的意料，因为它返回了一个结果！这很令人惊讶，因为我一直在研究一阶理论，据我所知，LIA 是可判定的，而 NIA 不是（理性也一样）。顺便说一句，结果是[]：即有效。

于是我在这边搜索了一下这个问题，发现（How do dos Z3 handle non-linear integer algorithms?），里面是Leonardo de Moura自己回答的：如果一个公式有解，我们总能通过蛮力找到力量。也就是说，我们不断枚举所有可能的赋值，并测试它们是否满足公式。这与尝试通过运行程序并检查它是否在给定数量的步骤后终止来解决停机问题没有什么不同。

好的，所以我知道 NIA 是半可判定的。这样对吗？然而...

在（https://hal.archives-ouvertes.fr/hal-00924646/document）中陈述了以下内容：哥德尔表明（NIA）是一个无法确定的问题。

此外，在（量词消除 - 更多问题）中，同样指出：NIA 不承认量词消除。此外，NIA 的决策问题是不可判定的。

那么，NIA 是不可判定的还是半可判定的？显然，我看到可以有一些解决方案。那么哥德尔在不可判定的意义上是否意味着不可判定（但对半可判定性只字未提）？

是否存在完全无法确定的 LIA 片段？例如，在 NRA 中，在（Z3 支持非线性算术）中声明只有非线性多项式是可判定的（对于 Z3）。

谁能提供一些澄清？