王垠：理論是圍城

發了上一篇博文之后，很多人來信表示慰問。在此深表感謝。回想這么多年來的經驗，真是有點乾坤扭轉的感覺。曾經認為是錯誤的東西，后來又覺得是正確的，過一段時間它又好象確實是錯誤的。真是捉摸不定。

就拿之前遇到的問題來說吧，其實就是一個對待理論的態度問題。人們往往對數學一類的“純理論”學科充滿了敬畏和盲目的崇拜，看到別人論文里出現一堆數學公式就覺得很了不起。可是殊不知，理論的東西作假的可能性其實比“coding”這種“低等活”要大很多。程序的代碼都是可以運行的，直接一跑，誰快誰慢，誰正確誰錯誤，經常都一目了然。可是理論的東西卻說不準，里面如果有錯誤甚至“抄襲”，就算你是頂尖的研究者，都不一定看得出來。

這就是為什么某些完全不可能有實用價值的理論能夠在某個時期風靡學術界，甚至召開自己的會議。舉一個例子就是上學期被我判“死刑”的一種類型系統，叫做 intersection types，到現在都還存在它的 workshop（通常跟 LICS 會議在同一個地方召開）。可是這個類型系統卻幾乎是完全不能實用的，因為它的類型檢查需要的時間跟運行這個程序是一樣的。類型系統的初衷就是在程序運行之前迅速的查找出錯誤，如果你花跟運行這個程序同樣多的時間來檢查它，那么你還不如就直接運行這個程序！我很驚訝的是人們花了 20 多年才發現這個問題，而且在發現了這個問題之后還繼續研究這個東西。幸運的是，我只在上面花了兩個星期不到就實現了這個系統，并且發現了這個問題。后來看了著名的 Benjamin Pierce 的博士論文，就是關于 intersectiontypes。鋪天蓋地的公式，其實基本沒有任何意義。后來又跟這領域的某頭號大牛（不是 Benjamin Pierce）發 email，試圖得知這個系統是否能夠實用。來回一趟之后，就再也沒有了消息 :)

“抄襲”的判定在理論的領域也很糾結。到底誰的思想是原創的？什么樣的行為算作抄襲？這是無法說清楚的。很多當今程序語言界最時髦的話題，其實在幾十年前早就有人提出來了。很多時候做理論的人都在“重復發現”以前的結果，到頭來很難說清楚他們的論文里有什么“新東西”。你甚至不可能跟他們“理論”。如果你說理論A跟理論B，實際效果是完全一樣的，你有什么證據呢？有趣的是，就算你覺得是幾句話就說得清楚的事情，它們的支持者也會視而不見，要求你用“數學證明”的方式證明你的說法。可是某些人的公式和證明是如此的丑陋，就像一個人寫的程序代碼毫無章法。你愿意花功夫去證明他的理論跟另一個是等價的嗎？所以你就懶得去跟他們說了。你就說，你們信就信，不信就算了。

其實學術界最嚴重的問題就是總是要求“新”的東西，“獨創”的東西。研究了快一百年的領域，每年有那么多的會議，哪里可能有那么多新東西啊。所以大家就開始給老的概念起新的名字。

理論就像一個圍城，外面的人想進來，里面的人想出去。其實我最想做的事情是做一些實際對人有用的，工程性質的東西。當然，之前學會的理論很可能在里面會起到重要的作用。