Endgame

剛才把 Star Trek: Voyager 七季全看完了。個人覺得 VOY 整體的感覺比 TNG 要好：故事有個主軸貫穿，畫面效果不用說，而且相同議題 VOY 往往敢呈現得更尖銳。這樣 Star Trek 的「當代史」就只剩 Deep Space Nine 啦。

--
感覺上一下子就看完了 XD。

超 High

XOO 寄來的影片。沒想到 category theory 也可以講得這麼 high XD。

--
這應該是英國腔吧？XD

破功

下學期第一次代數導論作業就破功了 ─ 用到第二張紙 XD。

--
都是 ring 的檢查太煩的緣故 XD。

全力進攻

沒想到連 OTT 那邊也發現 HOAS 並不單純，這下只好全力進攻 Yoneda lemma 盡快看懂 HOAS paper 了。雖然 Mac Lane 的銅牆鐵壁難以攻破，但假以時日還是有機會成功的 XD。

--
下午才和 universal arrows 戰了一輪 XD。

---

讀 category theory 總是伴隨著一種特定的頭痛…

--
應該給個學名才對 XD。

Componentwise

當我們有兩個 groups G 和 G'，我們可以取它們的 direct product G × G'，其上的操作是對每個分量個別運算。可以很直覺地想像，這樣的定義確實造就一個 group。

另一方面，任意的函數集 G^A = (A → G)（其中 G 是一個 group）也可以擴充成一個 group ─ 只要定義 (f · g) x = f(x) · g(x) 即可。Martin-Löf 這時會跳出來說：A → G 其實是一堆 G 的 cartesian product，以 A 的元素當作 index。例如 ℕ → G 就相當於 G × G × G × ⋯，一個函數 f : ℕ → G 就相當於一個 countably infinite tuple (f(0), f(1), f(2), ...)。如此詮釋下，(f · g) x = f(x) · g(x) 的意義就很明顯：「f · g 的 x 分量」是「f 的 x 分量」乘上「g 的 x 分量」，其實就是推廣的 direct product。

--
和 accessibility 一樣，這裡丟掉 higher-order 的想法會更直覺簡單 XD。

Meeting day

明天早上到中研院參加 scm 老師召開的 meeting，緊接著下午趕回台大參加隨機實驗室的 meeting 到傍晚。

--
貨真價實的 meeting day XD。

Type-theoretical checking and philosophy of mathematics

下午到圖書館借 Saunders Mac Lane 的《Categories for the Working Mathematicians》，想說如果只是要看前面一點的話或許有機會看懂 XD。在附近瞄到一本《Twenty-Five Years of Constructive Type Theory》，裡面收錄 15 篇論文，包括一些大頭如 Per Martin-Löf 和 N.G. de Bruijn 的文章。其中 de Bruijn 的文章標題是〈Type-theoretical checking and philosophy of mathematics〉，就「machine-checked proofs 和數學活動的相互影響」發表一些看法，讀起來挺有趣的，摘錄兩段於下。第一段對 truth-value semantics 發了一點牢騷：

So natural deduction is by no means a new idea. On the contrary, it follows the way people reasoned before it was tried to explain logic by means of an algebra of truth values. Such Boolean logic is the metatheory of classical reasoning. It does not show what that reasoning is. It is silly that education in elementary logic so often takes truth values as the point of departure.

The idea that truth values are the basis of logic may have been one of the reasons why Brouwer's rejection of the law of the excluded middle was so little understood in his time. If one starts from Boolean logic instead of from natural deduction it is impossible to understand what that rejection means.

第二段對於 mathematical platonism 提出生動的比喻：

A historian writes about things that happened in the past, a journalist writes about what is happening today, but a novelist gets everything from his or her imagination. The first two write non-fiction, the novelist writes fiction, but all use the same language; there are no separate languages for fiction and non-fiction.

