实用的非图灵完备语言？

Question

几乎所有使用的编程语言都是图灵完备的，尽管这使得该语言能够表示任何可计算算法，但它也带来了自己的一套问题。考虑到我编写的所有算法都旨在停止，我希望能够用一种保证它们会停止的语言来表示它们。

在词法分析时，用于匹配字符串的正则表达式和有限状态机被使用，但我想知道是否有更通用、广泛的语言，而不是图灵完备的？

编辑：我应该澄清一下，所谓“通用”并不一定意味着要能够在语言中编写所有停机算法（我认为这样的语言不存在），但我怀疑停机证明中存在可以归纳出的共同点，从而产生一种保证所有算法都将停止的语言。

还有另一种解决这个问题的方法——消除对理论上无限的内存的需求。一旦限制了机器允许的内存量，机器所处的状态数量是有限且可数的，因此您可以确定算法是否会停止（通过不允许机器进入之前已经进入过的状态）。

- nobody

---

SQL可能是我最好的选择。但是，一个不是图灵完备的通用语言相当不实用。你将无法进行循环或递归。 - jalf

这跟停机问题有什么关系？？？ - user3850

想象一种语言，从设计上来说，所有的程序都会停止运行 - 我意识到这在很大程度上是一个理论计算机科学的练习，但它也有一些实际应用。 - Kyle Cronin

SQL（不使用递归、动态SQL或通用WHILE循环）保证会停止（因此不是图灵完备的），但仍然非常实用。当然，严格来说，它也不是通用目的语言。 - RBarryYoung

如果可能的话，请提供“通用”的有意义的定义。这是一个可能适用于上下文的定义：“能够完成所有可由通用图灵机可判定的问题”，当然这是一种重言，因为语言现在将是图灵完备的。如果您有一个更弱的定义，请建议。 - SingleNegationElimination

Answer 1

不要听那些唱衰的人。在某些情况下，有很好的理由选择非图灵完备语言，例如如果你想保证程序终止，或者简化代码，例如通过消除运行时错误的可能性。有时候，仅仅忽略事物可能是不够的。

论文《全函数式编程》更或多或少地论证了我们实际上应该几乎总是更喜欢这样的受限语言，因为编译器的保证要强得多。能够证明程序停机本身就可能很重要，但实际上这是更简单语言所提供的更容易推理的结果。作为语言层次结构中的一个组成部分，非通用语言的效用范围相当广泛。

另一个更全面地解决这种分层概念的系统是Hume。Hume报告对该系统及其五个层次的更完整但更不安全的语言进行了全面描述。

最后，别忘了Charity。虽然有点抽象，但它也是一种非常有趣的方法，可以用基于范畴论的概念来实现有用但非通用的编程语言。

- Mr. Putty

---

我很高兴你喜欢它们。 如果那些对你有趣，你可能还想看一下Epigram（http://www.e-pig.org/和http://www.e-pig.org/downloads/ydtm.pdf是一个好的开始）。 尽管可能略微偏题，但上述论文第3节中有一个有趣的讨论，涉及关于总体价值的问题，以及能够指示程序哪些部分是总体的，哪些部分不是总体的问题。 Epigram的观点是依赖类型允许我们做到这一点。 - Mr. Putty

Answer 2

BlooP（缩写为Bounded loop）是一种有趣的非图灵完备语言。它本质上是一种图灵完备语言，但有一个（重要的）限制：每个循环必须包含对迭代次数的限制。无限循环是不允许的。因此，可以解决BlooP程序的停机问题。

- Adam Rosenfield

---

BlooP是一个很好的例子。还可以看看FlooP（相同的链接），它是具有自由（无限制）循环的图灵完备版本。 - aib

有人可能会认为“最多x次”使其不符合“通用”的标准。这必然将对问题结果的洞察力注入到问题的定义中。 - Larry OBrien

假设它们没有无限递归或动态自我评估/执行的能力，这两者都是无限迭代后门。 - RBarryYoung

BlooP的能力是无用的。对于（有界2^32-1）对于（有界2^32-1）逐步评估可行的无限循环在实践中是无限的。 - Joshua

Answer 3

问题不在于图灵机，而在于“算法”。你无法预测算法是否会停止的原因是这样的：

function confusion()
{
    if( halts( confusion ) )
    {
        while True:
            no-op
    }
    else
        return;
}

任何不能进行递归或循环的语言都不算是真正“通用”的。

正则表达式和有限状态机是相同的东西！词法分析和字符串匹配是相同的东西！有限状态机之所以停止是因为它们永远不会循环；它们只是逐个字符地传递输入并退出。

编辑：

对于许多算法，它们是否会停止是显而易见的。

例如：

function nonhalting()
{
    while 1:
        no-op
}

这个函数显然永远不会停止。

而这个函数明显会停止：

function simple_halting_function()
{
    return 1;
}

所以，结论是：你可以保证算法终止，只需要设计它使得它能够终止。

如果你不确定算法是否能始终终止，那么你可能无法在任何保证“终止”的语言中实现它。

