“非图灵完备”到底意味着什么

Posted 2023-01-21 3A是个坏同志

设计一个图灵非完备的编程语言。这件事情在外行人看来一点也不酷。就好比如果有人声称自己要做个“解决宇宙间一切计算问题的终极语言”，不管做得出来做不出来，总会有人把他奉若神明；也许很少有人意识到，只要有纸和笔，人人都是一台能解决任何计算问题的通用图灵机。自然，程序语言的可编程能力是纸带所无所比拟的：对于计算的规范化表述，高阶的数据抽象能力，丰富的类型系统，高度模块化及可重用性，等等。但，如果你不知道在纸上计算矩阵乘法的算法，而你的程序语言的库（注意——库不被看作是语言本身的一部分，即使是标准库）未曾实现这个功能，那么，再图灵完备、抽象能力再强的语言，也终究无法帮助你实现一个最简单的矩阵乘法。由此看来，设计一门语言并不能解决任何实际的问题；真正解决具体问题的，只能是设计算法的人。程序语言只是工具：表达思想的工具，表述计算过程的载体，无他。没有作为思想的算法灵魂，语言只是徒有其表的空壳。这就是为什么说程序语言的作用，常常被过分高估了的理由。

当然，如果有谁一上来就把“我想做个程序语言，它不是图灵完备的，基本上不可能解决所有的计算问题……”作为广告词，恐怕看见的人也只会哑然失笑。对于稍通一点计算理论的人来说，计算机具有和图灵机理论等价的计算能力是常识中的常识；而给某种计算机语言加上“图灵非完备”的限定，似乎等于是放弃了表达一切通用计算的能力，转而成为一个领域专有语言。

我要说的是，作为理论模型计算能力的图灵完备性质，与作为一种计算机语言的实际可编程能力之间是没有太多直接联系的。即使是理论上可以被证明是图灵非完备的计算机语言，仍然可以做到很多事情，从而足够资格被称作通用计算语言：

1、它可以用来实现一切可形式化验证的正确算法，但无法实现你自己都不知道是否停机的算法；

2、它可以用来实现永不终止但持续执行有效计算的软件，如一个操作系统、一个网站；但它无法实现空的死循环、爆栈而不产出有效数据输出的递归，或其他一切任何你认为“无用却不停机”的计算。

换言之，图灵机（或任何一种图灵完备语言）能实现而它所不能实现的计算，从实际的角度来看，基本上可说是没有意义的。譬如：你试图写一个“寻找正整数集中最大的素数”的算法，那么你在运行这个程序之前应该先从逻辑上理清这么做的意义：一旦程序找到了一个极大的素数，因为无法确定它是否为最大，它必须继续找下去。因此，不管这个最大的素数是否存在，程序为了输出正确的结果，将永远不会停机，你也就永远无法知道确切的答案。这样的计算除了让机器发热之外，意义何在？又譬如，你的程序若是要“寻找尽可能大的素数”，那么它总得时不时输出点什么，来确保它于你是有用的。一种图灵非完备的程序语言应当拒绝执行前一种 不停机不产出 的无效计算，从而使得自身失去和图灵机等效的计算能力；但它应当允许后一种 不停机持续产出 的有效计算，从而确保用它写出的程序永远是“有用的”。这些，构成了一种语言虽非图灵完备、其“有用”程度却丝毫不输于任何图灵完备语言的关键要素。

这样的图灵非完备程序语言实际存在着，但它们大多是因程序语言类型系统的研究用途而生，作为软件形式化验证的辅助工具而存在，并未有实际作为通用语言直接用于软件开发的尝试：如 Coq、Epigram 和 Agda。由于标准库中缺乏相应的支持，前两者甚至难以完成最简单的标准输入输出；而因为缺乏原生数据类型的实现，实际编程中司空见惯的整数、浮点数和字符串运算，到了这些语言中仍然极端繁琐。

作为证明辅助工具的它们，就纯函数式编程而言，其用途相当有限，不会超出为了对应 Curry-Howard 同构所需的范围。从它们的设计目的上很容易知道，这些语言本身不可能是图灵完备的；因为图灵完备意味着你可以写出没有终止的递归，这就破坏了类型所对应于逻辑的自恰和完备性，正如要回答“全能的上帝能造出一块他自己都搬不动的石头吗？”这个问题般，让机器的类型检查陷入无尽的逻辑循环推演；而我们知道，一次永不停机的证明是一次无效的证明，否则我们也就能够轻易地写出一个不停机的程序去验证哥德巴赫猜想对于一切数的情形都成立了。至于“纯函数计算是没有副作用的”，这一点更是老生常谈了，一个东西一旦被定义，那么它的值绝不能被改变；因为对于依赖于值的类型而言，一个值若可以在运行时改变，那么类型系统（编译时的类型检查即为证明）将失去它的意义，故而 依赖类型的语言几乎总是纯函数式的 ，从而使得它们无法直接完成对 状态量 的操作。

