2012 「邏輯、語言與計算」暑期研習營 (FLOLAC ’12)

因為今年做的種種改變,FLOLAC 2012 的籌備比起往年慢了一些。這兩天發現已經有人在詢問了。是的,今年 FLOLAC 照常舉辦,而且將成為大學部的正式暑修課程!也因此,FLOLAC 開課時間改為暑期後半(8月27日至9月7日)而非傳統的七月。今年的國外講者是任職於 Max Planck Institute for Software Systems 的 Arthur Charguéraud, 將為我們介紹程式語言學界影響力日增的定理證明/程式驗證工具 Coq.

2012 Formosan Summer School on Logic, Language, and Computation (FLOLAC ’12)

2012 「邏輯、語言與計算」暑期研習營暨「程式語言理論與型態系統」暑期課程。

  • 日期: 2012 年八月廿七日(週一)至九月七日(週五)。
  • 時間: 每週一至週五早上九點至下午五點。
  • 地點: 台大共同教室(暫定)。

宗旨

近年來,從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識。然而,國內從事此類研究的學者分散在各校,難以僅靠一己之力開設整套課程。因此,我們邀請有相同興趣的學者一同開課,訓練下一代的研究人才。

「邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力。從第二年起,本研習營在兩大主題 — 程式語言,模型檢查與程式驗證之間輪流替換。今年(偶數年)之主題為程式語言理論與型態系統。

今年的 FLOLAC 研習營有如下改變:

  • 本研習營首次成為台灣大學正式暑修課程,針對大學生開課。台灣大學學生可透過國立台灣大學暑期課程網選課,有學籍之其他學校學生可透過校際選修選課。無學籍之社會人士也可旁聽。詳見報名資訊頁。
  • 為配合暑修時間,今年 FLOLAC 改於暑期後段(8月27日至9月7日)舉辦。
  • 今年請到任職於 Max Planck Institute for Software Systems 的 Arthur Charguéraud 介紹程式語言學界影響力日增的定理證明/程式驗證工具Coq.

「邏輯、語言與計算」暑期研習營曾在 2007、 2008 、2009 、2010 、2011 年舉辦,今年為第六屆。

主辦單位

中央研究院資訊科學研究所、台灣大學資訊管理學系聯合主辦。

課程委員

陳恭 Kung Chen, 政治大學資訊科學系。
莊庭瑞 Tyng-Ruey Chuang, 中央研究院資訊科學研究所、台灣大學資訊管理學系。
穆信成 Shin-Cheng Mu, 中央研究院資訊科學研究所。
謝邁思 Max Schaefer, Oxford University Computing Laboratory.
蔡益坤 Yih-Kuen Tsay, 台灣大學資訊管理學系。
王柏堯 Bow-Yaw Wang, 中央研究院資訊科學研究所、台灣大學資訊管理學系。
楊武 Wuu Yang, 交通大學資訊工程學系

課務統籌

張少娟 Shao-Chuan Chang, 中央研究院資訊科學研究所。

報名資訊

詳見網站: http://flolac.iis.sinica.edu.tw/flolac12/

Posted in 活動消息 | Tagged | 1 Comment

Benoît Mandelbrot 與碎形

Benoît Mandelbrot (20 November 1924 – 14 October 2010, 本人使用的中文名為本華·曼德博) 上週因癌症逝世。以下資料大多來自 Wikipedia 和 BBC 報導。

Mandelbrot 出生於波蘭華沙一個猶太家庭,母親是醫生,從小有兩位叔叔常教他數學,其中一位是數學家,父親則作布匹生意。十一歲時,全家為躲避納粹迫害搬到巴黎。1945 到 47 年間他在法國巴黎綜合理工學院 (École Polytechnique) 求學,1949 年在加州理工學院獲得航空工學碩士,1952 年在巴黎大學得到數學博士學位。Mandelbrot 曾先後在法國國家科學研究中心 (Centre National de la Recherche Scientifique), 法國 Lille Nord 大學 (Université Lille Nord de France), IBM Thomas J. Watson 研究中心任職,並曾在 von Neumann 邀請下訪問普林斯頓高等研究院,後來成為 IBM 榮譽 fellow.

