52

几乎所有使用的编程语言都是图灵完备的，虽然这提供了表示任何可计算算法的语言，但它也带来了自己的一系列问题。鉴于我编写的所有算法都打算停止，我希望能够用一种保证它们会停止的语言来表示它们。

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

编辑：我应该澄清一下，通过“通用”我不一定希望能够用该语言编写所有停止算法（我认为这种语言不会存在）但我怀疑有共同的线程停止证明，可以推广以产生一种语言，其中所有算法都保证停止。

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

4

8 回答 8

60

不要听那些反对者的话。如果您想保证终止或简化代码，例如通过消除运行时错误的可能性，那么在某些情况下，人们可能会更喜欢非图灵完备的语言，这是有充分理由的。有时，仅仅忽略一些事情可能还不够。

Total Functional Programming一文或多或少有说服力地指出，事实上我们几乎总是应该更喜欢这种受限制的语言，因为编译器的保证要强得多。能够证明程序停止本身就很重要，但实际上这是更简单的语言提供的更容易推理的产物。作为具有不同能力的语言层次结构中的一个组成部分，非通用语言的实用范围非常广泛。

另一个更充分地解决这种分层概念的系统是Hume。休谟报告全面描述了该系统及其五层逐渐更完整、逐渐降低安全性的语言。

最后，不要忘记慈善。它有点抽象，但对于一种有用但非通用的编程语言来说，它也是一种非常有趣的方法，它非常直接地基于类别理论的概念。

于 2009-07-05T03:24:24.687 回答
34

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

于 2008-11-24T20:52:43.300 回答
14

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

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

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

正则表达式和有限状态机是一回事！词法分析和字符串匹配是一回事！FSM 停止的原因是它们从不循环；他们只是逐个传递输入并退出。

编辑：

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

例如：

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

这个功能显然永远不会停止。

而且，这个函数显然会停止：

function simple_halting_function()
{
    return 1;
}

所以底线：你可以保证你的算法停止，只需设计它就可以了。

如果您不确定算法是否会一直停止；那么您可能无法用任何保证“停止”的语言来实现它。

于 2008-11-24T20:44:11.757 回答
9

Charity is not Turing complete, still, it is not only theoretically, didactically interesting (category theory), but moreover, it can solve practical problems (Hanoi towers). Its strength is so great that it can express even Ackermann function.

于 2009-09-10T09:35:06.077 回答
7

事实证明，图灵完备是相当容易的。例如，你只需要 8 条指令 ala BrainF**k，更重要的是你真的只需要一条指令。

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

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

于 2008-11-24T20:51:57.250 回答
2

“消除对理论上无限记忆的需求。” ——嗯，是的。任何物理计算机都受到宇宙熵的限制，甚至在此之前，还受到光速（== 信息传播的最大速率）的限制。

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

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

于 2008-11-24T22:49:24.533 回答
2

恕我直言，做到这一点的正确方法是拥有一种图灵完备的语言，但要提供一个系统来说明可由证明检查器处理的语义。

然后，假设您正在特意编写一个终止程序，您心中有一个很好的论据来说明它为什么会停止，并且使用这种新的语言，您应该能够表达这个论点，并证明它。

作为我的生产编译器的一个旁白，我知道我肯定不会在某些输入上停止递归。我使用了一个讨厌的技巧来阻止它：一个具有“合理”限制的计数器。仅供参考，实际代码涉及单态多态代码，并且在使用多态递归时会发生无限扩展。Haskell 捕捉到了这一点，我的 Felix 编译器没有（这是编译器中的一个错误，我碰巧不知道如何修复）。

根据我的一般论点..我肯定想知道哪种注释对所述目的有好处：我碰巧控制了一种语言和编译器，因此只要我知道确切的内容，我就可以轻松添加此类支持添加:)我已经看到为此目的在循环中添加了“不变”和“变体”子句，尽管我不认为该语言扩展到使用该信息来证明终止（而是在如果我没记错的话，运行时间）。

也许这值得另一个问题..

于 2011-12-15T10:54:18.030 回答
-3

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

于 2008-11-24T20:39:59.020 回答