更改

=== 三种等价表述 ===

=== 三种等价表述 ===

'''表述 A（Kleene 原始形式，1938）'''：对任意可计算的部分函数 <math>\psi(z, x)</math>，存在编号 f 使得对所有 x：

* '''表述 A（Kleene 原始形式，1938）'''：对任意可计算的部分函数 <math>\psi(z, x)</math>，存在编号 <math>f</math> 使得对所有 <math>x</math>：

> <math>\phi_f(x) = \psi(f, x)</math>

: <math>\phi_f(x) = \psi(f, x)</math>

即：'''存在一个程序 f，它在输入 x 上的行为，恰好等于"把 f 自己的编号当作第一个参数喂给 <math>\psi</math>"的行为。''' 程序 f 在某种意义上"知道自己的代码"<ref name="kleene1938" />。

即：'''存在一个程序 <math>f</math>，它在输入 <math>x</math> 上的行为，恰好等于"把 <math>f</math> 自己的编号当作第一个参数喂给 <math>\psi</math>"的行为。''' 程序 <math>f</math> 在某种意义上"知道自己的代码"<ref name="kleene1938" />。

'''表述 B（Rogers 不动点形式，1967）'''：对任意可计算的'''全'''函数 f（程序变换规则），存在编号 n 使得：

* '''表述 B（Rogers 不动点形式，1967）'''：对任意可计算的'''全'''函数 <math>f</math>（程序变换规则），存在编号 <math>n</math> 使得：

> <math>\phi_n = \phi_{f(n)}</math>

: <math>\phi_n = \phi_{f(n)}</math>

这是 Rogers 的原话——"''Let f be any recursive function; then there exists an n such that <math>\phi_n = \phi_{f(n)}</math>.''"<ref name="rogers1967" />。意思是：f 拿着程序 n 的源代码算出一个新程序 f(n)，而'''新程序与旧程序计算的是同一个函数'''。<ref name="rogers1967" />

这是 Rogers 的原话——"''Let f be any recursive function; then there exists an n such that <math>\phi_n = \phi_{f(n)}</math>.''"<ref name="rogers1967" />。意思是：<math>f</math> 拿着程序 <math>n</math> 的源代码算出一个新程序 <math>f(n)</math>，而'''新程序与旧程序计算的是同一个函数'''。<ref name="rogers1967" />

'''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 y——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 e 的程序在参数 y 下的行为"。那么存在一个可计算的全函数 z：你输入 y，它就输出针对这个参数的不动点编号 z(y)，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 x 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 y 给出不同的编号（z 是'''单射'''，即一对一）。<ref name="rogers1967" /><ref name="moschovakis2010" />

* '''表述 C（带参数的强化形式）'''：A、B 只断言不动点"存在"，表述 C 进一步保证：不动点'''能被程序机械地找出来，并且能随参数连续变化'''。设想变换规则额外带一个参数 <math>y</math>——用一个三元函数 <math>\psi(e, y, x)</math> 表示"编号为 <math>e</math> 的程序在参数 <math>y</math> 下的行为"。那么存在一个可计算的全函数 <math>z</math>：你输入 <math>y</math>，它就输出针对这个参数的不动点编号 <math>z(y)</math>，使得 <math>\phi_{z(y)}(x) = \psi(z(y), y, x)</math> 对所有 <math>x</math> 成立。此外还能要求：①不动点不止一个，而是'''无穷多个'''；②不同参数 <math>y</math> 给出不同的编号（<math>z</math> 是'''单射'''，即一对一）。<ref name="rogers1967" /><ref name="moschovakis2010" />

=== 推论：SRT 衍生出的若干重要结果 ===

=== 推论：SRT 衍生出的若干重要结果 ===