3,094
个编辑
更改
跳到导航
跳到搜索
第470行：
第470行： − + − + − + − | ! Lawvere 抽象范畴概念 !! 克林第二递归定理中的具体对应 |+ − + − + − + − + − + − + − + − + − + − + − + − + − + − + − + + + + + + + +
→与SRT的对应
{| class="wikitable"
{| class="wikitable"
|+ Lawvere定理与克林第二递归定理的对应
| + Lawvere定理与克林第二递归定理的对应 |
|-
| --- |
! Lawvere 抽象范畴概念
! 克林第二递归定理中的具体对应
| - |
|-
| 笛卡尔闭范畴 <math>\mathcal{(\mathcal{C})}</math> |
| 笛卡尔闭范畴 <math>\mathcal{C}</math>
| - |
| 部分递归函数范畴 <math>\mathbf{PartRec}</math>：对象为自然数幂 <math>\mathbb{N}^k</math>，态射为部分递归函数的外延等价类
| 对象 <math>A</math> |
|-
| - |
| 对象 <math>A</math>
| 对象 <math>Y</math> |
| 自然数集 <math>\mathbb{N}</math>，作为程序与函数的哥德尔编号论域
| - |
|-
| 指数对象 <math>Y^A</math> |
| 对象 <math>Y</math>
| - |
| 自然数集 <math>\mathbb{N}</math>，作为函数计算输出的值类型
| 弱点满射 <math>g : A \to Y^A</math> |
|-
| - |
| 指数对象 <math>Y^A</math>
| 自态射 <math>t : Y \to Y</math> |
| 全体一元部分递归函数构成的函数空间
| - |
|-
| 结论：<math>Y</math> 具有不动点性质 |
| 弱点满射 <math>g : A \to Y^A</math>
| } |
| 哥德尔编号机制：每个一元部分递归函数都对应至少一个自然数编码；通用图灵机可根据编码执行对应函数的计算
|-
| 自态射 <math>t : Y \to Y</math>
| 任意可计算的程序变换：对输出值的可计算操作，对应到函数编号上的递归变换
|-
| 结论：<math>Y</math> 具有不动点性质
| 对任意递归变换 <math>f</math>，都存在程序编号 <math>e</math>，使得 <math>\varphi_e \simeq \varphi_{f(e)}</math>（第二递归定理的标准表述）
|}
'''关系定性'''：
'''关系定性'''：