递归函数(三)
哥德尔在 1934 年春天访问普林斯顿大学时发表了这些讲座(Gödel 1934)。当时,丘奇和他的学生克莱尼和罗瑟已经在开发函数应用和抽象的形式系统方面取得了实质性进展,现在被称为无类型 lambda 演算。该系统还提供了一种将自然数表示为形式项的方法——即所谓的丘奇数字。这导致了函数可 lambda 定义的概念,其形式类似于 (9)。因此,丘奇的定义也刻画了一类与广义相对论形式相似的 lambda 可定义函数。在此期间,克莱尼证明了大量数论函数都包含在内,部分是通过展示如何在 lambda 演算中实现原始递归。这最终导致丘奇在 1934 年初提出,lambda 可定义函数与那些具有他称之为“有效可计算性”的性质的函数相一致。[17]
因此,一个自然的猜想是,lambda 可定义性在外延上与一般递归性相一致。与 (CT)(将非正式表征的函数类等同于具有精确数学定义的函数类)不同,语句 GR=� 可能允许形式化证明。Church (1936b) 给出了这样的证明,Kleene 1936b 对此进行了更详细的说明,提供了几个外延等价结果中的第一个,Kleene (1952: sec. 60, sec. 62) 最终将其引用为他提议称之为“Church 论文”的证据。
Church 论文是当代可计算性理论的基础,因为它证明了以下假设:通过研究相对于单一形式主义(例如 GR 或�)的可计算性,我们从而提供了一个一般性的说明,说明哪些外延函数在原则上可以通过算法有效计算,哪些不能。鉴于此,将一些额外的证据以 GR 与斯坦福百科全书中提出的其他几种计算形式等价的形式编入丘奇论题中将大有裨益:
设 � 为一致的、可计算的公理化理论,扩展 �(即罗宾逊算术)。那么,函数类 �� 可在 � 中表示,其意义如上所述(用 � 代替 �),且 ��=GR。(参见哥德尔不完备性定理和 Odifreddi (1989: ch. I.3) 中的可表示性。)
类 REC 由属于部分递归函数类(通过在无界最小化操作下关闭类 PR 而形成)的全函数组成,且 REC=GR。 (参见第 2.2.1 节和 Odifreddi [1989:第 I.2 章]。)
组合逻辑(与 lambda 演算相关的形式系统)中可表示的函数类 CL 满足 CL=GR。(参见组合逻辑条目和 Bimbó [2012:第 5.3 章中的可计算函数和算术。)
图灵机可计算的函数类 �(其定义的几种变体)满足 �=GR。(参见图灵机条目和 Odifreddi [1989:第 I.4 章中的可计算性替代历史模型。)
Shepherdson & Sturgis (1963) 引入的无限寄存器机可计算的函数类 �满足 �=GR。 (参见 Cutland [1980:第 1-3 章] 和 Cooper [2004:第 2 章]。)
这些形式的等价结果证明了 GR 类的数学稳健性,从而也证明了有效可计算性这一非正式概念本身的数学稳健性。正如我们所见,哥德尔最初是通过尝试分析递归定义的背景概念作为有效计算的模型而得出一般递归性的公式,这种分析受到 19 世纪末和 20 世纪初基础发展的启发。[18] 关于丘奇、图灵和波斯特的工作如何被视为提供独立动机的可计算性分析,这些分析也支持丘奇的论点,可以在 Gandy (1980) 和 Sieg (1994, 1997, 2009) 中找到进一步的讨论。
1.7 判定性问题和不可判定性
除了扩大哥德尔不完备性定理的范围之外,20 世纪 30 年代研究递归函数的另一个动机是研究所谓的不可判定(或不可解)问题。此类问题的原始例子是确定一阶逻辑的给定公式是否有效,即在其所有模型中都为真。希尔伯特和阿克曼在他们的教科书《理论逻辑学基本原理》(1928 年)中首次将其描述为一阶逻辑的判定问题(或决策问题):[19]
如果知道一个程序,可以通过有限多个操作判定给定逻辑表达式的普遍性 [即有效性] 或可满足性,则判定问题即可解决。判定问题的解决对于所有领域的理论都至关重要,这些领域的命题可以用有限多个公理进行逻辑描述。(希尔伯特和阿克曼 1928:73)[20]
这段话从另一个意义上说明了逻辑可推导性的可判定性问题与希尔伯特研究元数学的关注点有关。请注意,如果 Γ 是一组有限公理 {�1,…,��},那么 � 是否是 Γ 的逻辑结果的问题等同于句子 �=df(�1∧…∧��)→� 是否逻辑有效。根据一阶逻辑的哥德尔完备性定理(参见哥德尔词条),这等同于从 Hilbert & Ackermann 的一阶逻辑公理化中 � 的可推导性。因此,对判定问题的肯定回答可以解释为表明有可能将数学中对证明的搜索机械化,即允许我们通过算法确定表达开放问题的公式(例如黎曼假设)是否是足够强大的有限公理化理论(例如哥德尔-伯内斯集合论)的逻辑结果。
除了分析有效可计算性概念本身之外,图灵 (1937) 和丘奇 (1936a,b) 的数学目标是为判定问题提供一个数学上精确的否定答案。他们提供的答案可以理解为分为三个阶段:
通过第 1.3 节中描述的语法算术化方法,图灵和丘奇展示了判定问题如何与一组自然数 � 相关联。
然后他们从数学上证明了 � 是不可判定的,即其特征函数在形式意义上不可计算,分别相对于模型 � 或 �。
他们最后提出了进一步的论据,表明这些模型包含所有有效可计算函数,从而表明该函数在非正式意义上也是不可计算的。
第一步可以通过定义
�={⌜�⌝:� 在所有 ��-模型 � 中都是逻辑有效的}={⌜�⌝:�⊨�
其中 ⌜⋅⌝ 是 � 语言的哥德尔编号,如第 1.3 节所述。图灵和丘奇对判定性问题的否定回答的第二步依赖于他们先前对模型 �、� 和 GR 的类似决策问题的指定。他们与 Kleene (1936a) 一起证明了以下内容:
命题 1.1:以下集合的特征函数对于相关模型而言是不可计算的:
HP�={⟨�,�⟩:图灵机��在输入�时停止}
HP�={⌜�⌝:无类型�-项�具有规范形式}
HPGR={⌜�⌝:方程组�-项确定一般递归函数}
例如,命题 1.1 的第 i 部分表明,如果��在�时停止,则没有图灵机输出 1,否则输出 0。因此,这是图灵众所周知的停机问题不可解性的表述(参见图灵机条目)。第二部分和第三部分现在也被描述为表示集合 HP�、HP� 和 HPGR 都是不可判定的。通过考虑第 1.6 节中总结的等价结果,命题 1.1 表明,这些集合中的成员资格无法相对于任何相关模型来决定。
在此基础上,图灵(对于�)和丘奇(对于�和 GR)证明了以下内容:
命题 1.2:如果�是可判定的(相对于任何相关模型),那么 HP�、HP� 和 HP�� 也将是可判定的。
图灵和丘奇对这些事实的证明是建设性的,因为它们展示了如何有效地将其中一个模型的单个实例转换为一阶公式,使得该公式在且仅当该实例具有所讨论的属性时才有效——例如,给定一个图灵机��和输入�∈�,我们构造一个公式��,�,使得当且仅当��,�有效时,计算��(�)才会停止。因此,该方法预期了下面第 3.5.1 节中给出的多对一可约性的定义。
结合丘奇和图灵已经提出的支持丘奇论题的其他论据(见第 1.6 节),命题 1.1 和 1.2 可以表明判定问题确实不是希尔伯特和阿克曼 (1928) 描述的非正式意义上的可判定问题,即不能通过“使用有限多个操作的机械程序”来判定。正如我们将在第 3 节中看到的那样,希望开发一种关于此类不可判定结果及其相互关系的一般理论,这是从 20 世纪 40 年代开始进一步发展可计算性理论的重要动机。
1.8 递归函数理论和可计算性理论的起源
刚刚描述的发展构成了当代数理逻辑子领域的史前史的一部分,该子领域最初被称为递归函数理论(或更简单地称为递归理论)。该主题由克莱恩、图灵和波斯特在 20 世纪 30 年代末开始认真研究,直接基于第 1.6 节和 1.7 节中总结的包含等价性和不可判定性结果的论文。克莱恩的论文(1936a、1938、1943、1955a、b、c)尤为重要。这些论文分别包含部分递归函数的定义、它们与 GR 等价的证明、范式定理、递归定理以及算术和分析层次的定义。同样重要的是图灵的论文(1937 年、1939 年)(分别包含停机问题的不可判定性和图灵可约性的定义)和波斯特的论文(1944 年)(引入了多一和一对一可约性,并提出了后来被称为波斯特问题的问题)。
这些发展将在第 3 节中进行概述。正如我们将在那里看到的,可计算性理论早期阶段的一个重要主题是描述一种有效可计算性的概念,该概念能够支持基于对算法可计算性的直觉的严格证明,但它抽象出了第 1.6 节中提到的模型的细节。为此,在早期的教科书处理中(例如,Shoenfield 1967;Rogers 1987),哥德尔对一般递归方程的原始定义被克莱尼对部分递归函数的定义所取代,该定义采用第 2.2 节中介绍的无界最小化算子。这种表征又被后来教科书(例如 Soare 1987;Cutland 1980)中基于机器的表征所取代,例如 Turing (1937) 或 Shepherdson & Sturgis (1963) 的表征,其形式更接近非正式描述的计算机程序。
这些处理保留了对计算的理解,即以有效方式对有限组合对象进行操作,这些对象仍然可以理解为属于早期理论家 Skolem、Hilbert、Gödel 和 Péter 所理解的“递归思维模式”。但与此同时,递归函数理论中的许多基本定义和结果仅与本节中描述的非正式意义上的递归可定义性间接相关。鉴于此,Soare (1996) 建议将递归函数理论改名为可计算性理论,因此我们应将传统上称为递归函数的函数称为可计算函数。
这种术语变化在当代实践中得到了广泛采用,并反映在最近的教科书中,例如 Cooper (2004) 和 Soare (2016)。尽管如此,这两组术语仍然被广泛使用,特别是在哲学和历史资料中。因此,建议读者记住第 3 节开头的术语讨论。
2. 递归形式
注意:建议寻找递归函数数学概述的读者从这里开始。本节主要定义和结果的历史背景讨论可在第 1 节中找到。
本节介绍了可计算性理论中研究的主要递归定义函数类的定义。其中,原始递归函数 PR 和部分递归函数 PartREC 是最基本的。前者基于本条目介绍中描述的递归过程的形式化,几乎涵盖了普通数学中研究的所有数论函数。部分递归函数是通过在无界最小化操作(即搜索可判定谓词的最小见证)下关闭原始递归函数形成的。递归函数 REC 类(即在所有输入上定义的部分递归函数)传统上被认为通过 Church 论文(第 1.6 节)对应于可以通过算法有效计算的函数。
本条目的其余部分将使用以下概念惯例:
�={0,1,2,…} 表示自然数集,�� 表示 k 次叉积 �×…×�,�→ 表示固定数向量 �0,…,��−1(当元数从上下文中清楚时)。
小写罗马字母 �,�,ℎ,… 表示类型为 ��→�(对于某些 �)的函数 - 即具有定义域 �� 和值域 � 的函数类。对于固定的 �,�:��→� 表示 � 是 j 元函数(或具有元数 �) - 即 � 具有定义域 �� 和值域 �。小写希腊字母将类似地用于特殊函数(例如投影),如下所定义。
�0,�1,�2,… 用作 � 上的正式变量,用于指示函数的参数。 �,�,�,… 也将非正式地用于此列表中的任意变量。 �→ 将用于缩写变量向量 �0,…,��−1 (当元数从上下文中清楚时)。
粗体字母 �,�,�,… (或缩写,如 PR )将用于表示属于 ⋃�∈�(��→�) 子集的函数类。
书法字母 �,�,�,… (或缩写,如 Comp�� )将用于表示 ��→� 上的泛函——即将一个或多个类型为 ��→� (可能具有不同元数)的函数映射到其他函数的运算。
大写字母 �,�,�,… 将用于表示关系(即 �� 的子集),范围 �,�,�,… 保留用于表示一元关系(即 � 的子集)。
关系 �⊆�� 的特征函数表示为 ��(�0,…,��−1),即
��(�0,…,��−1)={1 if �(�0,…,��−1)0 if ¬�(�0,…,��−1)
2.1 原始递归函数 (PR)
2.1.1 定义
递归定义函数的类 � 可以通过给出初始函数类 �� 来指定,然后在类 Op� 中的一个或多个函数下关闭。通常可以在任意一组初始函数上以这种方式定义一个类。但是,本条目中考虑的所有函数类都将确定类型为��→�的函数,即,它们将以 k 元组自然数作为输入,并(如果已定义)返回单个自然数作为输出。
对于原始递归函数 PR,初始函数包括返回值 0(因此可以视为常量符号)的零元零函数 0,�(�) 表示一元后继函数 �↦�+1,�� 表示到第 � 个参数的 k 元投影函数(其中 0≤�<�),即
���(�0,…,��,…��−1)=��
此类函数将表示为�PR={0,�,���}。请注意,由于 ��� 对于每个 �,�∈� 都是一个不同的函数,因此 �PR 已经包含无数个函数。
PR 的函数是组合和原始递归的函数。组合采用元数为 � 的� 个函数 �0,…,��−1 和一个元数为 � 的单个函数 � 并返回它们的组合——即类型为 ��→� 的函数
ℎ(�0,…,��−1)=�(�0(�0,…,��−1),…,��−1(�0,…,��−1))
。例如,假设 � 是乘法函数 mult(�,�),�0 是常数 3 函数(我们可以认为它隐式地接受单个参数),�1(�) 是后继函数 �(�)。然后,�与�0 和 �1 的组合是一元函数 ℎ(�)=�(�0(�),�1(�))=����(3,�(�)) 我们通常将其表示为 3×(�+1)。
%00
%00组合运算可以理解为一类函数,对于每个�,�∈�,其输入为�个元数�的函数�0,…,��−1�和一个元数�的单个函数�,并返回以刚才说明的方式组合这些函数的k元函数ℎ作为输出。这由以下方案描述:
定义2.1:假设�:��→�和�0,…,��−1:��→�。则术语Comp��[�,�0,…,��−1]表示类型为��→�的函数
�(�0(�0,…,��−1),…,��−1(�0,…,��−1))
。
原始递归也是一种函数运算。在最简单的情况下,它通过采用单个一元函数 �(�) 和一个自然数 �∈� 来运行,并返回由以下定义的一元函数
(14)ℎ(0)=�ℎ(�+1)=�(ℎ(�))
在这样的定义中,第一个子句(称为基本情况)确定 ℎ 在 0 处的值,而第二个子句确定其在 �+1 处的值如何取决于其在 � 处的值。在这种情况下,很容易看出 � 的值决定了函数 � 在确定 ℎ 的值时迭代(即应用于自身)的次数。例如,如果 �=3 且 �(�)=�2,则 ℎ(�)=32�。
完整的原始递归方案以两种方式概括(14)。首先,它允许函数 ℎ 在 �+1 处的值不仅取决于其在 � 处的值,还取决于变量 � 本身的值。这导致了方案
(15)ℎ(0)=�ℎ(�+1)=�(�,ℎ(�))
例如,本条目介绍中定义的阶乘函数 fact(�) 的定义可以通过 (15) 获得,其中 �=1 并且
�(�0,�1)=����(�(�02(�0,�1)),�12(�0,�1))。
(14) 的第二个可能的推广是允许 ℎ 的值依赖于称为参数的辅助变量的有限序列,这些参数也可能是基本情况的参数。对于单个参数 � 的情况,这会导致以下方案
(16)ℎ(�,0)=�(�)ℎ(�,�+1)=�(�,ℎ(�,�))
例如,加法函数 add(�,�) 可以通过取 �(�0)=�0 和 �(�0,�1)=�(�1) 来定义。此定义也可以被认为是指定总和 �+� 是从初始值 � 开始迭代应用后继函数 � 次得到的值,方式与 (14) 相同。类似地,mult(�,�) 可以通过取 �(�0)=0 和 �(�0,�1)=���(�0,�1) 来定义。这将乘积“×”定义为从初始值 0 开始迭代将“×”添加到其参数“×”次的函数所获得的值。
因此,可以理解为提供用于计算如此定义的函数值的算法。[21] 观察到每个自然数“要么等于 0,要么是“+1”的形式,其中“+1”是某个“∈”。如果我们现在引入缩写“=”(“(“…(“(0))))”n 次,则将后继函数“应用于用“”表示的数字的结果将得出用“+1”表示的数字。因此,我们可以使用先前的加法递归定义来计算 �+� 的值,如下所示:
(17)add(2―,3―)=�(add(2―,2―))=�(�(���(2―,1―)))=�(�(�(add(2―,0―))))=�(�(�(2―)))=�(�(�(�(�(0)))))=5―
原始递归运算的完整定义将 (14) 的两个泛化合并为一个方案,该方案以 k 元函数 �、�+2 元函数 � 作为参数,并返回 �+1 元函数 ℎ 定义为如下
(18)ℎ(�0,…,��−1,0)=�(�0,…,��−1)ℎ(�0,…,��−1,�+1)=�(�0,…,��−1,�,ℎ(�0,…,��−1,�))