更改

! SRT 实例化

! SRT 实例化

|-

|-

| Cartesian 闭范畴 C

| Cartesian 闭范畴 <math>C</math>

| 取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi:\mathbb{N}^k\rightarrow\mathbb{N}</math> 的等价类"，态射是可计算变换；或者更技术地说，<math>P_\omega</math> 或 K1 范畴（Gödel 编码的可计算函数论范畴）

| 取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi:\mathbb{N}^k\rightarrow\mathbb{N}</math> 的等价类"，态射是可计算变换；或者更技术地说，<math>P_\omega</math> 或 K1 范畴（Gödel 编码的可计算函数论范畴）

|-

|-

| 函子 F

| 函子 <math>F</math>

| 适当选取（C 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 F 取作"按编号 e 取 <math>\phi_e</math>" 的函子

| 适当选取（<math>C</math> 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 <math>F</math> 取作"按编号 <math>e</math> 取 <math>\phi_e</math>" 的函子

|-

|-

| 满射态射 f: A <math>\to F(A)</math>

| 满射态射 <math>f: A\to F(A)</math>

| 取定 §2.1 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 e 看作可枚举的元素、保证 F(A) 的每个元素都能表示为"以 f(e) 为参数的程序"，这一步在 SRT 证明中就是 §5.3 一行对角线 e <math>\mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）

| 取定 §2.1 中 <math>\phi_e</math> 的"自枚举"——把 <math>\phi_e</math> 编号 <math>e</math> 看作可枚举的元素、保证 <math>F(A)</math> 的每个元素都能表示为"以 <math>f(e)</math> 为参数的程序"，这一步在 SRT 证明中就是 §5.3 一行对角线 <math>e \mapsto \Phi_h(f(e), e)</math>（也称"自评价插值器"）

|-

|-

| 任意态射 g: F(A) <math>\to A</math>

| 任意态射 <math>g: F(A)\to A</math>

| 取 g = SRT 推论里那个'''给定的全可计算函数 f'''（"按它编程序"）。注意：SRT 表述要求 f: <math>\mathbb{N} \to \mathbb{N}</math> 是'''全'''可计算的——Lawvere 框架对应"f 处处有定义"这一约束，保证 g 在 F(A) 的全部范围内都有意义。

| 取 <math>g =</math> SRT 推论里那个'''给定的全可计算函数 <math>f</math>'''（"按它编程序"）。注意：SRT 表述要求 <math>f:\mathbb{N} \to \mathbb{N}</math> 是'''全'''可计算的——Lawvere 框架对应"<math>f</math> 处处有定义"这一约束，保证 <math>g</math> 在 <math>F(A)</math> 的全部范围内都有意义。

|-

|-

| 不动物 x: A <math>\to A</math>

| 不动物 <math>x: A\to A</math>

| 正是 SRT 给出的那个'''不动点编号 c'''——它满足 F(c) ∘ f = g ∘ f，即 <math>\phi_c = \phi_{f(c)}</math>

| 正是 SRT 给出的那个'''不动点编号 <math>c</math>'''——它满足 <math>F(c) \circ f = g \circ f</math>，即 <math>\phi_c = \phi_{f(c)}</math>

|}

|}

- 因此在写作时应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的[[对角线论证]]）。

- 因此在写作时应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的[[对角线论证]]）。

'''对读者的现实意义'''：如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容。<ref name="lawvere1969" />

'''对读者的现实意义'''：如果你做的是程序语义、形式化验证、自指系统、AI 反思架构等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969" />。

=== 自指现象：SRT 的"自指"一面 ===

=== 自指现象：SRT 的"自指"一面 ===