1951 年起,Mandelbrot 不僅研究數學,也在資訊理論、經濟學、流體力學等領域發表論文。在許多領域中他發現了同樣的特性:厚尾分佈自我相似結構。市場價格並不符合高斯分佈;如果恆星以碎形方式分佈,可不必靠大爆炸理論解釋天文學中的 Olbers’ 謬論。1975 年,他用「碎形 (fractal)」一詞描述此現象。從此這詞進入了大家的日常語彙中。

然而,碎形是什麼呢?很難找到一個同時可兼顧簡單和精確的解釋。一種說法是:碎形可用來描述自然界層出不窮的不平滑 (roughness) 現象。傳統數學善於描述圓與直線。但在 Mandelbrot 的 The Fractal Geometry of Nature 一書有這麼一段著名的話:「雲不是球形的,山不是圓錐形,海岸線不是圓圈,樹皮不平滑,閃電也從不順著直線走。」雲、山、海岸線、閃電等都是自然界可看到的碎型,複雜而不規則。然而這是自然之所以美的原因。如果雲是圓形的,那多無聊。而如果數學不能捕捉自然之美,那是多麼可惜的事情。碎形理論揭去了這層神秘的面紗,告訴我們,這些自然事物的「規則」其實隱藏在另一個維度中。

「自我相似性」是碎形的另一個特色。將一片雲的一部分放大,看來和整片仍很相似;松樹的一個分支看來就像是整顆松樹的縮小版。這種自我相似性在自然界中也隨處可見。


牛頓法分析中出現的 Mandelbrot set. 來自Wikimedia Commons.

高中、大學時代我曾對碎形著迷過一陣子,試著寫程式畫 Mandelbrot set. 老實說,只是把書上找來的公式拿來用,裡頭牽涉到的數學當時不懂,現在仍不懂。用當時算快的 Mac II,一張圖得畫好幾個鐘頭,若是放大,得花一整個晚上。現在的電腦快多了,找了一些程式來玩,繪圖、放大、縮小,幾乎是一瞬間的事。

參考資料

Posted in 人物 | Tagged , | Leave a comment

荷蘭國旗問題 The Dutch National Flag Problem(下)

Quicksort 是實用上表現很好的排序法。眾所皆知,quicksort 的缺點是碰到大致上已排好的、大致上逆向排好的、或著有許多重複元素的陣列時,效率就變差了。若把荷蘭國旗問題用在 quicksort 中,用紅、白、藍三色分別代表小於、等於、大於 pivot 的元素,由於等於 pivot 的元素已被放在一起,應有易於處理重複元素的好處。然而,直到 90 年代中期之前,大家的一般認知是解荷蘭國旗問題需要太多次交換,不值得做。一般做法是把大陣列先用 quicksort 分割,等切得夠小就換成 bucket sort 或 radix sort.

到了 90 年代, Lee McMahon 為第七版 UNIX 寫的 quicksort 函式和其衍生版本已經流傳將近二十年之久。Bentley 和 McIlroy 發現,對所有他們能找到的 quicksort 實作,都可很容易地做個輸入讓它得花輸入長度平方的時間跑完。於是他們決定寫個更有效的 quicksort. 為了處理重複元素,他們又回頭研究了荷蘭國旗問題。

上次我們看了排序 [w,r,b,b,r,b,r,r,b,r,r,w,r,r] 的例子。SrSb 兩種情況的交換分別用 表示。這個例子中,陣列有 14 個元素,而我們用了 13 次交換。

為什麼這麼慢呢?Bentley 和 McIlroy 認為問題出在我們花了太多工夫把兩個白色元素一步步挪到中間(也就是發生的情況)。與其如此,不如先把白色元素放到兩邊去,把陣列排成「白、紅、藍、白」。等排序完成,再把白色換回中間就可以了!他們用的不變量是這樣:

M ≤ w ≤ r ≤ u ≤ b ≤ N ∧ Pw1 ∧ Pr ∧ Pb ∧ Pw2

Pw1 ≡(∀i : M ≤ i < w : white(i))
Pr ≡ (∀i : w ≤ i < r : red(i))
Pb ≡ (∀i : u ≤ i < b : blue(i))
Pw2 ≡ (∀i : b ≤ i < N : white(i))

我用這不變量寫了一個程式:

  w, r, u, b := M, M, N, N
  { Inv: M ≤ w ≤ r ≤ u ≤ b ≤ N ∧ Pw1 ∧ Pr ∧ Pb ∧ Pw2, bound: b - w }
; do r < u →
    if red(r)             → r := r + 1
     | white(r)           → swap(w,r); w, r := w + 1, r + 1
     | blue(r) ∧ red(u-1) → swap(r,u-1); r, u := r + 1, u - 1
     | white(u-1)         → swap(u-1,b-1);  u, b := u - 1, b - 1
     | blue(u-1)          → u := u - 1
    fi
  od
  { M ≤ w ≤ r ≤ u ≤ b ≤ N ∧ Pw1 ∧ Pr ∧ Pb ∧ Pw2 ∧ r = u }

迴圈主體是對稱的五個情況,其中三種需要交換。以下是執行同一個輸入的結果:

確實不僅迴圈執行次數變少(由於 blue(r) ∧ red(u-1) 的情況可把灰色區域縮小兩個元素),交換次數也減少到了六次。當然,我們還需要兩次交換把白色元素放回中間。如果白色元素多,交換次數就多。但 Bentley 和 McIlroy 指出這部份的代價可分配到演算法其他部份去,因為白色元素一旦放到正確位置,便不用再被遞迴排序了。更詳盡的實驗結果可看他們的論文。

這兒的程式和 Bentley-McIlroy 的稍有不同。Bentley-McIlroy 用了兩個迴圈分別推進 r 與 u 的值。我個人比較喜歡這裡的做法,一來迴圈主體和不變量一樣對稱,二來這個程式非必須的限制較少:例如當 red(r) 與 blue(u-1) 都成立,在這裡可看出執行哪個指令對程式的正確性沒有影響。


只是,這麼一來,這迴圈解的好像不是荷蘭國旗問題了。有什麼國旗是「白、紅、藍、白」四色的呢?我找不出分出四條色塊的國旗。如果把顏色交換一下,倒是找到了右邊這幅 Rypin 的旗幟。Rypin 是波蘭的一個小鎮,根據 06 年的統計,人口約一萬六千人。

References

Jon L. Bentley, M. Douglas McIlroy. Engineering a sort function. Software—Practice & Experience 23(11), pp. 1249 - 1265. Nov. 1993.

Justin Peel. Has anyone seen this improvement to quicksort before? Stack Overflow , Jan 20, 2010.

Posted in 計算算計 | Tagged , | Leave a comment

荷蘭國旗問題 The Dutch National Flag Problem(中)

上回說到,為解荷蘭國旗問題,我們至少有兩種不變量可選。一是把未知區段放旁邊:一是把未知區段夾在某兩色之間:
該用哪個比較好呢?

答案是:用兩者都寫得出可運作的程式,但後者好寫得多。原因是:未知區段是我們的工作區,而我們有三種顏色要搬來搬去,把未知區段放在旁邊會使得某些搬移相當不便。

因此以下我們用第二個不變量,寫成邏輯式子是這樣的:

M ≤ r ≤ w ≤ b ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧
(∀i : r ≤ i < w : white(i)) ∧
(∀i : b ≤ i < N : blue(i))

最初若把 r, w, b 設為 M, M, N,不變量自然成立 --- M ≤ i < r, r ≤ i < w, 和 b ≤ i < N 三個區段都是空的,整個陣列都視為灰色的未知區。接下來我們希望在一個迴圈中逐漸縮小 wb 的差距。當 w = b 時,陣列就照我們想要的顏色順序排好了。

