與騎士共度兩載

六月 22 號舉行最後一次居家音樂會，名為《離別曲》，以蕭邦離別曲收尾。七月 31 號下午騎士鋼琴蹣跚爬上返回 Roberts Pianos 的箱型車，空出位置讓我堆起裝箱的各式家當，兩天後我和僅剩的另一位屋友 (housemate) 也隨之遷離住了兩年的 45 Marlborough Road.

循一貫作風，與騎士共度的這兩年我求深不求廣，絕大多數時間彈的都是蕭邦。不僅忽略其他作家，我也不花時間在基礎練習（如音階）上，每次都直接彈我有興趣的蕭邦曲子。未花時間獨立練習技巧，愈到後期彈較難的曲子時，其缺點愈明顯，因為若不以較嚴苛的標準獨立鍛鍊技巧，曲子要求的技巧難度就不會掉在舒適區段內，每次彈都逼近自己的難度上限，不容易跳躍到專業水準。不過這確實是我一開始就擬定的方針：時間有限，我只想把時間花在「音樂」上，而不打算在技巧上多加琢磨，只要不嚴重妨礙音樂表達即可。我猜想，因為練每首曲子都必須克服技巧上的困難，曲子初練的時間會拉比較長，但反正後階段音樂性的琢磨本來就需要很多時間，初練時間拉長一些對總需時間影響沒那麼大。特別在讀了 Boris Berman 的《Notes from the Pianist's Bench》著意照練並時時錄音檢討後，現在我能較順暢地處理樂句呼吸，注意以低音伴奏帶出韻律，以及較完整地呈現多聲部和對位，兩年下來我明顯感覺到自己在音樂表達上進步甚多。在這方面，獨練蕭邦一家的好處就呈現出來，因為我有足夠多的時間去琢磨蕭邦的神韻，每練一首蕭邦的曲子都有助於我對蕭邦曲風的理解（至於觸類旁通就留待未來了）。彈到後來，我愈能體會「鋼琴演奏乃用腦而非用手」之意思 — 手指落在正確琴鍵上僅僅是開始的一小步而已，樂句、韻律、聲部唱和、結構對比，這些音樂上更重要的性質是每次演奏都必須全神貫注方能塑造出來的，就算只稍微疏忽都會走樣，遠非機械式練習所能達成。

一般若在家，我每天固定下午四點練彈，短則一小時，長可至兩小時。週間這時間經常只有我在家（但也不見得），週末就比較多人，很難不造成干擾。儘管屋友（至少表面上）全力支持，彈到得用力砸的橋段時，我仍不免感到些許愧疚。於是我想，能不能讓這架鋼琴貢獻除了噪音以外的東西？我的答案是：辦鋼琴沙龍與人同樂。騎士鋼琴擺在客廳裡，客廳不大，用來辦鋼琴沙龍正能提供生動溫馨的音場，可彈出大型演奏廳或音響所缺乏的親密感，也恰好呼應蕭邦的喜好。客廳大小也支持我的另一個設定：小而美的聽眾。蕭邦的音樂往往表達很私密的情感，較難向不熟的人傾訴，因此每位聽眾都是精挑細選，並慎重邀請。音樂會的型式不拘，我唯一堅持的是音樂響起時必須成為主角，其他活動必須暫歇 — 無論演奏完不完美，認真聆賞的音樂和當背景伴奏聽的音樂可謂天差地遠，而我想帶給大家的是前者。標準音樂會是兩小時，但我不覺得我的水準值得讓人忍耐兩小時，而且兩小時的曲目我也準備不來。至此我有所領悟：就算以音樂會作為號召，整場聚會不應該是我唱獨角戲，和音樂相比，應該留更多時間讓大家進餐和聊天。最後音樂本身的長度設定為半小時，幾次辦下來我覺得很適當，大家不會被音樂鎖住太久，有充足時間交誼，音樂本身又不會短到淪為配角。整場聚會於是從晚餐開始，約一小時，吃完接半小時音樂，最後約兩小時供大家任意聊天。把晚餐排在音樂前面有個潛在的副作用 — 聽音樂時比較想睡覺，不過實際執行上似乎沒太嚴重。另外我自己得儘快草草吃完，在進食和演奏間留足夠的休息時間。與這兩個副作用相比，把晚餐排在音樂後面的缺點大得多 — 大家必須看著滿桌晚餐吞著口水聽音樂，如果設計成這樣顯然太殘酷了。

音樂會實辦三場。我配曲都是選一首大曲（約十分鐘）搭幾首小曲。第一場辦在 16 April 2012, 晚餐 pizza, 曲目為

1. (Franz Schubert) Impromptu in G-flat major, D. 899 No. 3
   
2. Nocturne in E major, Op. 69 No. 2
   
3. Nocturne in F major, Op. 55 No. 1
   
4. Nocturne in F-sharp major, Op. 15 No. 2
   
5. Barcarolle in F-sharp major, Op. 60
   
6. Encore: Piano Sonata No. 2 in B-flat minor, Op. 35, Mov. 3
   

（若未說明即為蕭邦作品。）第一場以幾首技巧較單純又容易入耳的夜曲（和一首舒伯特即興曲）為主力，以雅致氣勢兼具的船歌壓軸。騎士鋼琴音色深刻清亮，非常適合表現船歌之水波盪漾。彈過這場我才知道現場演奏和平常練習的落差有多大。即使是這麼小的場合，我仍然很難保持平常心，手指僵硬錯誤百出，彈出來的水準比預期低了不少。如 Berman 所說，職業鋼琴家的厲害之處在於保持一貫水準，光就這一點我就清楚體認到我毫無希望達到職業等級。不過接受這事實後，後面兩場我就能放手去彈 — 反正我能提供的本來就只是業餘水準，無需為達不到職業水準而愧疚。原本 21 August 2012 要辦一場畢業屋友的送別音樂會，隔天 22 號飛回台灣教 FLOLAC’12 的邏輯，但因天坪颱風來勢洶洶，臨時決定提前在 20 號返台，音樂會沒辦成。下一場就到了 10 March 2013, 晚餐仍是 pizza, 曲目為

1. Prelude in F-sharp major, Op. 28 No. 13
   
2. Prelude in E-flat minor, Op. 28 No. 14
   
3. Waltz in A minor, Op. 34 No. 2
   
4. Nocturne in B major, Op. 32 No. 1
   
5. Nocturne in A-flat major, Op. 32 No. 2
   
6. Polonaise-Fantaisie in A-flat major, Op. 61
   
7. Encore: Nocturne in E-flat major, Op. 9 No. 2
   

這場乃匆匆召集而成，因那時波蘭幻想曲已大致練好，我想儘快把波蘭幻想曲清倉出去，好移往下一首大曲（第四號敘事曲），趕上搬家前最後一次音樂會。自此場開始，我在每曲之前加一點先導介紹，讓大家聽曲時有點頭緒。如第一首升 F 大調前奏曲 (Op. 28 No. 13) 旋律線很長，如果預先告知的話，（理想上）聽眾就會記得去串起旋律，不至於被一個個單音弄得哈欠連連。波蘭幻想曲只有自己彈過才真正理解其精微之處，其和弦與織理的轉接能拉扯出變化萬千的隱晦情感，能練到這首，租騎士鋼琴就不算浪費了。三個月後，22 June 2013 就是第三場《離別曲》，晚餐由手藝精湛的屋友掌廚，曲目是

1. Nocturne in B major, Op. 62 No. 1
   
2. Mazurka in A minor, Op. 17 No. 4
   
3. Mazurka in E minor, Op. 41 No. 1
   
4. Ballade No. 4 in F minor, Op. 52
   
5. Etude in E major, Op. 10 No. 3
   
6. Encore: Mazurka in F minor, Op. 68 No. 4 (partial)
   
7. Encore: Waltz in A-flat major, Op. 69 No. 1
   

此場大曲是第四號敘事曲，但壓軸是離別曲，向即將各奔四方的屋友以及返台的朋友說再見。（安可曲「告別圓舞曲」也呼應主題。）第四號敘事曲在當兵期間的週末練習，始終沒能練到最後狂風暴雨的尾奏，不料竟在英國練成。除第四號敘事曲需艱深技巧以外，第一首 B 大調夜曲 Op. 62 No. 1 用我最害怕的長串顫音重現主旋律，以往是絕不敢碰，但經兩年鍛鍊，此曲竟已彈得出模樣，相當欣慰。到此場我已能無視於技巧侷限而盡興演奏，離別曲中段的雙手平行半音列和整串六度音群毫無準度可言，彈個大概意境便算，到了曲終幾小節的聲聲道別，我竟經歷與初聆悲愴相似的情感衝擊，自認彈得可圈可點。這場音樂會結束至今我沒有再彈過離別曲 — 我不忍回憶那時的強烈情感。

音樂作為情感載體有個極大優勢：音樂和口說或書寫語言相比抽象許多，是一般人不那麼敏感的頻道，不易令人不適。強烈情感以言語表達，除非有特定語境支持（或曰「氣氛醞釀」），否則往往顯得太突兀，改以音樂抒發就沒這顧慮。例如在一般交際場合坐下彈一曲，再怎麼淋漓真摯也不會有多少人覺得莫名其妙。（與之相比，想像若在同樣場合突然大聲訴說自己有多感動，人們的表情會有多尷尬。）反面論之，這代表音樂是個無法信賴的媒介，不能指望自己所想能忠實傳遞于人。因此，雖然我滿心期待每次音樂會得以和好友分享我的最新體驗，卻也不得不承認聽者和我的音樂間完全可能存在無法跨越的隔閡。我只希望這三場音樂會不完全是我自己一廂情願，前來捧場的好友們能從我的音樂中各取所需並有所感動，至於我的意念是否忠實傳達就不那麼在乎了。

