• 对于任意 f∈C[σ,τ] ,我们存在 f'∈D[γσ,γτ] 能追踪 f ,即若 α'⊩γσα 且 f(α) 有定义,则 f'(α') 也有定义且 f'(α')⊩γτ f(α) (直观来说, f' 在我们 γ 所描述的表示的含义下模拟 f )。
容易看出的是,对于任意计算模型C 我们有一个恒等模拟;两个模拟 γ:C → D 和 δ:D → E 之间也能够复合。这表示在模拟作为态射下,计算模型本身构成了一个范畴 Cmp。从计算模拟的定义我们可以简单地理解为,如果有一个 γ:C → D 的模拟,则从某种程度上而言 C 中的计算概念更加“抽象”,而这种抽象的计算概念通过 γ 有了一个在 D 中更加具体的实现。
但在此之上还有更进一步的结构可以考虑,在之前的文章中我们曾经提到过,Cmp 自然地构成了一个 2阶范畴 [2-category]。和函子间的自然变换类似,对于两个模拟 γ,δ:C → D ,我们有如下可计算转换 [computable transformation] 的概念:我们说可以将 γ-模拟可计算地转换为 δ-模拟,记为 γ⪯δ ,当对于任意 C 中的计算类型 σ ,存在 D 中的一个可计算函数 t∈D[γσ,δσ] 使得如下成立:
∀α∈C(σ),∀α'⊩γσ α.t(α')⊩δγα.(1)
熟悉自然变换概念的读者可以看出,其与可计算转换的概念有着相似性。但在考虑可计算转换时,我们只考虑这些可计算函数t∈D[γσ,δσ] 的存在性,而 t 本身不是可计算转换这个结构的一部分。这使得 C 到 D 的计算模拟这个集合构成了一个预序 [preorder],而不是像两个范畴之间的函子和自然变换那样是一个更为一般的范畴。我们之所以这样定义,是因为和之前定义弱笛卡尔积闭结构时类似,在计算模型中这样的可计算函数 t 通常并不具有唯一性, 在 D 中我们可以有很多不同的函数使得 γ 可以可计算地转换到 δ ,而在实际应用中我们只关心这样转换的可能性,而似乎并不关心具体转换实现的方式。因此,Cmp 是一个 preorder-enriched category,或者说一个任意两个 1-cell 之间的 2-cell 都同构的 2-category。
对于任意一个 2阶-范畴,我们都有一个自然的弱于同构的对等价的定义。以范畴为例,我们通常说两个范畴C,D 是等价的 [equivalent] 当我们有如下两个函子 F:C → D , G:D → C ,使得两边的复合并不直接等于 C,D 上的恒等函子,但和它们之间自然同构:
idᴄ≃GF,idᴅ≃FG (2)
同样的,在计算模型的语境下,我们说两个计算模型C,D 之间是等价的,当我们有两个计算模拟 γ:C → D , δ:D → C 使得它们满足
idᴄ≃δγ,idᴅ≃γδ (3)
其中,idᴄ≃δγ 表示 idᴄ ⪯ δγ 且 δγ ⪯ idᴄ 。因此,基于这个 2阶-范畴 Cmp 我们对计算模型之间的模拟和等价便有了一个完整地描述了。
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。