近期計畫

上禮拜去河岸聽王若琳用手機順手拍的,好想要台數位相機 …

正在看 mathematical logic 的東西:

  • Proposition Calculus
  • Predicate Calculus ( First-order logic )
  • Second-order and Higher-order logic
  • and finally, Intuitionistic Logic

以及 lambda calculus with type,看的是 Barendregt 的書,兩者在很多面向遇到的問題是一樣的,例如在 variable 的 substitution rule 的部份,兩者處理的方式也大致雷同。

以上兩塊了結之後,就是 Curry-Howard Isomorphism,估計沒問題的話,這之後應該可以對 type 跟 logic 兩邊來去自如?對於要怎麼用 dependent type 作證明比較能得心應手 XD

另外一方面正在想的是,關於將 algorithm 抽象化,就像 C++STL 作的那樣,但是我們將要求的 relation, operation (function) 寫在 type 裡頭,而 algorithm 可以用這些去做,最好的狀況連 complexity 都嵌入 type 裡頭,依據這些資料作 type 推導選擇最恰當的演算法。

STL 的出發點很好,但是到頭來 sort() 還是被綁在 array 等資料結構上,只不過比原本的 C 上 sort 比較不受限制一點。要拿來對 list 結構作 sort… 所以我們又有一個 list.sort() ,又把資料結構跟演算法接在一起。所以最後希望將演算法完全抽象化出來,將需要的 relation, operation, complexity 抽出來,這樣做也方便分析演算法本身的complexity 哪些是依據 DATA 而不是演算法本身。

作這個之前看看 Purely Functional Data Structure …

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s