Mathematics seems to talk about things, but do these really exist? We seem to have no way to find out, and, worse, we have no way to express what we mean by existence. It is called mathematical platonism to consider the mathematician as a journalist, and anti-platonism to consider him or her as a novelist.

--
這種文章已經可以當作我的休閒讀物了 XD。

大預告

看來大四下回顧會被跳過，直接寫一篇四年總回顧，而且應該會是一篇細緻的自我分析。我已經隱約開始構思脈絡了 XD。

--
說不定應該寫成中英對照，以後申請學校要自傳就給英文版 XD。

OTT

今天和 Weijin 到花蓮拜訪高中同學。因為三人只有一輛機車，所以長距離移動時必須分兩趟，我在等的時候就拿預先準備好的 HOAS paper 和 OTT paper 出來看。HOAS paper 看來並不特別難，只超出我目前的 category theory 知識一點點，最關鍵的 machinery 似乎就是 Yoneda lemma，所以先搞懂 Yoneda lemma 再繼續嘍。至於 OTT paper 還真如 scm 老師所說，是看得懂的耶！而且前幾天用 W-types 模映 lists，試圖把 W-elimination 特化成完整的 dependent foldr 時遇到了問題 ─ 沒辦法證明 [] 只可能有一種實作（intensionally）。讀了 OTT paper 才發現這正是其中一個懸疑點，paper 裡面也沒辦法從 W-elimination 特化出 induction on natural numbers，正是同一個問題，而稍後 OTT 將提供解答！這下我對 OTT 更有興趣了 XD。

--
我會試著在我的系統裡面為（我認知的）慈濟大學的精神找個位置的…

戰意

Haskell-cafe 一個討論串突然拐到 dependent types 來，有人寫了一小段 Coq 證明 length (map f (xs ++ ys)) = length xs + length ys，駁斥「dependently-typed languages 裡的證明都極為冗長、寫起來很煩」的說法。看到 Coq 不知所云的證明（XD）頓時不知從哪裡湧出一股戰意：Agda 的證明漂亮得多呀！Agda 有直覺的 proof terms 和美麗的 mixfix unicode operators，造就了人人稱讚的 equational reasoning combinators，Coq 怎麼比呀！

很快就意識到這種情緒實在太不邏輯了，顯然是因為 Coq 的 pi-calculus code 裡面用上千行 tactics 堆起來的證明不用 coqide 看就看不懂的緣故 XD。

--
顯然今天沒辦法實現新策略 XD。

新策略

發現「十點多上床看 paper 和《Gödel, Escher Bach》看到不支睡著」是個不錯的方案，有助提升睡眠品質 XD。如果有了 iRex iLiad 而不用把 paper 印出來，就更理想了 XD。

最近的主題是「HOAS 沒你想像得那麼簡單」，解法是大家的好朋友 category theory，請讀 Martin Hofmann 的〈Semantical analysis of higher-order abstract syntax〉。

--
不過這樣會打壓到 MSN 時間就是了 XD。

禮物

如果有人想送我禮物的話，我現在最想要的是可以輕鬆舒服地閱讀 PDF 的電子閱讀器 XD。

--
我樂意在螢幕上看論文，可是看久了真的會累…

---

看來只有 iRex 的產品符合要求，主要是螢幕夠大。我目前著眼於 iRex iLiad Book Edition，價錢是唯一令人卻步的因素（雖然這已經是最低階的版本了）…

--
一如往常？XD

Nu

和 nu 有關的性質總是證不出來。覺得可能是因為用 lambda 做 modelling 太強了，之前忽略的條件 name occurrences 似乎也對情勢沒什麼影響。又卡住了…

--
趁機跳回 graphical games 一陣子？XD

---

看起來是 "name" type 的問題。Coq paper 裡面直接預設一些關於 name type 的性質（as Axioms），而我們的 encoding 裡面 name type 是任意的 a : Set，直覺上的確性質比較少。

