3,094
个编辑
更改
跳到导航
跳到搜索
第438行：
第438行： + + + + + + + +
→SRT与自指
'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，[[#证明|§5.2]] 的对角线证明就是你所需要的——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 停机统一为范畴论特例】【§[[#Lawvere 不动点定理（1969）|5.6.2]]】</ref>。
'''对读者的现实意义'''：如果你做的是[[程序语义]]、[[形式化验证]]、[[自指系统]]、[[AI反思架构]]等领域，理解 Lawvere 框架能让你看清'''为什么"自指"在这些领域无处不在'''——而不是递归论特有的怪癖。但若你只想用 SRT 构造自指程序做现实计算，[[#证明|§5.2]] 的对角线证明就是你所需要的——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 停机统一为范畴论特例】【§[[#Lawvere 不动点定理（1969）|5.6.2]]】</ref>。
==== λ演算视角：与 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与自指===
=== SRT与自指===