实用的非图灵完整语言? [英] Practical non-Turing-complete languages?

问题描述

几乎所有使用的编程语言都是 Turn Complete ，尽管这提供了代表任何语言的语言可计算算法，它还带有自己的

Nearly all programming languages used are Turing Complete, and while this affords the language to represent any computable algorithm, it also comes with its own set of problems. Seeing as all the algorithms I write are intended to halt, I would like to be able to represent them in a language that guarantees they will halt.

正则表达式用于匹配字符串和 lexing时，使用wikipedia.org/wiki/Finite_state_machine"rel =" noreferrer>有限状态机 ，但是我想知道是否还有一种更通用的，不通用的图灵语言?

Regular expressions used for matching strings and finite state machines are used when lexing, but I'm wondering if there's a more general, broadly language that's not Turing complete?

我应该通过通用"来阐明，我不一定希望能够用该语言编写所有停止算法(我认为这样的语言不会存在) )，但我怀疑暂停证明中存在一些通用线程，可以将其通用化，以产生一种可以保证所有算法都停止的语言.

edit: I should clarify, by 'general purpose' I don't necessarily want to be able to write all halting algorithms in the language (I don't think that such a language would exist) but I suspect that there are common threads in halting proofs that can be generalized to produce a language in which all algorithms are guaranteed to halt.

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

There's also another way to tackle this problem - eliminate the need for theoretically infinite memory. Once you limit the amount of memory the machine is allowed, the number of states the machine is in is finite and countable, and therefore you can determine if the algorithm will halt (by not allowing the machine to move into a state it's been in before).

推荐答案

不要听反对者的话.如果您要保证终止或简化代码(例如通过消除运行时错误的可能性)，则在某些情况下可能会倾向于使用非图灵完整的语言，这是有很好的理由.有时，仅仅忽略事情可能还不够.

Don't listen to the naysayers. There are very good reasons one might prefer a non-Turing complete language in some contexts, if you want to guarantee termination, or simplify code, for example by removing the possibility of runtime errors. Sometimes, just ignoring things may not be sufficient.

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

The paper Total Functional Programming argues more or less persuasively that in fact we should almost always prefer such a restricted language because the compiler's guarantees are so much stronger. Being able to prove a program halts can be significant in and of itself, but really this is the product of the much easier reasoning that the simpler languages afford. As one component in a hierarchy of languages of varying capability, the range of utility of non-universal languages is quite broad.

另一个可以更全面地解决此分层概念的系统是休ume . 休姆报告提供了完整的说明系统及其五层逐渐完善，越来越不安全的语言.

Another system that addresses this layering concept much more fully is Hume. The Hume Report gives a full description of the system and its five layers of progressively more complete, and progressively less safe, languages.

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

And finally, don't forget Charity. It's a bit abstract, but it is also a very interesting approach to a useful but not universal programming language, which is based very directly on concepts from category theory.

这篇关于实用的非图灵完整语言?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！