摘錄一句（from p.~22）：These properties capture the idea that functions of type name->proc are actually "processes with a hole", which can be filled in by any name without changing the structure of the process itself.

--
可是隨便 postulate 好像有危險…

放榜

還是先把這篇打起來，免得畢業之後才放榜 XD。2007 年 4/11--4/17：

本週最令人振奮的消息自然是台大放榜結果。當時是體育課接近下課的時段，一干人往教務處設備組去，想借台電腦放在教室裡連網路（JK 注：這耍特權也耍得太嚴重，難怪會引人非議 XD），12:00 一到就查榜。不料到了那裡，設備組阿姨竟然說「台大放榜了啊」（JK 注：可以回想起當時的晴天霹靂 XD），立時一堆人湧到註冊組長的身邊，然後就是一堆人上了，包括我在內！高中努力不就是為了這一刻嗎？！（JK 注：欸… 也是啦，的確是特別重要的一個目標啦 XD。）回到家想寫信給侯 Sir，卻驚喜地發現侯 Sir 已經在中午以語音查榜，並捎來一封信恭喜了！4/15 還真不是普通的興奮！當然，這樣子就有點對不起交大，尤其是在後來接到交大通知函的時候，交大竟然提供我十二萬五千元的入學獎學金！嘖嘖，這數字的確構成相當的誘惑力，不過我仍然在網路上向台大報到了。另外有個奇怪的地方，是我在台大考的程式設計竟然拿到意想不到的低分，幸好備審資料和學測都不錯，才沒慘遭滑鐵盧，將來到了台大如果可以的劃一定要調出來看看才行。（JK 注：當然後來沒去理它 XD。）

導師的話：當再加強自我，並磨練！ (4/19)

另外也翻一下三上的週記。三上念書念到發慌，竟然在連載老師側寫 XD。

--
剩下的留到下一次回家吧，內容說少也不少，有幾週（如台大遊記）還寫到三面 XD。

高三下週記摘要

高三下學期已經改用鉛筆寫週記，筆跡也潦草得肆無忌憚，內容幾乎都是升學相關。寫第一篇時學測已經考完了，正在等成績，杞人憂天一番之後描述寒假的成果，其中包括學 LaTeX。下一篇就拿滿級分了，再下一篇寫自傳，接下來兩篇等著到台大考試，然後下一篇是台北遊記。再來一篇交大放榜了，台大也在後一篇放榜。接下來一篇是 iPod 使用心得 XD，然後是新竹遊記（拜訪侯 Sir），最後是肉麻的感謝導師文 XD。

這些週記還挺有紀念價值的，大概是高中時期唯一留下的個人資訊，以後回家時慢慢把它們數位化吧。先打一篇起來 ─ 2008 年 2 月底：

完全出乎意料之外，學測竟然拿了滿級分！上一篇週記的擔心全成泡影，不過第一時間取而代之的卻不是狂喜，而是一種從來沒體驗過的茫茫然感覺。不僅是因為沒預料到而沒作準備，同時也因為自己從來沒有在高中時期達到頂峯過。（唯一一次例外是英文才藝競賽，不過我認為那個太顯然。）（JK 注：怎麼有點嗆的感覺 XD。）最近整理備審資料整理到大小賽事，最漂亮的名次只停在中區學科第二，其餘的都是「優勝」、「第三等」、「第七」、「第六」，看上去實在沒有說服力（更別說代表安慰獎的「佳作」）。就連校內的國文朗讀、英文演說，最高也只能到第二（JK 注：看起來很不知足的樣子 XD）。真的是在高中沒嚐過真正的第一名感覺。既然現在已經這樣了，我想下一步就是調適心情，別老是讓 75 這數字踞在心裡。原先在學測前，總覺得第二階段比較好過，現在真的要面對時，才感到壓力。博盛找到了台大程設的考古題，並沒有想像中的簡單，需要好好地複習一下，但也不是太難啦。總之加點油就是了，不能掉以輕心。

