Функция Маккарти 91 - McCarthy 91 function

Функция Маккарти 91 - это рекурсивная функция , определенная компьютерным ученым Джоном Маккарти как тестовый пример для формальной проверки в компьютерных науках .

Функция Маккарти 91 определяется как

{\ Displaystyle M (n) = {\ begin {case} n-10, & {\ mbox {if}} n> 100 {\ mbox {}} \\ M (M (n + 11)), & {\ mbox {if}} n \ leq 100 {\ mbox {}} \ end {case}}}

Результаты вычисления функции равны M ( n ) = 91 для всех целочисленных аргументов n ≤ 100 и M ( n ) = n - 10 для n > 100. Действительно, результат M (101) также равен 91 ( 101-10 = 91). Все результаты M (n) после n = 101 постоянно увеличиваются на 1, например M (102) = 92, M (103) = 93.

История

Функция 91 была представлена в статьях, опубликованных Зохаром Манной , Амиром Пнуели и Джоном Маккарти в 1970 году. Эти статьи представляли собой ранние разработки в направлении применения формальных методов для проверки программ . Функция 91 была выбрана как вложенно-рекурсивная (в отличие от одиночной рекурсии , такой как определение с помощью ). Этот пример был популяризирован книгой Манна « Математическая теория вычислений» (1974). По мере развития области формальных методов этот пример неоднократно появлялся в исследовательской литературе. В частности, это рассматривается как «проблема вызова» для автоматизированной проверки программ. ${\ Displaystyle f (п)}$ ${\ displaystyle f (n-1)}$

Проще рассуждать о хвостово-рекурсивном потоке управления, это эквивалентное (с точки зрения расширения ) определение:

{\ Displaystyle М_ {т} (п) = М_ {т} '(п, 1)}

{\ displaystyle M_ {t} '(n, c) = {\ begin {cases} n, & {\ mbox {if}} c = 0 \\ M_ {t}' (n-10, c-1), & {\ mbox {if}} n> 100 {\ mbox {and}} c \ neq 0 \\ M_ {t} '(n + 11, c + 1), & {\ mbox {if}} n \ leq 100 {\ mbox {и}} c \ neq 0 \ end {case}}}

В качестве одного из примеров, используемых для демонстрации таких рассуждений, книга Манна включает хвостовой рекурсивный алгоритм, эквивалентный вложенной рекурсивной функции 91. Многие статьи, в которых сообщается об «автоматической проверке» (или доказательстве завершения ) функции 91, обрабатывают только хвостовую рекурсивную версию.

Это эквивалентное взаимно рекурсивное определение:

{\ Displaystyle M_ {mt} (n) = M_ {mt} '(n, 0)}

{\ displaystyle M_ {mt} '(n, c) = {\ begin {cases} M_ {mt}' '(n-10, c), & {\ mbox {if}} n> 100 {\ mbox {} } \\ M_ {mt} '(n + 11, c + 1), & {\ mbox {if}} n \ leq 100 {\ mbox {}} \ end {case}}}

{\ displaystyle M_ {mt} '' (n, c) = {\ begin {cases} n, & {\ mbox {if}} c = 0 {\ mbox {}} \\ M_ {mt} '(n, c-1), & {\ mbox {if}} c \ neq 0 {\ mbox {}} \ end {cases}}}

Формальный вывод взаимно хвостовой рекурсивной версии от вложенной рекурсивной версии был дан в статье Митчелла Ванда 1980 года , основанной на использовании продолжений .

Примеры

Пример А:

M(99) = M(M(110)) since 99 ≤ 100
      = M(100)    since 110 > 100
      = M(M(111)) since 100 ≤ 100
      = M(101)    since 111 > 100
      = 91        since 101 > 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 > 100
      = 91        since 101 > 100

Код

Вот реализация вложенного рекурсивного алгоритма в Лиспе :

(defun mc91 (n)
  (cond ((<= n 100) (mc91 (mc91 (+ n 11))))
        (t (- n 10))))

Вот реализация вложенного рекурсивного алгоритма в Haskell :

mc91 n 
  | n > 100   = n - 10
  | otherwise = mc91 $ mc91 $ n + 11

Вот реализация вложенного рекурсивного алгоритма в OCaml :

let rec mc91 n =
  if n > 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 > 100 then aux (n - 10) (c - 1)
    else aux (n + 11) (c + 1)
  in
  aux n 1

Вот реализация вложенно-рекурсивного алгоритма в Python :

def mc91(n: int) -> int:
    """McCarthy 91 function."""
    if n > 100:
        return n - 10
    else:
        return mc91(mc91(n + 11))

Вот реализация вложенно-рекурсивного алгоритма на C :

int mc91(int n)
{
    if (n > 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 > 100) {
            return mc91taux(n - 10, c - 1);
        } else {
            return mc91taux(n + 11, c + 1);
        }
    } else {
        return n;
    }
}

Доказательство

Вот доказательство того, что

{\ displaystyle M (n) = {\ begin {case} n-10, & {\ mbox {if}} n> 100 {\ mbox {}} \\ 91, & {\ mbox {if}} n \ leq 100 {\ mbox {}} \ end {case}}}

который предоставляет эквивалентный нерекурсивный алгоритм для вычисления . ${\ displaystyle M}$

При n > 100 равенство следует из определения . Для n ≤ 100 можно использовать сильную индукцию вниз от 100. ${\ displaystyle M}$

Для 90 ≤ n ≤ 100,

M(n) = M(M(n + 11)), by definition
     = M(n + 11 - 10), since n + 11 > 100
     = M(n + 1)

Итак, M ( n ) = M (101) = 91 для 90 ≤ n ≤ 100. Это можно использовать как базовый случай.

Для шага индукции пусть n ≤ 89 и M ( i ) = 91 для всех n < i ≤ 100, тогда

M(n) = M(M(n + 11)), by definition
     = M(91), by hypothesis, since n < n + 11 ≤ 100
     = 91, by the base case.

Это доказывает, что M ( n ) = 91 для всех n ≤ 100, включая отрицательные значения.

Обобщение Кнута

Дональд Кнут обобщил функцию 91, включив в нее дополнительные параметры. Джон Коулз разработал формальное доказательство тотальности обобщенной функции Кнута, используя средство доказательства теорем ACL2 .

использованная литература

Манна, Зоар; Пнуэли, Амир (июль 1970 г.). «Формализация свойств функциональных программ». Журнал ACM . 17 (3): 555–569. DOI : 10.1145 / 321592.321606 .
Манна, Зоар; Маккарти, Джон (1970). «Свойства программ и частичная функциональная логика». Машинный интеллект . 5 . OCLC 35422131 .
Манна, Зохар (1974). Математическая теория вычислений (4-е изд.). Макгроу-Хилл. ISBN 9780070399105.
Палочка, Митчелл (январь 1980 г.). «Стратегии преобразования программ, основанные на продолжении». Журнал ACM . 27 (1): 164–180. DOI : 10.1145 / 322169.322183 .

Languages

In other projects