硬

今天上的第一次 type system 和第二次的 program derivation 都比較硬，跟的時候比較辛苦 XD。陳恭老師的語調不特別激昂，可是我卻總有種很熱血的感覺 XD。大二上先修自動機果然是正確的，decidability、halting problem 此類詞彙這幾天一直出現，陳老師講到 "function equality can be reduced from halting problem" 時，我（幸好）還隱約能想到大概怎麼做 XD。（不過 Max 提到 first order logic 可從 post correspondence problem 重整而得時，我就不能掌握做法了 XD。） 兩門課之堅硬原因其實不太一樣：上 type system 會一直和以前所學的東西（遠至 C++，近至 intuitionistic logic）產生連結（這要花不少的額外力氣），至於 program derivation 當然是因為抽象層次愈拉愈高的關係，現在我的直覺層頂多到 fold/unfold，再往上把 fold/unfold 這個層級的 entities 當作直覺思考的原子就有障礙了，要看穿更高的抽象層更是辛苦（e.g. hylomorphism）。今天應該要花不少時間消化，希望還有時間寫作業 XD。

Fold-fusion theorem 名字裡的 "fusion" 很生動，幾乎可以看到 fold 外的函數與 fold 融化生成一個新的 fold。Maximum segment sum 的 derivation 看起來的確很過癮，好像在演電影一樣 XD。

--
不消化，危樓就愈砌愈高了 ─ 樓層又剛好蓋得特別快 XD。

---

11:18，把 program derivation 複習一遍並寫完作業。比較習慣這種抽象層級了，可是只是「比較」XD。On the other hand，親手操作 fold fusion 真的有快感 XD。我特別喜歡 banana-split rule 的 fold fusion，雖然簡單，效果卻十足 ─ 兩個隔開的 folds 真的被熔鑄成一個 fold！更別提這是明確把 identity function 寫出來、轉成 fold 後做 fold fusion 了，elegant 到讓人起雞皮疙瘩 XD。

Type system 就只好先排到 waiting queue 裡 XD。（BTW，陳老師沒把投影片放上網站，但我其實習慣看螢幕 ─ 尤其現在這個狀況看螢幕方便許多 XD。）