麦卡锡91函数

麦卡锡91函数是一个递归函数，由计算机科学家约翰-麦卡锡定义为计算机科学中形式化验证的一个测试案例。

对于所有整数参数n≤100，评估该函数的结果为M(n)=91，对于n>100，M(n)=n-10。

事实上，M(101)的结果也是91（101-10=91）。在n=101之后，M(n)的所有结果都持续增加1，例如，M(102)=92，M(103)=93。

91函数是由ZoharManna,AmirPnueli和JohnMcCarthy在1970年发表的论文中介绍的。这些论文代表了形式化方法应用于程序验证的早期发展。选择91函数是因为它是嵌套递归的（与单一递归不同，如定)。

这个例子在曼纳的《计算的数学理论》（1974）一书中得到推广。随着形式化方法领域的发展，这个例子反复出现在研究文献中。

特别是，它被视为自动程序验证的一个挑战问题。推理尾部递归控制流更容易，这是一个等价（扩展上相等）的定义。

作为用来证明这种推理的例子之一，曼纳的书中有一个相当于嵌套递归91函数的尾部递归算法。许多报告91函数自动验证（或终止证明）的论文只处理尾部递归版本。

MitchellWand在1980年的一篇文章中给出了从嵌套递归版本中推导出的互为尾部递归版本的正式方法，该方法基于连续性的使用。

这里是Lisp中嵌套递归算法的一个实现。

它提供了一个等同于c的非递归算法