更改

'''背景'''：一个"程序变换"<math>\Phi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Phi(\phi)</math>。有两种实现方式：'''按代码操作'''（给 <math>\Phi</math> 输入 <math>\phi</math> 的程序编号，让它随便分析代码——类似"按名调用"）与'''按值操作'''（<math>\Phi</math> 只能查询 <math>\phi</math> 在具体输入上的输出，像黑盒——类似"按值调用"）。直觉上按代码操作更强大（能读源代码），但：

'''背景'''：一个"程序变换"<math>\Phi</math> 把函数 <math>\phi</math> 变成新函数 <math>\Phi(\phi)</math>。有两种实现方式：'''按代码操作'''（给 <math>\Phi</math> 输入 <math>\phi</math> 的程序编号，让它随便分析代码——类似"按名调用"）与'''按值操作'''（<math>\Phi</math> 只能查询 <math>\phi</math> 在具体输入上的输出，像黑盒——类似"按值调用"）。直觉上按代码操作更强大（能读源代码），但：

'''Myhill–Shepherdson 定理（1955）'''：对可计算变换而言，两种方式恰好等价——任何"按代码"的可计算变换都能改写成"按值"的图灵机计算，反之亦然<ref name="myhill1955" /><ref name="moschovakis2010" />.

'''[[Myhill–Shepherdson定理]]（1955）'''：对可计算变换而言，两种方式恰好等价——任何"按代码"的可计算变换都能改写成"按值"的图灵机计算，反之亦然<ref name="myhill1955" /><ref name="moschovakis2010" />.

证明的两个关键引理（变换必然是单调的、必然是连续的）都依赖 SRT：构造一个"监视 <math>\Phi</math> 是否已输出、在此之前模仿函数 <math>\phi_1</math>、之后叛变为函数 <math>\phi_2</math>"的程序 z——z 的行为取决于 z 自己（经 <math>\Phi</math> 处理后）的表现，由 SRT 提供，再用"同一函数的不同编号必须得到同一结果"逼出矛盾<ref name="moschovakis2010" />.

证明的两个关键引理（变换必然是单调的、必然是连续的）都依赖 SRT：构造一个"监视 <math>\Phi</math> 是否已输出、在此之前模仿函数 <math>\phi_1</math>、之后变为模拟函数 <math>\phi_2</math>"的程序 z，其中 z 的行为取决于 z 自己（经 <math>\Phi</math> 处理后）的表现，由 SRT 提供，再用"同一函数的不同编号必须得到同一结果"逼出矛盾<ref name="moschovakis2010" />。

'''Kreisel–Lacombe–Shoenfield–Čeĭnin 定理（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现<ref name="moschovakis2010" />.

'''[[Kreisel–Lacombe–Shoenfield–Čeĭnin定理]]（1957/1962）'''：作用在全函数上的可计算变换必然是'''连续'''的——输出在任何点的值只依赖输入函数的有限个值；而且可用确定性图灵机实现<ref name="moschovakis2010" />。

[[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''构造性分析'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。

[[尤里·切宁|Čeĭnin]] 的版本——"构造度量空间之间的每个可计算算子都是有效连续的"——是俄罗斯'''构造性分析'''学派（用可计算性重新奠基数学分析）的中心结果之一<ref name="moschovakis2010" />。证明中 SRT 出现两次，用法与上述如出一辙。