Функция McCarthy 91
-
Определение и результаты функции McCarthy 91
- Функция McCarthy 91 является рекурсивной функцией, определенной Джоном Маккарти для проверки компьютерных программ.
- Результаты функции: M(n) = 91 для n ≤ 100 и M(n) = n — 10 для n > 100.
- Функция также имеет постоянное увеличение значений после n = 101.
-
История и значение функции
- Функция была представлена в статьях 1970 года, которые были ранними работами в области формальных методов верификации программ.
- Функция была выбрана из-за своей вложенной рекурсии, что делает ее сложной для автоматизированной верификации.
- Функция стала популярной благодаря книге Зоара Маны «Математическая теория вычислений».
-
Эквивалентные определения и автоматизированная верификация
- Функция имеет эквивалентное определение с хвостовой рекурсией.
- Многие статьи рассматривают только конечную рекурсию, что упрощает доказательство завершения функции.
- В статье Митчелла Ванда 1980 года было дано доказательство взаимно-хвостовой рекурсии.
-
Примеры и реализация
- Приведены примеры кода для вложенной и хвостовой рекурсии на разных языках программирования.
-
Доказательство эквивалентности
- Доказано, что функция эквивалентна нерекурсивному алгоритму.
- Используется индукция для доказательства равенства значений функции для всех n ≤ 100.
-
Обобщение функции Кнута
- Дональд Кнут расширил функцию, добавив дополнительные параметры.
- Джон Коулз доказал полноту обобщенной функции Кнута с помощью теоремы ACL2.