Busy beaver

Пошук старанних бобрів(англ.busy beaver) - відоме завдання в теорії обчислюваності. Під старанним бобром у теорії обчислюваності розуміють машину Тьюринга із заданим числом станів кінцевого автомата, яка, будучи запущеною на порожній стрічці, записує на неї максимальну кількість ненульових символів і зупиняється.

У цьому конспекті буде розглянуто функцію, яка використовується в цьому завданні для підрахунку числа кроків для завершення програми за певної кількості станів.

Визначення:
[math]BB(n)[/math]— функція від натурального аргументу [math]n[/math] , що дорівнює максимальному числу кроків, які може зробити програма довжиною [math]n[/math] символів а потім зупинитися.
Твердження:

[math]\triangleright[/math]Розглянемо програму довжини [math]n[/math] , що здійснює максимальну кількість кроків. Існує програма довжини [math]n + 1[/math] , яка робить стільки ж кроків: виходить додаванням до попередньої одного незначного символу, наприклад, пробельного. Отже, існує програма довжини на один більше, яка робить не менше кроків. Отже, [math]BB[/math] не зменшується.[math]\triangleleft[/math]
Твердження:
[math]\triangleright[/math]

Доведемо, що для будь-якої обчислюваної функції [math]f(n)[/math] функція [math]BB(n)[/math] перевищуватиме її значення (за винятком кінцевої множини значень числа [math]n[/math] ) . Нехай [math]f(n)[/math] представлена ​​своїм кодом. Для кожного [math]n[/math] визначимо програми виду:

Кожна така програма робить щонайменше [math]f(n) + 1[/math]кроків.

Оскільки ми розглядаємо [math]n[/math] у десятковому записі, то довжина [math]p_n[/math] дорівнюватиме [math] \lg n + const [/math] , де [math]const[/math] - Довжина коду без десяткового запису [math] n [/math] . Нехай [math] n_0 [/ math] - Розв'язок рівняння [ math] \ lg n + const = n [/ math] . Тоді для всіх натуральних [math] n \gt \left \lceil n_0 \right \rceil [/math] буде виконано нерівність: [math] n \gt len(p_n) \Rightarrow BB(n) \geqslant BB(len(p_n) )) m = f(n) [/math] . Цей перехід коректний, оскільки довели, що [math]BB(n)[/math] — монотонно зростаюча функція. Оскільки [math]n_0[/math] звичайно, ми завжди можемо знайти такі значення [math]n[/math] , у яких виконуватиметься отримане нерівність. Звідси випливає, що твердження доведене.

[math]\triangleleft[/math]

Висновок:довівши попереднє твердження, ми перевірили, що максимальна кількість кроків, яку може зробити програма і при цьому зупинитися, насправді зростає з більшою швидкістю, ніж будь-яка функція, що обчислюється. Звідси випливає, що [math]BB(n)[/math] необчислювана.

Твердження:

[math]\triangleright[/math]

За теоремою про рекурсію програма може знати свій вихідний код. Отже, у неї можна написати функцію [math] \mathrm [/math] , яка поверне рядок - вихідний код програми. Припустимо, що функція Busy beaver обчислювана. Тоді напишемо таку програму