验证自我实现的伪汇编的暂停问题
Verifying halting-problem on self-implemented pseudo-assembly
我写了一个非常简单的实现，可能与 Assembly/machine 代码相似。
它甚至可以递归，如本例所示：
9 6
IFEQ R0,0
RET 1
ENDIF
MOV R1,R0
SUB R1,1
CALL R1
MOV R2,R9
MUL R2,R0
RET R2
输出：720（6 的阶乘）
描述：
9 = Program Lines
6 = Program Input. Will be set to registry R0 value at class construction
CALL = calls the program again with the passed value (recursion)
RET = returns the program with the specified value. Sets registry R9 value to output value.
R0 to R9 -> general purpose registry.
R0 - program input value
R9 - program output value
-编辑：程序命令：
MOV, ADD, SUB, MUL, DIV, MOD, IFEQ, IFNEQ, IFG, IFGE, IFL, IFLE, ENDIF, CALL, RET
但是程序可以无限进入loop/recursion。例如：
2 0
CALL 10
RET 1 //will never be reached
如何验证我的程序是否会进入无限loop/recursion?
这是我的实现，不知道是否有必要，但以防万一。 （这是完整的代码......希望你不介意）。
#include <iostream>
#include <map>
#include <string> //std::getline
#include <sstream>
#include <vector>
namespace util
{
template<typename I>I readcin(I& input) {
std::cin >> input;
std::cin.clear(); std::cin.ignore();
return input;
}
template<typename I, typename...O> I readcin(I& input, O&... others) {
readcin(input);
return readcin(others...);
}
}
//operations
enum OP
{
MOV, ADD, SUB, MUL, DIV, MOD,
IFG, IFL,
IFEQ, IFGE, IFLE,
IFNEQ,
CALL,
RET,
ENDIF,
};
std::map<std::string, OP> OPTABLE
{
{"MOV", MOV}, {"ADD", ADD}, {"SUB", SUB}, {"MUL", MUL}, {"DIV", DIV}, {"MOD", MOD},
{"RET", RET},
{"IFG", IFG}, {"IFL", IFL},
{"IFNEQ", IFNEQ}, {"IFEQ", IFEQ}, {"IFGE", IFGE}, {"IFLE", IFLE},
{"CALL", CALL},
{"ENDIF", ENDIF}
};
//registry index
enum RI
{
R0, R1, R2, R3, R4, R5, R6, R7, R8, R9, RI_MAX
};
std::map<std::string, RI> RITABLE =
{
{"R0", R0}, {"R1", R1}, {"R2", R2}, {"R3", R3}, {"R4", R4}, {"R5", R5},
{"R6", R6}, {"R7", R7}, {"R8", R8}, {"R9", R9}
};
struct Instruction
{
OP op;
RI r1;
int r2value;
Instruction() = delete;
Instruction(OP operation, RI firstRegister, int _2ndRegValue = -1)
{
op = operation;
r1 = firstRegister;
r2value = _2ndRegValue;
}
};
class Assembly
{
private:
int REG[RI::RI_MAX] {0};
int GetRegistryValue(RI ri) const { return REG[ri]; }
void SetRegistryValue(RI ri, int val) { REG[ri] = val; }
enum CMP_FLAG{ CMP_FAIL, CMP_OK };
CMP_FLAG flag { CMP_OK };
CMP_FLAG GetFlag() const { return flag; }
void SetFlag(bool setFlag) { flag = static_cast<CMP_FLAG>(setFlag); }
std::vector<std::string> programLines;
OP ExtractOP(const std::string& line);
RI ExtractRI(const std::string& line, OP op);
int Extract2ndRIval(const std::string& line, OP op);
public:
void addCommand(const std::string& line) { programLines.push_back(line); }
void Execute();
Assembly() = delete;
Assembly(int inputValue) { REG[R0] = inputValue; }
int ReturnValue() const { return REG[R9]; }
private:
//recursion only
Assembly(int inputValue, const std::vector<std::string>& progLines) {
REG[R0] = inputValue;
programLines = progLines;
this->Execute();
}
};
OP Assembly::ExtractOP(const std::string& line)
{
std::istringstream issline{ line };
std::string operation;
issline >> operation;
return OPTABLE[operation];
}
RI Assembly::ExtractRI(const std::string& line, OP op)
{
auto space = line.find(' ');
if(op <= IFNEQ){
auto comma = line.find(',');
return RITABLE[std::string(line.begin() + space + 1, line.begin() + comma)];
}
return RI_MAX;
}
int Assembly::Extract2ndRIval(const std::string& line, OP op)
{
if(op == ENDIF) {
return -1;
}
std::size_t spaceOrComma;
if(op == CALL || op == RET) {
spaceOrComma = line.find(' ');
} else {
spaceOrComma = line.find(',');
}
std::string opval = std::string(line.begin() + spaceOrComma + 1, line.end());
auto it = RITABLE.find(opval);
if(it != RITABLE.end()){
return this->REG[it->second];
}
auto num = std::atoi(opval.c_str());
return num;
}
void Assembly::Execute()
{
for(const std::string& line : programLines)
{
OP op = ExtractOP(line);
RI r1 = ExtractRI(line, op);
int r2value = Extract2ndRIval(line, op);
Instruction command ( op, r1, r2value );
if(GetFlag() == CMP_FAIL)
{
if(command.op == ENDIF){
SetFlag(CMP_OK);
}
continue;
}
switch(command.op)
{
case MOV: { SetRegistryValue(command.r1, command.r2value); } break;
case ADD: { SetRegistryValue(command.r1, REG[command.r1] + command.r2value); } break;
case SUB: { SetRegistryValue(command.r1, REG[command.r1] - command.r2value); } break;
case MUL: { SetRegistryValue(command.r1, REG[command.r1] * command.r2value); } break;
case DIV: { SetRegistryValue(command.r1, REG[command.r1] / command.r2value); } break;
case MOD: { SetRegistryValue(command.r1, REG[command.r1] % command.r2value); } break;
case IFEQ: { SetFlag(GetRegistryValue(command.r1) == command.r2value); } break;
case IFNEQ: { SetFlag(GetRegistryValue(command.r1) != command.r2value); } break;
case IFG: { SetFlag(GetRegistryValue(command.r1) > command.r2value); } break;
case IFL: { SetFlag(GetRegistryValue(command.r1) < command.r2value); } break;
case IFGE: { SetFlag(GetRegistryValue(command.r1) >= command.r2value); } break;
case IFLE: { SetFlag(GetRegistryValue(command.r1) <= command.r2value); } break;
case RET:
{
SetRegistryValue(R9, command.r2value);
return;
}break;
//oh boy!
case CALL:
{
// std::cout << "value to call:" << command.r2value << std::endl;
Assembly recursion(command.r2value, this->programLines);
SetRegistryValue(R9, recursion.ReturnValue());
}break;
}
}
}
int main()
{
while(true)
{
int pl, input;
util::readcin(pl, input);
if(pl == 0){
break;
}
Assembly Asm(input);
for(auto i=0; i<pl; ++i)
{
std::string line;
std::getline(std::cin, line);
Asm.addCommand(line);
}
Asm.Execute();
std::cout << Asm.ReturnValue() << std::endl;
}
return 0;
}
How do I verify whether a program will enter into an infinite loop/recursion?
实践中；停机问题很容易解决。这在理论上是不可能的。
人们认为停机问题无法解决的原因是该问题被构造为错误的困境 (https://en.wikipedia.org/wiki/False_dilemma)。具体来说;这个问题要求确定一个程序是否总是会停止或永远不会停止；但还有第三种可能性——有时会停止（有时不会停止）。例如，假设有一个程序询问用户是要永远停止还是立即退出（并正确执行用户请求的操作）。请注意，所有理智的应用程序都是这样的 - 它们不应该退出 until/unless 用户告诉他们。
更正确；实际上，有 4 种可能性：
- 运行直到外部原因导致它停止（电源关闭、硬件故障、
kill -9、...）
- 有时会自行停止
- 总是自己停止
- 不确定（无法确定是其他 3 种情况中的哪一种）
当然有这 4 种可能性，你可以说你已经创建了一个 "halting problem solver" 只是通过将每个程序分类为 "indeterminate"，但这不是一个好的解决方案。这给了我们一种评级系统——极好的 "halting problem solvers" 很少将节目分类为 "indeterminate"，极差的 "halting problem solvers" 经常将节目分类为 "indeterminate"。
所以；你如何创造一个好的"halting problem solver"？这涉及两个部分——为整个程序生成控制流图（ https://en.wikipedia.org/wiki/Control-flow_graph ) for each function and a call graph ( https://en.wikipedia.org/wiki/Call_graph ）；和价值追踪。
控制流图和调用图
为每个function/procedure/routine生成控制流图并不难，只需检查控制流指令（调用、return、跳转、条件分支）即可；在执行此操作时生成调用图并不难（只需在看到调用指令时检查节点是否已在调用图中，如果不存在则添加它）。
在执行此操作时，您想将控制流更改（在每个函数的控制流图中）标记为 "conditional" 或 "not conditional"，并且您想标记函数（在调用图中对于整个程序）作为 "conditional" 或 "not conditional".
通过分析结果图，您可以将普通程序分类为 "runs until something external causes it to halt" 或 "always halts itself"（例如，这足以将 OP 的原始代码分类为 "runs until something external causes it to halt"）；但大多数程序仍将是 "indeterminate".
价值追踪
价值跟踪是（试图）跟踪在任何时间点可能位于任何 register/variable/memory 位置的可能值。例如，如果一个程序从磁盘读取 2 个无符号字节到 2 个单独的变量中，您知道这两个变量的值将从 0 到 255。如果将这些变量相乘，您知道结果将是从 0*0 到 255*255 的值;如果添加了这些变量，您知道结果将是一个从 0+0 到 255+255 的值；等等。当然，变量的类型给出了绝对的最大可能范围，即使对于汇编（没有类型的地方）也是如此 - 例如（不知道它是有符号的还是无符号的）你知道从内存中读取 32 位将 return 一个从 -2147483648 到 4294967296 的值。
价值跟踪的要点是为每个功能在控制流图中注释条件分支；这样您就可以使用这些注释来帮助将程序分类为 "indeterminate".
以外的东西
这就是事情变得棘手的地方 - 提高 "practical halting problem solver" 的质量需要增加价值跟踪的 sophistication/complexity。我不知道是否有可能写出一个完美的 "halting problem solver"（永远不会 returns "indeterminate"），但我知道有可能写出一个足够的 "halting problem solver"对于几乎所有实际目的（returns "indeterminate" 很少有人关心）。
如果程序两次进入相同的配置，那么它将永远循环下去。
图灵机也是如此，只是（无限）输入是机器配置的一部分。
这也是泵引理背后的直觉。
模型中的配置是什么？
由于您没有内存也没有 IO，因此配置由寄存器的内容和当前指令的行号（即指令指针）给出。
什么时候更改配置？
在每条指令之后，当然。但是在非分支指令的情况下，它前后的配置肯定是不同的因为即使指令是NOP，行号也改变了
在分支的情况下，行号可能是我们之前看到的行号（对于向后分支），因此机器可以从那里进入相同的配置。
对我来说，唯一感兴趣的跳跃指令似乎是call。 IF 类似的总是会产生不同的配置，因为它们的表现力不足以产生迭代（跳回并重复）。
call 如何更改配置？它将行号设置为 1 并将所有寄存器（r0 除外）设置为零。
因此调用产生相同配置的条件减少为具有相同的输入。
如果您检查，在 call 实现中，操作数值是否已经在之前（在模拟中）使用过，那么您可以判断程序将永远循环。
如果一个寄存器的大小是n，那么可能的状态就是O(2n)，一般是很多。
您必须准备好在达到（可能可定制的）阈值后放弃。或者在您的寄存器为 int 的情况下，大多数 C++ 实现具有 32 位 int，而现代机器可以处理 2^32 位的 512MiB 位图。 （例如，std::vector<bool> 实现打包位图；使用 unsigned 对其进行索引以避免负整数）。散列 table 是另一种选择 (std::unordered_set<int>)。但是，如果您为寄存器使用更广泛的类型，则状态将太大而无法实际记录每一个可能的类型，您将需要一些限制。限制是您的实现中内置的一种限制，因为您将在看到被模拟机器的 2^32 次重复附近的任何地方之前溢出 C++ 调用堆栈（C++ 递归深度）。
如果寄存器的值是无限的，这就减少了停机问题，因此在一般情况下是不可判定的。 （但正如@Brendan 所说，您仍然可以寻找状态的早期重复；许多程序将以一种简单的方式终止或无限重复。）
如果您将 call 实现更改为不将其他寄存器置零，则必须回退以检查调用站点的整个配置（而不仅仅是操作数）。
要检查每个输入的程序终止，您必须非确定性和符号性。
有两个问题：分支和输入值。
一个著名的定理是，一个TM可以以指数级的步数模拟一个NDTM w.r.t。 NDTM的步骤。
唯一有问题的指令是 IF 指令，因为它们会产生不确定性。
您可以采取多种方法：
- 将模拟分成两个分支。一个执行 IF 一个不执行。
- 重写要模拟的代码以生成指数级（以分支数计）数量的无分支代码变体。您可以延迟生成它们。
- 保留一棵配置树，程序中的每个分支在树的当前节点中生成两个子节点。
它们都是等价的。
输入值未知，因此很难判断 call 是否以相同的配置结束。
一种可能的方法是记录对输入寄存器的所有更改，例如，您最终可能会得到类似 "sub(add(add(R0, 1), 4), 5);".
的描述
这个描述应该很容易操作，因为在上面的例子中很容易看到 R0 没有改变，因为你得到 "sub(add(R0, 5), 5);" 然后 "R0;".
这依赖于算术定律，你必须注意逆运算、标识元素 (1 * a = a) 和溢出。
基本上，您需要简化表达式。
然后您可以检查输入是否在模拟时间内的给定时间点发生了变化。
在一般情况下，检查程序是否陷入无限循环的唯一方法是检查程序是否进入了与先前状态相同的状态。如果它之前进入了完全相同的状态，那么它必须继续执行循环 returning 到相同的状态，按照相同的步骤序列。在实际程序中，这基本上是不可能的，因为程序可能处于大量可能的状态，但您的汇编语言只允许更有限数量的可能状态。
由于您的 CALL 指令就像在开始时调用程序一样工作，并且这是唯一的循环形式，这意味着检查代码是否两次进入相同状态很简单。带有特定参数的 CALL 指令与以该参数作为输入调用程序具有完全相同的效果。如果 CALL 指令与任何先前执行的 CALL 指令或程序的输入值具有相同的参数，则它必须在循环中无限地继续执行 returning 以相同的步骤序列进入相同的状态。
换句话说，唯一需要检查的状态是程序开始时的R0值。由于这个值存储在 int 中，它在任何常见的 C++ 实现中只能有 2^32 个可能的值，因此暴力检查是否合理且容易地检查具有给定输入的给定程序是否陷入无限环形。
事实上，可以使用 return 值中的 memoization 在 O(N) 时间和 O(N) space 中强制检查所有可能的输入，其中N 是可能输入的数量。有多种方法可以做到这一点，但我会这样做的方法是创建三个向量，所有向量的元素数量都等于可能的输入数量。第一个向量是一个bool（位）向量，记录给定的输入是否已经被记忆，第二个向量也是bool向量，它记录给定的输入是否已经被使用过调用堆栈，第二个向量是记录结果的 int 向量，并使用输入值的链表创建调用堆栈以保存 space。 （在下面的代码中，这些向量分别被称为 is_memoized、input_pending 和 memoized_value。）
我会把你的解释器循环重写为非递归的，类似于这样的伪代码：
input = reg[R0]
if is_memoized[input]:
reg[R9] = memoized_value[input]
return
input_pending[input] = true
memoized_value[input] = input // mark the top of the stack
while true:
for command in program:
...
if command.op == CALL:
argument = command.r2value
if input_pending[argument]:
// Since this input value is ready been used as input value
// somewhere on the call stack this the program is about to enter
// an identical state as a previous state and so is stuck in
// a infinite loop.
return false // program doesn't halt
if is_memoized[argument]:
REG[R9] = memoized_value[argument]
else:
memoized_value[argument] = input // stack the input value
input = argument
REG = [input, 0, 0, 0, 0, 0, 0, 0, 0, 0]
input_pending[input] = true
break // reevaluate the program from the beginning.
if command.op == RET:
argument = command.r2value
stacked_input = memoized_value[input]
input_pending[input] = false
if stacked_input == input: // at the top of the stack
REG[R9] = argument
return true // program halts for this input
is_memoized[input] = true
memoized_value[input] = argument
input = stacked_input
REG = [input, 0, 0, 0, 0, 0, 0, 0, 0, 0]
break // reevaluate the program from the beginning
然后您将为每个可能的输入调用此解释器循环，如下所示：
for i in all_possible_inputs:
if not program.execute(input = i): // the function written above
print "program doesn't halt for all inputs"
return
print "program halts for all inputs"
递归版本应该更快，因为它不必在程序中的每个未记忆的 CALL 指令上重新评估程序，但在最坏的情况下需要数百 GB 的堆栈 space。这个非递归版本只需要 17 GB 内存。无论哪种方式，它仍然是 O(N) space 和时间，你只是让一个常数因子变小，另一个常数因子变大。
为了在合理的时间内执行此代码，您可能还需要解析一次代码，然后执行一些字节代码表示。
我认为您正在寻找跳出框框的思维方式。
这样想一下停机问题。图灵证明的程序是不受控制的。但为什么？因为语言有控制执行的指令。这意味着在程序中可行地调节和预测执行需要从语言中删除所有控制语义。
即使是我的协作流程架构也无法做到这一点。它只是因为他们造成的混乱而禁止他们。它仍然由包含它们的语言组成。例如，您可以使用 IF 来中断、return 或继续，但不能用于其他操作。函数调用是非法的。我创建了这样的限制以实现可控性。然而，即使是协作组织也不会从语言中删除控制结构以防止其被滥用。
我的架构通过我的个人资料在线，在我的 W 文章中有一个阶乘示例。
我写了一个非常简单的实现，可能与 Assembly/machine 代码相似。
它甚至可以递归，如本例所示：
9 6
IFEQ R0,0
RET 1
ENDIF
MOV R1,R0
SUB R1,1
CALL R1
MOV R2,R9
MUL R2,R0
RET R2
输出：720（6 的阶乘）
描述：
9 = Program Lines
6 = Program Input. Will be set to registry R0 value at class construction
CALL = calls the program again with the passed value (recursion)
RET = returns the program with the specified value. Sets registry R9 value to output value.
R0 to R9 -> general purpose registry.
R0 - program input value
R9 - program output value
-编辑：程序命令：
MOV, ADD, SUB, MUL, DIV, MOD, IFEQ, IFNEQ, IFG, IFGE, IFL, IFLE, ENDIF, CALL, RET
但是程序可以无限进入loop/recursion。例如：
2 0
CALL 10
RET 1 //will never be reached
如何验证我的程序是否会进入无限loop/recursion?
这是我的实现，不知道是否有必要，但以防万一。 （这是完整的代码......希望你不介意）。
#include <iostream>
#include <map>
#include <string> //std::getline
#include <sstream>
#include <vector>
namespace util
{
template<typename I>I readcin(I& input) {
std::cin >> input;
std::cin.clear(); std::cin.ignore();
return input;
}
template<typename I, typename...O> I readcin(I& input, O&... others) {
readcin(input);
return readcin(others...);
}
}
//operations
enum OP
{
MOV, ADD, SUB, MUL, DIV, MOD,
IFG, IFL,
IFEQ, IFGE, IFLE,
IFNEQ,
CALL,
RET,
ENDIF,
};
std::map<std::string, OP> OPTABLE
{
{"MOV", MOV}, {"ADD", ADD}, {"SUB", SUB}, {"MUL", MUL}, {"DIV", DIV}, {"MOD", MOD},
{"RET", RET},
{"IFG", IFG}, {"IFL", IFL},
{"IFNEQ", IFNEQ}, {"IFEQ", IFEQ}, {"IFGE", IFGE}, {"IFLE", IFLE},
{"CALL", CALL},
{"ENDIF", ENDIF}
};
//registry index
enum RI
{
R0, R1, R2, R3, R4, R5, R6, R7, R8, R9, RI_MAX
};
std::map<std::string, RI> RITABLE =
{
{"R0", R0}, {"R1", R1}, {"R2", R2}, {"R3", R3}, {"R4", R4}, {"R5", R5},
{"R6", R6}, {"R7", R7}, {"R8", R8}, {"R9", R9}
};
struct Instruction
{
OP op;
RI r1;
int r2value;
Instruction() = delete;
Instruction(OP operation, RI firstRegister, int _2ndRegValue = -1)
{
op = operation;
r1 = firstRegister;
r2value = _2ndRegValue;
}
};
class Assembly
{
private:
int REG[RI::RI_MAX] {0};
int GetRegistryValue(RI ri) const { return REG[ri]; }
void SetRegistryValue(RI ri, int val) { REG[ri] = val; }
enum CMP_FLAG{ CMP_FAIL, CMP_OK };
CMP_FLAG flag { CMP_OK };
CMP_FLAG GetFlag() const { return flag; }
void SetFlag(bool setFlag) { flag = static_cast<CMP_FLAG>(setFlag); }
std::vector<std::string> programLines;
OP ExtractOP(const std::string& line);
RI ExtractRI(const std::string& line, OP op);
int Extract2ndRIval(const std::string& line, OP op);
public:
void addCommand(const std::string& line) { programLines.push_back(line); }
void Execute();
Assembly() = delete;
Assembly(int inputValue) { REG[R0] = inputValue; }
int ReturnValue() const { return REG[R9]; }
private:
//recursion only
Assembly(int inputValue, const std::vector<std::string>& progLines) {
REG[R0] = inputValue;
programLines = progLines;
this->Execute();
}
};
OP Assembly::ExtractOP(const std::string& line)
{
std::istringstream issline{ line };
std::string operation;
issline >> operation;
return OPTABLE[operation];
}
RI Assembly::ExtractRI(const std::string& line, OP op)
{
auto space = line.find(' ');
if(op <= IFNEQ){
auto comma = line.find(',');
return RITABLE[std::string(line.begin() + space + 1, line.begin() + comma)];
}
return RI_MAX;
}
int Assembly::Extract2ndRIval(const std::string& line, OP op)
{
if(op == ENDIF) {
return -1;
}
std::size_t spaceOrComma;
if(op == CALL || op == RET) {
spaceOrComma = line.find(' ');
} else {
spaceOrComma = line.find(',');
}
std::string opval = std::string(line.begin() + spaceOrComma + 1, line.end());
auto it = RITABLE.find(opval);
if(it != RITABLE.end()){
return this->REG[it->second];
}
auto num = std::atoi(opval.c_str());
return num;
}
void Assembly::Execute()
{
for(const std::string& line : programLines)
{
OP op = ExtractOP(line);
RI r1 = ExtractRI(line, op);
int r2value = Extract2ndRIval(line, op);
Instruction command ( op, r1, r2value );
if(GetFlag() == CMP_FAIL)
{
if(command.op == ENDIF){
SetFlag(CMP_OK);
}
continue;
}
switch(command.op)
{
case MOV: { SetRegistryValue(command.r1, command.r2value); } break;
case ADD: { SetRegistryValue(command.r1, REG[command.r1] + command.r2value); } break;
case SUB: { SetRegistryValue(command.r1, REG[command.r1] - command.r2value); } break;
case MUL: { SetRegistryValue(command.r1, REG[command.r1] * command.r2value); } break;
case DIV: { SetRegistryValue(command.r1, REG[command.r1] / command.r2value); } break;
case MOD: { SetRegistryValue(command.r1, REG[command.r1] % command.r2value); } break;
case IFEQ: { SetFlag(GetRegistryValue(command.r1) == command.r2value); } break;
case IFNEQ: { SetFlag(GetRegistryValue(command.r1) != command.r2value); } break;
case IFG: { SetFlag(GetRegistryValue(command.r1) > command.r2value); } break;
case IFL: { SetFlag(GetRegistryValue(command.r1) < command.r2value); } break;
case IFGE: { SetFlag(GetRegistryValue(command.r1) >= command.r2value); } break;
case IFLE: { SetFlag(GetRegistryValue(command.r1) <= command.r2value); } break;
case RET:
{
SetRegistryValue(R9, command.r2value);
return;
}break;
//oh boy!
case CALL:
{
// std::cout << "value to call:" << command.r2value << std::endl;
Assembly recursion(command.r2value, this->programLines);
SetRegistryValue(R9, recursion.ReturnValue());
}break;
}
}
}
int main()
{
while(true)
{
int pl, input;
util::readcin(pl, input);
if(pl == 0){
break;
}
Assembly Asm(input);
for(auto i=0; i<pl; ++i)
{
std::string line;
std::getline(std::cin, line);
Asm.addCommand(line);
}
Asm.Execute();
std::cout << Asm.ReturnValue() << std::endl;
}
return 0;
}
How do I verify whether a program will enter into an infinite loop/recursion?
实践中；停机问题很容易解决。这在理论上是不可能的。
人们认为停机问题无法解决的原因是该问题被构造为错误的困境 (https://en.wikipedia.org/wiki/False_dilemma)。具体来说;这个问题要求确定一个程序是否总是会停止或永远不会停止；但还有第三种可能性——有时会停止（有时不会停止）。例如，假设有一个程序询问用户是要永远停止还是立即退出（并正确执行用户请求的操作）。请注意，所有理智的应用程序都是这样的 - 它们不应该退出 until/unless 用户告诉他们。
更正确；实际上，有 4 种可能性：
- 运行直到外部原因导致它停止（电源关闭、硬件故障、
kill -9、...） - 有时会自行停止
- 总是自己停止
- 不确定（无法确定是其他 3 种情况中的哪一种）
当然有这 4 种可能性，你可以说你已经创建了一个 "halting problem solver" 只是通过将每个程序分类为 "indeterminate"，但这不是一个好的解决方案。这给了我们一种评级系统——极好的 "halting problem solvers" 很少将节目分类为 "indeterminate"，极差的 "halting problem solvers" 经常将节目分类为 "indeterminate"。
所以；你如何创造一个好的"halting problem solver"？这涉及两个部分——为整个程序生成控制流图（ https://en.wikipedia.org/wiki/Control-flow_graph ) for each function and a call graph ( https://en.wikipedia.org/wiki/Call_graph ）；和价值追踪。
控制流图和调用图
为每个function/procedure/routine生成控制流图并不难，只需检查控制流指令（调用、return、跳转、条件分支）即可；在执行此操作时生成调用图并不难（只需在看到调用指令时检查节点是否已在调用图中，如果不存在则添加它）。
在执行此操作时，您想将控制流更改（在每个函数的控制流图中）标记为 "conditional" 或 "not conditional"，并且您想标记函数（在调用图中对于整个程序）作为 "conditional" 或 "not conditional".
通过分析结果图，您可以将普通程序分类为 "runs until something external causes it to halt" 或 "always halts itself"（例如，这足以将 OP 的原始代码分类为 "runs until something external causes it to halt"）；但大多数程序仍将是 "indeterminate".
价值追踪
价值跟踪是（试图）跟踪在任何时间点可能位于任何 register/variable/memory 位置的可能值。例如，如果一个程序从磁盘读取 2 个无符号字节到 2 个单独的变量中，您知道这两个变量的值将从 0 到 255。如果将这些变量相乘，您知道结果将是从 0*0 到 255*255 的值;如果添加了这些变量，您知道结果将是一个从 0+0 到 255+255 的值；等等。当然，变量的类型给出了绝对的最大可能范围，即使对于汇编（没有类型的地方）也是如此 - 例如（不知道它是有符号的还是无符号的）你知道从内存中读取 32 位将 return 一个从 -2147483648 到 4294967296 的值。
价值跟踪的要点是为每个功能在控制流图中注释条件分支；这样您就可以使用这些注释来帮助将程序分类为 "indeterminate".
以外的东西这就是事情变得棘手的地方 - 提高 "practical halting problem solver" 的质量需要增加价值跟踪的 sophistication/complexity。我不知道是否有可能写出一个完美的 "halting problem solver"（永远不会 returns "indeterminate"），但我知道有可能写出一个足够的 "halting problem solver"对于几乎所有实际目的（returns "indeterminate" 很少有人关心）。
如果程序两次进入相同的配置，那么它将永远循环下去。
图灵机也是如此，只是（无限）输入是机器配置的一部分。
这也是泵引理背后的直觉。
模型中的配置是什么？
由于您没有内存也没有 IO，因此配置由寄存器的内容和当前指令的行号（即指令指针）给出。
什么时候更改配置？
在每条指令之后，当然。但是在非分支指令的情况下，它前后的配置肯定是不同的因为即使指令是NOP，行号也改变了
在分支的情况下，行号可能是我们之前看到的行号（对于向后分支），因此机器可以从那里进入相同的配置。
对我来说，唯一感兴趣的跳跃指令似乎是call。 IF 类似的总是会产生不同的配置，因为它们的表现力不足以产生迭代（跳回并重复）。
call 如何更改配置？它将行号设置为 1 并将所有寄存器（r0 除外）设置为零。
因此调用产生相同配置的条件减少为具有相同的输入。
如果您检查，在 call 实现中，操作数值是否已经在之前（在模拟中）使用过，那么您可以判断程序将永远循环。
如果一个寄存器的大小是n，那么可能的状态就是O(2n)，一般是很多。
您必须准备好在达到（可能可定制的）阈值后放弃。或者在您的寄存器为 int 的情况下，大多数 C++ 实现具有 32 位 int，而现代机器可以处理 2^32 位的 512MiB 位图。 （例如，std::vector<bool> 实现打包位图；使用 unsigned 对其进行索引以避免负整数）。散列 table 是另一种选择 (std::unordered_set<int>)。但是，如果您为寄存器使用更广泛的类型，则状态将太大而无法实际记录每一个可能的类型，您将需要一些限制。限制是您的实现中内置的一种限制，因为您将在看到被模拟机器的 2^32 次重复附近的任何地方之前溢出 C++ 调用堆栈（C++ 递归深度）。
如果寄存器的值是无限的，这就减少了停机问题，因此在一般情况下是不可判定的。 （但正如@Brendan 所说，您仍然可以寻找状态的早期重复；许多程序将以一种简单的方式终止或无限重复。）
如果您将 call 实现更改为不将其他寄存器置零，则必须回退以检查调用站点的整个配置（而不仅仅是操作数）。
要检查每个输入的程序终止，您必须非确定性和符号性。
有两个问题：分支和输入值。
一个著名的定理是，一个TM可以以指数级的步数模拟一个NDTM w.r.t。 NDTM的步骤。
唯一有问题的指令是 IF 指令，因为它们会产生不确定性。
您可以采取多种方法：
- 将模拟分成两个分支。一个执行 IF 一个不执行。
- 重写要模拟的代码以生成指数级（以分支数计）数量的无分支代码变体。您可以延迟生成它们。
- 保留一棵配置树，程序中的每个分支在树的当前节点中生成两个子节点。
它们都是等价的。
输入值未知，因此很难判断 call 是否以相同的配置结束。
一种可能的方法是记录对输入寄存器的所有更改，例如，您最终可能会得到类似 "sub(add(add(R0, 1), 4), 5);".
这个描述应该很容易操作，因为在上面的例子中很容易看到 R0 没有改变，因为你得到 "sub(add(R0, 5), 5);" 然后 "R0;".
这依赖于算术定律，你必须注意逆运算、标识元素 (1 * a = a) 和溢出。
基本上，您需要简化表达式。
然后您可以检查输入是否在模拟时间内的给定时间点发生了变化。
在一般情况下，检查程序是否陷入无限循环的唯一方法是检查程序是否进入了与先前状态相同的状态。如果它之前进入了完全相同的状态，那么它必须继续执行循环 returning 到相同的状态，按照相同的步骤序列。在实际程序中，这基本上是不可能的，因为程序可能处于大量可能的状态，但您的汇编语言只允许更有限数量的可能状态。
由于您的 CALL 指令就像在开始时调用程序一样工作，并且这是唯一的循环形式，这意味着检查代码是否两次进入相同状态很简单。带有特定参数的 CALL 指令与以该参数作为输入调用程序具有完全相同的效果。如果 CALL 指令与任何先前执行的 CALL 指令或程序的输入值具有相同的参数，则它必须在循环中无限地继续执行 returning 以相同的步骤序列进入相同的状态。
换句话说，唯一需要检查的状态是程序开始时的R0值。由于这个值存储在 int 中，它在任何常见的 C++ 实现中只能有 2^32 个可能的值，因此暴力检查是否合理且容易地检查具有给定输入的给定程序是否陷入无限环形。
事实上，可以使用 return 值中的 memoization 在 O(N) 时间和 O(N) space 中强制检查所有可能的输入，其中N 是可能输入的数量。有多种方法可以做到这一点，但我会这样做的方法是创建三个向量，所有向量的元素数量都等于可能的输入数量。第一个向量是一个bool（位）向量，记录给定的输入是否已经被记忆，第二个向量也是bool向量，它记录给定的输入是否已经被使用过调用堆栈，第二个向量是记录结果的 int 向量，并使用输入值的链表创建调用堆栈以保存 space。 （在下面的代码中，这些向量分别被称为 is_memoized、input_pending 和 memoized_value。）
我会把你的解释器循环重写为非递归的，类似于这样的伪代码：
input = reg[R0]
if is_memoized[input]:
reg[R9] = memoized_value[input]
return
input_pending[input] = true
memoized_value[input] = input // mark the top of the stack
while true:
for command in program:
...
if command.op == CALL:
argument = command.r2value
if input_pending[argument]:
// Since this input value is ready been used as input value
// somewhere on the call stack this the program is about to enter
// an identical state as a previous state and so is stuck in
// a infinite loop.
return false // program doesn't halt
if is_memoized[argument]:
REG[R9] = memoized_value[argument]
else:
memoized_value[argument] = input // stack the input value
input = argument
REG = [input, 0, 0, 0, 0, 0, 0, 0, 0, 0]
input_pending[input] = true
break // reevaluate the program from the beginning.
if command.op == RET:
argument = command.r2value
stacked_input = memoized_value[input]
input_pending[input] = false
if stacked_input == input: // at the top of the stack
REG[R9] = argument
return true // program halts for this input
is_memoized[input] = true
memoized_value[input] = argument
input = stacked_input
REG = [input, 0, 0, 0, 0, 0, 0, 0, 0, 0]
break // reevaluate the program from the beginning
然后您将为每个可能的输入调用此解释器循环，如下所示：
for i in all_possible_inputs:
if not program.execute(input = i): // the function written above
print "program doesn't halt for all inputs"
return
print "program halts for all inputs"
递归版本应该更快，因为它不必在程序中的每个未记忆的 CALL 指令上重新评估程序，但在最坏的情况下需要数百 GB 的堆栈 space。这个非递归版本只需要 17 GB 内存。无论哪种方式，它仍然是 O(N) space 和时间，你只是让一个常数因子变小，另一个常数因子变大。
为了在合理的时间内执行此代码，您可能还需要解析一次代码，然后执行一些字节代码表示。
我认为您正在寻找跳出框框的思维方式。
这样想一下停机问题。图灵证明的程序是不受控制的。但为什么？因为语言有控制执行的指令。这意味着在程序中可行地调节和预测执行需要从语言中删除所有控制语义。
即使是我的协作流程架构也无法做到这一点。它只是因为他们造成的混乱而禁止他们。它仍然由包含它们的语言组成。例如，您可以使用 IF 来中断、return 或继续，但不能用于其他操作。函数调用是非法的。我创建了这样的限制以实现可控性。然而，即使是协作组织也不会从语言中删除控制结构以防止其被滥用。
我的架构通过我的个人资料在线，在我的 W 文章中有一个阶乘示例。