期考將至

我現在覺得拿起 AoP 或 Intro. to FP（而不是拿紫龍書或白算盤）好罪惡 Orz。

不過與其浪費時間掙扎，不如就來看吧 XD。

--
scm 老師快來系上開課啦！！！

報告 Reprise

很不願意寫報告，所以就開始在 iCal 裡面乾坤大挪移，把後面的事項挪到今天，報告儘可能往 deadline 擠 XD。

--
編譯器作業其實就是往前挪的其中一項 XD。

詭異歸納

證明編譯器作業二 3. b.。很自然地想用 induction，但寫到一半突然想到圖論張老師和助教的教誨，就改用 maximal principle 來證，結果寫出一個我覺得很詭異的證明：

--
是我不習慣用 minimal/maximal principle，還是我根本是在亂寫？XD

---

我猜我覺得詭異的原因是我用了 maximal principle 又用了標準的 induction，而其實應該只需要其中一個，把兩個混在一起就覺得很怪。希望待會改寫之後看起來會比較順眼 XD。

--
果然是亂寫一通 XD。

---

好啦，我現在寫不出來了 XD。

--
其實是 ambiguous？XD

---

結果是 ambiguous，一開始的證明根本是亂寫嘛 XD。好吧，至少又見證一次證明與反證的 duality XD。

--
"Somehow" 代表我的詭異直覺是對的？XD

---

把作業傳上 FTP 伺服器，mkdir 之後沒 cd 就 put，之後 rm mv 都無效，只好趕快寄信給助教 XD。

--
希望不要太多人發現 XD。

Relational Division

向 scm 老師求得看懂兩個 relations 相除意義的撇步後，一些本來跟天書一樣的定義如 specifications of optimisation problems 裡面最重要的

min R = ∈ ∩ (R/∈)

和 thinning algorithms 用的

thin Q = (∈\∈) ∩ ((∋·Q)/∋)

突然都讀得出意思了！

--
又燃起了希望 XD。

偷轉

承接〈Parser Combinators in Haskell〉，Wikipedia 上的 left recursion 條目下有個 pitfall 子項，裡面用的 example grammar 正好就是我用的，一模一樣。它說經過 left-recursion elimination 之後，加法的 association 就從 left-associative 變成 right-associative，parse tree 會向右傾。

我就很納悶了：我造出來的 abstract syntax tree（ExprTree）都是 left-associative 啊，怎麼會發生這種事勒？原來當我看到 Expr 或 Expr' 展開成 Term 和 Expr' 的時候，生成 syntax tree 的函式會把 Term 的 syntax tree 塞到 Expr' 的 partial syntax tree 左側，就如同對 parse tree 做 left-rotation！轉兩次之後，加法（和乘法）就又變回 left-associative 了 XD。

從這例子也可以清楚看出 parse tree 和 abstract syntax tree 是不一樣的東西。

--
挺有趣的 XD。

Parser Combinators in Haskell

（以下大部份說明文字亂譯自 scm 老師的原文 XD。）

考慮這種 binary tree：

data Tree = A | B | Bin (Tree, Tree)
     deriving Show

