赖斯的定理

在计算理论中，稻米定理指出，程序的所有非平凡语义特性都是不可决定的。语义属性是关于程序行为的一种（例如，程序是否终止所有输入），与句法属性不同（例如，程序是否包含If-then-else语句）。如果每个程序既不正确，也不是每个程序的错误，则属性是不平凡的。

赖斯的定理也可以根据功能来提出：对于部分功能的任何非平凡属性，没有一般有效的方法可以决定算法是否使用该属性计算部分函数。在这里，如果部分函数具有所有部分可计算函数或无用的属性，则称为“微不足道” ，如果为每个算法正确决定正确决定，则称为“有效的决策方法”。该定理以亨利·戈登·赖斯（Henry Gordon Rice）的名字命名，亨利·戈登·赖斯（Henry Gordon Rice）在1951年在锡拉丘兹大学（Syracuse University）在1951年的博士学位论文中证明了这一点。

换句话说，它告诉我们，不可能创建一个计算机程序，该程序可以可靠地决定有关其他程序的某些有趣的事情。具体而言，当涉及程序在执行过程中的行为等方面时，没有通用方法来确定程序是否具有特定的，更复杂的性状。如果您有适用于正式语言的属性，并且至少有一个具有该属性的语言的示例，而没有一个属性，则确定给定的Turing机器是否具有该属性是一个不可决定的问题。

介绍

让P是非平凡的正式语言的属性，意思是

存在具有属性P的递归枚举语言，
存在一种递归枚举的语言，没有财产p ，

（也就是说，对于所有递归枚举的语言， P既不是统一的，也不是统一的错误）。

然后，对于给定的Turing Machine M ，确定它是否具有属性p是不可决定的。

在实践中，这意味着没有机器可以始终决定给定图灵机的语言是否具有特定的非平凡属性。特殊情况包括，例如，非平凡的简单机器（例如有限的自动机）是否可以识别出图灵机识别的语言的不可证明性（这意味着，图灵机的语言是否常规是不可否认的）。

重要的是要注意，大米的定理与机器或程序的特性无关；它涉及功能和语言的属性。例如，即使是非平凡的，机器是否在特定输入上运行100个以上的步骤都是可决定的。确定同一语言的两台不同的机器可能需要不同数量的步骤才能识别相同的输入字符串。同样，机器是否具有五个状态是机器的可决定性属性，因为可以简单地计算状态的数量。对于这种属性，它涉及一台图灵机，但不涉及它所识别的语言，赖斯的定理不适用。

利用罗杰斯对可接受的编程系统的表征，赖斯的定理可以从图灵机概括到大多数计算机编程语言：没有自动方法可以决定对计算机程序行为的一般性非平凡问题。

例如，考虑停止问题的以下变体。令P为一个参数的部分函数f的以下属性： p （ f ）意味着f是为参数“ 1”定义的。这显然是不平凡的，因为有部分函数定义为1，而其他函数则在1处。1-HALTING问题是确定任何算法是否使用此属性（IE，IE，IE）确定函数的问题算法是否停止输入1。通过RICE的定理，不可确定的问题。同样，Turing Machine T是否在最初空的磁带上终止（而不是以T的最初单词为w ，除了对T的描述（如在完整的停止问题中），但仍无法确定。

正式声明

让我们表示自然数，并表示一级（部分）可计算函数的类别。令可允许的计算函数编号。用ETH（部分）可计算函数表示。

我们确定可计算函数可能具有与该属性的功能组成的子集所具有的每个属性。因此，给定一个集合，可计算函数在且仅当时才具有属性。对于每个属性，都有一个相关的会员决策问题，即确定e，是否存在。

赖斯的定理指出，在且仅在或之后，决策问题是可决定的（也称为递归或计算）。

例子

根据Rice的定理，如果在特定的部分可计算函数的C类中至少有一个部分可计算函数，而另一个不在C中的部分可计算函数，则确定特定程序是否计算C中的函数是否无法确定的问题。例如，稻米定理表明，以下每一组部分可计算函数都是不可决定的（即，该集合不是递归的，或者不可计算的）：

每个输入及其补充的部分可计算函数类别返回0 。
至少一个输入及其补充的部分可计算函数类别返回0 。
恒定的部分可计算函数及其补体。
与给定的部分可计算函数相同的部分可计算函数及其补充。
某些输入及其补充的部分差异（即，未定义）的部分可计算函数类别。
总计可计算函数的索引类别。
递归枚举集合的指数类别。
递归递归集的索引索引类别。

克莱恩的递归定理证明

Kleene递归定理的推论指出，对于可计算函数和每个可计算函数的每个Gödel编号，都有一个索引，因此返回。（在下面，我们说“返回”如果或两者兼有，并且是未定义的。）直觉上是quine，是返回其源代码（gödel号）的函数，只是，除非直接返回它，否则Gödel号码并返回结果。

假设矛盾是一组可计算的函数。然后是可计算的功能。假设一组可决定的索引；然后，存在一个函数，可以返回if，否则。根据递归定理的推论，有一个索引返回。但是，如果，如果，那就与，因此是相同的功能；如果是，则是，因此。在这两种情况下，我们都有矛盾。

通过减少停止问题来证明

证明草图