迴圈中應該作什麼呢?既然目標是把 b - w 變小,關鍵的元素可能是 a[w]a[b-1]. 也許我們可以先看看 a[w] 是紅、白、或藍色,分三種情況處理:或著我們也可檢查 a[b-1] 的顏色。個中優劣只有試過才知道了。依後見之明,我們發現先檢查 a[w] 較好。另一種選擇待會兒再談。

所以,程式架構大約是這樣:

   r, w, b, := M, M, N
   { Inv: M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb, bound: b - w }
 ; do w < b →
     if red(w)   → Sr
      | white(w) → Sw
      | blue(w)  → Sb
     fi
   od
   { M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb ∧ b = w }

其中 Pr, Pw, 和 Pb 分別是關於三個顏色之條件的簡寫:

Pr ≡ (∀i : M ≤ i < r : red(i))
Pw ≡ (∀i : r ≤ i < w : white(i))
Pb ≡ (∀i : b ≤ i < N : blue(i))

我們還需找出 Sr, Sw, 和 Sb 分別該是什麼。

white(w) 的情形最簡單:把 w 遞增之後不變量仍然滿足。Sw 可以是 w := w + 1.

blue(w) 的情況呢?若把 a[w]a[b] 交換,我們可把 b 遞減,不變量也剛好滿足。Sb 可以是 swap(b,w); b := b - 1.

最複雜的是 red(w) 的情況。我們可把紅元素換到後面去,但之後為了滿足不變量,我們得把 rw 都遞增。

總結下來,我們的程式是:

  r, w, b, := M, M, N
  { Inv: M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb, bound: b - w }
; do w < b →
    if red(w)   → swap(r,w);  r, w := r + 1, w + 1
     | white(w) → w := w + 1
     | blue(w)  → swap(b,w);  b := b - 1
    fi
  od
  { M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb ∧ b = w }

然而,上面的圖片其實遺漏了許多情況。例如,在 red(w) 的情形中,如果 b = w ,程式還會對嗎?我們得切記畫圖僅可幫助理解,程式的推導驗證還是得回到形式系統來作。

red(w) 的情況為例,我們得證明:

  { M ≤ r ≤ w < b ≤ N ∧ Pr ∧ Pw ∧ Pb ∧ red(w) }
  swap(r,w)
  { (M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb)[r, w := r + 1, w + 1] }
; r, w := r + 1, w + 1
  { M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb }

據我所知,在國內只有 FLOLAC 程式建構課教過這種證明(如果你會的話,來認識一下吧!),所以除非有人要求,這裡就只透露我們得分出 r = wr < w 的兩種情形,不深入談細節了。

這是一個 O(N-M) 的程式。如果三色數量相同,我們平均需要大約 2(N-M)/3 次交換。如果我們當初選擇從檢查 a[b-1] 開始,也可做出一個稍微不同的程式,但平均需要的交換次數增加到 N-M 次。

下圖是排序 [w,r,b,b,r,b,r,r,b,r,r,w,r,r] 的例子。SrSb 兩種情況的交換分別用 表示。這個例子中,陣列有 14 個元素,而我們用了 13 次交換。

Posted in 計算算計 | Tagged , | Leave a comment

荷蘭國旗問題 The Dutch National Flag Problem(上)


一個陣列 a[M], a[M+1] ... a[N-1] 裡頭每個元素都是紅、白、藍三色之一。如何把它們由左至右依紅、白、藍的順序排好呢?您可用 red, white, 和 blue 三個述語測元素的顏色;要改變陣列內容則只能用 swap(i,j),交換索引為 i 和 j 的兩個元素(因此不能先把紅白藍三色的數目分別數出來之後再把陣列整個重寫一次,也不能把 a 的內容複製到別處之後再複製回來)。整件工作希望在 O(N-M) 的時間內完成。