導師的話：如果解出，可和博盛討論！ (3/1)

這種長期被壓在下面的情況應該算造成正面影響吧，有一點小小的鼓勵但又時時被現實地提醒還有得拚。其實高中時是有個很紮實的第一名，不過那是班際英文合唱比賽，不算個人成績。不幸的是二下的週記似乎消失了，BBS 班板精華區又突然被板主鎖上、說十年後解密 = =，因此暫時找不到此事件的史料。

--
大學要結束了才急急忙忙要整理高中生活，太遲了吧 XD。

高中週記 No. 10

第十篇高中週記（仍然在一年級上學期），寫於 2002 年 11 月中：

這個星期五數學課教得的是遞迴。之前看遞迴時，總覺得跟程設中的遞迴沒什麼關係。（JK 注：這就是不教 functional programming 的後果 XD。）但這個星期剛好把快速排序法的架構研究出來，對遞迴的應用有了較深的體驗。結果老師拿出「河內塔」並講解它的運作原理後，忽然任督二脈大通，數學和程設的遞迴出現了連結！之後回家後花了幾個小時把河內塔寫成程式，之中還有一次觀念大修正。隔天早上七點多，我將「當天」早上十二點多完成的 BETA 4 版輸入電腦編譯連結後（JK 注：竟然特地寫「編譯連結」XD），執行程式的畫面終於一步一步地出現三層河內塔的詳解，核心部份終於成功了！之後又逐步地加入檔案輸出等功能（JK 注：高中生很喜歡寫這些 systems programming 的東西？XD），加上註解及分段後，約一百五十行左右。（不過後來上網一看，原來早就有一堆人在寫了，而且還是標準遞迴題型、基本遞迴程設……。想想也對，這河內塔又不是什麼稀奇玩意，我想得到自然有更多人也想得到。而且，還是因為看老師的一番講解我才有靈感……。）

還有，老師曾在上課時提到氣泡排序及快速排序。（JK 注：是在什麼語境下會提到排序啊？XD）我在書上看到說有三個著名的排序法：快速、謝耳、夏克排序法。（JK 注：哪本怪書啊？XD）那後兩者的原理是什麼呢？

導師的話：一、欲知內容，多查查資料！二、非一言兩語可完！三、一般而言，快速較快！ (11/18)

這篇模糊提及我對遞迴運算（in particular, tower of Hanoi）的了解是在半夜。用撲克牌搬了好一陣子的河內塔之後，我練習到能夠快速、毫無障礙地搬任意多層的河內塔，之後常用來唬同學 XD。根據記憶，我已經知道可以畫出某種 call tree 並對它做 traversal 而得到解答。

--
做自己的史料分析挺有趣的 XD。

高中週記 No. 4

第四篇高中週記，寫於 2002 年 9 月底（有點距離了…）：

程式設計組在這個禮拜一口氣上了兩次課，內容是 C 語言的基本概念。雖然說是 C 語言，但由於實在太基本了，這個部份因應該是各語言都差不多。（JK 注：我相信你指的是 mainstream imperative languages :)。）由於之前已經接觸過 Java（JK 注：精確說應該是 Java 的「基本概念」），所以對這一段並不陌生。不過，在更進一步學到有關函式數的部份後，對程式裡的函式也有更深一步的了解。邏輯部份在程式裡也是重要的一部份。雖然目前接觸到的沒像課本那麼複雜（JK 注：數學課本嗎？不知道你在說什麼 XD），但少了它是絕對不行的。希望以後數學和程式兩方面能夠相輔相乘，一起往上發展。

導師的話：有關聯，但多麼相關，端看您學到哪裡？ (11/18)

結果學到現在已經相關得不得了了 XD。不過我不認為這段感想對我日後的發展有太大的指標意義，因為高中的時候沒有數學成熟度可言，當時觀察到的關聯應該相當淺顯。

