Определите, сходится ли рекурсивная функция

Рассмотрим следующую рекурсивную факториальную функцию:

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)

Вышеупомянутая функция сходится для всех целых чисел.

Я хотел знать, как бы вы статически определили, сходится ли рекурсивная функция.


static-analysis function parsing recursion convergence
person Aadit M Shah    schedule 21.01.2013    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Хорошо, что вы не указали язык и намекнули, что думаете о неограниченных целых числах, потому что это означает, что я могу указать вам на этот прототип анализатора для игрушечного языка доступен в виде веб-приложения.

С неограниченными целыми числами Ричи прав, это проблема остановки. Однако большинство других задач, решаемых статическими анализаторами, также эквивалентны проблеме остановки. Это не мешает рассматриваемым статическим анализаторам быть полезными. Они обходят неразрешимость, допуская ложноотрицательные, ложноположительные результаты или и то, и другое.

Если вы предпочитаете использовать C-подобный синтаксис, вы также можете использовать анализ значений Frama-C для определения заканчивается ли простая программа на C. Этот анализатор не обрабатывает рекурсивные функции и рассматривает целочисленные типы как ограниченные (какими они и являются). Ограниченные целочисленные типы упрощают проблему в теории (для некоторых определений входного языка она становится разрешимой), но на практике она все еще сложна.

person Pascal Cuoq    schedule 21.01.2013

arrow_upward
3
arrow_downward

Нельзя, в общем случае. Этот вопрос как раз и является проблемой остановки.

Вот простой пример рекурсивной функции, которая, вероятно, завершается для всех положительных входных данных, написанная в стиле хвостовой рекурсии (утверждение, что она останавливается для всех положительных n, является гипотеза Коллатца):

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)
person rici    schedule 21.01.2013