Функция Маккарти 91 - это рекурсивная функция, определенная компьютерным ученым Джоном Маккарти как тестовый пример для формальной проверки в компьютерных науках.
Функция Маккарти 91 определяется как
Результаты вычисления функции равны M ( n) = 91 для всех целочисленных аргументов n ≤ 100 и M ( n) = n - 10 для n gt; 100. Действительно, результат M (101) также равен 91 ( 101-10 = 91). Все результаты M (n) после n = 101 постоянно увеличиваются на 1, например M (102) = 92, M (103) = 93.
Функция 91 была представлена в статьях, опубликованных Зохаром Манной, Амиром Пнуели и Джоном Маккарти в 1970 году. Эти статьи представляли собой ранние разработки в направлении применения формальных методов для проверки программ. Функция 91 была выбрана как вложенно-рекурсивная (в отличие от одиночной рекурсии, такой как определение с помощью). Этот пример был популяризирован книгой Манна « Математическая теория вычислений» (1974). По мере развития области формальных методов этот пример неоднократно появлялся в исследовательской литературе. В частности, это рассматривается как «проблема вызова» для автоматизированной проверки программ.
Проще рассуждать о хвостово-рекурсивном потоке управления, это эквивалентное (с точки зрения расширения ) определение:
В качестве одного из примеров, используемых для демонстрации таких рассуждений, книга Манна включает хвостовой рекурсивный алгоритм, эквивалентный вложенной рекурсивной функции 91. Многие статьи, в которых сообщается об «автоматической проверке» (или доказательстве завершения ) функции 91, обрабатывают только хвостовую рекурсивную версию.
Это эквивалентное взаимно рекурсивное определение:
Формальный вывод взаимно хвостовой рекурсивной версии от вложенной рекурсивной версии был дан в статье Митчелла Ванда 1980 года, основанной на использовании продолжений.
Пример А:
M(99) = M(M(110)) since 99 ≤ 100 = M(100) since 110 gt; 100 = M(M(111)) since 100 ≤ 100 = M(101) since 111 gt; 100 = 91 since 101 gt; 100
Пример Б:
M(87) = M(M(98)) = M(M(M(109))) = M(M(99)) = M(M(M(110))) = M(M(100)) = M(M(M(111))) = M(M(101)) = M(91) = M(M(102)) = M(92) = M(M(103)) = M(93).... Pattern continues increasing till M(99), M(100) and M(101), exactly as we saw on the example A) = M(101) since 111 gt; 100 = 91 since 101 gt; 100
Вот реализация вложенного рекурсивного алгоритма в Лиспе :
(defun mc91 (n) (cond ((lt;= n 100) (mc91 (mc91 (+ n 11)))) (t (- n 10))))
Вот реализация вложенного рекурсивного алгоритма в Haskell :
mc91 n | n gt; 100 = n - 10 | otherwise = mc91 $ mc91 $ n + 11
Вот реализация вложенного рекурсивного алгоритма в OCaml :
let rec mc91 n = if n gt; 100 then n - 10 else mc91 (mc91 (n + 11))
Вот реализация алгоритма хвостовой рекурсии в OCaml :
let mc91 n = let rec aux n c = if c = 0 then n else if n gt; 100 then aux (n - 10) (c - 1) else aux (n + 11) (c + 1) in aux n 1
Вот реализация вложенно-рекурсивного алгоритма в Python :
def mc91(n: int) -gt; int: """McCarthy 91 function.""" if n gt; 100: return n - 10 else: return mc91(mc91(n + 11))
Вот реализация вложенно-рекурсивного алгоритма на C :
int mc91(int n) { if (n gt; 100) { return n - 10; } else { return mc91(mc91(n + 11)); } }
Вот реализация алгоритма хвостовой рекурсии на C :
int mc91(int n) { return mc91taux(n, 1); } int mc91taux(int n, int c) { if (c != 0) { if (n gt; 100) { return mc91taux(n - 10, c - 1); } else { return mc91taux(n + 11, c + 1); } } else { return n; } }
Вот доказательство того, что
который предоставляет эквивалентный нерекурсивный алгоритм для вычисления.
При n gt; 100 равенство следует из определения. Для n ≤ 100 можно использовать сильную индукцию вниз от 100.
Для 90 ≤ n ≤ 100,
M(n) = M(M(n + 11)), by definition = M(n + 11 - 10), since n + 11 gt; 100 = M(n + 1)
Итак, M ( n) = M (101) = 91 для 90 ≤ n ≤ 100. Это можно использовать как базовый случай.
Для шага индукции пусть n ≤ 89 и M ( i) = 91 для всех n lt; i ≤ 100, тогда
M(n) = M(M(n + 11)), by definition = M(91), by hypothesis, since n lt; n + 11 ≤ 100 = 91, by the base case.
Это доказывает, что M ( n) = 91 для всех n ≤ 100, включая отрицательные значения.
Дональд Кнут обобщил функцию 91, включив в нее дополнительные параметры. Джон Коулз разработал формальное доказательство тотальности обобщенной функции Кнута, используя средство доказательства теорем ACL2.