BTW，所謂「程式設計組」是「資訊社」的一組，另外還有人數比較單薄的「電研社」，據說後者是學長因為某些不快事件而出走創立，兩社有些對立情緒。我二年級時，一些人覺得是時候結束這種尷尬局面了，畢竟繼承前朝恩怨沒什麼好處（甚至在行政上遇到麻煩），於是兩社合併，不過根據新社名「電研社」來看可能是簽了不平等條約 XD。不過時間一久這「不平等」也就沒什麼了，現在的電研社學弟們想必都活得很快樂 XD。（欲知詳情請洽 Yen3 XD。）

--
待續 XD。

AC!

XOO 寫信來討論，我才赫然發現證明 weak bisimilarity 的 transitivity 時為了方便而寫的

λΣ₁₁-dist : {A : Set} {P : A → Set1} {Q : (z : A) → P z → Set1} →
             (∀ z → Σ₁₁ (P z) (Q z)) → Σ₁₁ (∀ z → P z) (λ p → ∀ z → Q z (p z))
λΣ₁₁-dist f = (λ x → proj₁₁₁ (f x)) , (λ x → proj₁₁₂ (f x))

竟然就是 ITT 的 Axiom of Choice！突然從實用情境當中跳出來，嚇死我了 XD。

--
所以我們現在轉向研究 type theory 了嗎？

Rach2

又重新迷戀上 Rachmaninoff's Piano Concerto No. 2。另外最近常聽的還有 Bach's Brandenburg Concerto Nos. 2 & 3 和 Tchaikovsky's Symphony No. 6 "Pathétique"。

--
好曲愈揣摩愈有味啊！

過保

不知不覺，PB 三週年紀念日過了大約一個月。這三年和 PB 相處下來，我的心得是以後只要買 Mac 就好了，完全迎合我的需求 XD。希望再撐個一年半到兩年我就可以讓它光榮退休 XD。

--
預計出國的時候換機，所以最後一句暗喻早點解決兵役、學校申請順利 XD。

Back to the Equations

寫完 summation 的 congruence rules 和 commutativity，現在可以做「勉強算是 non-trivial」的 equational reasoning 了：

test : ∀ {a b : Set} {x : Chan a} {y : Chan b} {p q r s z w} →
  p ≈ q  →  r ≈ s  →  (x ! z · p) + (y ! w · r) ≈ (x ! z · q) + (y ! w · s)
test {a}{b}{x}{y}{p}{q}{r}{s}{z}{w} p≈q r≈s =
  ≈-begin
     (x ! z · p) + (y ! w · r)
  ≈⟨ +-cong₁ p≈q ⟩
     (x ! z · q) + (y ! w · r)
  ≈⟨ +-comm ⟩
     (y ! w · r) + (x ! z · q)
  ≈⟨ +-cong₁ r≈s ⟩
     (y ! w · s) + (x ! z · q)
  ≈⟨ +-comm ⟩
     (x ! z · q) + (y ! w · s)
  ≈∎

看到漂亮的 equational reasoning 就覺得前途一片光明啊 XD。

--
睡醒再戰 XD。

Late Semantics

剛寫完新一版的 pi-Calculus modelling，包括 syntax、LTS semantics、weak late bisimilarity 和它是 equivalence relation 的證明。受不了 PB 的速度，只好把 Agda 裝在系上工作站，透過 ssh 把 emacs 的 X Window 畫面傳回來，原本就不知所云的證明搭配預設字型，證得我眼花撩亂 XD（不休息一下眼睛會爆掉…）。用 HOAS 模映 late semantics 意味著要處理 higher-order terms，而這在 Agda 裡面特別不方便。不過用了一個 lemma "lambda distributes over Sigma" 之後，目前的複雜度還算可以接受。Transition rules 有些 side conditions 沒有檢查，所以有可能出錯。下一步是證明所有 congruence rules。

--
證得出來就有進度了 XD。

動手

看起來不太可能復用那套 Coq 的 pi-Calculus library 了：

