regex - 实用的非图灵完备语言？

Question

几乎所有使用的编程语言都是Turing Complete ，虽然这提供了代表任何 computable 的语言算法，它还自带一套problems 。鉴于我编写的所有算法都是为了停止，我希望能够用一种保证它们会停止的语言来表示它们。

Regular expressions用于匹配字符串和 finite state machines当 lexing 时使用，但我想知道是否有一种更通用、更广泛的语言不是图灵完备的？

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

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

Answer 1

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

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

另一个更全面地解决此分层概念的系统是 Hume 。 Hume Report给出了该系统及其五层逐渐更完整和逐渐不安全的语言的完整描述。

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