6

在学习递归时，我遇到了 McCarthy 91 函数，它为所有整数参数 n <= 101 返回值 91，对于 n > 101，返回 n - 10。

 int McCarthy(int n)
 {
   if (n > 100)
     return n - 10;
   return McCarthy(McCarthy(n+11));
 }

int main()
{
  printf(" %d ", McCarthy(45));
  return 0;
}

我只是想知道它在计算机科学中的意义是什么？维基百科文章说它被用作形式验证的测试用例。这意味着什么。？

有人可以为我简化它的用法吗？

4

1 回答 1

8

想象一下，您正在编写一个 C 编译器，它接受与您编写的程序类似的程序并生成可执行代码。您想测试您的编译器是否正常工作。您编写了一个测试用例，它是您编写的函数的递归定义，并断言当您运行编译后的代码时，您会得到易于计算的结果（在这种情况下，程序应该输出 91）。如果您开始为编译递归调用编写优化，像这样的困难测试用例将特别有用。

想象一下，您正在编写一个尝试编写证明的程序，而不是编写编译器，就像您在数学课上编写一样。程序的输入可能是一组转换，例如您用来编写证明的代数定律，以及程序试图证明的语句。计算机科学的这一分支称为形式验证。涉及 McCarthy 91 函数的陈述很难证明。例如（对于所有 x <= 100，M(x) == 91）将很难证明。对于您的证明编写程序和生成证明的转换来说，这将是一个非常困难的问题。

于 2013-08-12T17:20:02.350 回答