实用的非图灵完备语言？

Question

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

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

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

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

Answer 1

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

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

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

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

Answer 2

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

Answer 3

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

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

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

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

编辑：

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

例如：

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

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

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

function simple_halting_function()
{
    return 1;
}

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

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

Answer 4

慈善并不是图灵完备的，但它不仅在理论上、说教上都很有趣（类别理论），但更重要的是，它可以解决实际问题（河内塔）。 它的力量非常强大，甚至可以表达阿克曼函数。

Answer 5

事实证明，图灵完备相当容易。 例如，您只需要 ala BrainF**k 等 8 条指令，更多的是您实际上只需要需要一条指令。

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

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

Answer 6

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

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

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

Answer 7

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

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

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

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

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

Answer 8

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