问题标签 [computability]

所以这里有一个语法R和一个Langauge L，我想证明从R出来L。

所以我想我会证明 L(G) ⊆ L 和 L(G) ⊇ L 是对的。

对于 L (G) ⊆ L：我通过对导数步骤数 i 的归纳表明，在每个导数步骤 u → w 之后，根据 R 的规则，w = v1v2 或 w = v1v2w 通过 | v2 | = | v1 | 和 v1 ∈ {a} ∗ 和 v2 ∈ {b} ∗。并且在归纳开始中：在 i = 0 时，它产生 w 是 ε 并且在 i = 1 时 w 是 {ε,abS}。

到目前为止是对的吗？

我目前正在阅读 John C. Mitchell 的Foundations for Programming Languages。练习 2.2.3 实质上要求读者证明（自然数）幂函数不能通过小语言的表达式隐式定义。该语言由自然数和所述数字的加法（以及布尔值、自然数相等谓词和三元条件）组成。没有循环、递归结构或定点组合器。这是精确的语法：

同样，目的是表明幂函数 n^m 不能通过该语言中的表达式隐式定义。

直觉上，我愿意接受这一点。如果我们将求幂视为重复乘法，似乎我们“就是不能”用这种语言表达它。但是如何正式证明这一点呢？更广泛地说，你如何证明一种语言的表达不能用另一种语言表达？

为了使用可数集，我必须定义 N（自然数）的所有有限子集的编码函数。我怎样才能做到这一点？我从寻找所有自然数的函数开始：f(n)=1+2+...+(n-1)+n。但是我怎样才能为所有可能的 f 子集表达一个编码函数呢？我怎么能说 f 包含所有有限的自然数呢？我不能说 n=infinity-1 因为 infinity-1 仍然是无穷大。有没有一种正式的方式构成所有有限的自然数？

如何用 lambda 项表示以下函数？

如果 n != 0，则 f(n) = T。如果 n = 0，则为 F。

n 代表教堂数字。

我知道 0 := λf.λx.x 其中 λx.x 是恒等函数，所有其他自然数可以用 n := λf.λx.f (f ... (fx)) 表示，其中包含 fn 倍比 0 项。例如 3 := λf.λx.f (f (fx))。

但是我怎样才能为上面的函数推导出一个有效的 λ 项呢？我想我也需要获得 T/F。因此我可以用 λf.(λxy.fxy) 来表示数字 n，对吧？但是F和T呢？以下是上述函数的正确 λ 项吗？λf.(λxy.fxy(yFT)) 其中 T=λxy.x 且 F=λxy.y？

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

所谓的通用语言 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 中给出的，采用了非常相似的推理。

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

我有一个问题。假设我有一种语言，它只分配给变量、一些操作，但只有 do-while 作为流控制结构。我怎样才能模拟一段时间的结构？

让我们假设这个简单的语法更容易沟通，但我接受任何其他可读的语法：

有了这个语法，我们就可以有很多程序了。我要问的是，¿是否可以模拟 while 循环行为，或受此限制的 if() 行为？

如果不是，我如何证明这种语言不如仅使用 while() 的语言。（或一种方法）

我已经证明这一点的主要问题来自“无迭代”流程，在一个while循环中，你可以有一个没有迭代的代码，使用“while语言”我可以跳过代码，但我不是能够找到任何解决方案，既不是通过重新排列句子或尝试其他方式来做到这一点。

这是一个可计算性问题。这对我来说太复杂了，我不知道从哪里开始。现在，我想也许我应该尝试证明，既然 N 是递归的，那么 A 是创造性的，如果 $A\otimes N$ 是创造性的，那么我可以证明 $A\otimes N$ 一定不是创造性的，但是即使这个证明让我很困惑。此外，我不确定递归可枚举（重新）完整集是否是创造性集这一事实是否有帮助。

任何想法将不胜感激！

顺便说一句，这里 $A\otimes B$ 的意思是 {$(a,b)| a\in A$ 和 $b\in B $}。

几天前我有一个测试，并不能通过它。

有一个问题我没有正确回答，也没有看懂：

会有一个项目列表。假设我们有两个玩家（第一个和第二个）。

会有项目意义的价值函数：

• 该项目的价值不是负数（至少 - 零）。
• 值不一定是整数。

项目组的值也定义为。

让我们看看两个玩家的彩信问题。我们的目标是在两个玩家之间划分所有物品（即，将他们分成两个外来的组，其单位是所有物品）。

我们将计算所有可能的分区 1,2,3 ... 等等。给定所有可能的划分中的第 i 个划分，我们用的较小子群的值来表示。这意味着：。我们将设置一个最小-最大值（最大最小尺寸）为。

例如：有 4 个项目。它们的价值：. 可能的划分是：

• , {2,3,4,5} - 小子组的值为 0。
• {2} , {3,4,5} - 小子组的值为 2。
• {3} , {2,4,5} - 小子组的值为 3。
• {4} , {2,3,5} - 小子组的值为 4。
• {5} , {2,3,4} - 小子组的值为 5。
• {2,3} , {4,5} - 小子组的值为 5。
• {2,4} , {3,5} - 小子组的值为 6。
• {2,5} , {3,4} - 小子组的值为 7。

子组之间的排列并不重要，所以这些都是可能的划分。最大最小值为 7，并从除法 {2,5} , {3,4} 中获得。

在决策版本 MMS(E, v, z) 中，给定项目、价值函数和非负数 z，我们被问到 - 最大最小值是否等于 z？

问题1：确定该语言属于哪个等价部门：

1. 
2. 
3. 
4. 不知道有没有

问题 2：谁将成为见证人或算法？

1. 有一个多项式算法在所有玩家之间贪婪地划分项目
2. 可以构造非归属验证算法。我们的见证将被分成两个小组。验证算法将检查是否. 如果是这样，则表明给我们的 -z 不是最小值-最大值，因为存在最小值大于 -z 的除法。
3. 假设我们的见证是分成两个子组的。如果z小于最大最小值，我们可以找出来。但是在 z 大于最大最小值的情况下，作为除法的见证对我们没有帮助。也就是说，在这个见证中，我们只能根据需要对部分输入进行反驳，而不是对所有输入进行反驳。

我不明白这两个问题。我无法在考试中回答他们。

哈林问题的这个说明是否正确？

如果是这样，为什么这么多描述涉及一个带有两个参数的函数，其中一个是程序，另一个是与程序输入相同的程序？

例如：

假设我们有一个函数 Halts(P, W)，如果程序 P 在输入 W 上停止，它就会停止。然后我们编写这个完全有效的 Python 函数：

现在，当我们调用 K(K) 时会发生什么？如果 Halts(K,K) 为 True，则 K(K) 挂起（永远运行） 如果 Halts(K,K) 为 False，则 K(K) 停止 所以无论哪种方式，Halts(K,K) 都是错误的。因此，Halts 函数不存在！

我目前在 coq 的一个项目中工作，我需要使用nat -> nat. 所以基本上我会有一个定义，它接受一个list (nat -> nat)和一个命题f : nat -> nat作为参数，目标是检索f给定列表中的索引。

我所做的是我实现了一个通过列表并将每个元素f与相等性进行比较的固定点=。但是我发现这是不正确的，并且此类类型的相等性是无法确定的。

有谁知道解决这个问题的替代方法？或者更简单的方法来检索f列表中的索引？