2009/03/03

Hackers

因為跟了隨機客的專題,對於那邊 algorithms research 的情況逐漸有點體驗。其實那邊除了研究對象換成 algorithms 以外,做的事情和一般數學家沒什麼差別。特別地(in particular),他們對於演算法的描述並不講究,證明內容豐富但型式天馬行空,就好像我們現在看 60, 70 年代的 hackers 寫程式一樣(Curry-Howard, informally XD),有天才的成就,但寫出的程式(包括證明)沒什麼結構。看他們在證明就好像在鋼索上跳舞一樣,看得下面的人心驚膽跳。可是這邊「怎麼寫好程式和證明」的理論還遠遠追不上他們,只好先讓他們繼續跳了 XD。

還有一個現象是,他們(和數學家)所謂的 constructive proofs 是存在演算法能構造出 desired objects,但證明演算法正確性時大量使用反證法。所以 existential proposition 的 witness 確實找到了,但「這個 witness 符合規格」的證明只在 classical logic 下面有效。其實我不太了解這樣到底發生什麼事…

另一方面,「假裝自己其實看得懂」地硬鑽 HOAS paper 似乎有點成果。看著 Yoneda lemma 把「表示成某種 functors 的 meta-level terms」和「表示成某種 arrows 的 object-level terms」拉在一起還挺炫的 XD。

--
選定領域後帶著立場看看其他領域,收穫反而更大 XD。

Labels:

Blogger XOO3/03/2009 3:40 pm 說:

這就是所謂 proof-irrelevant ? XD

 
Blogger yen33/04/2009 1:15 am 說:

你這樣子說是代表,那些證明其實離不嚴謹只差一點點而己 XD ?

我最近覺得 Artificial Intelligence 和 IC Design 深得我心,或許就此有機會繼續發掘我的領域 XD?

 
Blogger Josh Ko3/04/2009 3:17 pm 說:

嚴謹程度是沒問題的,就像能跑的程式一定都先通過編譯器檢查一樣 XD。寫得好不好看就是另一回事了 XD。

 

<< 回到主頁