這個「荷蘭國旗問題」由 Feijen 和 Dijkstra 提出 — 紅白藍是荷蘭國旗的顏色。(為何不是法國國旗?恐怕因為 Feijen 和 Dijkstra 都是荷蘭人吧?)對演算法熟悉的朋友可能知道這可在 quicksort 中作分割用:選定一個元素當 pivot, 紅、白、藍三色分別代表小於、等於、和大於 pivot 的元素。和傳統將陣列分割成兩塊的做法比較,這種「三向」分割法不僅可能把陣列切得較小,也便於處理陣列中的重複元素。然而,Sedgewick 和 Wayne 的上課資料 (1, 2)提到,直到 90 年代中,大家仍認為三向分割法效率差,不值得做。直到 Bentley 與 McIlroy 提出了更快的三向分割法,Sedgewick 和 Bentley 也證明了此種 quicksort 是熵值最佳解 — 每元素平均被比較數在熵值的常數比率之內,三向分割法終於漸漸被用在包括 Java 與 C 的函式庫中。

九月的 IFIP Working Group 2.1 會議中,Wouter Swierstra 示範如何在 Agda 中證明此程序能正常終止,引起了一些相關討論。我才因此聽 Peter Pepper 說到,Dijkstra 當初研究這問題倒不是基於效率考量,而是他認為分割成兩份的傳統 quicksort 的終止證明不漂亮。Dijkstra 希望採用三向分割法後能更容易表達紅(小於 pivot)和藍色(大於 pivot)的區塊絕對比原陣列短的性質。然而,在 Peter 的印象中 Dijkstra 從沒把這層考量寫下來。「我們如果不告訴學生,以後就沒人知道了呢!」他說。

解一個問題前總得先看看如何精確描述我們要什麼。初始條件是 M ≤ N, 以及每個元素的顏色只可能是紅白藍之一:

M ≤ N ∧ (∀i : M ≤ i < N : red(i) ∨ white (i) ∨ blue(i))

而在程式結束時,我們希望找到 rw 兩值, 滿足:

M ≤ r ≤ w ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧                                  (*)
(∀i : r ≤ i < w : white(i)) ∧
(∀i : w ≤ i < N : blue(i))

注意在此我們用 Dijkstra 常使用的方法,以一對變數 x, y 表示 a[x], a[x+1] .. a[y-1] 這個區段(較正式的寫法是 a[x..y) -- 左合右開)。一個區段 a[x..y) 的元素數目剛好是 y-x, 而當 x = y 時該區段是空的。前面的規格涵括了輸入為空陣列的可能性(M = N),也允許某些顏色沒有元素(如 r = w 時,輸出陣列沒有白色的元素)。

這種程式至少得用個迴圈,而既然有迴圈,我們得為它找個不變量。通常的作法是把 (*) 擴充。我們也可猜到程式執行中必定有一段「未知」的區段。一個可能性是允許這個未知區段出現在右邊:

或著,我們也可能允許這段未知區段出現在白色與藍色之間:

剩下兩種情形則分別與前兩種對稱,因此我們只需考慮前兩者即可。

圖片可以幫助理解,但真正的理解仍得靠形式化的描述。第一種情形可描述為:

M ≤ r ≤ w ≤ b ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧
(∀i : r ≤ i < w : white(i)) ∧
(∀i : w ≤ i < b : blue(i))

那麼我們可採用的策略就是最初讓 r,w,b := M,M,M,每次在迴圈中試著遞增 b, 當 b = N, (*) 就成立了。

若選擇第二種可能,形式化的描述是:

M ≤ r ≤ w ≤ b ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧
(∀i : r ≤ i < w : white(i)) ∧
(∀i : b ≤ i < N : blue(i))

三個變數可先設為 r,w,b := M,M,N, 如果 b = w, (*) 便能成立。

哪個不變量比較好用呢?讀者不妨試試看。我們下回分解。

Posted in 計算算計 | Tagged , , | 4 Comments

Milner 消失的論文

以 ML, π-calculus, LCF, 和 Hindley-Milner 型別推導聞名的 Turing 獎得主 Robin Milner 於 2010 年三月逝世。這年的 ICFP 於是邀請劍橋大學同事 Mike Gordon 講述 Milner 生平。

