计算机构造（三） (6-2)

例子2: untyped λ-calculus. Church 最早对于可计算性地研究基于 λ-calculus，是一种语形（syntactical）的进路。假设我们固定了一个变元集合 [variable set] P （通常其是可数无穷的），则我们可以如下递归定义所有 untyped λ-calculus 的项 [terms]：

M：＝x∈P│MM│λx. M .(1)

我们定义∧ 为所有的项构成的集合在模掉 α-等价后所得到的集合（我们假设读者熟悉 α-等价的概念，其表示的是对于限制变元 [bounded variable] 的重命名）。在 ∧ 上我们还可以进一步定义 β-等价关系，即由下面的条件所生成的最小等价关系：

(λx.M)N ∼ M[N/x]，M ∼ N ⇒ PM ∼ PN，M ∼ N ⇒ λx.M ∼ λx.N . (2)

其中M[N/x] 表示将 M 中的自由变元 [free variable] x 替换为 N 后所得到的项（为了避免 N 中的自由变元在替换到 M 后被限制我们可能需要先替换 M 中限制变元，但这是良定义的，因为在 ∧ 中 α-等价的项代表同一个元素）。我们用 [M] 表示项 M 在 ∼-等价关系下所对应的等价类，将 ∧/∼ 记为 ∧ 在这个等价关系下的商。则我们同样有一个只有一个类型 ℓ 的计算模型，其中 C(ℓ)＝∧/∼ 。对于任意 P∈∧ ，其都对应着一个良定义的映射函数 P：∧/∼ → ∧/∼ ，其定义为 [M] ↦ [PM]。这样的映射称为 λ-可定义函数，在我们的计算模型中，我们也令 C[ℓ，ℓ] 为所有 λ-可定义函数所构成的集合。值得注意的是，所有这样的函数都是完全函数而不是部分函数。感兴趣的读者应自行验证 C 构成一个范畴，即 ∧/∼ 上的恒等映射是 λ-可定义的，且若两个映射均为 λ-可定义，则其复合映射同样为 λ-可定义。

在 Higher-Order Computability 一书中还给出了许许多多的可计算模型的例子，有基于图灵机的，有基于编程语言的，还有和传统递归论和可计算理论中所研究的计算模型更贴近的，限于篇幅我们就不一一介绍了。我们后面的理论介绍将都基于上面给出的这两个最基本的计算模型的例子。

计算模型上的弱笛卡尔闭 [Weakly Cartesian Closed] 结构

我们提到了，我们有许许多多地理由关心高阶的可计算性，但高阶可计算性的具体数学结构只有在今天介绍了详细的计算模型的定义后才能展开说明。对应到我们前面提到的计算模型的范畴结构，高阶计算性表示这个范畴是弱笛卡尔闭的。这一节我们便详细地谈谈这一点。

给定一个T 上的可计算模型 C ，我们说 C 上有一个弱笛卡尔结构 [weak Cartesian structure] 当满足条件：对于 T 中的任意两个类型 σ，τ 我们有一个对应的类型 σ × τ∈T 和两个投影映射 [projection map] πσ∈C[σ × τ，σ] ， πτ∈C[σ × τ，τ] ，使得对于任意 η∈T 和任意 f∈C[η，σ] g∈C[η，τ]，存在一个函数 h∈C[η，σ × τ] 使得对于任意 c∈C[η] 我们有：

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。