假设为具体性，我们有一种用于检查程序P的算法，并确定p是否是平方函数的实现，该功能采用整数D并返回D ² 。如果我们有用于决定程序行为的任何其他非平凡属性（即语义和非平凡属性），并且通常在下面给出，则证明也同样有效。

主张是我们可以将算法转换为识别平方程序的算法，以识别停止功能的算法。我们将描述一种采用输入A和I的算法，并确定在给出输入i时是否停止程序。

用于决定这一点的算法在概念上很简单：它构造了一个新程序t的新程序t ，该参数n （1）首先执行输入i上的程序a （ a和我都被用硬编码为t的定义），（2）然后返回n的平方。如果a （ i ）永远运行，那么无论n如何然后清楚地， t是计算正方形的函数，并且仅当步骤（1）终止时。由于我们假设我们可以完全识别计算平方的程序，因此我们可以确定取决于A和I的T是否就是这样的程序；因此，我们获得了一个计划，该程序决定程序是否停止输入i 。请注意，我们的停止决策算法永远不会执行t ，而仅将其描述传递给平方识别程序，该程序始终通过假设终止；由于T的描述的构建也可以始终终止，因此停止决定也不能停止。

 halts (a,i) {
   define t(n) {
     a(i)
     return n×n
   }
   return is_a_squaring_function(t)
 }

此方法不具体取决于能够识别计算正方形的功能。只要某些程序可以做我们要识别的事情，我们就可以向A添加一个呼叫以获取我们的t 。我们本可以使用一种方法来识别用于计算方形根的程序，或用于计算每月工资单的程序，或者在给出输入时停止的程序"Abraxas";在每种情况下，我们都将能够类似地解决停止问题。

正式证明

为了进行形式证明，假定算法可以定义局部功能，并由字符串代表。由字符串A表示的算法计算得出的部分函数表示为f _a 。该证明是通过还原荒谬进行的：我们假设有一个非平凡的财产由算法决定，然后证明我们可以决定不可能的停止问题，这是不可能的，因此是矛盾的。

现在让我们假设p （ a ）是一种决定f _a的非平凡属性的算法。如果没有一般性的损失，我们可以假设p （ no-halt ）=“ no”，而无需halt是永不停止的算法的表示。如果这不是真的，那么这将适用于计算属性p的否定的算法p 。现在，由于P决定了一个非平凡的属性，因此有一个字符串B表示算法F _B和P （ B ）=“ Yes”。然后，我们可以定义算法h （ a ， i ），如下所示：

1.构造代表算法t （ j ）的字符串t

t首先模拟f _a （ i ）的计算
然后t模拟F _B （ J ）的计算并返回其结果。

2.返回p （ t ）。

现在，我们可以证明H决定停止问题：

假设以输入i的停止表示的算法。在这种情况下， f _t = f _b和，因为p （ b ）=“ yes ” ，并且p （ x ）的输出仅取决于f _x ， i ）=“是”。
假设由A表示的算法不会停止输入i 。在这种情况下， f _t = f t = f _to-halt ，即，从未定义的部分函数。由于p （ no-halt ）=“ no”，并且p （ x ）的输出仅取决于f _x ，因此p （ t ）=“ no”，因此， h （ a ， i ）=“ no”。

由于已知停止问题是无法确定的，因此这是一个矛盾，并且假设存在算法P （ a ）决定以A表示的函数的非平凡性质必须是错误的。

大米的定理和索引集

赖斯的定理可以用索引集简洁地说明：

令一类带有索引集的部分递归函数。然后仅在或时才是递归的。

这是一组自然数，包括零。

大米定理的递归套件的类似物

人们可以将稻米定理视为断言不可能有效地决定是否具有某种非平凡性质的任何递归列举的集合。在本节中，我们将稻米定理的类似物用于递归集，而不是递归列举的集合。大粗略地说，模拟说，如果可以有效地确定每个递归设置是否具有某个特性，那么只有有限的整数有限地确定递归集是否具有该属性。该结果类似于米的原始定理，因为这两种结果都断言属性是“可决定的”，只有当一个人可以通过检查最多有限的多数（对于原始定理），确定一组是否具有该属性，，如果属于集合。

让作为递归集的类（称为简单的游戏，被认为是属性）。如果是递归集，则对于某些可计算功能是特征函数。我们称为特征索引。（有很多这样的这样的这样的人。

如果是属于递归集的特征索引，则该算法给出“是”；
如果是不属于递归集的特征索引，则该算法给出“否”。

一组将延伸一个0和1的字符串，如果每个（长度），则为1的元素为1 if;否则是0。例如，扩展字符串。字符串正在赢得确定是否扩展的每个递归集属于。字符串正在丢失确定是否不属于递归集合。

现在，我们可以陈述以下稻米定理的类似物：

当且仅当有一组递归列出的丢失的确定字符串和递归枚举的获胜集确定字符串以使每个递归集以每个递归集的时间扩展字符串时，就可以计算一类递归集。

该结果已应用于计算社会选择的基本问题（更广泛地，算法游戏理论）。例如，库玛贝（Kumabe）和米哈拉（Mihara）将此结果应用于对合作游戏理论和社会选择理论中简单游戏的中村数字的调查。