騎士離開時我心情激動。不只因為日復一日地練彈將情感澆灌在這架樂器上，還因為兩年下來 45 Marlborough Road 的大小事都有它默默見證，它離開讓人很具體地意識到這一切真的都結束了。不過至少我畫了美麗的句點 — 那首離別曲彈完時我是滿足的。

何謂定義

批踢踢 Math 板上有人問何謂定義 (#1HRMd9qw), xcycl 邀我回應，於是我（花了四小時）撰文 (#1HRpMZUa) 如下。

---

處理「定義」最簡單的方式我想應該是先區分「後設語言」(meta-language) 和「對象語言」(object language), 然後說「定義」是後設語言裡的機制，目的是為了方便寫出對象語言裡常用或重要的樣式。

我自己的經驗是傳統數學裡很少談「型式」「語法」(syntax) 這類數學物件，到了後設數學必須談這些了，傳統數學寫作風格卻又容易讓後設語言和對象語言混雜在一起。相較之下，程式的本質是符號操作 (symbol/syntax manipulation), 程式員的工作是撰寫（後設）符號以操作（對象）符號，因此若有程式基礎，要區分後設語言和對象語言應該是很容易的。

以下我嘗試簡單介紹一下程式觀點，用的語言基本上是 Haskell, 但符號上略作變動以利數學背景讀者理解，也不使用 Haskell 的完整語意。前半段是 Haskell 簡介，後半段我用 Haskell 寫一點點命題邏輯，藉以說明後設語言和對象語言之分別，以闡明上述「定義為後設語言裡的機制」之意思。

Haskell 程式是由「函式定義」構成，例如

double : Int -> Int
double x = x + x

square : Int -> Int
square x = x * x

這裡定義兩個函式 double 和 square, 它們都接收一個整數並算出另一個整數。（注意 Haskell 語法上套用函式時不寫 double(x) 而只寫 double x, 但必要時還是要加括號。欸，細節就不詳述了⋯ 這篇的例子應該都可以看懂才是。）Haskell 程式執行就只是把一個給定式子儘量化簡，遇到函式時參考其定義，將等號左邊的樣式換成右邊的式子。例如 square (double 4) 的計算過程是

  square (double 4)
= square (4 + 4)
= square 8
= 8 * 8
= 64

（假設 '+' 和 '*' 的行為是我們熟悉的那樣）計算結果即為 64. 簡單地說：直接理解成數學上的代換就行了。

在 Haskell 裡面我們可以處理比 Int 更複雜的資料型態 (datatypes), 例如下面這行

data IntList = Nil | Cons (Int × IntList)

定義了一個新的型態 IntList（想像成集合），裡面的元素是用

Nil : IntList

和

Cons : Int × IntList -> IntList

自由生成的。（Nil 本身就是個 IntList；Cons 接收一個 Int 和一個 IntList, 產出一個 IntList.）例如以下

Nil
Cons (0, Nil)
Cons (0, Cons (1, Nil))
Cons (0, Cons (1, Cons (2, Nil)))

都是 IntList 的元素（如同 0, 1, 2 都是 Int 的元素一般）。如此定義的資料型態我們稱為「代數型態」(algebraic datatypes).

Haskell 提供一種機制「樣式匹配」(pattern matching) 讓我們在代數型態上定義函式。例如，我們可以寫一個函式把某個 IntList 裡面所有的整數加起來：

sum : IntList -> Int
sum Nil            = 0
sum (Cons (x, xs)) = x + sum xs

如此我們便指定當 sum 遇到 Nil 和 Cons 時應如何化簡。因為 IntList 的元素只可能用 Nil 和 Cons 構造出來，有了以上兩條化簡規則，sum 便對任何 IntList 都定義妥當（亦即對任何 IntList 都能確切算出一個 Int）。例：

  sum (Cons (0, Cons (1, Nil)))
= 0 + sum (Cons (1, Nil))
= 0 + 1 + sum Nil
= 0 + 1 + 0
= 1

至此 Haskell 簡介結束。

接下來我們考慮命題邏輯語言最簡單、僅有「蘊含」的版本。這語言在 Haskell 裡定義成

data Prop = Var Int | Imp (Prop × Prop)

我們用 Prop 的元素表示「命題式」 (propositional formulae), 而且變數直接以整數命名（而非常見的 \(P\), \(Q\), \(R\), ... 之類的）。例如

Imp (Imp (Imp (Var 0, Var 1), Var 0), Var 0)

代表的是 Peirce's law, 對應的一般寫法是
\[ ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P \]（假設 \(P\) 對應於 0, \(Q\) 對應於 1.）命題邏輯上可定義二值語意：令真假值之型態為

data Bool = False | True

則命題式之真假值可如此定義：

truth : (Int -> Bool) × Prop -> Bool
truth (s, Var x)  =  s x
truth (s, Imp (p, q)) | truth (s, p) == False  =  True
                      | otherwise              =  truth (s, q)

即：固定變數上的真假值（表示為一個 Int 到 Bool 的函式），給定一命題式，此命題式只可能是變數或蘊含型式。第一個情況時，直接回傳賦予該變數之真假值；第二個情況時，令前件為 p, 後件為 q, 若 p 的真假值為 False, 整個命題式之真假值即算為 True, 反之則算為 q 之真假值。

循此脈絡，可繼續以 Haskell 寫下命題邏輯其餘定義（然後證明定理）。但至此我們已經可以試著理解後設語言和對象語言的分別：我們探討的「對象」是命題邏輯的語言，而探討所用的（後設）語言是 Haskell. 命題邏輯語言在 Haskell 裡面定義成一個資料型態（命題式之集合），其元素是以 Var 和 Imp 自由生成的樹狀結構，本質只是純粹的符號，而我們寫 Haskell 程式來操作這些符號。傳統數理邏輯的後設語言和對象語言直覺上太過類似，從而容易混淆兩種語言，改用 Haskell 的好處是後設語言和對象語言變得很容易區分（前者是整個 Haskell, 後者只是用 Haskell 寫下的一個資料型態）。

最後我們回到一開始的問題：何謂定義？例如，定義 bi-implication \(P \Leftrightarrow Q\) 為 \((P \Rightarrow Q) \wedge (Q \Rightarrow P)\) 是什麼意思？假設我們擴充 Prop 的定義，多加一條 Conj (Prop × Prop) 代表 conjunction. 雙向蘊含在 Haskell 便寫為

biImp : Prop × Prop -> Prop
biImp (p, q) = Conj (Imp (p, q), Imp (q, p))

即：biImp (p, q) 是在後設語言裡對 Conj (Imp (p, q), Imp (q, p)) 的縮寫，而不是對象語言內的構件。更進一步的定義可引用既有定義，但最終會全部化簡（展開）為對象語言。一般說數學基礎是公理化集合論也是這個意思：數學用的符號繁多，但這些（原則上）最終都可化簡（展開）為集合論的單純語言。

※ 引述《yueayase (scrya)》之銘言：
: 看了以上的討論, 我不知道type theory和邏輯符號語言之間的差別

Martin-Löf's type theory 可理解為表達能力極其豐富的程式語言或具完整計算意義的數學基礎理論（包括高階邏輯）—「直構數學」(intuitionistic mathematics) 的定理與證明可在 MLTT 內型式化，並等價於真正能跑的程式。

這領域仍在火熱發展，如近年來由 Fields Medal 得主 Vladimir Voevodsky 領軍的 univalent foundations of mathematics 企圖將 homotopy theory 帶入 type theory, 打造數學的全新基礎。（不過我不熟⋯）

: 因為我也曾經看過像logic set and recursion(http://ppt.cc/PatL)之類的書
: 裡面主要就是在說邏輯符號系統的language structure是怎樣
: 怎樣去interpret這些language意思
: 像之前提到的 A Mathematical Introduction to Logic也是在說這些東西
: 就不是很清楚type theory和這類書籍所說的有什麼差別
: 附帶一提,
: 這些東西又好像和computer science 的 formal language(eg: context-free grammar)
: 或是 computation theory(eg: Turing machine <=> λ-calculus, decidability...)
: 有一些關聯
: 的確, 聽說作Artificial Intelligence的人, 早期好像也在研究logic...

是的，關聯密切。整個來龍去脈詳細要說清楚得花不少篇幅，所以直接打個廣告：這些在「邏輯、語言、與計算」暑期研習營（的偶數年）會提到！課程教材都會上網，例如去年的在這裡。

--
感謝 xcycl 邀我下水以及審稿。

Russell's paradox

Dijkstra 在〈For brevity's sake〉(EWD1070) 用簡潔符號重述 Russell's paradox: 若集合 \(R \defeq \{\, x \mid x \notin x \,\}\) 存在，則
\[ x \in R ~\Leftrightarrow~ x \notin x \qquad \text{for all } x \]將上式之 \(x\) 代以 \(R\) 即得
\[ R \in R ~\Leftrightarrow~ R \notin R \]若接納排中律（從而 \(R \in R ~\vee~ R \notin R\)）則上式矛盾。我想到金次的一題練習：試證明集合 \(S\) 和 \(\mathcal P\,S\) 間不存在對射。這個證明應該也能三言兩語說完：假設 \(f : S \to \mathcal P\,S\) 為對射。定義 \(A \defeq \{\, x \in S \mid x \notin f\,x \,\}\), 則
\[ x \in A ~\Leftrightarrow~ x \notin f\,x \qquad\text{for all } x \in S \]將上式之 \(x\) 代以 \(f^{-1}\,A\) 即得矛盾
\[ f^{-1}\,A \in A ~\Leftrightarrow~ f^{-1}\,A \notin A \]（我們只用到 \(f \circ f^{-1} = \mathit{id}\), 所以「\(S\) 和 \(\mathcal P\,S\) 間不存在對射」其實是因為「不存在 \(S\) 到 \(\mathcal P\,S\) 的蓋射」。）

練習：將停機問題不可判定之證明以上述型式重寫。

--
其實這篇的主要目的是測試 MathJax XD。

Design Patterns @ Oxford

Jeremy 這週為系上的 software engineering programme 開一門 design patterns, 到開課前幾天才驚覺他忘了找助教，寄信給他三個學生討救兵。（或許該澄清一下：Jeremy 找我們純粹是想先找熟人，不是拗學生幫他工作 — 信裡特別說這不是我們的義務。這和我常聽到的師生關係相當不一樣。）我很有興趣聽 Jeremy 如何教這門課（而且報酬出奇優渥⋯），於是接下任務。Software engineering programme 是在職碩士班，每一門課都是一週的密集課程，週一到週四朝九晚五、週五到中午（Kellogg 學院每天供應午餐）。課程型式如同 Oxford 其他課程，講課和上機實習緊密交錯，比方說 design patterns 這門課的主要型式是 Jeremy 每講一兩個 patterns 學生就立刻上機做關於這幾個 patterns 的習題 — 我的任務是解決他們上機遇到的一切疑難雜症。

這五天講了十三個 GoF patterns，實習用的是一個簡單的繪圖程式，以 patterns 重構不良設計或加入新功能。以一般標準衡量，Jeremy 的課程設計和實際執行均屬一流：對每個 pattern 欲解決的問題（具體情境與抽象描述）、標準解法與各種變形、利弊和交互作用等，Jeremy 都給了詳細清楚的說明。實習題目絕大部份是有意義的重構（不會覺得是為了練習而硬套 patterns），各種難度的題目都有，所以進度快的人不會沒事做，進度慢的人可以從容把基本題做好。我相信學生都很滿意。

我就比較失望，因為聽到的東西和我六年前逃離的無甚差別。（不過我不會怪 Jeremy — 改良這種材料完全算是科研題目。）我當年逃離的是「本質上無法精確描述的方法」以及「難以控制的複雜語意」。才聽到第一個 Observer pattern, 當 Jeremy 搬出 sequence diagram 講解通知機制的運作流程時，我心中（的 Dijkstra?）就已不斷吶喊，如果到這個抽象層級還需要仰賴這麼低階的操作語意才講得清楚，情況真的是很糟糕。隨著 patterns 累積，程式行為急劇趨向複雜，協調這些 patterns 時，程式員所擁有最可靠的工具卻仍然是他們的直覺，仰賴的仍然是最原始的運行語意 (operational semantics)，程式不亂才怪。（或許 aspect-oriented programming 能幫點忙？不過我猜這仍是 ad hoc 的解法。）換句話說，patterns 沒有具體型式可供組合，也沒有精確刻劃讓人能在套用 patterns 之後方便推論程式性質，只能算是用來訓練程式員直覺的讀物，但我們真的還需要比直覺更好的東西。（換成 Dijkstra 會說「我們需要的是比直覺更好的東西」，不過我不認為我們有辦法丟掉直覺。）

Patterns 有個特徵倒是值得追求的：問題導向。任何 pattern 都從問題描述開始，之後才提出解法。我們需要更多這種把問題轉成解法的方法，而不只是一堆不知如何和問題連結的工具。最後是廣告時間：我和 Jeremy 剛投到 ICFP'13 的論文〈Relational algebraic ornaments〉正是企圖把 inductive families 這項工具透過 relational program derivation 連結到更多問題！

--
Dijkstra 不知何時才能瞑目 XD。

FLOLAC'12

四月 scm 老師寄信給我，問我有沒有意願接下 Max 的棒子，教 FLOLAC'12 的邏輯。這對我自然意義重大：踏入程式語言理論是因為參加 FLOLAC'07, 接著 '08 和 '10 兩次海洋年擔任助教，現在第一次正式授課也在 FLOLAC'12. 邏輯在兩週的 FLOLAC 課程裡扮演開天闢地的角色，讓學生第一次親密接觸型式系統，並擁有特權與義務點出 Curry–Howard correspondence, 連結數學與計算、證明與程式（這層非型式的連繫其實需要另外命名，例如 propositions-as-types principle 或 Brouwer's dictum），講授這門課的責任相當重大。不僅如此，數理邏輯本身有豐富的歷史脈絡，並有不少科普宣傳，學生勢必會對這塊很有興趣。我接下棒子，如臨大敵。

備課

五月底交出 WGP'11 paper 的期刊版，六月我便著手準備課程內容，直到八月初才大致底定。這樣的時程完全超出我的預期 — 我最先的計劃是花一個月連同最後的打磨拋光全部完成。七月中我和 Jeremy 見面，很慚愧地告訴他我都在準備 FLOLAC，博士論文要用的材料全無進度，Jeremy 卻出乎意料地笑著說「我能夠理解」，並說他的經驗是一小時的課至少得花十小時準備，如果對材料不熟還需要更多時間。Natural deduction 那些基本的東西我自然很熟，但是進一步的結果如 soundness, completeness, Gödel–Gentzen negative translation, canonicity 我並沒有真的證過，二十世紀初數學基礎大論戰的各流派與概念我也還沒理出足夠清晰的脈絡，這些都必須先自己補齊（我在課程網頁列的參考資料有不少是這段時間才第一次讀）。各主題的取捨、呈現、與串接都費了我不少工夫，一個小例子是 completeness 證明快寫完的時候決定換成結構化證明，前面寫好的十七世紀證明只能全部扔掉重寫。最終設計特別有趣的大概是下列幾點：強調直構主義（intuitionism）、解釋迭構法（induction）的立論基礎並操作之、緊扣數學與計算之間的連結。

我參考的是 '07 年 Max 的架構，一次講 intuitionistic logic 和 natural deduction, 一次講 classical logic 和 formal semantics, 最後一次講 Curry–Howard 並提點 languages, deduction systems, 和 semantics 的相對關係。（Max 在 '07 年第三次上課還有講 equational logic, 不過那算是 bonus, 我認為重點還是在 Curry–Howard 和整門課的架構提點。）與往年最大的差異是我特別把直構邏輯拉到第一次上課講（辦公室有位同事看到我的授課大綱，還很驚訝地說「你從直構邏輯開始耶」），因為 de Bruijn 在〈Type-theoretical checking and philosophy of mathematics〉諄諄告誡

[...] [N]atural deduction [...] 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.

古典語意被我刪減到差不多只剩基本定義，最後還收尾在 Gödel–Gentzen negative translation, 把古典邏輯嵌入直構邏輯，藉以說明前者的表達能力從某個角度來看其實弱於後者。這麼偏袒直構邏輯，我的辯解是：反正到其他地方都是古典數學說了算，直構數學根本連露個臉都沒機會，就只在 FLOLAC 這裡讓我們聚焦於直構數學吧。

邏輯從第一個定義（propositional formulas）開始就大量使用迭構法（induction），但很少有人真的從迭構定義（inductive definitions）開始解釋迭構法為何有效，頂多只是給一些型式原則。我對北京清華第二屆 Coq summer school 印象最深的是他們特地設計一門課來講迭構法的精神和各種型式，我認為這是非常恰當的設計，因為程式語言理論有一大半的根基是迭構法，沒好好解釋迭構法相當於沒紮好根基。但是我沒有時間從自然數的迭構法開始慢慢講，所以我選擇只在介紹 propositional formulas 的時候一併交代一下迭構法。另外我希望展示迭構法的有趣應用，在邏輯的話，最適當的應用應該非 soundness & completeness 這類性質莫屬了，但這是在 derivations 上的迭構，而 derivations 用一般的迭構法造不好，得用上 inductive families 或是 induction-recursion 之類的手法。我當時設計到這裡猶豫了一陣，不知道該不該深入至此，但最後還是把 derivations 寫成一個 inductive family 然後真的下去用迭構法證 soundness & completeness, 因為我猜測 Coq 真的想證點東西的話不可能不用 inductive families, 先講的話，到 Coq 那邊應該就比較不怕了。（結果我錯了，Arthur 只有展示 Coq 的火力，沒真的帶著學生用 Coq 寫各種迭構定義。）

我堅持要講 soundness & completeness 證明的另一個理由是，最後我希望把 induction 和函式編程的 fold 連結在一起，為此我採用和函式編程相近的語法，從一開始就強調 induction 的計算意義，並給一些證明，希望學生到最後能從這些例子隱約體會到證明與程式確實是同一件事。習題裡面還放一題請學生自己跑一次 completeness 的證明。（這計劃也以失敗告終。一個外在理由是：我預期函式編程是莊老師教，照莊老師的速度，fold 最慢到第二次上課就會出現，我第三天講這連結，剛好能銜接上。結果函式編程換成 scm 老師教，scm 老師又剛好決定要大幅簡化課程，只在他的課最後很快提一下有 fold 這種東西，所以連結失敗。）我一直覺得資訊系學生成天寫程式卻排斥證明，這種情況從 propositions-as-types principle 來看實在很不健康。要是我的邏輯課只是敘述一堆定理都不證明，那就又讓他們多看到一個壞榜樣。造成這種情況的原因大概是他們對程式的認識不夠健全，以及古典數學證明一般不具建構性，以至於難以發現程式其實和證明一樣，都是在描述如何建構具所需性質的物件（而不只是指引機器操作符號的腳本）。「補全對程式的認識」會是 FLOLAC 其他課程的目標，但最後想把程式和證明這兩條經脈打通的話，大概只能從邏輯這裡補上一指了。

整體設計我相信立意良好，但九小時要達成預定目標，無論對講者和學生都非常困難。我的設想是盡可能不要把東西直接丟給學生要他不假思索接受（所以比方說要下迭構定義之前最好先把迭構講清楚），但學生還是要自己掙扎一番才能納為己有。但掙扎需要時間。隨著投影片製作告一段落、實地演練授課之後（倒楣的 housemate 被我抓來上了好幾小時的課），時間不足的問題更是明顯。如果我有一學期的時間，我根本不會從邏輯開始 — 我一定先講基礎的函式編程和迭構證明，並搭配 Agda 之類的語言，悄悄引進 propositions-as-types principle. 等到對「程式／證明建構」培養出足夠的直覺之後，才開始講邏輯和 Curry–Howard. 這樣的順序呼應直構數學「邏輯是數學一部份」的看法，講邏輯的時候也才有更多具體經驗支持。但我只有九小時。最後我想，學生能聽多少就聽多少吧，反正真正有興趣的學生大可日後慢慢研究（掙扎）。

課程準備大致完成，八月 27 號逐漸逼近，但這時天坪颱風也逼近了⋯

食衣住行育樂

今年台灣颱風特別多。原本我預定八月 22 號倫敦起飛、於香港轉機、23 號傍晚抵達台北，但突然殺出一個天坪颱風。20 號看天坪的預測路徑，竟然正好在 23 號籠罩台灣，並繼續往香港推進，最壞情況我說不定得滯留香港機場不只一天。我於是決定改期，提早在 20 號當天晚上出發，搶在颱風抵達前回台。21 號原先有一場家庭音樂會，我準備蕭邦離別曲和 Op. 17 No. 4 馬厝卡等曲子要歡送拿到學位即將返台的 housemates, 也草草取消。FLOLAC 開始前幾天，天坪掠過南部，緊跟在後面的布拉萬也北偏撲向韓國。正當我以為逃過一劫，颱風們竟又發動速攻魔法「藤原效應」，布拉萬牽引下，天坪迴轉再次往北掃過台灣！眼看第三天的邏輯課就要泡湯，幸好最後天坪東偏，沒對台北造成什麼影響。

兩週的課程於是順利進行。回憶當年，FLOLAC'07 前夕我左手鷹嘴突骨折，吊著一隻手去中研院資訊所上課。Yen3 義務擔任書僮，和我住在中研院活動中心兩週，生活全賴 Yen3 打理。晚上寫完作業躺到床上，兩人胡亂閒聊，不亦樂乎。這次 Yen3 找到價格低廉的短期租屋再與我合住（不過這次聊的話題都比較沈重 – 我們已經不是當年無憂無慮的大學生了啊）。第一週我忘了帶睡衣，向 Yen3 借一條極其寬鬆的褲子，週末我回家重整行李，第二週輪到我借他浴巾。我們每天早上走一小段路去吃古亭站出口處的弘爺漢堡（「宮保鐵板麵」不錯）然後搭捷運到台大，晚上通常和一群人吃飯，然後帶著飲料回去。Yen3 每天要跟女友柔言細語一番，另選幾天外出和女友共度甜蜜時光。這次完全沒回 118 巷，因為認識我的兩家餐館都關了，只到台大牛肉麵和資管系對面巷子裡的平價拉麵重溫一下熟悉口味。Yen3 在拉麵店附近發現一家最近從師大夜市搬過來的店，賣綠色臭豆腐和蘭陽米粉羹，相當好吃，讓我回去好幾次。FLOLAC 的優良傳統「美味便當」仍然延續，好幾天讓我在不同便當菜色之間猶豫不決。雖然台北食物的 CP 值大勝，但習慣了中興新村和牛津的小鎮風光，對台北無止盡的水泥叢林不由得感到厭倦。唯一令人懷念的大概只有國家音樂廳，水準完全不輸倫敦。上次進國家音樂廳是兩年前，FLOLAC'10 進行中，我即將赴英，和奇特裸子植物（現於 UT Southwestern 攻讀博士）一塊聽的是 Garrick Ohlsson 的鋼琴獨奏會。這次我選 FLOLAC 中間那個週日下午和 Yen3 一塊去聽 Eldar Nebolsin 的鋼琴獨奏會，進場前還先席地坐在國家音樂廳的飛簷下改了一陣子作業。坐到離舞台這麼近的位子還是第一次，好像要帶領全場聽眾衝進 Nebolsin 捲起的旋風之中。

講課

不過重頭戲當然是邏輯課。要一言以蔽之的話，可以用英國人的說法 "could be worse". 第一天早上緊張得連喝杯豆漿都很勉強。很快共同教室 203 就坐滿人，蔡老師帶著資管系主任來開場。scm 老師今年沒放「煉獄與海灘」投影片，交代一點行政事項後就換資管系主任，後者還很有興致地講一大段。好不容易輪到我啦，第一段 propositional formulas & induction 講得還行，可是講完就下課了，和我「只使用半小時」的目標相差甚遠。下課時 Jaiyalas (or Yen3?) 偷偷跟我說 scm 老師聽到一半就狂皺眉搖頭，覺得內容太難。（我想：蛤，那明天還有 inductive families 怎麼辦⋯）第二段上 natural deduction, 已經講到有點昏了，速度愈飆愈快，例子除了前一兩個以外全部略過，到爆炸原理還絆了一下。第三段是我最不拿手也最討厭的 first-order logic, 撐到 variable capture 終於崩潰了，完全想不到該怎麼解釋「binding structure 改變」有什麼不好，結果硬生生斷開繼續往下講。到了 natural deduction for first-order logic, 這裡 forall-introduction 和 exists-elimination 的 side conditions 也相當棘手，我倒是有給解釋，只不過抽象得應該沒什麼人聽懂。第一天的課就這麼連滾帶跑，最後突兀地停在 natural deduction 的符號海當中。事前設計是第一天用 Heyting arithmetic & Hilbert's program 收尾，讓學生知道前面那套符號是因應什麼樣的問題而發展出來。現在糟啦，沒頭沒腦扔給學生一大堆符號卻沒交代清楚這是幹嘛用的；如果只是這樣那還算了，但我連關鍵技能 natural deduction 也沒講好。我覺得好對不起 scm 老師，把 FLOLAC 開宗明義的第一門課全搞砸了。中午只吃幾條海帶，下午精力耗盡，坐在教室後面倒頭就睡。

第一天晚上準備隔天的課時，心裡已經坦然許多：今早已經上得奇差無比，明天講再差也不會比今天差。傷害已經造成，現在該做的是損害控制，後面課程的難度也要下修。隔天早餐成功吃下一份玉米蛋餅配冰奶茶。第一堂課先重新講解 induction principle 為何有效（稍後將推廣到 inductive families 的 induction principle）和 natural deduction 由下而上和由上而下兩種方向的解讀方式（稍後的 soundness 其實就是由上而下的解讀），然後把 Heyting arithmetic & Hilbert's program 講完，講得出乎意料地順，特別是 Hilbert 將古典數學區分為真實、理想兩部分，然後舉射影幾何「無窮遠處的點和線」為例，這一段我還挺滿意的。第二堂課講 classical semantics 和 derivations as an inductive family, 也講得不錯，特別在解釋後者時行雲流水，從不能用一般 inductive definition 的原因到 inductive family 的直覺解讀方式都妥善交代了。這節下課我在回答問題時 scm 老師走來拍拍我的肩，似乎很滿意，不過我忙著回答問題沒細看，說不定只是跟我打招呼 XD。第三堂講 soundness & completeness, 並稍微提一下 Gödel–Gentzen negative translation 的意義。照原先計劃，我在實際的 derivation 上大略說明 soundness & completeness 是怎麼跑的，然後提點一下證明的架構如何和我講的實例對應，停在我認為滿適當的抽象層級。或許是一開始沒抱什麼期望，第二天講完覺得表現出乎意料地好，信心瞬間恢復。或許因為這樣，第三天太過放心，結果又講得零零落落。

第三天的備課是半夜在床上突然醒來，索性就躺著全程想一遍，想到不少好說法。事後證明這種備課模式極不可取，既沒有養精蓄銳，想到的東西又容易忘掉。下午換一間教室，草草把討厭的 classical semantics of first-order logic 結束掉，趕快進入 Curry–Howard correspondence. 半夜想到的說法重現比較成功的大概只有最一開始，把 natural deduction derivation 變成 typing derivation、然後把 lambda term 直接畫在 derivation 上，從而能直接觀察到 derivation 和 lambda term 的結構確實一樣。接下來 simply typed lambda calculus with constants 就只是一板一眼講過去（這次比較聰明，直接跳過 abort）。「Detours 講得不是很順，不過隨便啦，趕快跟 redexes 扯上關係，帶到 underivability.」講到一半，已經覺得精神不夠集中，不太能隨心控制講話內容，前面那句大致上是當時的想法。終於，到 propositions-as-types principle 又崩潰了，但這次是不自覺的崩潰：把直構數學和編程拉在一起的時候還好（可是請 Dijkstra 出來露臉的時候我忘記講投影片頁碼的字體是 Dijkstra 手寫體！），進入 type families 時竟然忘了闡述關鍵 "type = set = proposition"，證明程式直接全部摻一塊講得不亦樂乎，把台下學生甩到不知哪裡去，下課學生問問題，我才發現失誤得有多離譜。最後留下一點時間檢討第一次 natural deduction 的作業，效果也不好：早上收作業但看得不夠細，後來幾天改作業看到不少常見錯誤，檢討時都沒能提出來。第三天基本上也是失敗的。

讀了 Boris Berman 的《Notes from the Pianist's Bench》之後，我更加確定授課（演講）和音樂演奏有很多原則是共通的 — 兩者本質都是在時間上堆砌出某種結構（在音樂是情感的跌宕，在數學則是概念的排列連結），而且這結構有不同尺度的內容要呈現（在音樂必須兼顧每個樂句的語氣乃至整首曲子的分段，在數學則是從證明細節到重要概念的相對關係都必須說明清楚）。不過，相對於演奏，講課技巧上還是比較簡單，對語言精準程度的要求遠不如音樂家對於每個音強弱長短的拿捏；一句話說得不好，再說一次一般沒什麼大礙，但從沒聽過哪位鋼琴家彈到一半停下來說「抱歉我這段重彈」。如果把這次講課比作演奏，只能形容為荒腔走板，頂多聽得出大概是什麼曲子而已。不過真的獲得不少寶貴的實戰經驗，以後會講得更好。

順便提一下兩次作業。第一次全是 natural deduction, 我出題時不小心畫太多雙箭號，每畫一個就讓 derivation 變成兩倍大，學生痛苦完之後，就輪到我面對幾十份飽滿的作業，足足改了好幾天。不過大部份人都做得不錯，還有些導法是我沒想過的。（考試最後一題 admissibility 有人想到不用 weakening lemma 的導法，也出我意料之外。）第二次請大家寫證明，情況就很慘烈。尤其第一題 "Γ ⊧ φ iff (Γ, ¬φ) is unsatisfiable"，我出的時候完全認為是暖身題，連接詞和量詞小心弄清楚就行了（natural deduction 做了這麼多，應該能觸類旁通吧），結果收來一看，大部份都不知所云，想修補還不知道從何修補起。雖然我上課的確沒細講證明，也沒給多少時間消化吸收，但來修課的不乏大學高年級和研究所學生，這種程度的證明都寫不周全，很明顯反映出工科的數學教育輕忽證明訓練。這樣的教育方向真的好嗎？

聽課

scm 老師臨危受命，除了本來的 program construction 以外又接下 functional programming. 不知道 scm 老師在資管系受到什麼樣的打擊（或啓示），上課速度慢得不可思議。我私下向人解釋 Church numerals 的時候順便講了一下 fold, 以為破了 scm 老師的哏，結果十八小時的課別說 fold fusion, 連 fold 都沒真的講。Fold 算是學 FP 必撞的一道牆，既然如此不是應該編入課程幫助學生跨越嗎？而且我還是覺得沒有講 fold 的 FP 只是讓人稍微嘗鮮，跳不到全新的角度看編程。不過在意見調查表上 scm 老師的課得到一致好評，讓學生容易聽懂的設計確實有成功。另外邪教說已經成為 FLOLAC（海洋年？）傳統，今年邪教檢查表堂堂進佔意見調查表最後一頁，scm 老師更正式坐上邪教教主大位，可喜可賀 XD。

本次最期待、聽完也最滿足的是 Favonia 推銷直構數學的特別演講。Favonia 的演講風格在正經和玩笑之間取得巧妙平衡，而且有種現在已經很少見的誠懇。整場演講把直構數學的特點鋪敘得很成功，並引發 FLOLAC 史上最熱烈的討論。有不少說法（比方說爆炸盒！）是我往後打算一再引用的。陳恭老師、陳郁方老師、和董世平老師講的都是舊東西。今年外國講者 Arthur Charguéraud 負責介紹 Coq, 安排一次上課教 separation logic, 最後講他博士論文做的 characteristic formulae. 我本來很懷疑 Arthur 如何在九小時內教完 separation logic 而且還在 Coq 裡面驗證 imperative programs — 北京清華的 Coq summer school 是到第二週最後才有一個很簡單的 imperative programs 驗證練習。答案揭曉，原來 Arthur 給的比較像是火力展示，重點擺在「Coq 能做什麼」而不是「Coq 怎麼用」。Separation logic 就有細講，但對於剛接觸這一切的學生 Arthur 的速度應該算滿快的（我的課也差不多？）。Arthur 的英文沒什麼法國腔，有問 Arthur 問題的學生也能流暢溝通，但教學回饋一如往年還是有很多人說自己英文太爛聽不懂，甚至有人建議不要找外國講者。欸，要聽 Coq 這種主題想從國內找人講還真的找不到耶⋯

教與學

我在大學最狂妄的時期對老師的要求極其嚴格，現在自己上台才更真切了解那時的要求有多苛刻。教與學有某種關係是我以往沒有真正察覺的，一個有趣（但不深）的比喻是線性代數裡 linear forms 和 vectors 的關聯，兩者看似截然不同，深層卻有完美的對稱性。老師備課和回答問題，不妨看作是學生交作業和應試的升級版：備課是交出一份規模龐大又得精心雕琢的作業，回答問題則相當於應對五花八門甚至毫無預警的試題。備課不妨比喻作設立一套場景供學生跑跳，這套場景是否能讓學生輕易找到前進方向、是不是所有細節都設置妥當沒留下邏輯上的空白、有沒有呈現美感、啓發，諸般複雜考量若要兼顧，需要大量創意。至於學生問的問題，在這種入門課一般不需要太艱深的答案（反而應該避免），考驗的是老師是否已經為基本概念建立一套體系並能夠完善、白話地說明。說明的深度可以比科普難一點（多用一點術語）但還是接近科普 — 這不見得比直接技術上的討論簡單，往往需要回到概念的本質，從那裡開始重新打造易懂的說詞。整個對稱關係不光是師生一同研討一門知識學會新東西而已，學生和老師各有自己的工程要建構並接受檢驗，在「教學」這種互動模式下一起成長。這麼早被放到「教」這個位置倒是沒料到，有種被強迫長大的感覺。被叫老師很不習慣，可是中文的輩份表示又根深蒂固。英文這方面的規定輕鬆很多啊。

打從一開始我就決定要待滿兩週，希望見到很多熱情的學生、回答很多有趣的問題、參與很多深入的討論。事實證明我果然押對寶了。今年 FLOLAC 似乎因為口碑慢慢打響（還是因為開成暑修課程有正式學分？），修課席次供不應求，一掃往年「告急」的窘況，若計入旁聽席次更讓整體聽課人數翻倍，光從這種態勢就可預期今年會擦出很棒的火花。我後來一直說，這次邏輯課其實是被學生救回來的：我講得這麼不周全，學生卻能自己領會那麼多，課後又不吝於發問，讓我有機會好好重講一次。光邏輯一門課，來問我問題的人就比我想像的還多（其中真的去讀 soundness & completeness 證明或至少有興趣的人不算少，令我很欣慰），廣度和深度也令我驚嘆。事前花那麼多時間準備沒有白費！我應該是最常在場的講師，所以也得以回答一些其他課的問題，稍微復習一下基礎。最令我印象深刻的一幕當屬 Favonia 演講後那個場景，眾人自發形成數個圈圈熱力十足地討論起來。身處其中一個圈圈，我好像又變回熱情單純的大學生，和一群同樣熱情的同學討論超級有趣的學問。（這種盛大場景嚴格說來在我大學時期沒發生過 — 我大學時人際關係處理不佳，總是獨來獨往。）想到日後有更多與熱情學生切磋的機會，我就又燃起把博士讀完的動力。（殘酷事實先不用告訴我沒關係 XD。）這大概是我在 FLOLAC'12 最大也最意想不到的收穫吧。

--
28 Sep 2012: 抵英兩週年紀念日。

Divergence

我悄悄掩上門。門後會計處的大家圍成一圈開會，討論如何將工作重新分配給僅剩人力。會計處全員集合開會還是第一次見到，可以想見這次組織再造在即導致人力不足所造成的危機有多大。出內政部中部辦公室大門，順著府西路往下，經過已成一堆瓦礫的彰客總站舊址，在中興新村牌樓前等著回彰化的 6916 次公車繞過圓環。我想著，剛剛掩門前所見的景象作為最後一幕，應該滿恰當的吧。

早上抵達會計處時還真是大吃一驚，整間辦公室稀稀落落，透著一股破敗氣息。稍後才知道只是一群人送佳蓉姐去新單位報到，中午就回來。雖然如此，自年初以來，這次一口氣有好幾位退休調職，社會司也不再出借役男給會計處（便當業務歸老機科），科長另外找到兩位公行役分別幫忙帳務和收發。我的老位置現在空出來了，得以吃著上禾的海鮮燴飯、從熟悉的角度再次看著午休的中辦。當然，兩年過去，我已經不再對傳真機和電話敏感，雖身處熟悉場景但已然置身事外。而很快地，就連這個熟悉場景也要瓦解了。

前陣子最震撼的新聞當屬蔡專員調職台北。實在很難想像沒有蔡專員照顧的役男生活是什麼樣子，幸好我不需想像。剛好這次待在台北，傳簡訊約蔡專員吃飯，發出去沒幾分鐘電話就來了。我隻身抵達蔡專員的辦公室，蔡專員現在統轄數十人，但工作反而比較不費心力。蔡專員調出役男通訊錄連撥好幾人的手機，大家都忙，但最後承賢和顯光顯奕兄弟還是排除萬難前來赴會。蔡專員依舊健談，而且與蔡專員相處的感覺和以前相差並不太多，不像與會計處那樣明顯地漸行漸遠。這很好解釋：以往我與蔡專員互動的場合多是聚餐或閒聊，這次也是。我和會計處大家的互動就有很大一部份是「業務」，丟失那一部份後，感覺自然得變。

琦皓和振弘為我在台中辦了一場聚餐，找到兩位熟識學長，在台北沒見到面的威廷也特地南下。吃完飯全員至龍騰斷橋和勝興車站一遊，專業攝影師威廷臉一直埋在相機後，事後照片貼上臉書，張張是唯美沙龍照。大伙的工作各有變動，只有我仍維持學生身份。當年一起爬的虎山、一起拔的網路線、一起訂的大苑子、一起衝的合歡山，印象猶在但已逐漸褪色。之後大伙走上的路大概會更加歧異吧。

為什麼只靠陳舊的記憶，就可以把一群人繫在一塊？這問題我不想要任何答案。

--
下一篇是 FLOLAC'12 心得⋯

[facebook digest] Home and back

1. "[E]xcellence is a competitive notion, and that is not what we are heading for: we are heading for perfection." ↦ E.W.Dijkstra Archive: Introducing my fall 1987 course on Mathematical Methodology (EWD 1011)    [2011-11-08 23:30:37 +0100]
   • Josh Ko ⇒ But better not develop an aggressive personality like that of Steve Jobs or, indeed, Dijkstra..    [2011-11-08 23:34:01 +0100]
   • L********** ⇒ Sometimes a strong argument is necessary    [2011-11-09 01:54:31 +0100]
2. Tom Melham mentioned today that a philosopher did propose something like whatever can be expressed in a language is/should be correct. He said Spinoza but wasn't sure. (I guess it's not Spinoza.) Does anyone has a clue?    [2011-11-08 23:39:39 +0100]
   • Josh Ko ⇒ Can it be Wittgenstein? I am not familiar with his work (yet) and cannot be sure.    [2011-11-08 23:41:37 +0100]
3. Mail2000 just solved the IMAP problem. Good!    [2011-11-09 11:56:59 +0100]  [ 1 人說讚！]
4. There's a generic programming course at Utrecht, which requires students to present published papers and design problem sets about the papers. I looked forward to doing the problems on OAOAOO, but they turned out to be just about Conor's ornaments (i.e., Section 2).. well.
   
   http://www.cs.uu.nl/wiki/pub/GP/Exercises/Set4.pdf ↦ http://www.cs.uu.nl/wiki/pub/GP/Exercises/Set4.pdf    [2011-11-11 10:10:35 +0100]  [ 1 人說讚！]
5. It just occurred to me that I can apply for funding from the College instead of just draining Jeremy's project fund. Just wrote to the academic office to ask some questions.    [2011-11-11 16:26:58 +0100]
   • J********** ⇒ Can't be terribly much though?    [2011-11-11 17:50:06 +0100]
   • Josh Ko ⇒ No. But three hundred pounds are worth applying for, right? XD    [2011-11-11 18:16:50 +0100]
   • J********** ⇒ which is worth around 50 plates of pad thai, absolutel!    [2011-11-11 19:31:08 +0100]
   • Josh Ko ⇒ XD    [2011-11-11 21:15:24 +0100]
   • J************* ⇒ Even if the money isn't very good, you can add to your CV another source of funding.    [2011-11-11 23:56:12 +0100]
   • L********** ⇒ Is it open to students from other colleges?    [2011-11-12 02:09:38 +0100]
   • Josh Ko ⇒ It's for Univ students only, set up specifically for funding travels (maximum £300 per student per annum). St Catz might have something similar?    [2011-11-12 10:09:54 +0100]
   • L********** ⇒ Yes, we do.    [2011-11-12 12:59:53 +0100]
6. Don Knuth will give a departmental seminar on next Tuesday.    [2011-11-11 18:18:18 +0100]  [ 2 人說讚！]
   • L************** ⇒ I'd like to see it as well!!    [2011-11-11 18:34:05 +0100]
   • Josh Ko ⇒ You'll need to be in the lecture theatre by 4pm.    [2011-11-11 21:14:45 +0100]
7. Curious: While lots of efforts are putting into suppressing the second components of Sigma types, what I need is probably a way to suppress the first components.    [2011-11-13 20:46:00 +0100]
8. Ralf is right: Okasaki's numerical representations is likely to be closely related work. I wonder if the ornament framework will be able to subsume that?    [2011-11-14 11:22:33 +0100]
   • Josh Ko ⇒ Okasaki didn't make the connection between the implementations of number systems and containers explicit (he just pointed out the similarity informally), which is what the ornament framework can offer and even generalise.    [2011-11-14 11:25:37 +0100]
9. Just finished reading Steve Jobs' biography. He certainly should have been awarded a PhD - he had a clear thesis and developed strong arguments (the products) for it. The biography can be regarded as his dissertation (written by someone else, which is convenient!).    [2011-11-15 00:25:18 +0100]  [ 2 人說讚！]
10. Finished reading the /Hound of the Baskervilles./ Now there's only the /Valley of Fear/ that I haven't read (in English) among all Holmes' cases.    [2011-11-17 23:53:45 +0100]  [ 2 人說讚！]
11. Got the best poster award (from Jim Davis).    [2011-11-18 18:24:52 +0100]  [ 4 人說讚！]
    • D******** ⇒ 太強了！    [2011-11-18 18:25:32 +0100]
    • J********** ⇒ Jim Davies. Jim Davis is the cartoonist of garfield.    [2011-11-18 20:09:01 +0100]
    • Josh Ko ⇒ XD    [2011-11-18 20:09:50 +0100]
    • T************** ⇒ 你喜歡加菲貓    [2011-11-18 23:37:26 +0100]
    • Y********** ⇒ Congratulations!!!    [2011-11-19 01:12:11 +0100]
12. 看來我的船歌會比第一號敘事曲更快練到可以聽的地步。後面有第四號敘事曲和幻想波蘭舞曲在排隊，不用擔心沒大曲子練 XD。    [2011-11-19 01:08:25 +0100]
13. Checked-in online. Departure in 48 hours.    [2011-11-27 23:13:34 +0100]  [ 4 人說讚！]
    • J******************* ⇒ 你要去哪？    [2011-11-27 23:15:01 +0100]
    • Josh Ko ⇒ 回國 XD。    [2011-11-27 23:48:55 +0100]
    • M*********** ⇒ 你會待到農曆年嗎??!    [2011-11-28 02:23:34 +0100]
    • Josh Ko ⇒ 選舉結束就走 XD。    [2011-11-28 09:35:36 +0100]
    • M*********** ⇒ XDD 莫非你回來有特別目的!!! 這樣的話,就要看大家的時間了~~    [2011-11-28 16:48:39 +0100]
14. 逃出生天⋯    [2011-11-28 22:00:27 +0100]  [ 2 人說讚！]
    • L******** ⇒ 哈哈 我大概知道是什麼！    [2011-11-28 23:58:53 +0100]
15. With only my glasses and watch I still managed to make the metal detector beep..    [2011-11-29 20:49:52 +0100]  [ 2 人說讚！]
16. At Hong Kong airport.    [2011-11-30 10:37:30 +0100]  [ 4 人說讚！]
    • 翁** ⇒ 是要學成歸國嗎XD    [2011-11-30 10:46:08 +0100]
    • Josh Ko ⇒ 欸，算 1/4 成好了 XD。    [2011-11-30 16:56:46 +0100]
17. 到啦，看這次時差要調幾天。    [2011-11-30 17:02:42 +0100]  [ 4 人說讚！]
    • L************** ⇒ 去買褪黑激素 ..    [2011-11-30 17:08:59 +0100]
    • L********** ⇒ If possible, can you please buy me some pearl for making milk tea?    [2011-11-30 18:33:03 +0100]
    • L********* ⇒ 回來剛好台灣要變冷 XD    [2011-12-01 00:29:16 +0100]
    • Josh Ko ⇒ 不會比英國冷 XD。    [2011-12-01 00:54:21 +0100]
    • Josh Ko ⇒ I'll try to bring some to you, but you can buy some in London if you cannot wait.    [2011-12-01 00:56:19 +0100]
    • L********** ⇒ Thanks. I will probably stay here for the holiday as I've got some work to do...    [2011-12-01 01:25:41 +0100]
    • 周** ⇒ 我到今天才發現原來有翻譯喔~    [2011-12-01 05:45:46 +0100]
18. Hammers of the piano at home (to be reconditioned). ↦ http://www.facebook.com/photo.php?fbid=278765245509353&set=a.126799950705884.40277.100001276392360&type=1    [2011-12-01 04:11:02 +0100]  [ 2 人說讚！]
    • W************ ⇒ 哈，我下禮拜五要回家，可以找你吃飯嗎 XD?    [2011-12-01 05:43:11 +0100]
    • Josh Ko ⇒ 可啊 XD。    [2011-12-01 10:44:38 +0100]
19. 家裡的鋼琴已經老得不太聽話了⋯    [2011-12-01 14:25:55 +0100]
    • Josh Ko ⇒ 剛才彈船歌，那音色讓我頭好痛⋯    [2011-12-02 05:27:11 +0100]
20. Found an interesting paper (by people at NCKU!) in SIGGRAPH 2008 about generating patterns that cause illusory motion (which has been quite popular recently). ↦ http://graphics.csie.ncku.edu.tw/SAI/    [2011-12-02 02:07:50 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ Is there any evolutionary explanation of this kind of illusion?    [2011-12-02 02:08:19 +0100]
    • Josh Ko ⇒ It's probably "overcompensation". An excerpt from Wade and Swanston's "Visual perception: an introduction": "Our species, like all others, has evolved to process motions that occur in the natural environment and to compensate for the consequences of our own biological motions. These latter involve rotations of the eyes, and translations of the head produced by walking, running, jumping, and turning." And indeed I seem to perceive motion if and only if my eyes are rotating. As for how to design an experiment to show more convincingly that this is indeed overcompensation I have no idea..    [2011-12-02 02:40:48 +0100]
21. Luke Palmer on rationality and science as a religion (which is a position I'm taking). ↦ The Culture of Reason    [2011-12-03 19:27:54 +0100]
    • Josh Ko ⇒ My jetlag still persists, apparently..    [2011-12-03 19:48:04 +0100]
22. I feel that I was deceived for a long time about what omega means. Now knowing the definition, somehow the problem doesn't seem to be that interesting anymore. ↦ The Meaning of Omega    [2011-12-04 00:11:41 +0100]
    • Josh Ko ⇒ It's a very delicate play with the distinction between variables and constants, for sure.    [2011-12-04 00:18:41 +0100]
23. I just came up with the idea that I might be able to avoid doing deep embedding via Agda reflection. Sadly, the reflection API is not rich enough at the moment.    [2011-12-05 15:03:10 +0100]  [ 1 人說讚！]
24. 早上竟然出現一群陽明國中的學生！    [2011-12-06 03:46:06 +0100]  [ 4 人說讚！]
    • 賴** ⇒ 英國?    [2011-12-06 05:50:31 +0100]
    • Josh Ko ⇒ 墾丁福華 XD。    [2011-12-06 06:01:24 +0100]
    • 賴** ⇒ 回來了喔~~~    [2011-12-06 06:01:39 +0100]
    • Josh Ko ⇒ 對啊 XD。    [2011-12-06 06:01:54 +0100]
    • 賴** ⇒ 有空來基隆玩枕頭，順便來基隆玩^^    [2011-12-06 06:02:27 +0100]
    • Josh Ko ⇒ 再看看嘍 XD。    [2011-12-06 06:03:02 +0100]
    • 賴** ⇒ 他變超胖的    [2011-12-06 06:06:46 +0100]
    • 洪** ⇒ 你回來了ㄛ！要不要來台北玩阿？    [2011-12-06 07:03:05 +0100]
    • Josh Ko ⇒ 近期還沒有計劃 XD。    [2011-12-06 10:30:57 +0100]
25. Finished presenting the DNF poster and put it online (along with the original version). Now I can finally get rid of the transfer dissertation..
    http://www.cs.ox.ac.uk/people/hsiang-shang.ko/DNF/ ↦ Department of Computer Science, University of Oxford: Publication - Datatype ornamentation and the D    [2011-12-06 12:42:47 +0100]  [ 2 人說讚！]
26. Repost: http://www.youtube.com/watch?v=yL_-1d9OSdk ↦ Chicken chicken chicken    [2011-12-07 05:16:31 +0100]  [ 1 人說讚！]
27. No one is obliged to accept any argument; otherwise, it's dogmatism. (Ah, formal systems do not help here, as one can still reject the validity of such systems.)    [2011-12-07 21:53:42 +0100]  [ 1 人說讚！]
28. It seems the datatype I need is actually a first-order representation of dependent functions with finite domains.    [2011-12-13 04:38:54 +0100]  [ 1 人說讚！]
29. Hm, a naive modification of vectors does not serve adequately as a first-order representation of dependent functions whose domain is the finite numbers.    [2011-12-14 02:32:11 +0100]
30. 船歌終於背起來啦！    [2011-12-14 04:02:15 +0100]  [ 1 人說讚！]
31. Now I have a "large" datatype that does the job for Fin, but of course I'd prefer a small one..    [2011-12-14 07:21:05 +0100]
    • Josh Ko ⇒ And I don't quite see how to generalise the construction yet..    [2011-12-14 07:23:23 +0100]
    • Josh Ko ⇒ The problem is just the opposite of generic modalities as in Chapter 7 of Peter Morris' thesis, where an indexing datatype and a lookup function are derived from a container type. I need to be able to derive a container type whose elements can be indexed by a given datatype.    [2011-12-14 07:34:38 +0100]
    • Josh Ko ⇒ Shouldn't be that hard..    [2011-12-14 07:40:27 +0100]
    • Josh Ko ⇒ It's very much like generic enumeration, except that the usual approach to generic enumeration is coinductive, whereas I need it to be inductive.    [2011-12-14 07:56:33 +0100]
    • Josh Ko ⇒ (So I can get a fold operator for the derived containers.)    [2011-12-14 08:05:37 +0100]
32. Unlocked my Wildfire S for use in Taiwan.    [2011-12-14 11:59:16 +0100]
33. Would it be too picky to comment that "a tie is needed after 'et al.' "?    [2011-12-14 15:43:24 +0100]
    • Josh Ko ⇒ And functions names which are typeset like $er$ instead of $\mathit{er}$..    [2011-12-14 15:46:57 +0100]
    • M*********** ⇒ Reviewing?    [2011-12-14 16:16:48 +0100]
    • Josh Ko ⇒ Yeah, basically - I am producing some comments which will be sent to the authors directly.    [2011-12-15 00:45:43 +0100]
34. Argh, it's just so hard..    [2011-12-15 12:26:48 +0100]
35. This post starts to convince me that homotopy type theory is worth the effort: http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/ ↦ Just Kidding: Understanding Identity Elimination in Homotopy Type Theory    [2011-12-17 01:28:00 +0100]
36. Failure to make the trie types small now leads to very serious predicativity problems..    [2011-12-19 08:17:02 +0100]
    • 楊** ⇒ 你昨天打給我？    [2011-12-19 08:18:01 +0100]
    • Josh Ko ⇒ 對啊：這週末或下週末你要不要和香香許博肥傲笑等人看福爾摩斯二？    [2011-12-19 08:27:42 +0100]
    • 楊** ⇒ 在哪？    [2011-12-19 08:28:37 +0100]
    • Josh Ko ⇒ 彰化吧。    [2011-12-19 08:28:55 +0100]
    • 楊** ⇒ 不會在英國吧…    [2011-12-19 08:29:06 +0100]
    • Josh Ko ⇒ 你可以飛過去看沒字幕的 XD。    [2011-12-19 08:29:33 +0100]
    • 楊** ⇒ 這星期應該可以    [2011-12-19 08:35:04 +0100]
    • Josh Ko ⇒ 再下週不行？    [2011-12-19 08:37:47 +0100]
    • 楊** ⇒ 突然發現這週不行 要下星期才行    [2011-12-19 08:39:32 +0100]
    • Josh Ko ⇒ 你果然跟傲笑有串通 XD。    [2011-12-19 08:40:13 +0100]
    • Josh Ko ⇒ 你有在用 hotmail 嗎？我要把討論串轉給你。    [2011-12-19 08:42:57 +0100]
    • 楊** ⇒ 我都用gmail    [2011-12-19 08:48:09 +0100]
    • Josh Ko ⇒ c102570?    [2011-12-19 08:49:53 +0100]
    • 楊** ⇒ 嗯    [2011-12-19 08:54:01 +0100]
37. Now I've managed to type segs, though requiring --type-in-type..    [2011-12-19 08:31:45 +0100]
    • Josh Ko ⇒ Still far away from the goal.    [2011-12-19 08:32:45 +0100]
    • Josh Ko ⇒ At least there's progress..    [2011-12-19 08:34:24 +0100]
38. Ignoring the size problem and the lack of relationship between the container datatype and the indexing datatype, there's still the crucial question "what is the type of the fold operator for potentially heterogeneous lists?"    [2011-12-25 02:54:19 +0100]
    • Josh Ko ⇒ Well, of course, we always get the standard elimination operator. The type, however, is large and complicated. The size problem is more severe than I had imagined..    [2011-12-25 08:15:31 +0100]
39. Few papers have good discussions about, e.g., why their results really are interesting, what insights their solutions provide, etc. I consider the lack of such discussions unacceptable (but (reluctantly) accept that it has become the norm and that some might even argue against their significance).    [2011-12-29 14:11:57 +0100]  [ 2 人說讚！]
    • L********** ⇒ Very true indeed    [2011-12-29 15:32:28 +0100]
    • J************* ⇒ I think that's what the "conclusions" section should be for. (Most use it just for a summary.)    [2011-12-29 17:49:12 +0100]
40. Not satisfied with the new Holmes movie.    [2011-12-31 12:31:12 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ But of course, as Anton Ego in Ratatouille said: "In many ways, the work of a critic is easy. We risk very little yet enjoy a position over those who offer up their work and their selves to our judgment. [...] But the bitter truth we critics must face, is that in the grand scheme of things, the average piece of junk is probably more meaningful than our criticism designating it so."    [2011-12-31 12:34:24 +0100]
    • Josh Ko ⇒ And I wouldn't describe the movie as junk..    [2011-12-31 12:34:38 +0100]
41. foldr f e . concat = foldr (flip (foldr f)) e, if I eventually wish to fake doubly indexed collections.    [2012-01-01 08:26:26 +0100]
    • Josh Ko ⇒ Er, no, it does not generalise. That's unexpected..    [2012-01-02 02:45:55 +0100]
42. The red-black tree datatype is surprisingly "dissectable!"    [2012-01-02 13:05:04 +0100]  [ 1 人說讚！]
43. Ornament fusion, though conceptually simple, is indeed very helpful. The search tree property and the red-black balancing property can now be separately stated; moreover, the latter can be further dissected into two lines of ornamentations, one about the "red property" (there are no consecutive red nodes) and the other about the "black property" (every path from the root to a leaf contains the same number of black nodes). This will be a very nice example.    [2012-01-02 14:13:21 +0100]  [ 2 人說讚！]
    • J************* ⇒ I'm looking forward to a progress update...    [2012-01-02 18:57:18 +0100]
    • Josh Ko ⇒ Just sent one!    [2012-01-03 01:28:12 +0100]
44. We can probably design a GUI development environment, so the programmer can, for example, right-click on a field in a datatype and select "specialise"; the constructors would be rearranged accordingly, and, more interestingly, all existing declarations/expressions referring to (elements of) the datatype are automatically rewritten.    [2012-01-02 14:36:12 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ This will definitely not be in my thesis, though.    [2012-01-02 14:36:35 +0100]
    • P************* ⇒ are you developing a new IDE?    [2012-01-02 15:58:33 +0100]
    • Josh Ko ⇒ No, this is just a very rough idea and I don't plan to produce an implementation in the near future. (It's still too premature: We don't really understand how to program with full dependent types yet.) But I hope my thesis will serve as a foundation for such development environments.    [2012-01-03 00:05:52 +0100]
45. You should not quantify so boldly..    [2012-01-04 03:53:24 +0100]  [ 1 人說讚！]
46. Yes, the ornament framework easily subsumes data types á la carte.    [2012-01-07 10:39:35 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ It goes in the "opposite direction" and coexists with the refinement interpretation very nicely - and there's no need to expand the universe.    [2012-01-07 11:02:47 +0100]
    • Josh Ko ⇒ And there is no need for smart constructors at all, if datatypes are presented simply as codes - we can calculate composite datatypes such that they have proper constructors.    [2012-01-07 11:03:28 +0100]
    • J************* ⇒ Time to start thinking about ICFP?    [2012-01-07 19:46:23 +0100]
    • Josh Ko ⇒ Would it be somewhat weak to say only that "we can do data types á la carte with ornaments"? And somehow this is "cheating" if compared with Wouter's solution, as he aimed to solve the problem for Haskell, which has limited datatype-manipulating capabilities. (Indeed, there's no practical language which has enough datatype-manipulating capabilities yet. We would need Epigram 2, which is still hypothetical, though.)    [2012-01-08 04:48:50 +0100]
    • P************* ⇒ I "Like" this statement, but I would like a constructive proof better ... Code, or it didn't happen!    [2012-01-08 12:22:13 +0100]
47. A problem I've just realised is that ornament fusion is actually not a pushout (or pullback, depending on how you assign directions to ornaments)...    [2012-01-07 10:53:31 +0100]
    • Josh Ko ⇒ But perhaps it still is if interpreted in a "weaker" category.    [2012-01-07 12:41:51 +0100]
48. The SICP course at MIT resurrected. ↦ 6.S184 - Zombies drink caffeinated 6.001    [2012-01-10 10:21:40 +0100]  [ 2 人說讚！]
49. Impressive experiment result - Russell's paradox was comprehensible to a six-year-old girl! ↦ The Universe of Discourse : Elaborations of Russell's paradox    [2012-01-11 01:47:10 +0100]
50. Free monad to the rescue!    [2012-01-12 14:39:26 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ Didn't really make use of the monadic structure, though.    [2012-01-12 19:45:19 +0100]
51. Liskov: "I don't actually believe in functional programming." !!    [2012-01-16 04:20:58 +0100]  [ 4 人說讚！]
    • Josh Ko ⇒ "Because the purpose of programs is to manipulate states."    [2012-01-16 04:22:08 +0100]
    • L************** ⇒ I don't actually believe in listing a talk. XD    [2012-01-16 04:27:59 +0100]
    • 陳** ⇒ 今天是打臉大會XD    [2012-01-16 04:47:08 +0100]
52. Passed through Heathrow very smoothly for the first time.    [2012-01-17 22:23:09 +0100]  [ 4 人說讚！]
    • L********** ⇒ What happened before?    [2012-01-18 01:25:54 +0100]
    • F********* ⇒ Welcome come back!    [2012-01-18 09:44:41 +0100]
    • Josh Ko ⇒ I had to explain to the immigration officer about the visa, which looks as if it has never been used before, in my old passport.    [2012-01-18 09:54:16 +0100]
    • Josh Ko ⇒ Thanks, Frank!    [2012-01-18 09:54:19 +0100]
53. My eyes hurt and cannot look at the screen anymore.. This is probably the most annoying consequence of long-haul flights. (So it's time to sleep.)    [2012-01-18 01:05:02 +0100]
54. My eyes are still tired..    [2012-01-18 11:03:42 +0100]  [ 1 人說讚！]
    • 洪** ⇒ 熱敷可以幫助眼睛改善疲勞~小心溫度不要太燙!    [2012-01-18 11:12:31 +0100]
    • Josh Ko ⇒ 噢太好了，謝謝！    [2012-01-18 11:15:47 +0100]
55. 家裡的琴太軟，現在回來彈 Knight 琴鍵都壓不下去⋯    [2012-01-18 20:22:05 +0100]  [ 3 人說讚！]
    • 楊** ⇒ 練口琴！    [2012-01-18 20:22:44 +0100]
    • Josh Ko ⇒ 口琴一個人吹沒 fu 吧 XD。    [2012-01-18 20:43:45 +0100]
    • 楊** ⇒ 練獨奏其實也很有fu    [2012-01-18 20:44:13 +0100]
    • 楊** ⇒ 要幫你介紹琴種嗎？xd    [2012-01-18 20:44:19 +0100]
    • Josh Ko ⇒ 沒關係，反正現在我有琴彈 XD。    [2012-01-18 20:46:22 +0100]
    • 楊** ⇒ 真有錢！    [2012-01-18 20:47:14 +0100]
56. Summoning relations, the great weapon for specification!    [2012-01-20 10:52:40 +0100]
57. String diagrams for today's AoP meeting. Amazing indeed!    [2012-01-20 14:41:32 +0100]  [ 2 人說讚！]
58. So the hypothesis is that it's a good idea to relate the indices with the underlying data via an explicit relation.
    
    Questions to be answered:
    
    1) Would it be more "meaningful" to manipulate relations than dealing directly with ornaments?
    
    2) Can we actually manufacture datatypes that we want to program with (and at the same time get properties of these datatypes for free)?
    
    3) What composable structures of relations can be transferred to datatypes? (And how?)    [2012-01-21 23:17:38 +0100]
    • Josh Ko ⇒ For the first question I think the answer is positive. I may have had a preliminary answer to the second one. The third one is harder.    [2012-01-21 23:22:18 +0100]
59. The video of my WGP talk is online. Haven't got the courage to watch it, though.. ↦ SOURCE MATERIALS - Modularising inductive families    [2012-01-21 23:28:36 +0100]  [ 1 人說讚！]
60. Hadn't expected that I can do field swapping with deletion.    [2012-01-22 10:33:53 +0100]
61. And with deletion it seems I can get a stronger pushout (or pullback) property (the original one I had in mind, actually) for parallel composition. Great!    [2012-01-22 11:05:37 +0100]
    • Josh Ko ⇒ I really underestimated the power of deletion.    [2012-01-22 11:06:35 +0100]
62. Extending the universe of descriptions to cover general products, in case that I eventually decide to do levitation of ornaments in the future.    [2012-01-22 11:22:21 +0100]
63. "Too good to be true" does not apply to the Barcarolle. It's good, and it's true.    [2012-01-22 16:16:04 +0100]  [ 4 人說讚！]
64. Deletion, however, seems to prohibit the universe of ornaments from being levitated. Well, I'm not eager to do this anyway..    [2012-01-22 17:47:17 +0100]
65. C++ is indeed far away from me - I can now use // as an operator in Agda without regarding everything after that as irrelevant.    [2012-01-22 21:07:18 +0100]  [ 4 人說讚！]
    • L********** ⇒ Still a useful skill to have though    [2012-01-22 21:35:44 +0100]
66. Extensional equality of the induced forgetful maps - that should be an adequate equality for ornaments.    [2012-01-23 09:16:30 +0100]
67. I need a convenient way to reason about pullbacks..    [2012-01-23 11:12:21 +0100]  [ 1 人說讚！]
    • 楊** ⇒ 你在學微分幾何？    [2012-01-23 11:22:41 +0100]
    • Josh Ko ⇒ 不用到那麼複雜的東西就已經有 pullback 了 XD。    [2012-01-23 11:32:44 +0100]
    • 楊** ⇒ 我只知道微分幾何裡面要用而已    [2012-01-23 11:34:50 +0100]
    • T************** ⇒ 就是拉回來    [2012-01-23 14:42:56 +0100]
    • Josh Ko ⇒ 也可以推出去 XD。    [2012-01-23 14:45:40 +0100]
68. Fun in the Afternoon to take place at Oxford on 28 Feb. ↦ Fun in the Afternoon    [2012-01-24 17:31:49 +0100]  [ 1 人說讚！]
69. Vertical composition is very difficult to tame, whereas properties of parallel composition keep jumping out naturally..    [2012-01-25 10:55:46 +0100]
    • Josh Ko ⇒ On the other hand, it's not that easy to get a natural and easily manipulable definition of parallel composition (because of the need to deal with pullbacks), whereas the definition of vertical composition is straightforwardly inductive.    [2012-01-25 10:58:22 +0100]