3,094
个编辑
更改
跳到导航
跳到搜索
第356行：
第356行： − − === λ演算视角：与 Y 组合子的关系 === − − <math>\lambda</math> 演算（Church 1930 年代发明的、Lisp 等函数式语言的祖先）中有一个著名对象 '''Y 组合子'''：对任何函数 <math>F</math>，<math>YF = F(YF)</math>，即 <math>Y</math> 直接生产出 <math>F</math> 的不动点，纯函数式地实现递归——它让匿名函数也能"引用自己"。 − − Kiselyov 在'''分阶段 <math>\lambda</math> 演算'''（staged lambda-calculus，区分"代码"与"值"两个阶段的现代元编程框架）中重构了第二递归定理，得出一个漂亮的结论：'''第二递归定理就是 Y 组合子的"带代码"推广'''——[[Y组合子]]给出函数层面的不动点，SRT 给出"程序 + 自身代码"层面的不动点；当把"代码"取为平凡编码（程序即自身）时，SRT 的构造精确退化为 Y 组合子<ref name="kiselyov" />。 − − 这一视角澄清了 SRT 对计算机科学的意义：'''它陈述的是"任何合理的程序系统对自指构造封闭"，是把高阶操作（程序变换）降阶到数据层面（编号）的不动点原理'''——部分求值（partial evaluation）、编译器自举（bootstrapping）、宏系统的理论基础。 − − === 与其它不动点定理的关系 === − − SRT 衍生出许多重要推论（见 §5.2），但还有些定理与 SRT 的关系'''更微妙'''——它们与 SRT '''同源'''（都基于对角线 / 自指），却走的是独立证明路线，或者处于更高层的[[范畴论]]概括下。这里集中讨论两个最重要的"不动点定理"：Gödel 的[[不动点引理]]与 [[F. William Lawvere|Lawvere]] 的范畴论不动点定理，重点说明 SRT 与它们的精确定位关系。 − − ==== Gödel 不动点引理（对角引理） ==== − − 对任何包含足够算术的递归可公理化理论 <math>T</math>，对 <math>T</math> 中任何公式 <math>\phi(x)</math>，都存在一个"不动点句子"<math>\psi</math>，使得 <math>T</math> 可证 <math>\psi\iff\phi</math>(⌜<math>\psi</math>⌝)。它的证明手法（对角线替换）与 SRT 同源，但 Gödel 早在 1931 年就独立给出了完整论证，'''SRT 推不出 Gödel 自身的不完备定理'''——Gödel 不完备的全部内容（[[一致性]]、[[ω-一致性]]、[[不可判定性]]三层）见 §5.7.4 的详述。 − − 注：'''Gödel 不动点引理本身是 SRT 最干净、最纯粹的推论'''（既可以把 SRT 当证明工具来证它，也可以两边都用"自指 + 对角线"的同源手法独立证明）。它和 SRT 的关系是"同源、互为推论"；但 Gödel 不完备'''定理'''与 SRT 的关系另当别论，见 §5.7.4 的"双重身份"分析。 − − ==== [[Lawvere 不动点定理]]（1969） ==== − − 这一定理是 SRT 所在的整个"对角线 / 自指"现象的'''[[范畴论]]统一视角'''。它告诉我们：SRT 不是孤立的递归论怪事，而是任何"足够自指的计算系统"都会涌现出的通用结构。下面先用范畴论语言表述，再讲清它和 SRT 的接口。 − − '''[[Lawvere定理]]（标准陈述）'''：设 '''<math>C</math>''' 是一个 ''[[Cartesian 闭范畴]]''（Cartesian closed category，"对象 = 数据类型、[[态射]] = 数据类型间可计算变换、函数空间本身也是对象、可以反复变换"的信息世界）。设 '''<math>F: C \to C</math>''' 是一个[[函子]]（"世界内部的一种自我变换"）。如果存在一个'''满射态射'''（surjective morphism，形象地说"覆盖了 <math>F(A)</math> 的全部出口"） − − : <math>f: A \to F(A)</math> （每个 <math>F(A)</math> 元素都被 <math>f</math> 的像源元素覆写） − − 那么对'''任意'''态射 <math>g: F(A)\to A</math>，都存在一个不动物 <math>x: A\to A</math>，使得 − − : <math> F(x) \circ f = g \circ f</math> − − 即顺着"<math>A\to F(A) \to A</math>"这条回路绕一圈，既可以按 <math>g</math> 走、也可以按 <math>F(x)</math> 走，'''两条路径等价'''。 − − '''直观解读'''：所谓"自指世界"，就是那种'''函数空间可以作为自身参数来研究'''的地方（Cartesian 闭）。在这种世界里，只要有一个"程序能撞出比自己更复杂的结果"的接口（[[满射]]态射），'''任何"全局选择函数"（<math>g</math>）都必有不动物'''——你的 <math>g</math> 想要把世界再次变换回自己，总会撞到某个无法再造新东西的点（<math>x</math>），而那个点正好让变换等于"再变换一次"（<math>F(x) = g</math>）。"自指 <math>\to </math>不动点"在这种世界里是不可避免的结构——不论那世界是自然数 + 可计算函数（Turing、Kleene），还是形式系统 + 可证性（Gödel），还是集合论宇宙（Russell、Cantor）。 − − '''SRT 是 Lawvere 的特例'''：把上述抽象框架特殊化到可计算函数的世界，就回到 SRT。具体的接口是： − − {| class="wikitable" − |- − ! Lawvere 抽象成分 − ! SRT 实例化 − |- − | Cartesian 闭范畴 <math>C</math> − | 取 ''Enf''——其对象是"一切部分可计算函数 <math>\phi:\mathbb{N}^k\rightarrow\mathbb{N}</math> 的等价类"，态射是可计算变换；或者更技术地说，<math>P_\omega</math> 或 K1 范畴（Gödel 编码的可计算函数论范畴） − |- − | 函子 <math>F</math> − | 适当选取（<math>C</math> 上的函子"程序 <math>\to </math>它自己的不动点集"），在 SRT 证明里通常把 <math>F</math> 取作"按编号 <math>e</math> 取 <math>\phi_e</math>" 的函子 − |- − | 满射态射 <math>f: A\to F(A)</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>（也称"自评价插值器"） − |- − | 任意态射 <math>g: F(A)\to A</math> − | 取 <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> 的全部范围内都有意义。 − |- − | 不动物 <math>x: A\to A</math> − | 正是 SRT 给出的那个'''不动点编号 <math>c</math>'''——它满足 <math>F(c) \circ f = g \circ f</math>，即 <math>\phi_c = \phi_{f(c)}</math> − |} − − '''关系定性'''： − − * [[#Lawvere 不动点定理（1969）|Lawvere 不动点定理]]'''不是''' SRT 的"推论"（该定理没有反推 SRT，而是反过来把 SRT 概括出来）； − * Lawvere 也不仅是 SRT 的"更高层次表述"（它是数学基础层面的定理，把 SRT、[[#Gödel 不动点引理（对角引理）|Gödel 不动点引理]]、Turing 停机问题的不可判定性、Russell 悖论、Cantor 对角线'''全部统一为这一个抽象结构的不同侧面'''）； − * 因此应避免两种过度描述：①"Lawvere 推翻了 SRT 的独立性"（错，它们不在一个抽象层）；②"SRT 是 Lawvere 的特例，所以 SRT 的定理就是 Lawvere 给出来的"（错，Lawvere 是更高层的解释，不是 SRT 证明的工具；SRT 证明仍然是 §5.3 的[[对角线论证]]）。 − − '''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，§5.3 的对角线证明就是你所需要的——Lawvere 对那条一行的构造不增加任何可计算内容<ref name="lawvere1969">'''Lawvere, F. W. (1969).''' Diagonal arguments and cartesian closed categories. In ''Category Theory, Homology Theory and their Applications III'', Lecture Notes in Mathematics, vol. 92, Springer.【Lawvere 不动点定理，把 SRT、Gödel 不完备、Turing 停机统一为范畴论特例】【§5.6.2】</ref>。
无编辑摘要
——按规则展开后，这个短语恰好指称'''它自己'''<ref name="rogers1967" /><ref name="moschovakis2010" />。
——按规则展开后，这个短语恰好指称'''它自己'''<ref name="rogers1967" /><ref name="moschovakis2010" />。