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

Эта статья включает в себя список литературы , связанной литературы или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Октябрь 2015 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

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

Результаты вычисления функции равны 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). По мере развития области формальных методов этот пример неоднократно появлялся в исследовательской литературе. В частности, это рассматривается как «проблема вызова» для автоматизированной проверки программ. $f(n)$ $f(n-1)$

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

M_{t}(n)=M_{t}'(n,1)

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{ and }}c\neq 0\end{cases}}

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

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

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

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{cases}}

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)), поскольку 99 ≤ 100 = M (100), поскольку 110> 100 = M (M (111)), поскольку 100 ≤ 100 = M (101), поскольку 111> 100 = 91, поскольку 101> 100

Пример Б:

М (87) = М (М (98)) = М (М (М (109))) = М (М (99)) = М (М (М (110))) = М (М (100)) = М (М (М (111))) = М (М (101)) = М (91) = М (М (102)) = М (92) = М (М (103)) = М (93) .... Шаблон продолжает увеличиваться до M (99), M (100) и M (101), точно так же, как мы видели в примере A) = M (101), поскольку 111> 100 = 91, поскольку 101> 100

Код [ править ]

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

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

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

mc91  n  |  n  >  100  =  n  -  10  |  в противном случае  =  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 :  "" "Функция Маккарти 91." ""  if  n  >  100 :  return  n  -  10  else :  return  mc91 ( mc91 ( n  +  11 ))

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

int  mc91 ( int  n ) {  если  ( n  >  100 )  {  вернуть  n  -  10 ;  }  else  {  return  mc91 ( mc91 ( n  +  11 ));  } }

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

INT  mc91 ( INT  п ) {  mc91taux ( п ,  1 ); }int  mc91taux ( int  n ,  int  c ) {  если  ( c  ! =  0 )  {  если  ( n  >  100 )  {  вернуть  mc91taux ( n  -  10 ,  c  -  1 );  }  else  {  return  mc91taux ( n  +  11 ,  c  +  1 );  }  }  else  {  return  n ;  }}

Доказательство [ править ]

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

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

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

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

Для 90 ≤ n ≤ 100,

M (n) = M (M (n + 11)) по определению = M (n + 11-10), поскольку n + 11> 100 = М (п + 1)

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

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

M (n) = M (M (n + 11)) по определению = M (91) по условию, поскольку n <n + 11 ≤ 100 = 91 по базовому случаю.

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

Обобщение Кнута [ править ]

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

Ссылки [ править ]

^ Кнут, Дональд Э. (1991). "Учебные примеры рекурсии". Искусственный интеллект и математическая теория вычислений . arXiv : cs / 9301113 . Bibcode : 1993cs ........ 1113K .
^ Каули, Джон (2013) [2000]. «Обобщение Кнута 91 функции Маккарти» . В Kaufmann, M .; Manolios, P .; Стротер Мур, Дж. (Ред.). Компьютерное мышление: тематические исследования ACL2 . Kluwer Academic. С. 283–299. ISBN 9781475731880.

Манна, Зоар; Пнуэли, Амир (июль 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 .

[1] Кнут, Дональд Э. (1991). "Учебные примеры рекурсии". Искусственный интеллект и математическая теория вычислений . arXiv : cs / 9301113 . Bibcode : 1993cs ........ 1113K .

[2] Каули, Джон (2013) [2000]. «Обобщение Кнута 91 функции Маккарти» . В Kaufmann, M .; Manolios, P .; Стротер Мур, Дж. (Ред.). Компьютерное мышление: тематические исследования ACL2 . Kluwer Academic. С. 283–299. ISBN 9781475731880.

[1]