问题标签 [decidable]

我正在尝试使用上下文无关语法提出有限或无限语言的解决方案。

我有这些语法来确定它是有限语言还是无限语言的解决方案

所以我会做

所以我在这里知道如何生成这样的单词，但是我如何找到它的有限或无限语言呢？

确定性线性有界自动机 (LBA) 是一种单磁带 TM，不允许将其磁头移过输入的右端（但它可以在磁带最初包含输入的部分上进行读写）。

我如何证明确定性 LBA M 是否接受无限数量的输入是不可判定的？

我在字母表 {0,1} 上有语言 {4^(w⋅g)34^(g)|w,g∈NAT}。

我需要找出这种语言是可识别的、可判定的、上下文无关的、常规的还是这些都不是。

我将如何去做或知道？

谢谢

我对这些东西很陌生。希望这不是一个非常幼稚的问题。

我在 Prolog 中尝试了以下公式：A ⇒ B

并且鉴于B是真的，我评估A并且它说 FALSE。

我的问题是为什么 FALSE？（为什么不是 TRUE？）鉴于当前信息，我们对B一无所知。Prolog 是否基于以下假设工作​​：对于任何未知事物，它会输出 FALSE？

如果这是一个假设，这有多普遍？

想到的另一件事是，它正在寻找输入查询和公理的结合的分配（基本上是 SAT 求解）。由于结果输出为 TRUE，无论A有什么值，它只是随机选择一个（或默认为零？）。

基于一阶逻辑的性质，它是半可判定的。如果一个句子A 在逻辑上暗示了一个句子B，那么这可以被发现，但反过来就不行。那么，在没有 TRUTH 证明的情况下，后一种情况在实践中是如何处理的呢？

PS1。关于 Prolog 如何工作的一点解释，也可能有用。它是否使用 SAT 求解器作为黑匣子？还是贪心搜索算法？

我想定义一个参数化命题decidable，讨论其他参数化命题的可判定性。举一个常见的例子，even是一个参数化的命题，它接受 1 个类型的参数nat，它是可判定的。lt是一个带 2 个类型参数的参数化命题，nat它也是可判定的。我想decidable成为这样，decidable even并且decidable lt都是可证明的命题。

定义的主要困难decidable是指定它的类型。它必须接受任何类型的参数化命题A -> B -> C -> ... Z -> Prop，其中 A...Z 是类型，它们的总数是任意的。

这是我的第一次尝试：

我认为它应该可以P \/ ~ P用作前提，因为 Coq 足够聪明，可以在给定先验前提的情况下d_0弄清楚这一点。它不是。P : PropX = Prop

所以现在我找不到任何方法来拼出整个丑陋的东西：如果我想说 someP : A -> B -> C -> ... Z -> Prop是可判定的，它必须写成forall ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z \/ ~ P a b c ... z。啊。

但也许我错过了一些东西。由于我对 Coq 多态性的初步了解，我可能忽略了一些巧妙的技巧。

有什么建议么？

我试图证明机器 L(M) 中的字符串是否是可判定的，但我无法找到合适的结果。谁能帮我解释一些关于这个的例子。

我正在尝试的场景是我有两个字符串，S1 是 S2 的子集，因此显示机器 L(M) 是可确定的

我正在使用这种类型来推断可以执行可判定解析的字符串：

例如，像这样定义数字 [0-9]：

那么我们可以有以下功能：

这个s2n函数现在可以在编译时正常工作，但它本身并不是很有用。要在运行时使用它，我们必须先构造证明Every Digit (unpack s)，然后才能使用该函数。

所以我想我现在想写这样的函数：

或者我们想要返回成员资格证明或非成员资格证明，但我不完全确定如何以一般方式执行这些操作。因此，我尝试Maybe只为字符制作版本：

但后来我得到这个统一错误：

但p 属于类型Char -> Type。我不确定是什么导致了这个统一失败，但认为这个问题可能与我之前的问题有关。

这是我想要做的事情的明智方法吗？我觉得目前的工作有点多，这些功能的更通用版本应该是可能的。auto如果关键字可以用于编写一个函数给你一个Maybe proof或一个，这将是很好的Either proof proofThatItIsNot，就像DecEq类的工作方式一样。

如果 L 是任何语言。语言 perms(L) 是 L 中所有单词排列的语言。

对或错：如果 L 是递归可枚举的（可计算可枚举的），那么 perms(L) 也是递归可枚举的。

这是在之前的决赛中出现的问题：如果 L 是可判定的，那么 perms(L) 也是可判定的，我发现这是真的。

我想我会说假的，但我没有证据支持这种说法。

我在一个本科班，我们现在正在学习形式语法。我问我的老师是否有任何已知的规则来创建上下文无关语法

1) 保证产生明确的语法。2) 允许创建任何可能的明确语法。

我很清楚，确定语法是否模棱两可是不可判定的。我不确定上述想法是否可以简化为，但是在摆弄了一下之后，我想不出一种方法来进行这种简化。也就是说，我真的不是简化或语法方面的专家。我尝试了一段时间的谷歌搜索，但我只找到了关于不确定性的页面。有人知道吗？

任何专家都可以帮助我为什么这句话是真的？

如果 L ∈ NP 并且 L ≤<sub>p 3−SAT（即：在多时间内将 L 减少为 3-SAT），则 L 是 NP-Complete。