王垠：理论是围城

   <div id="news_body">     <p> 发了<a href="http://www.open-open.com/news/view/181e986">上一篇博文</a>之后，很多人来信表示慰问。在此深表感谢。回想这么多年来的经验，真是有点乾坤扭转的感觉。曾经认为是错误的东西，后来又觉得是正确的，过一段时间它又好象确实是错误的。真是捉摸不定。</p>     <p> 就拿之前遇到的问题来说吧，其实就是一个对待理论的态度问题。人们往往对数学一类的“纯理论”学科充满了敬畏和盲目的崇拜，看到别人论文里出现一堆数学公式就觉得很了不起。可是殊不知，理论的东西作假的可能性其实比“coding”这种“低等活”要大很多。程序的代码都是可以运行的，直接一跑，谁快谁慢，谁正确谁错误，经常都一目了然。可是理论的东西却说不准，里面如果有错误甚至“抄袭”，就算你是顶尖的研究者，都不一定看得出来。</p>     <p> 这就是为什么某些完全不可能有实用价值的理论能够在某个时期风靡学术界，甚至召开自己的会议。举一个例子就是上学期被我判“死刑”的一种类型系统，叫做 intersection types，到现在都还存在它的 workshop（通常跟 <a href="/misc/goto?guid=4958523928869050181" target="_blank">LICS 会议</a>在同一个地方召开）。可是这个类型系统却几乎是完全不能实用的，因为它的类型检查需要的时间跟运行这个程序是一样的。类型系统的初衷就是在程序运行之前迅速的查找出错误，如果你花跟运行这个程序同样多的时间来检查它，那么你还不如就直接运行这个程序！我很惊讶的是人们花了 20 多年才发现这个问题，而且在发现了这个问题之后还继续研究这个东西。幸运的是，我只在上面花了两个星期不到就实现了这个系统，并且发现了这个问题。后来看了著名的 Benjamin Pierce 的博士论文，就是关于 intersectiontypes。铺天盖地的公式，其实基本没有任何意义。后来又跟这领域的某头号大牛（不是 Benjamin Pierce）发 email，试图得知这个系统是否能够实用。来回一趟之后，就再也没有了消息 :)</p>     <p> “抄袭”的判定在理论的领域也很纠结。到底谁的思想是原创的？什么样的行为算作抄袭？这是无法说清楚的。很多当今程序语言界最时髦的话题，其实在几十年前早就有人提出来了。很多时候做理论的人都在“重复发现”以前的结果，到头来很难说清楚他们的论文里有什么“新东西”。你甚至不可能跟他们“理论”。如果你说理论A跟理论B，实际效果是完全一样的，你有什么证据呢？有趣的是，就算你觉得是几句话就说得清楚的事情，它们的支持者也会视而不见，要求你用“数学证明”的方式证明你的说法。可是某些人的公式和证明是如此的丑陋，就像一个人写的程序代码毫无章法。你愿意花功夫去证明他的理论跟另一个是等价的吗？所以你就懒得去跟他们说了。你就说，你们信就信，不信就算了。</p>     <p> 其实学术界最严重的问题就是总是要求“新”的东西，“独创”的东西。研究了快一百年的领域，每年有那么多的会议，哪里可能有那么多新东西啊。所以大家就开始给老的概念起新的名字。</p>     <p> 理论就像一个围城，外面的人想进来，里面的人想出去。其实我最想做的事情是做一些实际对人有用的，工程性质的东西。当然，之前学会的理论很可能在里面会起到重要的作用。</p>     <div id="come_from">     来自:      <a id="link_source2" href="/misc/goto?guid=4958523928965486570" target="_blank">blog.sina.com.cn</a>     </div>    </div>