问题标签 [decidable]

我将集合编码为关系，并将集合上的操作编码为普遍量化的含义。我有一个集合上的选择运算符，它通过选择满足一元谓词 p 的元素（例如：v<4、v>4、..）来生成新集合。由于这个运算符，我的公式中有简单的算术谓词。下面给出了这种公式的示例 Z3 编码 -

正如预期的那样，Z3 为上述公式返回 UNSAT。但是，我的问题是——

1. 鉴于我可以用 prenex 范式编写我的公式，它还在 EPR 类中吗？
2. 这样的公式是可判定的吗？z3 是此类公式的决策程序吗？我应该如何约束我的谓词以使公式是可判定的？

更新 - 上述一组公式可以表示为关系代数中的联合查询，但不等式。

我试图证明每一种常规语言都是可判定的。

因此，为了证明我试图证明我可以从确定性有限自动机（DFA）转移到图灵可判定机器。

所以我不确定如何构建一个模拟原始自动化（DFA）的图灵机。

状态（在自动机和图灵机中）当然会相似..但我不知道如何继续..

提前致谢。石然

我需要一些帮助来证明Total问题不是递归的（可判定的）。

我知道Halting问题的对角化证明，我只需要Total问题的相同证明。我发布了停止问题证明以供参考：

停止问题证明

假设我们可以决定停机问题。那么存在一些总函数 Halt 使得

在这里，我们对所有程序进行了编号，[x] 指的是此顺序中的第 x 个程序。我们可以将 Halt 视为从 ℵ 到 ℵ 的映射，将其输入视为一个数字，表示通过 one-one on 函数配对两个数字

现在，如果 Halt 存在，那么 Disagree 也存在，其中

由于不同意是从 ℵ 到 ℵ 的程序，因此可以通过 Halt 来推断不同意。令 d 满足 Disagree = Φd，则

Disagree(d) 已定义 ⇔ Halt(d,d) = 0 ⇔ Φd (d) 未定义 ⇔ Disagree(d) 未定义

但这意味着不同意与它自己的存在相矛盾。由于我们采取的每一步都是建设性的，除了最初的假设，我们必须假设最初的假设是错误的。因此，停机问题是无法解决的。

由所有图灵机描述 M 组成的语言 L，M 接受的语言是有限的。

我说 L 是一种可判定语言，因为我可以在函数 D(M) 上运行 M，如果在 M 的开始和接受状态之间存在循环，则返回 false，否则返回 true。

我感觉我错了，因为我低估了检测无限循环的难度。

感谢您的帮助，在此先感谢您。

在我的课堂上有一个关于以下语言是否有限的问题

{w : w 是 {a ^m b ⁿ :m+n≤k}} 的正则表达式，其中 k 是特定的自然数。

我认为它是有限的，因为语言中最多可以有(K+1)*k/2单词，但参考答案是 w 是无限的

谁能解释一下

ps：特定的正则语言只有一个正则表达式吗？

如何证明 L 不可识别？有任何想法吗？

我已经证明L compliment是可识别的：

我从数学交换中找到了以下解释

一种语言是可识别的，如果有一个图灵机将停止并仅接受该语言中的字符串，并且对于不在该语言中的字符串，TM 要么拒绝，要么根本不停止。注意：没有要求图灵机应该为非该语言的字符串停止。

一种语言是可判定的，如果有一个图灵机将接受该语言中的字符串并拒绝该语言中的字符串。”

我真的看不出两者有什么区别。仅接受语言字符串的图灵机与接受语言字符串的图灵机有什么区别？这是否意味着任何图灵机都可以接受任何东西？

我不明白为什么图灵机 T，在没有标记接受状态时接受并在标记接受状态时拒绝：

E(dfa) = {| A 是 DFA 并且 L(A) = 空集（没有符号）}

E(dfa) 是一种可判定语言。

证明：一个 DFA 接受一些字符串，当且仅当从开始状态通过 > 沿着 DFA 的箭头移动达到接受状态是可能的。为了测试这种情况，我们可以设计一个>TM T，它使用类似于示例 3.23 中使用的标记算法。

T= "在 input 上，其中 A 是一个 DFA： 1. 标记 A 的开始状态。 2. 重复直到没有新状态被标记： 3. 标记从已经标记的任何状态进入它的转换的任何状态. 4. 如果没有标记接受状态，则接受；否则，拒绝。

这对我来说似乎倒退了。谁能解释一下？

谢谢你。

我是 Agda 的新手，我需要帮助来了解Decidable功能和Dec类型。

我正在尝试定义一阶逻辑谓词，并且我想用证明对某种布尔值进行编码。我发现这样做的方法是使用 Dec 类型..

现在，据我所知，为了能够做到这一点，我必须将所有逻辑运算符重新定义为可判定类型而不是集合类型。为此，我将它嵌入到新类型中，这就是我为 and 运算符所做的：

是这样做的方法，还是有其他方法？

然后，我想使用这个运算符来定义 Nat 值的关系，所以我做了这样的事情：

但这会产生类型错误..

我不确定如何使用Dec，如果有人可以指导我使用它来证明逻辑陈述的教程或示例，我将不胜感激。

我知道 C++ 是不可判定的。但它是递归可枚举的吗？

让我们将一组有效的 C++ 程序定义为当前 C++ 标准下任何定义良好的程序。

是否有可能构建一个总能在有限时间内识别有效 C++ 程序的编译器？

还是它是递归可枚举的？

是否有可能构建一个总能在有限时间内识别无效C++ 程序的编译器？

或者两者都不是？