计算机构造（四）

剩余的问题

在前面两节中我们表述了最基础的高阶计算模型的数学结构，并陈述了我们常见的两个计算模型，即基于图灵机的自然数上的可计算模型和基于 λ-calculus 的可计算模型，如何融入到我们所定义的数学框架中。但这仅仅是一个开始。在本篇文章的最后我们阐述一下在此基础之上我们还应该关心什么基本问题。这一节可以看作一个预告，里面提到的内容将会在下一篇文章中具体地阐述。

问题1：计算模型之间的关系？

首先，范畴的基本思想仍然指导着我们，一旦当我们定义了某种数学对象（比如我们这里定义的高阶计算模型），我们应该立刻关心这些数学对象之间的关系，即什么应该是它们之间的态射。在计算模型的语境下，两个计算模型之间的态射C → D 直观上来说应该对应着某种用 D 来模拟 C 中的计算的方式。在理解态射之后，进一步我们便可以询问什么情况下两个计算模型之间是等价的？

我们可以从上面所提到的两个计算模型的例子入手。在基础的可计算性理论中一个非常重要的结果便是，在 untyped[公式] -calculus 中定义的可计算函数和用图灵机定义的可计算函数是完全相等的——在我们的话语体系中更准确地应说它们定义了相同的可计算函数的外延。更具体一些，我们在 untyped λ-calculus 中可以定义形如 λf.λx.fⁿx 这样的闭项 [closed term] 作为数字 [numeral]，其中 fⁿx 是 将 f 作用在 x 上 n 次，即 f(f(· · · f(x))) 的简写。则在 untyped λ-calculus 模型中的可计算函数（即由某个项所表示的函数）和图灵可计算函数在外延上是完全一致的。

更进一步，从直观上来讲我们似乎也的确能够用其中一个模型来模拟另一个模型的计算。对于用自然数模型来模拟λ-calculus 的模型，我们只需要使用我们非常常见的编码手段，将 untyped λ-calculus 的语形用自然数编码，便非常容易能够看出 λ-calculus 上语形的操作能够用自然数的操作来进行模拟。但反过来也同样，对于任意自然数上的操作我们可以用前面定义的 λ-calculus 中的数字和闭项来模拟。因此直观上讲，对于这两个模型而言我们能够在一个模型中模拟另一个模型的计算。

但再继续深入地问，这样的双向模拟表示这两个计算模型之间是等价的吗？事实上，由前面的论述我们可以看出这两个模型也有许多非常不同的地方。比如在 untypedλ-calculus 当中所有的可计算函数全是完全函数，但在自然数模型中显然不是。它们到底是否是等价的，我们留到在下一篇文章中详细探讨。

问题2: 我们有没有类似代数拓扑中的不变量来描述计算模型之间的等价性？

在拓扑的语境下，我们一个很基本的问题是判断两个空间是否是同胚的。我们能够写下的所有连续函数都不构成同胚这件事并不能说明这两个拓扑空间之间没有任何的连续函数使得它们同胚，这个问题使用传统的办法是非常难以回答的。为了解决这个问题，在拓扑的语境下我们发展了代数拓扑的工具使得对于一个拓扑空间我们能够赋予其一系列代数的不变量；通过比较这些不变量，我们能够在某种含义的等价下（如同伦、弱同伦等价）判断两个拓扑空间是否属于同一个等价类。

任意的完全格 [complete lattice] 都是一个笛卡尔范畴，但显然我们几乎不在任何意义上希望考虑格上的代数理论。比如任意格上的群都是 trivial 的，这是因为格 P 上的终对象是最大元，而对于任意元素 p ，若其是 P 中的一个群我们要求有一个态射 e：1 → p ，换句话说即有 1≤p 。这表明 p＝1 。因此，考虑一般范畴上的某个逻辑系统的模型太普遍了，对我们没有太大的作用。一个更加好的范畴类别是拓扑斯 [topos]，这是一类具有和 Set 十分结构的范畴，每一个拓扑斯都可以看作是某种构造性的数学宇宙 [constructive universe]；因此，在所有拓扑斯中看待逻辑系统的模型看起来至少是更为合理的。而由此我们生成了一种新的逻辑系统的 Morita 等价观念，即我们称两个系统是 Morita 等价的当且仅当它们在所有的拓扑斯中具有相同的模型。在这种等价观念下，我们在之前文章中介绍的逻辑系统的分类拓扑斯 [classifying topos] 便可看作是这种等价观念下逻辑系统所对应的完全不变量，即两个逻辑系统是 Morita 等价的当且仅当它们的分类拓扑斯是等价的。

回到我们的可计算模型上来。若我们对之前问题1有了一个好的答案，即我们有了一个计算模型之间的等价概念，我们能否找到这种等价概念下所对应的不变量，使得我们能够更加直接地判断两个计算模型之间是否是等价的？对这个问题的我们也会在下一篇文章中进行解答；事实上，和分类拓扑斯的构造类似，对于每一个计算模型C 我们也能够构造一个代表其计算结构的范畴 Ass(C) ，称为 the category of assemblies of C 。这个范畴和拓扑斯一样有着非常丰富的范畴结构，可以看作是对于计算模型的某种分类空间 [classifying space] 其能够解决很多我们关于计算模型的问题。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。