看起来，这种语言似乎没有什么实用价值。然而一旦接受了“计算过程本身也可以是计算处理的对象，对于计算之计算”这种设定，将对计算的描述本身借助于 Monad 归一化到它们的类型系统中，那么正如 Haskell 能够容纳副作用（状态、输入输出）于函数式计算的体系中一般，它本身虽为纯函数范式的数学语言，却可以用来实现非纯的外部物理过程；更进一步，一旦通过 codata 来描述无限的数据结构，它本身虽非图灵完备的语言，却可以用来模拟任何不停机的计算。

这是一个非常巧妙的问题：既然我已经鼓吹图灵非完备语言可以和图灵完备语言一样实用，足够完成任何有实际价值的计算，那么我必须用它写出一个图灵完备语言的解释器来证明这一点，因为“图灵完备语言的解释器”显然也属于所有“有实际价值”的程序范畴内；而一旦当我这样做了，似乎就等于是用一个计算模型模拟了一个图灵机，从而证明我原来的计算模型不可能是图灵非完备的。

现在，既然我们已经提到了这种图灵非完备语言的存在性与实用性，你可能不禁想问：能否用这种图灵非完备的语言，去实现一个图灵完备语言的解释器呢？这看似自相矛盾而又无比自恰，看似痴人说梦却又实在可及，其招致误解的根源在于人们总是习惯性地把“程序语言”和“计算模型”等同起来：Brainfuck、C、Pascal 是命令式的语言，它们等价于图灵机；Unlambda、Scheme、Haskell 是函数式的语言，它们等价于λ演算。故而这些语言都是图灵完备的，因为它们可以实现与图灵机等效的计算过程。这种说法看似没有什么问题，程序语言本来就是为了描述计算而生的实用工具，而抽象的计算模型才是真正描述计算的方法学。如果说图灵完备可以成为衡量计算模型计算能力的尺度，那么体现这些具体计算模型的程序语言，自然也就存在着相应计算能力的说法。我还可以在这里举出很多例子：正则表达式不是图灵完备的，所以像嵌入在通用程序语言里的 PCRE 库这类正则实现不是图灵完备的；谓词逻辑是图灵完备的，所以嵌入在通用程序语言里的 miniKanren 是图灵完备的；递归函数是图灵完备的，所以 C++ 里的模板是图灵完备的；项重写系统是图灵完备的，所以 Maude 是图灵完备的；马尔可夫算法是图灵完备的，所以 Refal 是图灵完备的；如此种种，数不胜数。

但是，今天的一些程序语言，已然超越了单一计算模型的范畴；单一的计算过程，已经不再适于描述所有程序语言的工作方式——不，我甚至不是在讨论副作用这件事情。就程序本身而言，有些程序语言能做的事情，图灵机是做不到的。这其中的一个典型例子，就是元编程。

给图灵机一连串指令，它能够执行任何计算，也可以模拟纯数学的λ演算；给λ演算一系列定义，它能够编码出世间万物，也可以模拟出基于顺序执行的机器。而它们都无法做到的，是改变自身被分配的指令或定义，也就是它们所注定的计算本身。然而，对于某些具有元编程能力的计算机语言来说，你可以在程序里嵌入一套规则，让这套规则具有操纵“计算”本身的能力。

以许多人都熟悉的 C++ 为例：你可以把 C++ 里的任意循环、递归函数的能力拿掉，从而成功地把它阉割成为一个必定停机的图灵非完备语言（事实上你不必通过强制所有程序停机来使得一个语言图灵非完备；但这么做可以简单粗暴地达到我们的目的）。在这种情形下，你将不能用 C++ 自身的语言来模拟一个图灵机，因为它已经不具备通用计算的能力；但是，没有什么能阻止你用 C++ 模板来实现这一切。换言之，C++ 的语言规范至少实现了两个相互独立的计算模型：C++ 自身的语言，和其嵌入的模板语言。由此来看，仅仅用“图灵完备”来形容 C++ 的计算能力是不够的，因为 C++ 作为一种程序语言，并不是 一个 图灵完备的计算模型，而体现着 两个 相互独立的图灵完备计算模型。

既然理解了“程序语言不必等同于计算模型”这件事情，前面的矛盾也就迎刃而解了：你实际上可以在图灵非完备的程序语言里内嵌一个图灵完备的计算模型 ；因为这个图灵完备的计算模型可以用来实现任何计算，因此，也就间接为使用该（图灵非完备）语言来实现一个图灵完备语言的解释器提供了无限的可能性。

这样容纳了另一个计算过程于自身内的程序语言，其计算潜力是无法用单一模型（如图灵机）的计算能力来完整表达的，正如你无法把 C++ （连同模板在内）的计算方式转化成单一的图灵机指令序列一样。C++ 模板元编程在这里也许并不是一个很好的例子；实际上，你可以把任何图灵完备的计算过程容纳到一门语言的类型系统里，从而让一门程序语言自身的计算模型虽非图灵完备，却可以借纯函数式的类型系统之手完整地描述图灵完备的计算模型。

图灵非完备语言的“有用性”，将会随着今后对于程序语言和类型论的研究愈加深刻地体现出来。