- hasen j

---

一个没有递归或循环的语言在大多数情况下并不会很有用，但一个只有受保护递归的语言可以是完全的，对于许多目的仍然很有用。 - Doug McClean

所有总是停机且不能表达无限的语言都不是图灵等价（或者说是图灵完备的）。但是有一些语言，例如Charity，可以表达一般递归（而不仅仅是它的子集原始递归），但它们也不是图灵完备的。 - Sean A.O. Harney

Answer 4

慈善不是图灵完备的，但它不仅在理论上、教学上有趣（范畴论），而且还可以解决实际问题（汉诺塔）。它的强大之处在于它甚至可以表达阿克曼函数。

- physis

Answer 5

原来实现图灵完备是相当容易的。例如，你只需要类似BrainF**k的8条指令，更重要的是，你实际上只需要一条指令。

这些语言的核心是一个循环结构，一旦你有了无限循环，你就会面临一个固有的停机问题。循环何时终止？即使在一个不支持图灵完备的语言中，如果它支持无限循环，你可能仍然会在实践中遇到停机问题。

如果你希望所有程序都能终止，那么你只需要仔细编写代码。特定的语言可能更符合你的喜好和风格，但我认为没有任何语言可以绝对保证生成的程序会停止。

- grieve

---

即使在支持循环的非图灵完备语言中，您仍然会遇到停机问题。如果教堂-图灵论点成立，那么您是错误的。 - user824425

停机问题对于计算模型X而言是有效可判定的，只要该模型比图灵机弱（即，图灵机可以模拟X的所有实例，但X无法模拟所有图灵机）。毕竟，这种模型可以被决策器模拟，对于决策器而言，停机问题是可判定的（决策器总是会停机）。CTT与此有何关系？它可以被解释为“图灵完备性是最强大的”，因此如果成立，非T-C事物始终较弱，因此它们的HP是可判定的。 - user824425

顺便提一下，有许多语言可以保证终止。这里最合适的是LOOP（Meyer＆Ritchie，1967年；也由Hofstadter在《哥德尔、艾舍尔、巴赫》中描述），它基于循环...但它们总是有界的。因此，所有LOOP程序最终都会停止，因此它们的停机问题是可判定的。另外，如其他答案所述，依赖类型编程语言通常限制您编写总函数，这些函数按定义必须终止。 - user824425

这也是错误的。有限状态自动机可以具有无界循环（例如，它们可以识别a*），但绝对不是图灵完备的。有限状态自动机的停机问题是可判定的。 - user824425

@Rhymoid 进一步澄清，理论上你可以决定程序是否会停止，但在实践中，它可能需要很长时间才能停止，以至于宇宙将首先陷入热死亡，这可能不是 OP 想要的。感谢您让我保持诚实。 :) - grieve

Answer 6

我认为，正确的做法是使用图灵完备的语言，并提供一个适合证明检查器处理的语义系统。因此，假设你有意写一个终止程序，你心中就有一个好的理由说明它会停止运行。使用这种新型语言，你应该能够表达这个论点，并将其证明。

顺便说一句，在我的生产编译器中，我有一些递归程序，我确定它们在某些输入上不会停止。我使用了一个“合理”的限制计数器来解决这个问题。FYI，实际的代码涉及到单态化多态代码，当使用多态递归时，无限扩展会发生。Haskell可以捕获这个问题，但我的Felix编译器不能（这是我不知道如何修复的编译器错误）。

根据我的总体论点，我想知道哪些注释对于所述目的是好的：我恰好掌握一种语言和编译器，所以如果我知道要添加什么支持，我可以很容易地添加它们 :) 我曾看到循环添加了“不变量”和“变量”子句，但我认为该语言没有扩展到使用该信息进行终止证明（如果我记得正确的话，它会在运行时检查不变量和变量）。

也许这值得再提一个问题。

- Yttrill

Answer 7

"消除理论上无限内存的需求。" -- 是的。任何物理计算机都受到宇宙熵的限制，甚至在此之前，还受到光速（即信息传播的最大速率）的限制。

更简单的方法是，在可实现的计算机中，只需监控资源消耗并对其进行一些限制。（例如，当内存或时间消耗 > 我的限制 时，终止该进程）。

如果您所问的是一个纯数学/理论解决方案，那么你如何定义“通用”？

- Larry OBrien

---

实际上，这是一个不错的解决方案，尽管有可能你会中止某些最终会终止的实例。这就是停机问题的问题所在：我们永远不知道程序只是运行时间太长还是根本不会终止。 - MauganRa

虽然有一个程序停止的良好证明，但你可以猜测程序需要多长时间以及它将使用多少内存（即其复杂性）。 - MauganRa

“通用型”的意思是指一种适合实现大多数计算机软件的编程语言，从“hello world”到射击游戏再到文本处理器都可以。 - MauganRa

Answer 8

任何非图灵完备的语言都不会作为一种通用语言而非常有用。你可能能够找到一些自称为通用语言但并非图灵完备的东西，但我从未见过。

- Robert Gamble