• Process terms 是用 inductive 的定義。理論上方便，實用上不好寫。
• 對於 (channel) names 的處理，scm 老師本來用的 polymorphic 版本雖然涉及 Set1，但實用上應該比較方便。（Universe construction 畢竟麻煩一些。）
• 只做了 strong bisimilarity，我們真正想要的是 weak congruence。

所以直接動手用 LTS semantics 寫一套新的 modelling of pi-Calculus 吧。還是用 Agda 試一試 ─ 內鎖效應很難掙脫 XD。雖然他們參考的 paper〈A Calculus of Mobile Processes, Part 2〉沒描述 weak bisimilarity（和 weak congruence），但反正就自己定義嘛，證不出來就知道錯了 XD。

另一方面，我們常看到類似「pi-Calculus 不適合用來做 practical programming languages」的說法。這樣的話，把 Haskell 的 concurrency library 和 pi-Calculus 拉在一起似乎引出兩個（或許是同一個）問題：

• 會不會這兩者的層級其實不一樣呢？我的意思是，直接使用 pi-Calculus 對於模映 Haskell's concurrent programs 會不會太低階了呢？
• pi-Calculus 能方便地寫出有意思的規格嗎？

如果有一個實際的好例子的話，這兩個問題就一併解決了，但我目前沒有很好的想法。

--
甩掉 structural congruence，路似乎就又鋪開了 XD。

Theoretically

〈pi-Calculus in (Co)Inductive Type Theory〉才看到 syntax 定義就暗喊不妙 ─ 那定義是 inductive 的！這樣如果要表示一個 coninductively-defined process 的話，就得用 replication operator '!' 模擬。例如持續往 channel x 輸出 t 的 process 'tick' 可自然地寫成

如果用 replication operator 模擬就得寫成

等於是無窮多個 processes 在接力。如果用起來真的很不方便，大概就要整套 pi-Calculus 重寫一次了…

--
理論上用 inductive definition 當然很快樂 XD。

大學技能表

類別	應修學分	實得學分	已修課程	本學期待修課程
共同必修	18	18	國文（6） 英文（6） 歷史（4） 公民教育（2）
系定必修	78	76	微積分甲（8） 普通物理學甲（6） 計算機概論（3） 計算機程式設計（3） 物件導向程式設計（3） 資訊系統原理（3） 線性代數（3） 離散數學（3） 計算機組織與組合語言（3） 資料結構與演算法（6） 自動機與形式語言（3） 數位電子學（3） 機率（3） 系統程式（3） 資料庫系統（3） 作業系統（3） 數位系統設計（3） 數位電路實驗（1） 計算機結構（3） 編譯程式設計（3） 計算機網路（3） 計算機系統實驗（2） 專題研究一（2）	專題研究二（2）
通識	12	13	邏輯丙（2） 宋明理學（2） 音樂作品欣賞（2） 生物多樣性概論（2） 工程發展與社會變遷（2） 東坡詞（3）
系內選修	18	12	人工智慧（3） 資訊理論與編碼技巧（3） 賽局理論（3） 高等編譯器設計（3）	模糊系統與應用（3） 圖形演算法及生物資訊應用（3）
系外選修	10	10	倫理學（4） 知識論（4） 西洋哲學史一上（2）
數學輔系	20	17	高等微積分（8） 圖論一（3） 線性代數一（3） 代數導論一（3）	代數導論二（3）
服務學習	0	0	服務一 服務二 服務學習三
體育	4	3	健康體適能（1） 高低衝擊有氧（1） 現代舞（1）	階梯有氧 + 塑身（1）
軍訓	0	0	軍訓一 軍訓二 軍訓三

主修資訊系、輔修數學系、系外選修全部獻給哲學系，這張技能表還滿好看的 XD。

--
所以最後因為東坡詞多修了一學分 XD。

大四上成績

