После десятилетий неопределенности команда программистов доказала, насколько сложными могут быть простые компьютерные программы.
Более 40 лет назад в городе Дортмунд, Германия, собрались компьютерные ученые со всего мира, чтобы найти ответ на одну из самых сложных задач в теории вычислений. Они искали « пятого занятого бобра » — программу, которая выполняет вычисления дольше всех других программ с аналогичными правилами. Тогда участникам не удалось добиться успеха, и решение задачи осталось не найденным.
Занятой бобёр – это не просто милый зверек, а увлекательная математическая задача, связанная с теорией вычислимости. Представьте себе машину Тьюринга, которая может выполнять простые действия, читая и записывая символы на ленте.
В задаче Занятой бобёр мы даем этой машине ограниченное количество состояний (как у кнопок на пульте) и просим её выполнить такую программу, чтобы работать как можно дольше, а потом остановиться.
"Дольше" в данном случае означает: записать на ленту максимально возможное число ненулевых символов (например, единиц) и закончить работу.
Задача Занятой бобёр как раз и заключается в том, чтобы найти такую программу для каждой машины Тьюринга (с заданным числом состояний), которая позволит ей записать максимально возможное число символов перед остановкой.
Эти программы представляют собой теоретические вычислительные машины, которые работают по заданным правилам, выполняя операции до тех пор, пока не остановятся. Их поведение связано с нерешаемыми вопросами в математике, такими как проблема остановки , доказанная Алланом Тьюрингом в 1936 году.
В 2022 году новый этап поиска был инициирован аспирантом Тристаном Стерином , который создал веб-сайт Busy Beaver Challenge . В отличие от предыдущих попыток, это мероприятие было направлено на сотрудничество, и к нему присоединились более 20 участников со всего мира. Сегодня команда объявила о своей победе: они смогли точно определить значение числа BB(5), которое составляет 47,176,870 шагов.
Для достижения этого результата использовалась программа Coq proof assistant , которая подтверждает правильность математических доказательств. По мнению экспертов, достигнутое решение — это настоящее инженерное и математическое достижение.
Поиск «занятых бобров» — это своего рода трофейная охота. Хотя конкретное значение BB(5) не имеет практического применения в других областях компьютерных наук, для охотников за «занятыми бобрами» сама победа над математической невозможностью является наградой.
Программы, представляющие интерес для охотников за «занятыми бобрами», описываются на языке теоретических машин Тьюринга . Эти машины выполняют вычисления, читая и записывая 0 и 1 на бесконечной ленте, используя набор правил. Некоторые машины быстро останавливаются, другие попадают в бесконечные циклы, а некоторые сложно классифицировать без длительного анализа.
Сама концепция «занятых бобров» была предложена математиком Тибором Радо в 1962 году. Он придумал игру, в которой машины Тьюринга делятся на группы по количеству правил, и задача заключается в нахождении машины с самым длинным временем выполнения в каждой группе.
Оказалось, что решение задачи BB(5) потребовало коллективного усилия. В течение последних лет сообщество исследователей разработало множество техник и программ для анализа поведения машин Тьюринга. Георгий Георгиев, также известный как Скелетон, в 2003 году классифицировал все машины Тьюринга, за исключением 43, с пятью правилами. Неподходящие, которые было крайне трудно анализировать, были названы в его честь машинами Скелетон.
Наконец, с использованием современных методов, таких как Coq, и с участием новых исследователей, удалось подтвердить, что машина, найденная в 1990 году Хайнером Марксеном и Юргеном Бантроком, действительно является пятой «занятой бобровой» машиной.
Теперь команда работает над оформлением своих результатов в научную статью. Однако успех в решении задачи BB(5) может оказаться последним достижением в этой области, поскольку задача определения BB(6) связана с нерешенной математической проблемой, известной как гипотеза Коллатца .
Этот результат подчеркивает важность совместной работы и использования современных технологий для решения сложных математических задач.
Узнайте как на нашем канале