整理文獻時,Gordon 發現了 An algebraic definition of simulation between programs 這篇論文的打字稿。該文中 Milner 提出了 "simulation" 的觀念,日後演變成現在的 simulation 和 bisimulation, 可說是篇重要的論文。這是一篇技術報告,後來另有篇會議版,應是本文和另一篇論文的綜合。[2]

令 Gordon 感興趣的是,稿子上方手寫著「投稿給 JACM, 1971 年九月」。但大家知道這篇論文一直都是技術報告。難道 JACM 把它退件了嗎?

Gordon 和 JACM 確認該文確實沒出版過。JACM 建議,當時的三位編輯都還健在,要不要寫信給他們看看是否還有紀錄留下來?

Gordon 寫了。三位編輯答案很一致。「什麼都不記得了!」

這場演講妙趣橫生,影片已經上網,很推薦大家看看。

References

Posted in 人物 | Tagged , | Leave a comment

ICFP 最具影響力論文獎

從 2006 年開始,每次的 International Conference on Functional Programming (ICFP) 回顧十年前發表的論文,看看哪篇最經得起歲月的考驗,在十年中發揮了最大的影響力。ICFP 2010 剛在上個月底落幕,而這是 ICFP 2000 的論文列表。如果您是評審,會頒獎給誰呢?

2010 年 ICFP 議程委員的選擇是…

Koen Claessen 和 John Hughes 的 Quickcheck: a lightweight tool for random testing of Haskell programs!

本文提出了一套相當簡單但有力的 Haskell 程式測試系統,為 Haskell 程式實務上的除錯帶來了重大的衝擊。本文描述了一個利用 type classes 和單子 (monads) 自動產生亂數測試資料的聰明技巧。此後 QuickCheck 成了極受歡迎、廣被程式員使用的 Haskell 函式庫,也被許多大學 Haskell 課程採用。本文描述的技巧引發了整套關於測試條件產生的後續研究,也被移植到其他語言上,包括為 Erlang 和 C 製作的商業版本。
Most Influential ICFP Paper Award.

John Hughes 在代表致詞時說,當時他正在忙另一個「很重要、很重要,可是我現在已經記不得了」的計畫。稍作歇息之時,Koen Claessen 提到了這個用 type class 產生測試資料的點子。他們覺得可用閒暇時間做做看。結果 QuickCheck 成了使用率最高的 Haskell 函式庫之一,不僅徹底改變了 Haskell 程式員的工作模式,還出了 Erlang 和 C 的版本。

「以一篇被 ESOP reject 的論文來說,還算不錯吧?」

ICFP 最具影響力論文獎自 2006 年起的歷屆得獎名單:

Posted in 計算算計 | Tagged , , | 2 Comments

Noam Chomsky 來台演講

Noam Chomsky 將於八月九、十兩日分別在中央研究院、清華大學進行兩場演講。

  • 八月九日 中央研究院 人文社會科學館國際會議廳 15:30 – 17:00: Contours of World Order: Continuities and Changes
  • 八月十日 清華大學 台積館孫運璿演講聽 11:00 – 12:00: Poverty of Stimulus: the Unfinished Business

以下簡介來自清華大學活動網站:

Noam Chomsky 教授 1955 年獲得賓州大學語言學博士學位。1951-1955 年榮獲哈佛大學獎學金 Junior Fellow of the Harvard University Society of Fellows, 並於此期間完成博士論文 Transformational Analysis, 其精華出版於 1957 年的劃時代巨著 Syntactic Structures 及其 1975 年的經典作品 The Logical Structure of Linguistic Theory. 1976 年獲選為 MIT Institute Professor.

Chomsky 教授的研究領域涵括語言學、哲學、認知科學、國際情勢與美國對外政策。他在五十年代提出了語言乃人類本能的學說,繼承理性主義的哲學傳統,但將語言落實在基因遺傳的基礎之上來談,奠定了生成語法 (generative grammar) 學派的基礎。其所主張「普遍語法」(Universal Grammar) 的概念也一反行為學派的看法,認為兒童學習語言皆有所本,引起了心理學革命性的變革。此外,他也是所謂 Chomsky hierarchy 的建構者,以數理分類來規範形式語言 (formal languages), 對資訊科學的發展產生了深遠影響。因此,他常被學界尊為現代語言學與認知科學之父。由於 Chomsky 教授長年以來關懷國際上的弱勢族群,並出版多部著作直言批評美國對外政策,他也成為全球文化界的表徵人物。

