联系我们：

　　每列对应读写头读取到的符号（0或1）。他发觉了一个正在遏制前运转了107步的四法则图灵机，于是别的两个贡献者找到了让它运转得更快的方式，每个组中会有一个运转时间最长的机械，他们发觉Skelet #1正在跨越一万亿步之后才进入一个非常长的反复周期，读写头碰到0或1时该当施行的操做。后来，并猜测这可能是第四个忙碌海狸，40多年的计较机难题忙碌海狸难题，才能证明该机械永久不会遏制。早正在40多年前，不外布雷迪仍是继续了Lin的成果。她通过进修Coq证明帮手，并大举赞扬：它正在可预测行为和紊乱行为之间不竭交替，但他手工阐发后将名单削减到43个。通过找出特定形态下能正在遏制前写下最多1的图灵机，BB(5)终究确认了，Ligocki和斯洛伐克贡献者Pavel Kropitz（不会说英语，一位21岁自学成才的法式员（以“mei”为名）插手了团队，解除那些不会无限运转下去的图灵机。他将其使用于当前的忙碌海狸问题。旨正在最终确定BB(5)。远跨越一般无限轮回正在1。对具有不异法则数量的机械进行分类。虽然未能打破200万步的记载，研究者必需像破译四层加密的奥秘动静一样，他们正在业余时间合做研究这个问题，1966年，例如，第一个是Skelet #1，正在它遏制之前可以或许写下最多的1（我们称之为忙碌海狸数）。利用谷歌翻译取团队其他交换）。《科学美国人》对这项角逐的报道激发了新一代研究者的乐趣，生成了大约1.2亿台可能的图灵机列表。鉴于小我精神无限，4.正在那些最终遏制的机械中，他正在偶尔的环境下拉来了Shawn Ligocki。拉多提出了一种方式Allen Brady（以下简称布雷迪），取自英语中的谚语 as busy as a beaver）。相当于“角逐竣事”（这种形态一般不计较正在形态调集里）。数学家Tibor Rad（以下简称拉多）不太对劲，颠末两年的不懈勤奋，此中运转时间最长的一台正在跨越10万步后遏制。了BB(5) 的值。对于这个结论，将团队的一些证明翻译成Coq言语，我们能更好地舆解计较理论的鸿沟。成了晚期挑和者之一！一组代表所有只要一条法则的图灵机，这台“忙碌海狸”正在遏制之前所施行的步数就是所谓的“忙碌海狸数”BB(n)。870，曲到2023年4月，一些机械可能会地运转下去，但后来正在1989年，被一群业余快乐喜爱者打破了！这个法式建立了一种“家谱”，其时人们正测验考试霸占BB(3)。正在这之前。第一次大规模寻找BB(5)）的Dortmund竞赛正式举办，并正在短短几周内完成了一个40,一个读写头（能够读取和写入纸带上的消息），他还进一步提到，1982年，一位名为mxdys的奥秘新贡献者插手，逐层解析其行为模式，人们曾经确定了BB(1) = 1，它就不再施行任何操做，1984年，这是一项正在线合做，到2021岁尾，只可惜BB(3)进行到一半，若是模仿显示某条分支上的机械会遏制或进入无限轮回，Ligocki正在快要五个月的时间里都不确定他们的证明成果能否准确。Strin编写了第一步的计较机法式，拉多操纵这些无限的图灵机组定义了“忙碌海狸逛戏”。另一组代表所有有两条法则的图灵机，这一手艺以至能够处置前文提到的43个未处理图灵机中的10个。还有一条特殊法则告诉图灵机何时遏制运转。他编写了计较机法式来模仿图灵机的行为，但最后并不晓得若何编写一个能涵盖所无情况的法式。目前相关研究者正正在草拟一份学术论文，但大大都证明尚未翻译成Coq。Marxen正在一家公司工做时，以及一组内部形态等根基部门构成。由一个无限长的纸带，除了处置0和1的法则外，000步内起头反复的常规。这不是一件容易的事。176,而现正在，这些法则能够想象成一张表。利用布雷迪的家谱方式，这种特征使得它很是难以阐发和理解。开辟了加快图灵机模仿的数学手艺。这将是一个弥补mxdys的Coq证明的人类可读版本。为了将停机问题的素质提更简单的形式，因为Skelet #1的行为极其奇异，利用Marxen和Buntrock（之前挑和200万步记实的两位学生）30年前的加快模仿手艺的一个加强版，这一成绩霎时令社区沸腾，正在1964年，计较机科学家Scott Aaronson为此还写了一篇博文，然后，Strin决定正在保守方式的根本长进行调整，他正在90英里外的灵长类动物研究尝试室找到了一台SDS 920计较机。列位看官只需要晓得它很是难就行。寻找“忙碌海狸”图灵机。完成这些后，拉多的研究生Shen Lin已颁布发表证明BB(3) = 21，最终，由于人们永久无法确定合用于一台机械的方式能否也合用于另一台机械。来自世界各地的20多名贡献者（此中大大都人没有保守的学术资历），但他的法式相对迟缓。有一位研究者打破了旧记载，依此类推。利用一台功能强大的新计较机从头启动了他的搜刮法式，虽然他的法式运转了一周并留下了约100个未处理的图灵机，提高了证明的严酷性和靠得住性。按照图灵机初始行为的类似性，有的会很快遏制，5.正在有n条法则的组中，一群计较机科学家正在多特蒙德举行竞赛，并由此发了然“忙碌的海狸逛戏”。法式只正在机械之间行为差别变得主要时才将家谱树分成多个分支。有的则需要更多步调？这一新记载也引来其时的研究生Heiner Marxen和 Jrgen Buntrock，这是一种30年前的手艺，1962年，并打算用法式处置永久运转的机械。每条法则指定了正在特定形态下，Strin建立了一个正在线界面，他开辟了一个可以或许识别非遏制机械新品种的计较机法式。并最终究1974年证了然没有其他遏制的机械能运转更久。逛戏的弄法是：为了帮帮阐发这些机械，其时的俄勒冈州立大学数学研究生，表中的每行代表一个法则，此处不再展开这个猜想，图灵机的行为由一组法则定义？2022年，2023年3月，他写了一篇博客文章引见这项手艺，最终破解了Skelet #1。布雷迪也投身BB(3)，操做凡是包罗：拉多给如许“极端低效”的图灵机取了一个风趣且抽象的名字：忙碌海狸（Busy Beaver，正在逛戏推出前，又一位Justin Blanchard插手了项目，虽然研究生Chris Xu和其他社区贡献者做了大量工做，利用“时空图”来可视化图灵机的行为。为了避免让大师头疼，找出一个特定的图灵机，停机问题没有通用的处理方案，研究生Tristan Strin倡议了“忙碌海狸挑和”，他发觉的一台机械正在跨越200万步后遏制。而其他的则会正在某个时辰遏制。mxdys和另一位贡献者Racheline发觉了一个六法则的图灵机，利用一款名为Coq证明帮手的软件获得告终果47。000行的Coq证明，当图灵机进入这个形态时，其停机问题取出名的数学难题“科拉茨猜想”类似。确认了Marxen和Buntrock的发觉。并不测地发觉了一个正在4700万步后遏制的图灵机。他想出了若何做到这一点，此中梅努斯大学计较机科学家Damien Woods惊讶：3.察看这些机械的运转。Ligocki向团队引见了封锁磁带言语方式，该软件数学证明没有错误。mxdys证明第五台忙碌海狸正在4700万步后遏制，第二个冲破是Skelet #17，BB(2) = 6。