数学2015arxiv.org
辫群问题是不可判定的(2014)
Braid is undecidable (2014)
进阶 · 约 45 分钟读完前置知识:可计算性理论、图灵机归约、Braid 时间倒流机制
导读
这篇论文研究电子游戏《Braid》中「时间倒流」机制所带来的计算问题,证明在一般设定下,判定玩家能否达成某个目标(即可解性)是不可判定的。作者先用 Rush Hour 这类直观例子建立读者的直觉,再给出不可判定性证明,并顺带讨论了他提出的另一个「看起来顺理成章」的变体(Bounded Braid),结论反而是可判定的。
HN 关注点:HN 读者既被这款经典独立游戏的情怀吸引,也对「一个游戏机制竟然不可判定」这一结论,以及论文清晰的论证结构感兴趣。
HN 评论精选
这几条评论里:支持 1 补充 2
补充技术性建议:arXiv 链接应指向摘要页而非 PDF。
提醒一下:如果要链接 arXiv,最好链到摘要页(http://arxiv.org/abs/1412.0784),而不是直接链 PDF。从摘要页可以轻松点进 PDF,反过来却不行;而且摘要页还能查看论文的不同版本、搜索同一作者的其他工作等等。谢谢!
Sniffnoy查看英文原文
A note -- if you're linking to arXiv, it's better to link to the abstract (http://arxiv.org/abs/1412.0784) rather than directly to the PDF. From the abstract, one can easily click through to the PDF; not so the reverse. And the abstract allows one to do things like see different versions of the paper, search for other things by the same authors, etc. Thank you!
支持称赞论文结构,并指出有界版本可判定,以及时间倒流树与编辑器 undo 树的类比。
这篇论文写得非常出色!该做的基本功都做到了:先说明目标、问题的范围,再用一个简短例子(Rush Hour)帮读者建立直觉,然后才去证明不可判定性。它甚至还讨论了作者另一个「看起来显然可行」的想法(有界 Braid 的情形),结果证明它其实是可判定的。另外我还在想,是不是大多数程序员都在不知不觉中积累了大量 Braid 直觉,因为时间倒流树和我们建模 $EDITOR 里 undo 树的方式很相似。
spranesh查看英文原文
What an excellently well written paper! It does all the basics right - describes it's objective, the domain of the problem, a quick example (Rush hour) to nudge some intuition toward the reader, before going on to prove undecidability. It even tackles the decidability of another "should-obviously-work" (Bounded braid) idea that the author had (turns out to be decidable). Also, I wonder if most programmers have unknowingly built a ton of Braid intuition because of the way the time reversal tree matches the way we model the undo tree in $EDITOR.
补充指出难点不在不可判定性,而在于构造可判定的非平凡模型。
在(因而是不可判定的)图灵完备系统里构造出各种行为其实相当容易。更难的是构造出仍然可判定、甚至是多项式时间可判定的非平凡模型(即能展现复杂行为)。
wolfgke查看英文原文
It is rather easy to build behaviors in systems that are Turing-complete (thus undecidable). What is more complicated is building nontrivial models (i.e. showing complex behavior) that are still decidable or even decidable in polynomial time.
历次讨论
- 2015Hacker News 讨论帖136 分 · 30 评
同领域还值得读
一种新的相关系数
A New Coefficient of Correlation
提出了一种新的相关性系数(由 Sourav Chatterjee 提出),能够检测变量之间任意形式(不限于线性)的相关关系,且计算简单高效,主要基于排序和距离计算。
数学2021 · 682 分 · 158 评 · 引用 1进阶 · 约 60 分钟编辑精选数学的两种文化
The Two Cultures of Mathematics (2000)
这是数学家 Timothy Gowers 于 2000 年发表的一篇随笔,他把数学研究大致分成两种文化:一类是“解题者”,热衷于攻克具体难题、发展技巧(如组合数学);另一类是“理…
数学2009 · 307 分 · 102 评入门 · 约 35 分钟编辑精选重新定义统计显著性
Redefine statistical significance
提议将统计显著性阈值从常用的 p<0.05 收紧到 p<0.005,以降低假阳性率、缓解可重复性危机。
数学2017 · 303 分 · 114 评入门 · 约 45 分钟编辑精选统计建模:两种文化(2001)
Statistical Modeling: The Two Cultures (2001)
讨论统计学中两种建模文化:一种假设数据由某种随机模型生成,侧重推断与系数解释;另一种把数据生成机制视为未知,侧重预测精度,主张使用算法建模。
数学2015 · 254 分 · 36 评进阶 · 约 60 分钟编辑精选通信的数学理论 (1948)
A Mathematical Theory of Communication (1948)
这是香农 1948 年的经典论文《通信的数学理论》,奠定了信息论的基础。
数学2016 · 169 分 · 53 评入门 · 约 90 分钟编辑精选