根據 1992 年 Arts and Humanities Citiation Index (A&HCI) 的統計,Chomsky 教授是 1980 – 1992 年期間著作被引用次數最多的現存學者(若從古至今來算則為第八位,僅次於馬克斯、列寧、莎士比亞、聖經、亞里斯多德、柏拉圖、與佛洛伊德)。

Posted in 活動消息 | Tagged | Leave a comment

Haskell 2010 出爐

一下子沒注意,Haskell 語言的新標準 Haskell 2010 已在七月六日出爐了。和 Haskell 98 比較,Haskell 2010 的主要變革是

  1. 原為增修功能的外部函數界面 (Foreign Function Interface)
  2. 階層模組 (Hierarchical modules) 改列入正式標準,
  3. 新增 pattern guards 語法,
  4. 拿掉了 n+k patterns.

Pattern Guards

Pattern guards 早在 1997 年便由 Simon Peyton Jones 提議,後來在 GHC 中實作。GHC 使用手冊中舉的例子是這樣的:已知 lookup 的型別是 Eq a ⇒ [(a,b)] → a → Maybe b, 假設你需要用 lookup 函數查環境 env 兩次。如果任一次結果是 Nothing, 程式就傳回 fail. 如果用 case, 程式得寫成這樣:

clunky env var1 var2 =
  case lookup env var1 of
    Nothing -> fail
    Just val1 -> case lookup env var2 of
      Nothing -> fail
      Just val2 -> val1 + val2

Pattern guards 讓我們可把程式寫成較清楚簡潔的形式:

clunky env var1 var2
  | Just val1 <- lookup env var1,
    Just val2 <- lookup env var2 = val1 + val2
  | otherwise = fail

我個人覺得這確實是很好用的語法。

n+k Patterns

Miranda 時代沿襲下來的 n+k patterns 則一直充滿著爭議。下面的階層函數中,第二行左手邊便使用了一個 n+k pattern:

fact 0 = 1
fact (n + 1) = (n + 1) × fact n

Richard Bird 是 n+k pattern 的擁護者,Philip Wadler 似乎也支持。Graham Hutton 的教科書 Programming in Haskell 中用了 n+k pattern. 他們認為自然數本來就是由 0 和後繼函數 (1+) 做出的資料型別,把串列中的資料拿掉,就成了自然數。教學上,他們認為很難跟學生解釋為什麼可對串列做配對:

foldr f e [] = e
foldr f e (x : xs) = f x (foldr f e xs)

卻不能對自然數做同樣的事:

foldN f e 0 = e
foldN f e (1 + n) = f (foldN f e n)

但更多人認為 n+k pattern 語意不清,問題多多。Lennart Augustsson 發起禁用 n+ k 運動, Paul HudakStefan Kahrs 立刻響應。 Malcolm Wallace 說 "(n+k) patterns are evil", John Launchbury 說他從語言品味的觀點就討厭 (n+k) patterns. 較早版本的 Haskell 98 報告中談及語言沿革,有如下的一節:

1.4 The n+k Pattern Controversy

For technical reasons, many people feel that n+k patterns are an incongruous language design feature that should be eliminated from Haskell. On the other hand, they serve as a vehicle for teaching introductory programming, in particular recursion over natural numbers. Alternatives to n+k patterns have been explored, but are too premature to include in Haskell 98. Thus we decided to retain this feature at present but to discourage the use of n+k patterns by Haskell users --- see Section 3.17. This feature may be altered or removed in Haskell 2, and should be avoided. Implementors are encouraged to provide a mechanism for users to selectively enable or disable n+k patterns.