我們可以用比較簡短的語法印出這種樹，把 A 印為 a、B 印為 b、Bin (t, u) 印為 (t,u)。例如 (Bin (A,Bin (B,A)) 就印為 (a,(b,a))。這樣的語法可用以下的 context-free grammar 描述：

S ::= ( S , S ) | a | b

在一般的程式語言之內寫一個 recursive-descent parser 並非易事。但若有了 higher-order functions，我們就可以如下為上述語言建造出一個 parser：

pTree :: Parser Char Tree
pTree =  (lit '(' *> pTree <*> lit ',' *> pTree <* lit ')') `using` Bin
      <|> lit 'a'                                           `using` const A
      <|> lit 'b'                                           `using` const B

pTree 的定義和 grammar S 面貌相似：每個 terminal（小括號、逗號、a 和 b）都套上 lit，concatenation (sequencing) 以 *>、<*、和 <*> 明確表示，各種可能情況之間則以 <|> 分隔。'using' 子句說明如何建造出對應的樹。

這是怎麼做的呢？

Parser a b 的輸入是一連串的 tokens of type a，它將這串 tokens 的某個 prefix 解析為某個型別為 b 的東西。這個型別該怎麼定義呢？很顯然，Parser a b 接收一個 list of a 並傳回一個 b-structure：

type Parser a b = [a] -> b

但 parser 不一定會耗盡所有的 input tokens，這樣的設計在我們把 parsers 串起來的時候會有用。因此我們除了讓 parser 傳回一個 b-structure 以外，也傳回尚未消耗的 list of tokens：

type Parser a b = [a] -> (b, [a])

最後，parser 可能會因為輸入不合法而解析失敗，或者它可能傳回多個可能的解析結果。因此我們讓 parser 傳回「可能的解析結果」所形成的序列（list）：

type Parser a b = [a] -> [(b, [a])]

如果解析失敗，parser 就傳回 []。

我們定義另一個函式 parse「執行」一個 parser。這個函式選出第一個「耗盡整個輸入字串」的解析結果：

parse :: Parser a b -> [a] -> b
parse p = fst . head . filter (null . snd) . p

fail 這個 parser 的解析永遠是失敗的：

fail : Parser a b
fail xs = []

與之相反的是 succeed，它總是立即解析成功，不消耗任何輸入：

succeed :: Parser a ()
succeed xs = [((), xs)]

換句話說，這個 parser 接受空字串。

lit x 這個 parser 檢查輸入的第一個 token 是否等於 x，如果真的是這樣就傳回 x（因此它的型別是 Parser a a）以及尚未解析的剩餘輸入。這是唯一可行的解析方式。若不然，它就傳回一個 empty list 代表解析失敗，因為沒有以 x 起頭的解析方式。

lit :: Eq a => a -> Parser a a
lit x (y : xs) | x == y = [(y, xs)]
lit x _ = []

p1 <|> p2 這個 parser（p1 OR p2）試著用 p1 和 p2 分別進行解析，然後合併兩者結果。那就單純是把兩個 parsers 傳回的 lists 串接在一起。

infixr 6 <|>
(<|>) :: Parser a b -> Parser a b -> Parser a b
(p1 <|> p2) xs = p1 xs ++ p2 xs

p1 <*> p2 這個 parser（p1 followed by p2）先用 p1 解析輸入字串，再用 p2 解析剩餘的字串。假設 p1 造出一個 b-structure、p2 造出一個 c-structure，那麼 p1 <*> p2 會把兩者的結果放進一個 pair (b, c) 裡面當作自己的結果。這個 parser combinator 用 list comprehension 會比較好寫：輸入 xs，對於 p1 xs 的每個解析結果 (b, ys)，用 p2 解析 ys 產生一群結果 (c, zs)，然後把 (b, c) 和剩餘的輸入 zs 組合成一個 pair 放進 resulting list。

(<*>) :: Parser a b -> Parser a c -> Parser a (b, c)
(p1 <*> p2) xs = [ ((b, c), zs) | (b, ys) <- p1 xs, (c, zs) <- p2 ys ]

給定一個 parser p :: Parser a b 和一個函式 f :: b -> c，(p `using` f) 是一個新的 parser，把 f 套用到 p 的結果：

using :: Parser a b -> (b -> c) -> Parser a c
p `using` f = map (cross f id) . p

其中 cross 是標準的 product functor：

split f g a = (f a, g a)
cross f g   = split (f . fst) (g . snd)

p1 *> p2 很類似 p1 <*> p2，但它會丟棄 p1 的結果。這個 combinator 可用 <*> 和 using 定義：

infixr 8 *>
(*>) :: Parser a b -> Parser a c -> Parser a c
p1 *> p2 = (p1 <*> p2) `using` snd

<* 是 *> 的對偶：

infixr 8 <*
(<*) :: Parser a b -> Parser a c -> Parser a b
p1 <* p2 = (p1 <*> p2) `using` fst

至此我們已經定義了一個內嵌於 Haskell 的 domain-specific embedded language，專門用來解析語言。讓我們試用這些 combinators。以下這個簡單的 grammar 描述「反二進位數字」：

B ::= 0 | 1 | 0 B | 1 B

例如 "11010" 的值是 11（因為數字的順序是反的）。欸，選這種奇怪的例子只是為了練習啦 XD。以下就是它的 parser：

pB :: Parser Char Int
pB =     lit '0'         `using` const 0
     <|> lit '1'         `using` const 1
     <|> (lit '0' *> pB) `using` (*2)
     <|> (lit '1' *> pB) `using` ((+1) . (*2))

一些執行例子：pB "1101" = [(1,"101"),(3,"01"),(3,"1"),(11,"")]、parse pB "1101" = 11。

如果我們改用下面這個 grammar 可以嗎？

B ::= 0 | 1 | B 0 | B 1

很可惜，這個 grammar 是個 left-recursive grammar，而我們的 recursive-descent parser 只能處理 LL grammar。LL 的第二個 L 代表解析方式是 leftmost derivation，所以如果有 left-recursion 就會遞迴個沒完。

回到我們一開始定義的 parser pTree。如我們一再提及，用這樣的方法寫出的 parsers 都是 recursive-descent (hence top-down) parsers，也就是從 start symbol 逐漸展開一棵樹（unfold?!）。詳情可參考 dragon book 2/e, section 4.4，其中 p.218 有精美插圖 XD。單純的 recursive-descent parsing 可能需要 backtrack，因為展開某個 nonterminal 的時候可能選錯 production rule。這裡的精神是 "nondeterministically" 選一個 production rule，實作上用 subset construction 把所有可能的結果收集起來，到最後才挑出成功解析的結果。

另一種印樹的形式是把 Bin (t, u) 印為 (t)u。例如 Bin (Bin (A,B), Bin (A,B)) 印為 ((a)b)(a)b。對應的 grammar 是

S ::= ( S ) S | a | b

Parser 則可寫為

pTree2 :: Parser Char Tree
pTree2 =
      lit 'a'                                   `using` const A
  <|> lit 'b'                                   `using` const B
  <|> (lit '(' *> pTree2 <*> lit ')' *> pTree2) `using` Bin

最後讓我們試一個稍微實際一點的例子，處理「反二進位數字」的加法與乘法算式。算式的 grammar 是

Expr ::= Expr + Term | Term
Term ::= Term * Factor | Factor
Factor ::= B | ( Expr )

是個超標準的版本。（我高中看 C++ grammar 的時候就看過啦 XD。）不過這個 grammar 是 left-recursive，所以我們必須做點變換，消除 left-recursion（ref. dragon book, section 4.3.3）。這過程其實就是把 non-empty snoc-lists 換成對應的 cons-lists。轉換後的 grammar 變成

Expr ::= Term Expr'
Expr' ::= + Term Expr' | ε
Term ::= Factor Term'
Term' ::= * Factor Term' | ε
Factor ::= B | ( Expr )

其實差不多就是 dragon book 的 example 4.27。

定義 Token 型別為

data Token = Number Int | Plus | Multiply | LeftP | RightP
     deriving (Eq, Show)

pToken :: Parser Char [Token] 會把輸入字串裂解為一連串的 tokens。為了讓效率好一點，我們定義 munch :: Parser a b -> Parser a b 把一個 parser 轉換為 "greedy" parser ─ resulting parser 只挑出剩餘字串長度最短的那個結果。

munch :: Parser a b -> Parser a b
munch p = cond null id ((:[]) . foldr1 f) . p
  where f p q = if sndlen p < sndlen q then p else q
        sndlen = length . snd

其中 cond 是 McCarthy conditional form：

cond p f g a = if p a then f a else g a

於是我們就可以定義 pToken：

pToken :: Parser Char [Token]
pToken =
      succeed               `using` const []
  <|> (lit ' ' *> pToken)
  <|> (lit '+' *> pToken)   `using` (Plus :)
  <|> (lit '*' *> pToken)   `using` (Multiply :)
  <|> (lit '(' *> pToken)   `using` (LeftP :)
  <|> (lit ')' *> pToken)   `using` (RightP :)
  <|> (munch pB <*> pToken) `using` (uncurry (:) . cross Number id)

其中第二條是忽略空格的規則。令

s = "001101 + 101 * (011 + 1 + 10)"

那麼 parse pToken s = [Number 44,Plus,Number 5,Multiply,LeftP,Number 6,Plus,Number 1,Plus,Number 1,RightP]。

接下來我們定義 abstract syntax tree 的型別。

data ExprTree = Operand Int
              | PlusBin ExprTree ExprTree
              | MultiplyBin ExprTree ExprTree
     deriving Show

對應的 fold operator 是

foldet f g h (Operand n) = h n
foldet f g h (PlusBin t u) = f (foldet f g h t) (foldet f g h u)
foldet f g h (MultiplyBin t u) = g (foldet f g h t) (foldet f g h u)

想對一個算式求值，可用以下函式：

evalExpr :: [Char] -> Int
evalExpr = foldet (+) (*) id . parse pExpr . parse pToken

其中 pExpr :: Parser Char ExprTree 是 Expr grammar 的 parser。例如 parse pExpr (parse Token s) = PlusBin (Operand 44) (MultiplyBin (Operand 5) (PlusBin (PlusBin (Operand 6) (Operand 1)) (Operand 1)))。定義 pExpr 會碰上一點麻煩，因為經過 left-recursion elimination 的 grammar 和我們想建造的樹形不一樣了！更精確地講，pExpr'（注意是 Expr "prime"）傳回的是個 partial syntax tree，裡面有個洞是要放 + 左邊的樹。But hey, we are working in a functional language! 我們就讓 pExpr' 的結果是 ExprTree -> ExprTree，這個 function 拿一個 ExprTree 塞到那棵 partial syntax tree 的洞裡面，傳回一棵完整的樹。這樣我們就可以定義出全部的 parsers：

pExpr :: Parser Token ExprTree
pExpr = (pTerm <*> pExpr') `using` uncurry (flip ($))

pExpr' :: Parser Token (ExprTree -> ExprTree)
pExpr' =
      succeed
          `using` const id
  <|> (lit Plus *> pTerm <*> pExpr')
          `using` (\(t, f) -> \u -> f (PlusBin u t))

pTerm :: Parser Token ExprTree
pTerm = (pFactor <*> pTerm') `using` (uncurry (flip ($)))
  
pTerm' :: Parser Token (ExprTree -> ExprTree)
pTerm' =
      succeed
          `using` const id
  <|> (lit Multiply *> pFactor <*> pTerm')
          `using` (\(t, f) -> \u -> f (MultiplyBin u t))

pFactor :: Parser Token ExprTree
pFactor = lit LeftP *> pExpr <* lit RightP
      <|> pNumber `using` Operand

pNumber :: Parser Token Int
pNumber (Number x : ys) = [(x, ys)]
pNumber _ = []

有了傳回 syntax tree 的 parser，要轉 postfix form 也很容易：

postExpr :: [Char] -> [Char]
postExpr = foldet f g h . parse pExpr . parse pToken
           where f s t = s ++ t ++ "+"
                 g s t = s ++ t ++ "*"
                 h x   = "[" ++ show x ++ "]"

例如 postExpr s = "[44][5][6][1]+[1]+*+"。

--
好長 Orz。

Parsing Combinators in Haskell

今天排定的進度算結束了，唸編譯器是其中一項，所以就順勢來做 scm 老師這次的 Haskell exercises。目標是寫出一組可合成 context-free parser 的 higher-order functions，精神和 Boost spirit library 應該是一樣的。後者我是上了大學才聽聞，沒怎麼研究過。

看來兩者產生的都是 recursive-descent (hence LL) parsers。然後 Haskell 版處理 nondeterminism 的方式是用標準的 subset construction，其中 sets 以 lists 實作。

--
先貼一篇佔位，之後會補完 XD。

---

(3:06AM) 寫了一個很簡單的算式求值器，支援 "reversed binary numbers" 的加法與乘法，可用小括號表示子算式。架構是標準的 tokenisation → parsing → tree flattening。為了讓加和乘是 left-associative，我寫出來的 grammar 是 left-recursive，所以還用上才剛讀到的 left-recursion elimination。

--
顯然又是寫篇 literate Haskell 的時候了，待續 XD。

---

我直接在 blog 上寫一篇好了，parsing combinator 的符號和 lhs2TeX 不太有默契 XD。

--
請見《Parser Combinators in Haskell》XD。

Selected Papers on Analysis of Algorithms

今天冷清的 MFN meeting 結束後，臨時起意到圖書館去翻翻 Knuth 的《Selected Papers on Analysis of Algorithms》。熟悉的 Knuth 風格躍然紙上，包括一頁接著一頁的高段數學… 聽說 Haskell programs 的時間複雜度分析比一般 imperative programs 還要難？真糟…

--
同時也看到傳說中的 Pascal 句點 XD。

報告

Undergrads 最麻煩的一點，就是要應付一大堆作業。這學期修了三門通識課，門門都要繳報告…

--
都是有點難又不太難的那種 XD。

不小心

因為臨時和 Agda 玩了一下，不小心就漏了一天沒寫，不過其實也沒什麼好寫 XD。真的要寫的話也只有發一頓牢騷：allegories 好難！又是方桌的（tabular），又是單元的（unitary），奇怪的模化律（modular law）超複雜，左除和右除（left-division/right-division）也很難懂。難怪 Richard Bird 要回去做 functional derivation 啦 XD。

--
卡在第四章動彈不得 ─ AoP 一共十章，其中一到六章只是 "basic theory" XD。

四超人

分別是卡塔．莫斐生（Cata Morphism）、安娜．莫斐生（Ana Morphism）、帕拉．莫斐生（Para Morphism）、艾波．莫斐生（Apo Morphism）XD。（或是只要前兩個也行 XD。）出場的時候可以大喊自己的 universal property，例如「在 alpha 之後，我的 F 映射就在 F 代數之前！」之類的，背後秀出對應的 commutative diagram（超熱血 XD）。平常四人可以靠各自的融合律（fusion law）與其他函式融合，加強自己的能力，當然前提是要唸出融合咒語（fusion condition）XD。危急的時候卡塔和安娜可以合體成為強大的海羅．莫婓生（Hylo Morphism），可是必須冒能力無法控制的危險（non-termination）XD。故事到了後期，四人背後錯綜複雜的連結應該可以和台灣連續劇拚，例如卡塔和安娜、帕拉和艾波兩兩之間的 duality，然後會有其他的合體形式像美塔．莫婓生（Meta Morphism）出現，帕拉和艾波也可以找到合體方式（吧？）。最後與涂林．馬釁（Turing Machine）大魔王決一死戰，帕拉、艾波相繼陣亡，卡塔與安娜迫不得已合體成為海羅．莫婓生，卻發現自身與魔王開始共鳴…

--
還滿奇幻的 XD。

架上書籍

剛剛為了找些過往資訊，回頭翻以前的 blog，發現我還滿常把我書架上的書列出來。既然如此現在也來列吧，以下是最底層書架（相當於 first-level cache）上的書，順序從左到右：

1. Rudin. Principles of Mathematical Analysis, 3/e.
2. Friedberg et al. Linear Algebra, 4/e.
3. Chung. A Course in Probability Theory, 2/e.
4. Sipser. Introduction to the Theory of Computation, 2/e.
5. Hopcroft et al. Introduction to Automata Theory, Languages, and Computation, 3/e.
6. Knuth. Selected Papers on Computer Science.
7. Knuth. The Art of Computer Programming Vol. 1: Fundamental Algorithms, 3/e.
8. Knuth. The Art of Computer Programming Vol. 1, Fasc. 1: MMIX.
9. Knuth. The Art of Computer Programming Vol. 2: Seminumerical Algorithms, 3/e.
10. Knuth. The Art of Computer Programming Vol. 3: Sorting and Searching, 2/e.
11. Cormen et al. Introduction to Algorithms, 2/e.
12. Graham et al. Concrete Mathematics, 2/e.
13. Bird and de Moor. Algebra of Programming.
14. Bird. Introduction to Functional Programming using Haskell, 2/e.
15. Bryant et al. Computer Systems: a Programmer's Perspective.
16. Hennessy and Patterson. Computer Architecture: a Quantitative Approach, 3/e.
17. Patterson and Hennessy. Computer Organization and Design, 3/e.
18. Knuth. MMIXware.
19. Silberschatz et al. Operating System Principles, 7/e.
20. Aho et al. Compilers: Principles, Techniques, and Tools, 2/e.
21. Kernighan and Ritchie. The C Programming Language, 2/e.
22. Stroustrup. The C++ Programming Language, 3/e (special edition).
23. Stroustrup. The Design and Evolution of C++.
24. Lippman et al. C++ Primer, 4/e.
25. 侯捷（譯）。C++ Primer 中文版，4/e。
26. Arnold et al. The Java Programming Language, 4/e.
27. Knuth. TeXbook.
28. Lamport. LaTeX: a Document Preparation System, 2/e.
29. Mittelbach et al. The LaTeX Companion, 2/e.
30. Knuth. Digital Typography.
31. Cover et al. Elements of Information Theory, 2/e.
32. Stevens et al. Advanced Programming in the UNIX Environment, 2/e.

竟然剛好 2⁵ 本！所以 first-level cache 只剩一本中文書了（而且還是特殊理由才在上面 XD）。有幾本放著是因為有紀念意義，另外還有好幾本幾乎沒翻到 XD。中間那一帶平時會被（用四張 A4 拼起來的）A2 大小的 MSS 海報遮住 XD。

--
其他 second-level cache 以下的就不列了 XD。

Paramorphisms

Paramorphisms correspond to the concept of primitive recursion. A paramorphism can be defined in terms of products and catamorphisms

or characterised by the universal property

It is a (strict) specialisation of the generalised tupling transformation mentioned before. I didn't get the statement about generalised tupling precise enough at the beginning, so I was confused by why the universal property of paramorphisms can be a bidirectional implication, until I realised that the statement of general tupling can be proven to be bidirectional:

Once the full-fledged tupling rule is established, the universal property of paramorphisms follows as an easy corollary since id = cata α.

--
It took me more time than I expected...

初投天

投完了！不知為什麼很緊張，我現在沒辦法很肯定我究竟蓋在哪個選項，也不確定圈選章的圖案到底是 o-lambda 還是 o-adbmal XD。我蓋的章水好多，希望不會變成廢票 XD。晚上開票的時候，會有好一些 succ 是我貢獻的喔 XD（包括那些區域性統計 XD）。

--
我不會再貼相關文章了，所以不要因為晚上我沒貼文就以為我投的是選輸那一邊 XD。

---

剛剛看到我貢獻的幾個 succ：選民總數 1732 萬 1622 人、男性選民總數 886 萬 9507 人、首次總統投票權人數 81 萬多人。

--
不過最後一個還有 bottom XD。

Print on Demand

回到家了。等在家裡的《Algebra of Programming》竟然是藍色的 print on demand edition，而且印刷有點糊糊的，只比圖書館裡那本 Intro. to FP 好一點。scm 老師那本已經翻到有「油墨記憶」（有標準的術語嗎？XD），翻開手上這本，乍看竟有全然陌生的感覺，而且用 sans serif 字型的 functor 變得比較難以和其他字區隔（因為字都暈開來）。好吧，至少這是屬於我的 copy XD。

--
這和我前一天夢到的書況完全不一樣啊 XD。

Modelling Digital Logic in Haskell

scm 老師這次出的 Haskell 練習題是用 Haskell 寫 digital logic components。這正是 OUCL 大學部教 digital logic 的方式，真是太浪漫了 XD。一條接線是以一個 list 表示，其中每個元素是那條線在各個離散時間點的訊號值。

type Wire = [Bool]

也就是說，Wire 這個 list 的 index 是時間（單位是 infinitesimal 吧，我們暫時不考慮 physical delays XD）。另一種正交觀點是在同一個時間點看多條線（一般就是一個 bus）的 states，我稱之為 time slice（從 OS 借來的詞）。

type TimeSlice = [Bool]

此時 list 的 index 是線的編號。後面會發現區分這兩個型別是有意義的。

我們先從簡單的開始。以下的函式 binary c 把一個整數轉為 binary representation：

binary :: Int -> Integer -> TimeSlice
binary c = take c . map ((/= 0) . (`mod` 2)) . iterate (`div` 2)

這產生出線數為 c 的 time slice。binary c 有反函式 numeric c：

numeric :: Int -> TimeSlice -> Integer
numeric c = sum . tri (*2) . map bit2num . take c

tri f（就是出現在 Horner's rule 裡面的那個函式）和 bit2num 的定義是：

tri f = foldr (\x xs -> x : map f xs) []
bit2num False = 0 
bit2num True  = 1

我們也可以產生承載常數的 bus：

constant :: Int -> Integer -> [Wire]
constant c = map repeat . binary c

其中 repeat a = a : repeat a 是 Haskell 內建的函式（吧）。

接著我們試試加法器的核心功能。以下函式 add c 把兩個 time slices 視為二進位數字加在一起，產生一個新的 time slice：

add :: Int -> TimeSlice -> TimeSlice -> TimeSlice
add c = curry (binary (c + 1) . uncurry (+) . parallel (numeric c))

add c 把它收到的兩個 time slices 轉為數值加起來，然後轉換回長度 c + 1 的 time slice，多一位是最高位的進位。這其實是加法電路的 specification，以後我希望能從這裡導出 ripple adder, carry look-ahead adder 等等的。(Hope it's possible. XD)

加法器的型別是

adder :: Int -> [Wire] -> [Wire] -> [Wire]

[Wire] 是一條一條的線，但 add c 處理的是一個一個的 time slice，我們必須寫個函式在這兩個觀點間轉換。稍微想一想就會發覺，這其實就是 matrix transposition，所以我們可以寫

transpose = foldr (zipWith (:)) (repeat [])

然後我們就可以寫出加法器：

adder c = curry (transpose . uncurry (zipWith (add c)) . parallel transpose)

其中 parallel 是 "square" functor。

split f g a = (f a, g a)
cross f g = split (f . fst) (g . snd)
parallel f = cross f f

寫完了很高興，我們測試一下，在 GHCi 下輸入

map head (adder 5 (constant 5 7) (constant 5 8))

卻發現 adder is unproductive！（意思是什麼東西都吐不出來。）追蹤一下就會發現，add 產生出來的是個 infinite list of time slices，而 transpose 是個 foldr，找不到 base case 可以停下來。因此我們被迫寫另一個 transpose，功能一樣但用 unfoldr 實作：

wirewise :: [TimeSlice] -> [Wire]
wirewise = unfoldr f
           where f ([] : xss) = Nothing
                 f xss        = (Just . split (map head) (map tail)) xss

其中 unfoldr f 是標準的定義：

unfoldr f a = case f a of
                Nothing -> []
                Just (x, b) -> x : unfoldr f b

本來的 transpose 也改名一下：

timewise :: [Wire] -> [TimeSlice]
timewise = foldr (zipWith (:)) (repeat [])

adder 於是就變成

adder :: Int -> [Wire] -> [Wire] -> [Wire]
adder c = curry (wirewise . uncurry (zipWith (add c)) . parallel timewise)

這樣我們就有一個把兩條二進位數字流加起來的加法器，而且是 productive。例如剛剛在 GHCi 下輸入的算式現在就能正確輸出結果了：

*Main> map head (adder 5 (constant 5 7) (constant 5 8))
[True,True,True,True,False,False]

我刻意把各個部份寫得很 compositional，希望可以多做到一點 derivations ─ 雖然我覺得規模有點恐怖了，而且還有 infinite lists 和 unfold XD。

--
還有得玩，不過要過一陣子 XD。

做功課

很快就要投人生第一次票，決定趕快來做點功課。（這大概是這個 blog 的第二篇政治文 XD。）於是我和 Weijin 上雙方網站很努力地瀏覽一遍兩邊的政見，目前結論如下：

• 雙方放在網站上的政見其實大同小異（我看不懂的除外 XD），甚至連表面上完全衝突的大陸政策（藍營說「九二共識」，綠營不要）稍微多想一下，表現出來（i.e., extensionally）都是差不多的；
• 然而，謝長廷的文筆真的比較好，而且背後的抽象支持理論（i.e., 幸福經濟、黃金三角）敘述得很完整；馬英九網站政見的表達風格就很不一樣，一點一點都是具體的牛肉，然後概論部份看起來好像公民課本的用句遣詞，乾乾澀澀的 XD；
• 兩邊網站設計都不太好，小夫網站我上的時候很常發生 database error，馬囧網站會無緣無故亂跳頁，最後兩邊都放一堆影片，一直把它們按停很煩 XD。

所以某種角度而言有很大的進展，另一種角度而言又回到原點。這功課難做 XD。

--
對啦，這篇單純是記事，不要戰我 XD。

Generalised Tupling

The generalised tupling transformation rule has been described earlier. The F-algebra <g, h . F outr> appearing in the conclusion is in fact not given in AoP --- the readers are asked to construct it. Today I tried a bit and found that it turned out to be quite easy. As soon as one comes up with the "tupling" revelation f = outl . <f, cata h>, Fokkinga's mutual recursion theorem, which is a simple consequence of universal properties of catamorphisms and products, immediately suggests itself:

With the tupling condition f . α = g . F <f, cata h> and universal property of catamorphisms, one can easily find that <f, cata h> = cata <g, h . F outr>. The intuition behind this tupling rule is that f by itself cannot be a catamorphism, i.e., we cannot find g such that the universal property f . α = g . F f is satisfied. However, if a somewhat relaxed condition f . α = g . F <f, cata h> is established, then f can be expressed "nearly" as a catamorphism.

This tupling rule seems less useful for solving the maximum segment sum problem, though. If we want to apply the rule to the algorithm after scanr fusion, f would be mss and cata h is the function that computes the maximum prefix sum of the input list (let's call the function mps). Then we have to synthesise a function g that combines a new element x, mss xs, and mps xs into mss (x : xs) and mps (x : xs), which is just the traditional approach to the problem and a bit more difficult than "mechanically" fusing <max, head> into the fold that generates all maximum prefix sums of suffixes.

--
I decided to write this blog post in English because hardly anyone who reads this blog cares about catamorphisms and I certainly need to practise writing in English. XD

Tchaikovsky: Symphony No. 6 (Pathétique)

我的語文表達能力不可能成功描述今天到國家音樂廳聽 Vladimir Jurowski 指揮倫敦愛樂演奏 Tchaikovsky 悲愴交響曲的感受，只能說 Tchaikovsky 真是太偉大了，我不知道我有沒有勇氣再（認真）聽一遍。第一樂章演奏到震撼處，我直感到音樂背後的作曲家冒了出來，向聽眾大聲呼籲著什麼。這恐怕是我又一次更深刻地認識音樂的近似能力。It makes me feel so bad just because it's such a fine piece of music.

--
Tchaikovsky: "Without exaggeration, I have put my whole soul into this work." (Wikipedia)

PB 劫數

今天「資訊理論與編碼技巧」上課，吳家麟老師正在講解幾組 coding 的特性（instantaneously decodable / uniquely decodable / ...），突然我的 PB 就從桌子上滑下去，摔在地上！拿起來稍微檢查一下，似乎沒什麼大礙。回來要插電才發現，那一帶外殼因為撞到而些微變形，使得插頭異常難插，幸好還插得進去。唔，既然插得進去就暫不送修啦 XD。

--
摔下去的時候其實沒有很驚慌，因為有 Time Machine XD。

追

Information theory 能不能安全過關，就看今晚了！XD

--
加油啦 XD。

---

以後要讀 information theory 的人記得和 probability theory 混熟一點，不然對 probability theory 和 information theory 之間巧妙的關連沒什麼感覺的話很可惜；然後讀過 probability theory 的人建議可以看看 information theory，會對 probability theory 的威力有全新的體驗。

--
真的有炫到 XD。

神祕清單

• product . descend
• sum . map square
• div . <sum, length>
• max . map sum . inits

--
應該很夠了 XD。

MSS 海報

也可視為 functional derivation of MSS 的終極懶人包 XD。

--
很難調 XD。

Maximum Segment Sum 的成長故事

前言

這篇我打算讓跟 program derivation 不熟的人也可以體會一下 squiggolists 是怎麼把 mss 的 linear-time, constant-space algorithm 變出來的。敘述有點冗贅，但稍微耐著性子應該不會很難讀（希望啦 XD），強烈建議讀一遍。對 derivation 有興趣的話，可以參考下面的懶人包：

• mss.lhs：包括可執行的 specification 和最終的 algorithm。
• mss.pdf：整個 derivation，需要一點 Algebra of Programming 的基礎。

如果看得懂 derivation，一定會感受到 functional program derivation 超強的表達能力 ─ 以下所有的解釋都可以收在 derivation 的符號裡面，更精簡也更準確。我會用 mss.pdf 第一頁 derivation 裡面的 premises 當作目前我們所在位置的提示。開始嘍！

definitions

怎麼算一個 list 的 maximum segment sum 呢？很簡單：先把這個 list 的所有 segments 產生出來，對每個 segment 算出元素和，然後取最大值。實作上，

1. 我們先找到 list 的所有 suffixes（例如 [1,2] 的所有 suffixes 是 [], [2], [1,2]），
2. 對於每一個 suffix 算出它的所有 prefixes（例如 [1,2] 的所有 prefixes 是 [], [1], [1,2]），
3. 把全部的 prefixes 放在一起後，
4. 算出每個 prefix 的和，
5. 最後取最大值。

naturality of concat

我們剛剛是先把每個 suffix 的 prefixes 放在一起之後再統一算出各個 prefix 的和。其實我們也可以在找到一個 suffix 的所有 prefixes 的時候就把這些 prefixes 個別的和算好，然後再把各個 suffix 對應的 prefix sums 收集起來。

claim: maximum . concat = maximum . map maximum

把每一個 suffix 的 prefix sums 收集起來是為了統一取最大值，但其實我們也可以在算出一個 suffix 的所有 prefix sums 後先取這些 prefix sums 的最大值，之後再對這些（與 suffixes 一一對應的）maximum prefix sums 取最大值。

map functor

現在的演算法是這樣的：

1. 找出 list 的所有 suffixes，
2. 對每個 suffix 算出全部的 prefixes，
3. 然後算出每一個 suffixes 的所有 prefix sums，
4. 在每一組 prefix sums 裡取最大值，
5. 最後在各組最大值裡面取最大值。

在取最後的最大值之前，我們都是對每一個 suffix 去算 prefixes、再對每一個 suffix 的 prefixes 算 prefix sums、再對每一個 suffix 的 prefix sums 取最大值，所以演算法也可以在找出 list 的所有 suffixes 之後對每一個 suffix 直接「算 prefixes、對每個 prefix 算出 prefix sum、取 maximum prefix sum」，三個動作一氣呵成，然後在「suffixes 對應的 maximum prefix sums」裡面取最大值。

first fusion

對於每一個 suffix 我們的最終目標是算出它的 maximum prefix sum，接下來的兩次融合會導出一個只做一次 traversal 的演算法計算這個值。第一次融合告訴我們，與其產出所有 prefixes 再算出每個 prefix 的和，不如直接產出所有的 prefix sums。算法是從 list 後面走回來：如果已經知道 xs 這個 list 的所有 prefix sums，那麼 x : xs（就是在 xs 前面接上元素 x）的 prefix sums 怎麼算呢？把 xs 的每一個 prefix sum 加上 x 就差不多是 x : xs 的 prefix sums，記得補上 empty prefix 的和 0 就行了。

second fusion

現在我們可以用一次 traversal 算出所有 prefix sums。第二次融合告訴我們，巡訪過程中可以順便算出 maximum prefix sum。算法是這樣的：既然我們只要 maximum prefix sum，何必在走過來的時候記住所有的 prefix sums 呢？假設 xs 的 prefix sums 是 s₁, s₂, ..., s_n，其中 s₁ 是最大的，那麼 x + s₁ 仍然是 {x + s_k}_{1 ≤ k ≤ n} 裡面最大的那一個，所以我們只要記住 xs 的 maximum prefix sum 就可以了。然而 x : xs 的 prefix sums 不只有 {x + s_k}_{1 ≤ k ≤ n}，還有一個 0，所以我們必須在 xs 的 maximum prefix sum 和 0 兩者當中取最大值，才是 x : xs 的 maximum prefix sum。

introducing scanr; third fusion

到這裡我們的演算法已經變成

1. 算出 list 的所有 suffixes，
2. 對每個 suffix 用一次 traversal 算出它的 maximum prefix sum，
3. 最後取最大值。

這種「對 list 所有 suffixes 做 traversal」的樣式叫做 scanr，而 scanr 其實也可以用一次 traversal 完成！如果我們已經有 xs 所有 suffixes 的 maximum prefix sums，我們也當然有 xs 本身的 maximum prefix sum，於是用和上面同樣的方法就可以算出 x : xs 的 maximum prefix sum。和原本那些 xs 所有 suffixes 的 maximum prefix sums 湊起來，就是 x : xs 所有 suffixes 的 maximum prefix sums。

split cancellation (backwards); fourth fusion

現在的演算法已經變得很簡單了：

1. 用一次 traversal 直接算出所有 suffixes 的 maximum prefix sums，
2. 然後在這些 maximum prefix sums 裡面取最大值。

看過這麼多次融合，一定猜到現在該做什麼了：把這兩步融合成單一次 traversal！計算 suffixes 的 maximum prefix sums 時，我們就不要把先前所有的 maximum prefix sums 都記住，只要記最大的那個就好 ─ 也就是標準的打擂台演算法。但是計算 x : xs 的 maximum prefix sum（也就是新的挑戰者）時我們需要 xs 的 maximum prefix sum，所以也要把它記住。如此一來，我們就得到標準的 linear-time, constant space algorithm，用一次 traversal 算出所有 suffixes 的 maximum prefix sums 當中的最大值。

結語

Functional program derivation 值得注意的一個特點是：每一步變換的結果都是一個新的演算法（當然解的是同一個問題），所以我們是在一開始顯然無誤的演算法裡面動手腳，逐漸改出最終的演算法。不得不說 squiggolists 選 mss 當作經典例子非常有道理，因為整個 derivation 都是 fold fusions（也就是 traversals 的合併），specification 拿起來拚命融就是了。做 derivation 的時候其實不用想這麼多具體的語意，只要操作語法和抽象語意（我保證這會簡單很多），程式就會像上面所描述地逐漸變換。Imperative programs 要做這種事情應該很難吧。

--
有整篇看完的人可以舉個手嗎？XD

（超）指數延展的前路

今天 MFN meeting 聽 scm 老師簡介 dependent type theory，覺得完蛋啦，又是一大堆東西要進來。當年從正常人變成 programmer，最近花半年變成 dependently-typed programmer，接下來又要再掙扎一次變成 dependent type theorist（斷句方式是 "dependent type" theorist 不是 dependent "type theorist"，雖然後者大概是近程目標 XD）。往資管系的路上把 MSS derivation 經過的變換想通了，待會寫一篇 blog 記下來，然後 derivation 就暫時放一旁，學校的東西弄一弄趕快看 (dependent) type theory。只要恍神一下大概就追不上了…

--
偶爾也讓我有一陣子「什麼都懂」的感覺也無妨啊 XD。

Say Goodbye

明天就要把《Algebra of Programming》還給 scm 老師嘍。這本真的是價值連城：有兩個作者的簽名，詳細精緻的便利貼註解，連書套都有紀念意義！還是早點還回去比較好，整天帶來帶去怕弄丟，而且邊角持續磨損…

--
所以有一個星期看不到 AoP XD。

Tupling Transformation

雖然昨天的兩篇 MSS 主要都是做 tupling transformation，但我還是看不懂 AoP 給的一個推廣。AoP exercise 3.4 說的是

形式長得還挺像的，可能再湊一湊吧。

--
先睡嘍。

不妙

我覺得我已經無心於課業了。現在明明離期考還有點距離，竟然就已經成天弄別的…（而且還是沒太大訓練效果的東西！）

--
讓你做這麼多 derivations 了，明天一定要寫作業喔 XD。

繼續做 MSS

先前導的 mss 只會傳回最大和，不會傳回對應的 segment，這樣實在不夠有趣 XD。定義

其中 xs ↑Σ ys 傳回 xs 和 ys 兩者當中總和較大的那一個。那麼我們就可用與 derivation of mss 差不多的過程導出 cmss (abbreviation of "complete maximum segment sum") 的 quadratic-time version：

Quadratic time?! 雖然我們已經用上 tupling transformation，但這只把 linear-space 降為 constant-space，而 f 裡面會呼叫 sum，所以並非 constant-time operation。展開 f 的實作會更清楚：

為此我們必須做第二次 tupling transformation，把 sum 的結果也放進 "induction hypothesis" 裡面。我們可以如下在 fst 右邊「憑空」（i.e., by introducing id）變出 fusion 使用的火種：

這樣我們就可以做 fusion 了（不過我這裡偷懶，沒真的做 XD）：

其中 newssp (abbreviation of "new segment-sum pair") 可實作為

我猜如果對 sum . cmss 做某種 fold fusion，應該就會得到本來 linear-time & constant-space 的 mss。

--
一般不呈現這個版本的理由應該很顯然 XD。

自己做 MSS Derivation

從來沒有自己做過一遍 maximum segment sum 的 derivation，對這個經典問題太失禮了。於是今天計算機網路課堂上就自己導一次。（啊，我真的聽不太下去 XD。）有進步的地方是一開始整理用到的其中兩條規則，我現在知道是 "naturality of concat : F ← FF" 和 "functor (map) respects composition"。可是到中間果然卡住了：在湊其中一個 fusion condition 時為了把 max 擠到 recursive term 旁邊，我直接和後面的 map (x+) 做 type functor fusion，然後就再也沒辦法把 max 析取出來。偷看 scm 老師的 slides，才知道這裡要一步到位，直接證明 max . map (x+) = (x+) . max。這個式子就很單純，左邊做 type functor (fold-map) fusion 右邊做 fold fusion 就得到同一個 fold，而右邊的 fold fusion 就會用到 scm 老師說的關鍵 "+ distributes into ↑"，即 x + (y ↑ z) = (x + y) ↑ (x + z)。

scm 老師最後停在一個 linear-time, linear-space algorithm，並說可藉著 tupling transformation 轉成一般看到的 linear-time, constant-space algorithm。既然如此就來導吧！We reason:

其中「天啟」（revelation）那一步其實也沒那麼神奇。如果我們想直接把 max 融進 scanr，試著證明 fusion condition：

這時就發現我們會用到 head xs，但我們只能用 max xs。於是為了兩個都能用，就很自然地引進 fst . <max, head> 啦。最後是 fusion condition 的證明：

可以看到最終演算法裡面的 0 ↑ (x + z) 算的就是 maximum prefix sum（"prefix" 是因為 foldr 是從尾端累積回來的），y 就是 maximum segment sum。

--
但我仍然還沒透徹了解為什麼四次 fold fusion 之後就能得到這個演算法…

---

想要一個也順便傳回那個 maximum segment 的演算法，但是改 specification 重導很麻煩。有好方法嗎？

--
該不會要用 monad 吧 XD。

Typing Rules

面對一大堆 typing rules，我目前歸納出來的情況是：厭煩不想看的程度和「個別 typing rule 的大小」、「typing rules 總數」、以及「符號多寡」三個變數呈指數成長關係…

--
希望強迫多讀一點可以把那關係降為多項式 XD。

唯美版

郎朗演奏的 Rachmaninoff's Piano Concerto No. 3，唯美風格的一個版本。

當然一如往常，對這首曲子不熟的人不建議看畫面。這如果在音樂作品欣賞課堂上放，課後心得一定都寫「鋼琴家的動作太瘋狂」之類的，聽不太到音樂 XD。

--
Cadenza 的詮釋很有趣，也讓人不禁有點擔心 XD。

Reviews

看 reviews 還滿好玩的，因為 reviewers 的意見會互相矛盾 XD。例如有人說這篇 paper 展示了這條進路的 scalability 而且給了一個 nontrivial example（不知道他指的是 maximum segment sum 還是 insertion sort ─ 應該是前者吧 XD）；另一個人說 dependently-typed programming 和 squiggol-style derivation 都不太 scalable，兩個合在一起就更難了 ─ 你看 insertion sort 顯然不是什麼 "rocket science" 就已經要證很多行。（我個人同意後者的說法 XD。）不過一個共通點就是全體一致都說 paper 寫得很好！第一個人說「擲地有聲（sound）、寫得很好」，他底下的 reviewer 說「技術上擲地有聲、例子很有說服力，建議採用（recommend acceptance）」；第二個人說「寫得很好、技術上擲地有聲、很好讀很容易跟上」「這篇 paper 顯然符合 MPC 的主題，我絕對建議採納這篇」；第三個人說「我還滿喜歡這篇 paper 的，的確寫得很好，行文非常清楚，技術發展也擲地有聲」。scm 老師邊看一定邊得意地笑 XD。（雖然三個人的讚美都用差不多的字 ─ 是公式嗎？XD）

--
技術、寫作上的評論與建議就省啦，這篇是普遍級的 XD。

ACCEPTED!!

中了！

MPC '08 Notification

Dear author,

Thanks for submitting a paper to MPC'08.
Your submission has been selected.
For your information, we selected 18 papers out of 38 submissions.
You will receive the detailed reports by wednesday with instructions for submission of the revised version of your paper.

Christine Paulin
MPC'08 chair

----------------------------------------------------------
Submission number: 6
Submission title: Derivation-Carrying Code using Dependent Types

也看得到 review comments，三則！

這時候配 Paganini 主題狂想曲第 18 號變奏再加慢動作播放的紀錄片最完美了 XD。

--
我本來已經準備好要面對人生第一次 paper rejection 了 XD。

Textbooks

我受夠了！Paper 裡面都是一堆奇怪的 XX-types 和各種令人眼花撩亂的 typing rules，該是讀一讀 textbooks 的時候了。上完知識論就去借 Benjamin Pierce 的《Types and Programming Languages》和《Advanced Topics in Types and Programming Languages》！

很久以前我在天瓏曾被《Types and Programming Languages》吸引，把它拿下來翻一翻，但顯然我那時沒料到日後會這麼迫切地需要它 XD。

--
有沒有時間看就是另一回事了…

歡呼轉播

等一下 Weijin 回來之前如果沒聽到像樣的歡呼，就是中華隊輸了 XD。

--
溢位溢到 -27xxx 真是不簡單…

---

聽到咒罵著進房間的聲音 XD。

--
所以輸了 XD。

Distraction

今天在編譯器課堂上讀 dragon book。效果沒很好，因為會被講課聲拉走。上一週在 202 讀，效果就好得多。我覺得以後還是不要去好了…

--
計算機結構大概也要比照辦理…

Indexed Containers

中午在網上閒逛等人，逛到 Conor McBride 的網頁（他真的很滑稽 XD），右邊赫然有一篇〈Indexed Containers〉，說不定能解決 internalism vs. externalism 的問題！

同時他們那一群人也都很恐怖，光理論上 type theory 和 category theory 和所有相關的東西都熟得跟什麼一樣…

--
好吧，慢慢看吧 XD。

緊張

Information theory 已經達到一種極端緊張的境界，不趕快讀點書紓壓一下的話，下星期再上課就爆定了！

Y 老師每次看到我（即二下導生宴和三年級兩次選課單簽名）一定都表情有點誇張地問「我是不是看過你啊？！」然後想起來我做過什麼瘋事之後再表情有點誇張地問「那這樣你不就聽兩次？！」XD

--
現在證明我那時候聽完是對的 XD。

Duality

因為通識課「音樂作品欣賞」上次播放，我現在開始聽 Rachmaninoff 的 "Rhapsody on a Theme of Paganini"（帕格尼尼主題狂想曲）。這首曲子針對 Paganini 狂想曲的一段主題做 24 段變奏，形式很像鋼琴協奏曲。系上工作站的網頁空間似乎把 mp3 擋掉了，我只好把今天想貼上來的兩段壓成 zip 檔案，請按標題下載。鋼琴是 Rachmaninoff 本人演奏的。"2-09" 開頭的檔案是 Paganini 原本的主題，"2-26" 是我突然發現很有意思的一段變奏（variation #18）。仔細比較一下，category theory 的一個重要現象 "duality" 就在裡面！

--
這裡是答案，還沒聽的先不要偷看喔：變奏是原主題的「上下」鏡射，連小調都變成大調了！

---

剛剛看 Wikipedia，發現這段變奏果然是最有名的，Rachmaninoff 本人好像也很喜歡？

--
我看不懂他講什麼 XD。

保護傘

想想還真恐怖，參加 FLOLAC '08 的時候我就升大四了，很快就沒有「還只是小小的 undergrad」的保護傘可用了…

可是我又好想有自己的成果，現在寫那些稍嫌無聊的作業（例如找出某顆 CPU 的 L1 cache size…）都覺得好煩 XD。

--
很顯然我到十二點多醒來後就睡不著了，只好起來翻一翻 information theory XD。

FLOLAC '08

2008「邏輯、語言與計算」暑期研習營暨碩士學分班（FLOLAC '08）的資訊漸漸出現了！我要在這裡大力呼籲：只要對 theoretical computer science 有那麼一丁點興趣的人就一定要來聽聽看！今年陣容更加堅強，不聽鐵定遺憾終生！不要學分的話我猜旁聽也沒問題的！如果自己不能到，就叫朋友去幫你聽課！當然和朋友一起去是最完美的！

--
我個人想旁聽就好，因為不想考試 XD。

快睡著了

所以我再一下下就要睡了 XD。

--
就這樣 XD。

離散與連續

與蕭邦第一號鋼琴協奏曲相遇已兩年餘，現在聽還是覺得蕭邦真是天才！鋼琴也能表現出這種連續滑順的質感，猶如一疋高貴絲綢，太美了！

--
如果不寫點別的，這個 blog 都快變成 research blog 了 XD。（謎：原來這不是 research blog？XD）

Building GHC

PB 現在正辛苦地建置（build）ghc-6.8.2，因為我覺得先前用的 ghc-6.8.1 binary dist. 裝得不好，連帶使 Agda 的表現一直怪怪的。例如自從升級到 Leopard 後我就沒有 "context" 可用了（要間接用 "infer type" 看），又如前幾天重新拉回（pull）並重建 Agda 之後仍然看不到 "deactivate Agda"，然後 standalone interpreter 一定建不起來…等等。這次來個釜底抽薪，希望 ghc 可以成功建置出來嘍。

--
至少到現在還沒跳出失敗訊息…

---

睡個覺起來，make 果然完蛋了。觀察網上的討論，看來又是 ld 的問題。試著把一大堆 Agda 需要的 dependencies 裝到 ghc-6.6.1 也有些 packages 會失敗。根本不可能在 Leopard PPC 上編譯 ghc-6.8+ 或新版的 Agda 嘛…

--
這時候還真的有堂皇理由申請「設備費」買一台 Intel-based Mac…

---

改用 ghc-6.8.2 的 Tiger PPC binary dist.，現在正在建置 Agda，到目前為止都還不錯。

--
這次看起來比較有希望 XD。

---

Agda 是成功編回來了（連 standalone interpreter 都成功了），可是功能跟以前一模一樣。我不死心，查了一下 configure 有什麼選項，然後就發現一些好像很棒的東西，例如 "--enable-optimization"！如果真的有效的話，我以後每次載入就不用再等那麼久了 XD。

--
重編中 XD。

---

然後我想到說不定是因為我沒更新 emacs 設定的關係。

--
等它編完再試嘍。

---

果然是這樣！現在我有好多新功能了，context 等老功能也回來了，真感動 XD。而且 Aquamacs 現在一進 Agda2 mode 就會自動變成 TeX input method，太完美了！

--
重新安裝果然有所回報 XD。

Causal vs. Casual

我正在譯 Intro. to FP 第一章。p.10 section 1.4.1 "Extensionality" 之前講 "function f(x)" 和 "function f" 兩種說法的區別。最後一句是

Accordingly, we cannot afford to be causal about the difference between a function and the result of applying it to an argument.

那個 "causal" 讓我百思不得其解，再怎麼廣泛詮釋字典給的意思（和我本來的理解差不了多少）也沒辦法拼進句子裡，和 Weijin 討論也沒有結果。最後在 Google 搜尋 "causal about" 第七頁看到一句

We might all be causal about a butane lighter, but they are dangerous as well and much lower pressure.

這句的上下文給了滿強烈的提示，我看了幾遍才恍然大悟 ─ 原來是把 "casual" 拼成 "causal" 了！我正想著 Richard Bird 害人不淺，再看一次原文，才發現從一開始就是我看錯，Richard Bird 用的字是 "casual" 沒錯 XD。說不定是最近知識論談 "reliable causal process" 的關係 XD。

--
還得感謝第二句拼錯的人 XD。

Proving Associativity of List Concatenation by Fold Fusion

概念上 fold 是 structural induction，所以任何 inductive proof 應該都可以用 fold 重寫吧？關鍵可能就在於從 pointwise style 轉移到 point-free style。以下證明 list concatenation 的結合律，第一步先把欲證明的式子轉成 point-free style：

等號左邊和右邊都是一個 function 跟在一個 foldr 後面（「(++ys) 和 (++) 如何表示為 foldr」留給讀者作練習 ─ Richard Bird 最愛講這句了 XD），所以很自然地我們對兩邊做 fold fusion。（TRICK: 整理成 point-free style 的時候我其實已經知道要對 xs 做 induction 了！）左邊的 base case 是 (++zs) ys = ys ++ zs，inductive case 則是

右邊的 base case 是 rapp (ys ++ zs) id = ys ++ zs，inductive case 則是

因此兩邊的函式都等於 foldr (:) (ys ++ zs)，即得證 list concatenation 的結合律。不過這樣做下來，我寧願直接做 pointwise induction XD。

--
To hcsoso: if you're interested, we can perhaps meet some day and I'll talk about the derivation lectures in FLOLAC '07. I think it would be a faster way to get familiar with functional programming and reasoning. :P

---

再多看一眼，其實 foldr (:) (ys ++ zs) xs 就是 (++(ys ++ zs)) xs，所以可以只做左邊的 fold-fusion。另外，這樣的結果某種角度而言暗示了 list concatenation 應該定義為 right-associative。

Haskell Exercises --- Done

寫完了！真正的程式只有二十幾行，產出的 pdf 卻有六頁 XD。

• haskell_exercises.lhs: literate Haskell source script;
• haskell_exercises.pdf: document typeset by lhs2TeX and pdfLaTeX.

--
後面就比較懶得正式證明 XD。

My Algebra of Programming!!

聽說我的《Algebra of Programming》終於到了！當時在 Amazon 的各國分店苦找，到 Amazon.ca 看到的竟然是 "Only 1 left in stock"！二話不說就打電話回家，買下來了 XD。Amazon.ca 的標準國際遞送應該是海運，不像 Amazon.com 那麼快，所以要等兩到三個月。幸好沒掉到海裡 XD。這樣 scm 老師就可以拿回他那本價值連城的唯一限定版啦 XD。

--
我會想念那些筆記的 XD。

Haskell Exercises

scm 老師突然出了一些 Haskell 題目讓我們練習，所以我把 lhs2TeX 裝起來，開始寫我的第一份 Haskell (literate) script XD。前兩題就讓我寫了三頁（LaTeX 標準頁面），因為第一題我先從 base functor 導出 fold of tip-valued trees 再用它定義 flatten，第二題則有詳細的 derivation，而且一樣先從 general fusion law 導出 tip-valued trees 的 fold-fusion theorem，最後還有感言 XD。剩下的明天寫吧…

--
(2008/3/4) 現在全部寫完啦 XD。

Feel Like Translating

以後想閒晃的時候就來譯一段 Intro. to FP 吧，好久沒翻譯了 XD。

--
今天衝了 11 頁的 monads XD。