function - 确定递归函数是否收敛

Question

考虑以下递归阶乘函数：

fact(n) =
    if (n = 0) return 1
    return n * fact(n - 1)

上述函数收敛于包括零在内的所有正整数。但是它不会收敛于负整数。

接下来，考虑以下程序：

fact(n) =
    if (n < 0) return 0
    if (n = 0) return 1
    return n * fact(n - 1)

上述函数收敛于所有整数。

我想知道您将如何静态确定递归函数是否收敛。

Answer 1

在一般情况下，您不能。这个问题正是停顿问题。

这是一个递归函数的简单示例，它可能对所有正输入都终止，以尾递归风格编写（断言它对所有正输入都停止n是Collat​​z 猜想）：

stop(n, a=0) =
  if (n == 1) return a
  if (n % 2 == 0) return stop(n / 2, a + 1)
  return stop(3 * n + 1, a + 1)

Answer 2

您没有指定语言并暗示您正在考虑无界整数，这是一件好事，因为这意味着我可以将您指向这个原型分析器，用于作为 Web 应用程序提供的玩具语言。

对于无界整数，rici 是对的，这是停止问题。然而，静态分析器解决的大多数其他问题也等价于停机问题。这并不妨碍所讨论的静态分析器发挥作用。他们通过接受假阴性、假阳性或两者兼而有之来解决不确定性。

如果您更喜欢使用类似 C 的语法，您还可以使用 Frama-C 的值分析来确定一个简单的 C 程序是否终止。此分析器不处理递归函数，它将整数类型视为有界（它们是）。有界整数类型在理论上使问题更容易（对于输入语言的某些定义，它变得可判定），但在实践中仍然很难。