課程名稱	學分	教師姓名	成績
東坡詞一	3	劉少雄	86
西洋哲學史一上	2	苑舉正	83
線性代數一	3	黃漢水	84
代數導論一	3	陳榮凱	94
專題研究一	2	呂學一	96
高等編譯器設計	3	陳俊良	85
賽局理論	3	呂學一	95
操行			85
平均			88.95

看來平均已經收斂在 88 附近了 XD。隨機客給分慷慨一如往常，線性代數大概是沒上助教課或期末考出差錯，其他分數都如預期。

--
來算一下學分 ─ 應該是沒問題了 XD。

充電期

不讀完 L1 doc cache 裡面的 papers 大概不會有創造力了，看能不能一週內完成。〈pi-Calculus in (Co)Inductive Type Theory〉裡面說 "[w]e can honestly say that we have a real, user-friendly interactive system for proving bisimilarity of processes"，等用了 Coq 就知道他們有沒有吹牛了 XD。另一方面，paper 裡面只做到 strong (late) bisimilarity，而我們最後需要的是 weak bisimilarity 和 process equality，所以說不定後兩者是我們要自己動手做的。

--
不過今天剩下時間我打算留給 graphical games XD。

摘要

明天預定要講的 Calculus of Communication Systems 好像其實只有一句話耶 ─ 和 pi-Calculus 差不多 XD。語法和 pi-Calculus 只差一兩個 operators，沒有 structural congruence 而直接用 LTS 定義語意，然後同樣進入 strong bisimulation、改成 weak bisimulation 再補成 congruence 當作 process equality，複雜度沒下降多少。倒是上次被 XOO 提醒，找到 paper〈pi-Calculus in (Co)Inductive Type Theory〉做 Coq formalisation of pi-Calculus，裡面很明確地說 structural congruence + reduction 不適合做 formalisation，所以他們採用 LTS semantics 再導出 structural congruence 的那些規則。

--
看起來要做就單純是做苦工吧 XD。

Type Metaphysics

最近 Haskell-cafe 有一串標題為 "type metaphysics" 的討論，沿途牽扯一些 computing science 的核心理論如 computability theory 和 domain theory，有點散亂不嚴謹，但可以當作複習 XD。不過這些討論其實離題了，因為發問者最一開始的問題是 "what is a type" 這個本體論問題，最後 Oleg 很適時地跳出來、引用 FLOLAC '08 "Interpreting Types as Abstract Values" 的 lecture notes 漂亮地結束這串討論。

--
要小心 diagonal argument 和 cpos 不太相容 XD。

Persistence

室友的傳統指針式鬧鐘平常設定在早上五點半，我常常被順便叫起床。喔，說「順便」或許不太準確，因為我醒過來的那些 instances 裡面有不少次鬧鐘主人沒醒 XD。此時鬧鐘就會從五點半叫到六點半才自然地噤聲，多次之後我也習慣了，被子蓋住耳朵往往就可以繼續睡下去。更有趣的是，如果下課後早點回來，經常都可以續攤 ─ 主人早上沒醒就沒想到要按掉鬧鐘，所以當指針又抵達五點半的 state 時，除非有人在，否則鬧鐘只好再叫一小時 XD。

今天晚上七點多回到宿舍（有雙螢幕就可以來編代數導論筆記的索引了 XD），鬧鐘又在響了，我還不打算去關掉它（等洗完澡再上別人的床比較好 XD）。做點雜事洗完澡回來，早已超過一小時，鬧鐘卻還在響！這和先前歸納得到的信念不合呀！上去一看，原來秒針凍結在 9 的位置爬不上去了 XD。我拍拍這個相當熟悉但才第一次見到面的鬧鐘，讓它安息 XD。

--
所以走比響更耗電？XD

Shuttlecraft

看了這麼多集的 Star Trek，只要 shuttlecrafts 一出現，大抵就是墜毀、迫降，或是被大船攻擊，很少安全飛完全程的 XD。

--
悲情的 shuttlecrafts XD。