3,094
个编辑
更改
跳到导航
跳到搜索
第154行：
第154行： − +
→意义：递归定义的"存在性定理"
=== 意义：递归定义的"存在性定理" ===
=== 意义：递归定义的"存在性定理" ===
第一递归定理的角色，类似于分析学中用[[不动点定理]]（如 Banach 压缩映像原理）证明微分方程'''解的存在性'''：它一劳永逸地保证"机械式递归定义必有可计算的解"，从此定义递归函数时无需逐个证明合法性。Rogers 指出，"递归定理"这个名字正来源于此——它是"解递归方程"的定理，类比[[集合论]]中沿序数递归定义函数的原理<ref name="rogers1967" />。Kleene 本人甚至把第一递归定理视为支持 '''[[Church–Turing论题]]'''（"可计算 = 递归/图灵可计算"这一哲学论题）的最强证据之一：它表明"可计算函数"这个类恰好封闭于最一般的机械递归定义方式之下，不多也不少<ref name="moschovakis2010" />。
第一递归定理的角色，类似于分析学中用[[不动点定理]]（如 [[Banach压缩映射原理]]）证明微分方程'''解的存在性'''：它一劳永逸地保证"机械式递归定义必有可计算的解"，从此定理出发定义递归函数时，我们无需逐个证明合法性。Rogers 指出，"递归定理"这个名字正来源于此——它是"解递归方程"的定理，类比[[集合论]]中沿序数递归定义函数的原理<ref name="rogers1967" />。Kleene 本人甚至把第一递归定理视为支持 '''[[Church–Turing论题]]'''（"可计算 = 递归/图灵可计算"这一哲学论题）的最强证据之一：它表明"可计算函数"这个类恰好封闭于最一般的机械递归定义方式之下，不多也不少<ref name="moschovakis2010" />。
数学血统上，它是 '''[[Knaster–Tarski 不动点定理]]'''（[[序理论]]中"[[完备格]]上的[[单调映射]]必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。
数学血统上，它是 '''[[Knaster–Tarski 不动点定理]]'''（[[序理论]]中"[[完备格]]上的[[单调映射]]必有不动点"）在"可计算"约束下的有效化版本<ref name="rogers1967" />。