現在 n+k pattern 終於在 Haskell 2010 中被拿掉了。被認為是替代方案的 View Patterns 還沒進入 Haskell 2010 標準,個人也覺得實在是太重量級了些。

Posted in 計算算計 | Tagged , | Leave a comment

計算多項式

FLOLAC ’10 最後一天我有大約 25 分鐘的時間和同學們介紹函數程式演算 (functional program calculation). FLOLAC ’10 的同學少部份學過 Haskell 或其他函數語言,大部份只在一週前學了三小時的 OCaml, 寫了一些程式作業,但對 fold 之類的抽象觀念可能還難以掌握。最大區段和問題很難在 25 分鐘內講完,用到兩次摺疊融合(fold-fusion), 而且這問題也已經講得有點煩了。另一個不錯的小例子「陡數列」問題的基本款大概只用得到五分鐘的時間。因此我得另外想個例子講。

最後想到的例子是這個:給一個數列 a₀, a₁, a₂ ... an 和一個常數 X, 計算 a₀ + a₁X, + a₂X² + ... + anXn. 在 Haskell 中可這樣一句搞定:

  poly as = sum (zipWith (×) as (iterate (×X) 1))

其中 sum, zipWith, iterate 等都是標準的串列函數,定義附在後面。這其實已經是個很好的 Haskell 程式了。只是如果我們還想再省幾個乘法,也許可再化簡一下。

當輸入是空串列,顯然 poly [] = 0. 考慮輸入是 a : as 的情形:

   poly (a : as)
 =   { poly 的定義 }
   sum (zipWith (×) (a:as) (iterate (×X) 1))
 =   { iterate 的定義 }
   sum (zipWith (×) (a:as) (1 : iterate (×X) X))
 =   { zipWith 的定義 }
   sum (a : zipWith (×) as (iterate (×X) X))
 =   { sum 的定義 }
   a + sum (zipWith (×) as (iterate (×X) X))

不幸地,在 a + 右邊那串式子無法收回成 poly asiterate 的最後一個參數是 X 而不是 1. 一個可能做法是把 poly 擴充一下,改收兩個參數。但這個問題還有更好的解法:

   a + sum (zipWith (×) as (iterate (×X) X))
 =   { iterate f (f b) = map f (iterate f b) }
   a + sum (zipWith (×) as (map (×X) (iterate (×X) 1)))
 =   { 如果 ⊗ 滿足遞移律, zipWith (⊗) as . map (⊗X) = map (⊗X) . zipWith (⊗) }
   a + sum (map (×X) (zipWith (×) as (iterate (×X) 1)))
 =   { sum . map (×X) = (×X) . sum }
   a + (sum (zipWith (×) as (iterate (×X) 1))) × X
 =   { poly 的定義 }
   a + (poly as) × X

因此我們導出了這個歸納定義:

  poly [] = 0
  poly (a : as) = a + (poly as) × X


除了 sum, zipWith, iterate 等標準函數的定義外,我們還用到了這些規則:

  1. map f (iterate f x) = iterate f (f x)
  2. zipWith (⊗) as . map (⊗X) = map (⊗X) . zipWith (⊗) as, 如果 ⊗ 滿足遞移律
  3. sum . map (×X) = (×X) . sum, a special case of foldr ⊕ e . map (⊗X) = (⊗X) . foldr ⊕ e, 如果 (a ⊕ b) ⊗ X = (a ⊗ X) ⊕ (b ⊗ X), 且 e ⊗ X = e.

這例子的優點是導出了 Horner’s rule, 缺點是最後的程式和原來的一行規格比並沒有快多少。我希望能有個像陡數列問題一樣,能在複雜度上有所改進的程式。大家有好建議嗎?

函數定義

sum 0 = 0
sum (x : xs) = x + sum xs

map f [] = []
map f (x : xs) = f x : map f xs

zipWith (⊗) [] _ = []
zipWith (⊗) _ [] = []
zipWith (x : xs) (y : ys) = x ⊗ y : zipWith (⊗) xs ys

iterate f x = x : iterate f (f x)

Posted in 計算算計 | Tagged , , , | Leave a comment