非图灵完整语言的实用性？
几乎所有使用的编程语言都是图灵完成的 ，虽然这提供了表示任何可计算algorithm的语言，但它也带有一套自己的问题 。 看到我写的所有algorithm都是想停下来的，我希望能用一种能保证停止的语言来表示它们。
用于匹配string和有限状态机的 正则expression式在使用时会被使用，但是我想知道是否有一个更一般，广泛的语言不是图灵完整的？
编辑：我应该澄清，通过'通用'我不一定要能够写所有停止algorithm的语言（我不认为这样的语言会存在），但我怀疑有共同的线程在停止certificate，可以推广到产生一种语言，其中所有algorithm都保证停止。
还有另一种方法来解决这个问题 – 消除理论上无限的记忆的需要。 一旦限制了机器的内存容量，机器所处的状态数就是有限且可数的，因此可以确定algorithm是否会停止（不允许机器进入之前的状态）。
不要听取反对者的意见。 有很好的理由，如果你想保证终止，或简化代码，例如通过消除运行时错误的可能性，人们可能更喜欢非图灵完整的语言在某些情况下。 有时候，只是忽略事情可能是不够的。
“ 全function编程 ”论文或多或less有说服力地说，实际上我们应该总是更喜欢这种有限制的语言，因为编译器的保证更强大。 能够certificate一个程序暂停本身可能是重要的，但实际上这是更简单的语言提供了更容易推理的产物。 作为不同能力语言层次结构的一个组成部分，非通用语言的效用范围相当广泛。
另一个更全面地解决这种分层概念的系统是休谟 。 “ 休谟报告”全面描述了该系统及其五层逐渐更完整，逐渐不太安全的语言。
最后，不要忘记慈善 。 这是一个有点抽象，但它也是一个非常有趣的方法来一个有用的，但不是通用的编程语言，它是直接基于类别理论的概念。
BlooP （简称为B 回路 ）是一种有趣的非图灵完备语言。 这本质上是一个图灵完备的语言，有一个（主要的）警告：每个循环必须包含迭代次数的界限。 无限循环是不允许的。 因此，BlooP程序可以解决停机问题。
问题不在于图灵机，而在于“algorithm”。 你不能预测一个algorithm是否会停止的原因是因为：
function confusion() { if( halts( confusion ) ) { while True: no-op } else return; } 任何不能做recursion或循环的语言都不是真正的“通用”。
正则expression式和有限状态机是一回事！ Lexing和string匹配是一回事！ FSM停止的原因是因为他们永远不会循环; 他们只是通过inputchar-by-char并退出。
编辑：
对于许多algorithm来说，它们是否会停下来是显而易见的。
例如：
function nonhalting() { while 1: no-op }
这个function显然不会停止。
而且，这个function显然停止了：
function simple_halting_function() { return 1; }
所以底线：你可以保证你的algorithm暂停，只需要devise它就可以了。
如果您不确定algorithm是否会一直停下来， 那么你可能无法用任何保证“停止”的语言来实现它。
慈善不是图灵完整的，它不仅在理论上是讲求趣的（分类理论），而且还可以解决实际问题（河内大厦）。 它的力量是如此之大，甚至可以expression阿克曼function 。
事实certificate，完成这个过程相当容易。 例如，你只需要8条指令ala BrainF ** k ，更重要的是你只需要一条指令 。
这些语言的核心是一个循环的结构，只要你有无限的循环，你就有一个固有的暂停问题。 循环何时终止？ 即使在支持无限循环的非图灵完备语言中，您在实践中 可能仍然存在停滞的问题。
如果你想要所有的程序终止，那么你只需要仔细写你的代码。 一种特定的语言可能更符合你的喜好和风格，但我不认为任何语言都可以绝对保证所产生的程序将停止。
“消除理论上无限的记忆的需要”。 – 好的，是的。 任何物理计算机都受到宇宙的熵的限制，甚至在这之前，受光速（==信息传播的最大速率）的限制。
更容易的是，在一个物理上可实现的计算机中，只是监视资源消耗并对其进行一些约束。 （即，当内存或时间消耗> MY_LIMIT时，终止进程）。
如果你所要求的是一个纯粹的math/理论的解决scheme，你如何定义“一般目的”？
做到这一点的正确方法，恕我直言，是有一个语言是图灵完成，但提供一个系统，说明语义适合处理由certificate检查。
那么，假设你故意写了一个终止程序，那么你为什么会停下来谈论一个好的论点，用这种新的语言，你应该能够expression这个论点，并且certificate它已经被certificate了。
在我的生产编译器中，我有recursion，我知道，当然，不会停止某些input。我用一个讨厌的黑客来阻止这个：一个“明智的”限制的计数器。 仅供参考，实际代码涉及单态多态代码，使用多态recursion时发生无限扩展。 Haskell捕捉到了这一点，我的费利克斯编译器不（这是编译器中的错误，我碰巧不知道如何解决）。
从我的一般论点来看，我一定会想知道什么样的注释对于这个陈述的目的会有好处：我碰巧控制了一个语言和编译器，所以我可以很容易地添加这样的支持，只要我确切知道该怎么做添加:)我已经看到增加了一个“不变”和“变体”子句来循环这个目的，虽然我不认为该语言扩展到使用该信息作为终止certificate（而不是检查不variables和变体运行时间，如果我没有记错的话）。
也许这值得另一个问题..
任何非图灵完备语言作为通用语言都不会很有用。 你也许能够find一些自己认为是通用语言的东西，而不是图灵完成的，但是我从来没有见过。
