高阶可计算性以及对可计算函数内涵和外延的区分,更是直接地与直觉主义逻辑的构造性或可计算性阐释息息相关,因此它对数理逻辑的研究也非常的重要。从高阶可计算性研究的历史来讲,的确也有很大一部分贡献和发展来自于对数理逻辑中直觉主义逻辑相关的研究。直观上来讲,我们常常声称直觉主义逻辑有某种构造性阐释,即某个命题在直觉主义逻辑下可证明当且仅当我们能够给出某种构造来直接地验证或说明它是正确的。在现代数学的语境下,构造数学 [constructive mathematics] 和直觉主义数学 [intuitionistic mathematics] 在很多时候是作为同义词被大多数数学家使用的。例如,在直觉主义的构造性阐释下,对于推出连接词A → B 的证明或构造指的是一个把 A 的证明或构造转化成 B 的证明或构造的一个程序。但在这种解释下,如果没有对高阶可计算性的刻画我们是无法理解有嵌套的推出连接词,如 (A → B) → C 等公式的构造性解释的:套用前面的说法,对 (A → B) → C 的一个证明是一个把将 A 的证明转化到 B 的证明的程序转化为 C 的证明的程序(这句话用自然语言写出来非常难读,正是因为其涉及可计算性的高阶嵌套)。对于涉及到多个存在量词嵌套时直觉主义逻辑公式的构造性解释也完全类似。为了能够给这些嵌套的直觉主义逻辑公式一个严格地构造性阐释,有一个准确的语言来描述高阶的可计算性是必要的。
比较不同计算模型之间的关系
本文的最后一节我们来探讨一下不同计算模型之间的关系。在上世纪三十年代,Turing、Church、Kleene 等人的工作让我们非常惊讶地发现,许许多多完全不同的定义ℕ 上可计算函数的方式所给出的是完全一样的同一族函数。Church 对于可计算函数的刻画是基于 λ-calculus 的,其中对数字和可计算函数的表示都是基于 λ-calculus 中的项 [terms],是一个完全从语言和语形出发给出的构造。Turing 定义的图灵机则有完全不同的直观,它是基于某种特殊的物理可实现的机器,这些机器也被称为图灵机 [Turing machine]。而 Kleene 创立的递归论则是一个从复合 [compositionality] 和递归 [recursion] 结构出发的进路。事实上我们还有许许多多的计算模型,比如和现代计算机更加接近的基于暂存器 [register machine] 的计算结构,或者从纯逻辑的证明角度出发基于一阶算数系统的计算结构。所有关于这些计算模型的讨论可以参见[2]。令人震惊的是,这些看似完全不同——有着完全不同直观且基于完全不同的出发点——的计算模型所最终定义的可计算函数是完全一样的!这个事实也可以看作是可计算性能够作为一个数学中值得研究的抽象概念存在的最有力证据。
但值得注意的是,这里我们所谓的这些不同的计算模型给出完全一样的可计算函数指的是在外延的层面上。换句话说,从 ℕ 到 ℕ 的部分可计算函数这个外延集合具有非常高的鲁棒性。但这些不同的计算模型给出相同的可计算函数外延是否真的表明这系计算模型是等价的?这个问题从我刚开始接触可计算理论就一直困惑着我;直到我看到这本书,才感到有一个足够普遍的数学理论框架能够真正意义上对这个问题进行一个回答。
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。