"Abstract" Interpretation

早上陳老師進入 lambda calculus 和 type judgements，我覺得講到 typing 的時候 Curry-Howard correspondence 根本就按捺不住要衝出來啦…

下午莊老師又飛也似地講完怎麼藉著解 least fixed point 而找到 recursive function 的本體，包括我之前一直不太懂的 mutually recursive functions。不過沒有講 recursive datatypes 的解法真是讓我太失望了 XD。最後進入 abstract interpretation，那些數學細節根本是講給在場的老師們聽爽的，我還來不及想通 Hoare power domain 到底是做什麼用，strictness analysis 就做完了 XD。看到 operator P 的時候我很直覺就往後縮一下：那是 functor 嘛！稍後果然也冒出兩張 commutative diagrams，第二張是不是 semi-commutative diagram？其實我一直看不太懂 AoP 的 semi-commutative diagrams XD。

最後果如前一天聽到的消息，到了今年的全場自我介紹時間，我很自然地把「邪教說」拿出來娛樂全場（希望有達到效果啦… XD）。其實我少講一個梗，就是 commutative diagrams 很像儀式圖騰 XD：

有個學弟看到我的 blog 煽動的、傳教式的熱情文字而報名了，真令人欣慰 XD。好像不去找他聊天一下不太負責，可是去找他聊天又有傳邪教的嫌疑呀… XD

--
明天下午是 derivation！scm 老師願意口頭偷加一點進階主題滿足我嗎？XD