几乎所有使用的编程语言都是图灵完备,虽然这提供了语言来表示任何可计算的算法,但它也有自己的一组问题.看到我写的所有算法都打算停止,我希望能够用一种语言来代表它们,以保证它们会停止.
正则表达式用于匹配字符串和有限状态机在使用时词法,但我不知道是否有这不是图灵完整更普遍的,广泛的语言吗？
编辑:我应该澄清,通过'通用'我不一定希望能够在语言中编写所有停止算法(我不认为这样的语言会存在)但我怀疑有共同的线程停止可以推广的证明,以产生一种语言,保证所有算法都停止.
还有另一种解决这个问题的方法 - 消除理论上无限记忆的需要.一旦限制了机器允许的内存量,机器所处的状态数是有限且可数的,因此您可以确定算法是否会停止(通过不允许机器进入之前的状态) ).
Scala使用基于SystemFω的类型系统,通常认为它是强正规化的.强烈归一化意味着非图灵完整性.
然而,Scala的类型系统是Turing-complete.
与正式算法和系统相比,哪些更改/添加/修改使Scala的类型系统图灵完整？