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

距離平方和

FLOLAC ’10 程式推導課的期末考出了這題:

|[ con N {N ≥ 2}; a : array [0..N) of int;
   var r : int;
   S
   { r = (Σ i,j : 0 ≤ i < j < N : (a.i - a.j)²) }
]|

用口語說:給定一個有兩個以上元素的陣列a, 計算任兩個元素前者減後者所得之差的平方的總和(這裡依照 guarded command language 的傳統把 a 的第 i 個元素寫成 a.i;函數取值 f(x) 也寫成 f.x)。

大家大概都能寫出一個使用兩層迴圈的程式。蠻可惜地,發現這題其實能只用一個迴圈、在線性時間內做完的則不多,因此我想可在這討論一下。

量詞 (Quantifiers)

先回顧一下關於量詞 (quantifiers) 的規則。給定一個滿足交換律、結合律、有單位元素 e 的二元運算元 。若將所有在區段 [A .. B) 之間的值非正式地寫成 i₀, i₁, i₂ ... in,那麼 F.i₀ ⊕ F.i₁ ⊕ F.i₂ ⊕ ... ⊕ F.in 就表示成:

   (⊕ i : A ≤ i < B : F.i)

更一般地說,若所有滿足 R 的值是 i₀, i₁, i₂ ... in,這個式子

   (⊕ i : R.i : F.i)

表示的就是F.i₀ ⊕ F.i₁ ⊕ F.i₂ ⊕ ... ⊕ F.in. 當確定不會混淆時,我們可把 R.iF.i 中的 i 省略。

關於量詞的規則有

  1. (⊕ i : false : F.i) = e
  2. (⊕ i : i = x : F.i) = F.x
  3. (⊕ i : R : F) ⊕ (⊕ i : S : F) = (⊕ i : R ∨ S : F) ⊕ (⊕ i : R ∧ S : F)
  4. (⊕ i : R : F) ⊕ (⊕ i : R : G) = (⊕ : R : F ⊕ G)
  5. (⊕ i : R.i : (⊕ j : S.j : F.i.j)) = (⊕ j : S.j : (⊕ i : R.i : F.i.j))

常用的「分出第n項」是規則 1 和 3 的結果:若已知 n > 0, 我們可把區段 0 ≤ i < n + 1 分為無交集的兩塊 -- 0 ≤ i < ni = n。由規則 3 (左右反轉後)和 1 我們得到:

  (⊕ i : 0 ≤ i < n + 1 : F.i) = (⊕ i : 0 ≤ i < n : F.i) ⊕ F.n

兩個變數的量詞可用一個變數的量詞定義:

   (⊕ i,j : R.i ∧ S.i,j : F.i.j) = (⊕ i : R.i : (⊕ j : S.i.j : F.i.j))

如果 可分配到 中,我們另有這項性質:

   x ⊗ (⊕ i : R : F) = (⊗ i : R : x ⊗ F)

習慣上我們常把 (+ i : R : F) 寫成 (Σ i : R : F).

計算平方和

大家都可猜到第一步是把常數 N 換成變數 n。整個程式會是一個迴圈,我們在不變量中試著維持這樣的關係:

   P  ≣  r = (Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²)

接下來,我們猜想程式中大概會用這樣一個迴圈,每次把 n 遞增,直到 nN 相碰為止:

   { Inv: P ∧ 2 ≤ n ≤ N , Bound: N - n}
   do n ≠ N → ... ; n := n + 1 od

那麼現在要討論的就是如何在 n := n + 1 之前更新 r 的值,使得不變量 P 仍能滿足了。

假設 P2 ≤ n ≤ N 成立,我們把 r 的值之中的 n 代換成 n + 1 試試看:

   (Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²)[n+1 / n]
 = (Σ i,j : 0 ≤ i < j < n + 1 : (a.i - a.j)²)
 =   { split off j = n }
   (Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²) + 
   (Σ i : 0 ≤ i < n : (a.i - a.n)²)
 =   { P }
   r + (Σ i : 0 ≤ i < n : (a.i - a.n)²)


大部分人推導至此,會想用一個內層迴圈算 (Σ i,j : 0 ≤ i < n : (a.i - a.n)²). 但細看這樣寫出的程式,會發現許多計算是重複的。確實,這個式子還可以再拆:

   r + (Σ i : 0 ≤ i < n : (a.i - a.n)²)
 =   { (x - y)² = x² - 2xy + y² }
   r + (Σ i : 0 ≤ i < n : a.i² - 2 × a.i × a.n + a.n²)
 =   { 規則 4 }
   r + (Σ i : 0 ≤ i < n : a.i²) 
     - (Σ i : 0 ≤ i < n : 2 × a.i × a.n) 
     + (Σ i : 0 ≤ i < n : a.n²)
 =   { a.n 已是常數,乘法與加法之分配律 }
   r + (Σ i : 0 ≤ i < n : a.i²) 
     - 2 × (Σ i : 0 ≤ i < n : a.i) × a.n 
     + (Σ i : 0 ≤ i < n : a.n²)
 =   { 化簡最後一項 }
   r + (Σ i : 0 ≤ i < n : a.i²) 
     - 2 × (Σ i : 0 ≤ i < n : a.i) × a.n + n × a.n²

所以我們可另用兩個變數分別儲存 (Σ i : 0 ≤ i < n : a.i²)(Σ i : 0 ≤ i < n : a.i) 的值:

  Q₀  ≣  s = (Σ i : 0 ≤ i < n : a.i²)
  Q₁  ≣  t = (Σ i : 0 ≤ i < n : a.i)

st 兩個變數的更新方式則不難推導出來。最後得到的程式如下:

|[ con N {N ≥ 2}; a : array [0..N) of int;
   var r, s, t, n : int;

   r, s, t, n := (a.0 - a.1)², a.0² + a.1², a.0 + a.1, 2
   { Inv: P ∧ Q₀ ∧ Q₁ ∧ 2 ≤ n ≤ N , Bound: N - n }
 ; do n ≠ N → 
      r := r + s - 2 × t × a.n + n × a.n²;
      s := s + a.n²;
      t := t + a.n;
      n := n + 1 
   od
   { r = (Σ i,j : 0 ≤ i < j < N : (a.i - a.j)²) }
]|

其他解答

大部分(有寫出答案的)同學寫的是兩層迴圈,O(N²) 的程式。少部份導出了上述的 O(N) 程式(很棒唷!)。另有一位同學給了個我沒想到的解:

|[ con N {N ≥ 2}; a : array [0..N) of int;
   var r, i, j : int;

   r, i, j := 0, 0, 0
   { Inv: ... ∧ 0 ≤ i ≤ j ∧ 0 ≤ j ≤ N, Bound: ? }
 ; do j ≠ N →
       if i < j → r := r + (a.i - a.j)²;  i := i + 1
        | i = j → i, j := 0, j + 1
       fi
   od
]|

這仍是一個 O(N²) 的程式,基本上是把兩層 loop 的內層用手動的方式做。但我蠻想看看它的證明。可惜那位同學的程式、給的不變量、和 bound 都有些小瑕疵(可能時間真的不夠吧)。大家想試著證明看看嗎?

Posted in 計算算計 | Tagged , , | 3 Responses

傑出學者系列講座: Euterpea: from Signals to Symphonies

中研院資科所傑出學者系列講座六月份邀請到了函數語言學界有名的 Paul Hudak. Hudak 是 Haskell 語言設計者之一,IFIP Working Group 2.8 (函數編程) 的成員,以及 Journal of Functional Programming 共同總編輯之一。

1992 – 1996 年間他曾在自己的 Jazz 樂團擔任鋼琴手,難怪他很受函數語言初學和入門者喜愛的 The Haskell School of Expression 一書會以音樂、繪圖、動畫為例示範如何以函數語言思考和解決問題。他也是耶魯大學「計算與藝術創意交融(C2 – the Creative Consilience of computing and the arts)」學程創辦人之一。這次他將介紹一個描述電腦音樂的特殊領域語言 Euterpea

  • 主題 : Euterpea: from Signals to Symphonies
  • 主講人 : Dr. Paul Hudak
  • 主講人單位 : Department of Computer Science, Yale University
  • 聯絡人 : 王佩琪小姐, Miss Peichi Wang
  • 地點 : 中央研究院資訊科學研究所 新館106演講廳
  • 時間日期 : 2010/6/25 週五, 10:00~12:00

Euterpea is a new domain-specific language and programming environ- ment for computer music applications, that showcases the use of advanced programming language ideas in its design. It is being developed in the context of Yale’s new C2 Initiative (Creative Consilience of Computing and Arts), and is the only computer music programming environment based on a purely functional programming model.

In this talk we discuss the design rationale for Euterpea, describe its basic functionality, and highlight some of its more innovative features: a vertical language design (from audio signals to symphonic compositions), a separation between structure and interpretation (form and function), a monadic musical user interface (MUI), real-time sound synthesis (using arrows), and the use of functional reactive programming (FRP) in interactive music applications. We also discuss how teaching computer music using Euterpea is an excellent way to teach fundamental principles of pro- gramming, in a fun and rewarding application area.

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

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

FLOLAC 2010 的網站已經做好很久了。之前一直在等所上和台大進修推廣部正式通過。今年請到了、 Yale University 的 Paul Hudak 來演講。課程則聚焦在語意上,對於正式學習程式語言相關知識應會很有用。對了,還送課本一本唷!請大家多幫忙把消息傳出去吧!

2010 Formosan Summer School on Logic, Language, and Computation (FLOLAC ’10)

2010 「邏輯、語言與計算」暑期研習營暨「高等程式語言:語意、分析與工具」暑期課程碩士學分班。

  • 日期: 2010 年六月廿八日(週一)至七月九日(週五)。
  • 時間: 每週一至週五早上九點至下午五點。
  • 地點: 國立台灣大學進修推廣部 2 樓 207 教室(台北市106羅斯福路4段107號)。

宗旨

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

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

本研習營同時為台灣大學進修推廣部「高等程式語言:語意、分析與工具」暑期碩士學分班,研習時數(含考試)共 54 小時。修習結束經考試及格後,授予碩士學分三學分。也歡迎有興趣之社會、業界人士參加。

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

課程與講者

課程 講者
函數編程
Functional Programming
陳恭 Kung Chen
政治大學資訊科學系
特別演講
Special Lecture
Paul Hudak
Yale University
操作語意
Operational Semantics
陳恭 Kung Chen
政治大學資訊科學系
邏輯
Logic
謝邁思 Max Schäfer
Oxford University Computing Laboratory
莊庭瑞 Tyng-Ruey Chuang
中央研究院資訊科學研究所, 台灣大學資訊管理學系
指稱語意
Denotational Semantics
程式建構與推理
Program Construction and Reasoning
穆信成 Shin-Cheng Mu
中央研究院資訊科學研究所
使用 Frama-C: 以整合靜態分析技術驗證 C 程式
Using Frama-C: Collaboration of static analysis techniques towards the verification of C code
Pascal Cuoq
Commissariat à l’Énergie Atomique

主辦單位

中央研究院資訊科學研究所、台灣大學資訊管理學系、政治大學資訊科學系聯合主辦,台灣大學進修推廣部協辦。

課程委員

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

課務統籌

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

報名資訊

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

Posted in 活動消息 | Tagged | 2 Responses

中研院資訊所誠徵 2010 年暑期實習生

來自所上的消息

為鼓勵與學校教授學術交流,本所徵求暑期實習生10名

申請資格:資訊相關科系學生(研究生優先錄取)
工作時間:2010/07/01 ~ 2010/08/31
待遇:每個月新台幣貳萬元整

有興趣者請下載申請表(DOC檔),詳述您的暑期研究題目與內容,然後請您的指導教授簽名後,寄至台北市研究院路2段128號資訊科學研究所王佩琪小姐, Email: peichi@iis.sinica.edu.tw

Posted in 活動消息 | Leave a comment

Charles P. Thacker 獲得 2009 年 Turing 獎

ACM 昨天宣佈 Charles P. Thacker 為 2009 年 Turing 獎得主

Thacker 1967 年於 UC Berkeley 畢業。1974 年 Thacker 在 Xerox PARC (Palo Alto 研究中心) 製作了第一台現代個人電腦 Alto, 具有點陣式螢幕、圖形介面、和最早的所見即所得 (WYSIWYG) 文件編輯器。Thacker 同時也是 Ethernet 的共同發明者之一,直到今日 Ethernet 仍是區域網路的主要協定。

1983 年,Thacker 加入 DEC 並成為系統研究中心 (Systems Research Center) 創始者之一。在 SRC, Thacker 設計了共享記憶體非對稱多處理器工作站 Firefly。1997 年他幫忙創立微軟劍橋研究中心,並監督設計最早的 tablet PC 原型。目前他仍在微軟矽谷從事電腦結構研究。

New York Times 很快地刊出了一篇 Thacker 的專訪

Alto

Alto 技術上接近迷你電腦,但放在桌上、由一個人使用。基於這點,有人認為 Alto 是第一台個人電腦。 Alto 早期的軟體由 BCPL 寫成,後來則用 Mesa, 兩個語言在 PARC 之外都沒有得到廣泛使用。Alto 的鍵盤沒有底線符號,而多了一個表示賦值的左箭頭。有人認為這可能是 CamelCase 這種變數命名習慣的根源。

Alto 上的軟體包括:

  • 最早的所見即所得文件編輯系統 BravoGypsy,
  • email 系統 Laurel 與 Hardy,
  • 用於畫電路與其他技術圖示的矩陣圖像編輯器 Sil,
  • paint 類繪圖軟體的前身 Markup,
  • 最早的 Smalltalk 環境,
  • Interlisp,
  • 最早的多人網路遊戲之一 Alto Trek.

Alto 生產了上千台,但從未成為商業產品。有些機器捐給了大學,政府曾想採購 Alto 但並未談成。後來最有名的發展就是 Steve Jobs 訪問 PARC…

Xerox 經歷過收購 SDS 但經營不善的失敗後,在個人電腦市場上相當保守。整個 70 年代, Xerox 對 PARC 的成果一直興趣缺缺。當 Xerox 終於決定進場, 甚至特別迴避了 Alto 的技術,僅推出了保守的 CP/M 機器 Xerox 820. 等到 Xerox Star 終於出現,卻也為時已晚了。

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

再看二元搜尋法 Binary Search(下)

已知兩整數 M < N 使得 Φ(M,N) 成立。上次我們介紹了 Netty van Gasteren 和 Wim Feijen 的二元搜尋法,能找到某個 l, M ≤ l < N,使得 Φ(l,l+1) 成立。給定一個排序好的陣列 a[0..N)(其元素為 a[0], a[1] ... a[N-1]), 0 ≤ N。如何用 van Gasteren 與 Feijen 的方法判斷其中是否含有某個關鍵值 K 呢?

第一個念頭是用這個 Φ:

Φ(i,j) = a[i] ≤ K < a[j]

並令 M = 0。演算法結束後,Φ(l,l+1) = a[l] ≤ K < a[l+1] 一定成立,只要再看看 a[l] 是否等於 K 就可以了。但問題來了:van Gasteren-Feijen 演算法正確的兩個先決條件之一是 M < N -- van Gasteren-Feijen 演算法的迴圈設計便假設 [M,N) 這個區段不是空的,因此我們無法處理空陣列。其次是 Φ(0,N) 得要成立,但 a[0] ≤ K < a[N] 並不一定成立呢。

我們可以把上述的例外都分開測試。但 van Gasteren 與 Feijen 建議的作法是在陣列頭尾各補一個想像元素:a[-1] 小於任何數,a[N] 大於任何數。一個等價的說法是用這個Φ:

Φ(i,j)  =  (i = -1  ∨  a[i] ≤ K)  ∧  (K < a[j]  ∨  j = N)

最初令 l, r := -1, N, 那麼初始條件就滿足了。程式如下:

  { 0 ≤ N ∧ Φ(-1,N) }
  l, r := -1, N
  { Inv: -1 ≤ l < r ≤ N  ∧  Φ(l,r),   Bound: r - l }
; do l+1 ≠ r →
    { l + 2 < r }
    m := (l + r) / 2
  ; if a[m] ≤ K → l := m
    [] K < a[m] → r := m
    fi
  od
  { -1 ≤ l < N  ∧  Φ(l,l+1) }
; if l > -1 → found := a[l] = K
  [] l = -1 → found := false
  fi

如果在陣列頭尾補元素讓你覺得很不妥,別擔心。迴圈不變量保證了 -1 < m < N,因此從頭到尾,a[-1]a[N] 兩個位置都沒被讀過 -- 陣列 a 並不用真正有什麼改變,兩個想像元素只是為了證明演算法正確而假想出來的。這也讓我們可以處理空陣列了。我覺得這是 van Gasteren-Feijen 演算法漂亮之處。

Bentley 的程式

Jon Bentley 在 Programming Pearls 一書中給的二元搜尋法程式如果翻譯成 guarded command language, 並把陣列索引從 [1..N] 改成 [0..N-1], 大約是這樣:

  l, r := 0, N-1
; do l ≤ r →
    m := (l + r) / 2
  ; if a[m] < K → l := m + 1
    [] a[m] = K → found := true; break
    [] K < a[m] → r := m - 1
    fi
  od
; found := false

Bentley 書中也有以口語描述的正確性證明。我原想在課堂上講解這個程式,畢竟這個版本流傳較廣 -- 許多函式庫裡的二元搜尋法程式就是這麼寫的。但困難之一是若要把 K < a[m]r := m - 1 牽上關係,似乎非得提早用上陣列已排序好的性質。這個演算法便比較難在更廣泛的脈絡中解釋了。當然,另一個困難是我不知如何在 Hoare logic 中簡單地解釋 break

乍看之下我以為 Bentley 演算法的搜尋範圍縮小得比 van Gasteren-Feijen 快:lr 分別設為 m+1m-1,並不是 m. 細看之後又發現並不盡然。變數 l 可設為 m+1, 因為 m 的位置已由另一個比較 a[m] = K 處理;變數 r 設為 m-1,則可能僅因為 Bentley 將陣列區段用 a[l..r-1] 表示,而 van Gasteren-Feijen 演算法把同一個區段表達為 a[l..r).

Bentley 與 van Gasteren-Feijen 演算法解的是問題並不完全相同。當 K 在陣列中出現一次以上,Bentley 演算法不限定傳回哪個,van Gasteren-Feijen 則必定傳回索引最大的那個。當 K 不在陣列中時,van Gasteren-Feijen 演算法似乎較快,因為兩者都得跑完,而 van Gasteren-Feijen 的迴圈中只有一個比較(最後一個比較可省去)。Bentley 演算法若提早發現 K 可隨時跳出迴圈,代價是迴圈中多了一個比較。當陣列中確實找得到 K, 這樣的交換是否值得呢?Timothy J. Rolfe 的實驗似乎認為只用一個比較的演算法平均上仍快一些。

習題

Van Gasteren 與 Feijen 建議的幾個習題中包括這個:假設陣列 a[0..N) 是一串嚴格遞增的數字緊接著一串嚴格遞減的數字,試用二元搜尋法找到陣列中的最大值。本問題中我覺得合理的假設是遞增和遞減數列均可能為空的,但 a 至少有一個元素:

0 < N ⋀
(∃ M: 0 ≤ M < N :
  (∀ i,j : 0 ≤ i < j ≤ M : a[i] < a[j]) ⋀
  (∀ i,j : M ≤ i < j < N : a[i] > a[j]))

這剛好是「最大密度區段」問題的演算法之一需要的一個副程式。我記得當時也是先隨便寫寫,幾次寫不對才發現真是難。現在總算是知道一點理論背景,覺得安心多了。你要試試看嗎?

中間索引怎麼取?

關於中間值 m := (l+r)/2, 後來另有些其他故事。Google 的 Joshua Bloch 發現當陣列夠大時,lr 相加可能造成溢位。他可不是故意挑毛病,這個 "bug" 是 Sun 抓到的。他建議該這麼寫:

int m = l + ((r - l) / 2);                          /* for Java/C/C++ */
int m = (l + r) >>> 1;                              /* for Java */
m = ((unsigned int)l + (unsigned int)r)) >> 1;      /* for C/C++ */

Bloch 的發現自然引起了不少討論。有人認為這是整數型別的問題,而不是二元搜尋法的 bug. 有人質疑,討論 int 無法索引的陣列是否有意義?接下來可能一路談到組合語言定址法上頭。有人說,要造成索引溢位,陣列得有 4GB 大,你這輩子在 4GB 的陣列中作二元搜尋過嗎?有人便答,人家可是 Google 來的。Google 的陣列比常人的大上幾倍也不是不可能的唷。

如果往抽象的極端走,Roland Backhouse 在 Program Construction: Calculating Implementations from Specifications 書中則建議應該用 m := (l + r - 1) / 2 -- 如此一來不管該語言的整數除法到底是無條件消去、四捨五入、或是無條件進入,算出來的 m 值都會是 ⌊(l + r)/2⌋.

參考資料

Posted in 計算算計 | Tagged , | 1 Response

再看二元搜尋法 Binary Search(上)

如果你自認對二元搜尋(binary search, 大陸譯作折半搜索) 夠熟悉了,卻沒讀過 Netty van Gasteren 和 Wim Feijen 的研究筆記 The Binary Search Revisited, 強烈建議你找時間看看。

最近為了今夏的 FLOLAC 研習營開始找些資料。為了教些離開研習營後仍有用的東西,今年我想教 Hoare 邏輯與 Dijkstra 使用最弱前提(weakest precondition) 的程式建構法。對想寫好程式的人來說,這應是基礎知識,但大家對這些題目卻陌生得令人驚訝。

二元搜尋似乎是個該談到的例子:給一個排序好、長度為 N 的陣列,在 O(log N) 的時間內決定其中是否有某個值。資訊系學生在演算法課上一定學過二元搜尋。身經百戰的程式員寫個二元搜尋程式應該也不是難事吧?然而 Jon Bentley 在他有名的 Programming Pearls 一書中卻提到只有大約一成的專業程式員能第一次把這程式寫對。這一定要親身試試看才會相信。我抱著警覺心試了一次,寫了一個應該正確(畢竟我對這套方法算是比較熟了),但不怎麼漂亮的程式。請朋友寫寫看,也果然出現了一些常見的 bug. 看來這確實是個程式設計課堂上該講的好例子。

迴圈、不變量、與界限

Van Gasteren 和 Feijen 在一篇 1995 年的研究筆記中釐清了大家常有的一個迷思:你認為你對二元搜尋很了解嗎?那您可知道,二元搜尋其實並不一定要用在排序好的陣列上?事實上,他們認為總是把二元搜尋類比為翻字典找字,反倒造成了一個教學盲點。

Van Gasteren 和 Feijen 先試解一個更廣的問題:給定整數 MN, 和一個接受兩個整數參數的布林函數 Φ,已知 M < N,並知 Φ(M,N) 成立。Φ 另需滿足一些條件,待會兒再談。試寫一個程式,找兩個介於 MN 之間、滿足 Φ 的相鄰整數。若寫成邏輯式子,程式執行完畢後需滿足:

M ≤ l < N   ∧   Φ(l,l+1)

這是 Van Gasteren 和 Feijen 的程式:

  { M < N ∧ Φ(M,N) }
  l, r := M, N
  { Inv: M ≤ l < r ≤ N  ∧  Φ(l,r),   Bound: r - l }
; do l+1 ≠ r →
    { l + 2 < r }
    m := (l + r) / 2
  ; if Φ(m,r) → l := m
    [] Φ(l,m) → r := m
    fi
  od
  { M ≤ l < N  ∧  Φ(l,l+1) }

這裡的虛擬碼使用的是 Dijkstra 的 Guarded Command Language。多個變數可同時設值(如 l, r := M, N),do 相當於 while 迴圈。條件判斷 if 和一般程式語言不同之處是若不只一個條件成立,程式可任選一個分支執行。註解依照 Algol 系語言的傳統用大括號,但此處我們也把註解視作斷言 (assertion), 表示程式執行到此處一定會成立的條件。這是給人看的資訊,也是我們藉以證明程式正確的重要線索。

證明迴圈正確性的兩大關鍵是其不變量 (loop invariant)界限 (bound)。本程式只有一個迴圈,不變量和界限註記在這一行:

{ Inv: M ≤ l < r ≤ N  ∧  Φ(l,r),   Bound: r - l }

「不變量」事實上並不是一個「量」,而是程式每次執行到迴圈進入點前必定會滿足的條件。此處不變量為 M ≤ l < r ≤ NΦ(l,r)。變數 lr 的初始值分別是 MN. 依照假設,M = l < r = NΦ(l,r) = Φ(M,N) 確實成立。因此第一次執行到迴圈之前,不變量確實是滿足的。

迴圈的進入條件是 l+1 ≠ r,和不變量中的 l < r 合起來看,意思是 lr 不是相鄰的整數。因此m := (l + r) / 2 執行後,m 必定在 lr 之間,但不等於 lr。接下來的 if 敘述中,變數 l 會被設成 m 的先決條件是 Φ(m,r),變數 r 會被設成 m 的先決條件是 Φ(l,m)。不論是哪種情形,執行完 if 敘述後,Φ(l,r) 一定還是成立。所以再回到迴圈開頭時,不變量仍被滿足。

長此以往,直到有一天剛好 l+1 ≠ r 不成立了,也就是說 lr 已是相鄰的整數,和不變量合起來看,剛好我們要的 結束條件 M ≤ l < N ∧ Φ(l,l+1) 就被滿足了!

只是還有兩個但書:首先,if 敘述中的 Φ(m,r)Φ(l,m) 這兩個條件至少要有一個成立。這是 Φ 的另一個要求:

 Φ(l,r)  ∧  l < m < r   ⇒   Φ(l,m)  ∨  Φ(m,r)(*)

其次,我們怎知道迴圈會有停下來的一天呢?這就是「界限」 r-l 處理的部份。由於 M < N, 我們知道 r-l 最初會是一個正整數。而如前所述,每次進入迴圈後,m 的值必定在 lr 之間,但不等於 lr。因此迴圈每執行一次,r-l 就變小一些。當 r-l 等於一時,迴圈就得停了。因此我們知道這迴圈不可能永遠執行下去。

以上便是該程式正確的大略證明。我們只是用中文說說,更仔細的證明是應該要有些數學演算的。關於什麼算是證明、為何要有「形式」證明,希望以後有機會寫寫看。

有哪些函數 Φ 滿足條件 (*) 呢? Van Gasteren 與 Feijen 舉的例子包括:

  • Φ(i,j) = a[i] ≠ a[j],此處 a[M..N] 是某陣列。程式會幫我們找到兩個相鄰但不相等的元素。Van Gasteren 與 Feijen 認為這個特例可能是解說二元搜尋比較合適的例子。
  • Φ(i,j) = a[i] × a[j] ≤ 0, 程式將找到兩個相鄰但正負號不相等,或至少有一個為零的元素。
  • Φ(i,j) = a[i] < a[j],
  • Φ(i,j) = a[i] ∨ a[j], 等等。

再回到最初的問題:怎麼在排序好的陣列中找某個關鍵值呢?理想上我們希望設計某個 Φ,然後套用上面的程式。先賣個關子,下回分解。 🙂

參考資料

Posted in 計算算計 | Tagged , | 3 Responses

演算邏輯 Calculational Logic(二)騎士與惡棍之島

一個島上住著兩種人,騎士 (knight) 與惡棍 (knave) 。騎士總說實話,惡棍總說謊話,但從外表看不出誰是騎士或惡棍。某天,居民 A 和你說「B 剛剛說他自己是騎士」。由此你可知道 A 說的是實話還是謊話嗎?B 呢?傳說島上藏著金子,怎麼設計一個問題,查出傳言的真假呢?

只要有耐心把各種狀況列出來作分析,這類邏輯問題總是可以找到解答的。既然演算邏輯號稱是為了應用設計的邏輯,以演算邏輯的眼光看這種問題,是否比較好解呢?

上次我們談到 這個運算元,知道它滿足交換律和結合律,是演算邏輯最基礎的運算元。在談騎士與惡棍問題之前,我們得先提另一條規則:

[const. true] true ≡ p ≡ p

如果讀解成 true ≡ (p ≡ p), 意思是 也滿足同一律:任何值都等於自己。如果讀解成 (true ≡ p) ≡ p,則是強調 true 的單位元素。

騎士與惡棍

我們將「A 是騎士」簡寫成 A. 如果 A 說了某個陳述 S, 我們無法知道 S 是否成立,但我們知道

A ≡ S

如果 A 是騎士,S 便是真的;如果 A 是惡棍,S便是假的。

假設我們問 A:「你是騎士嗎?」A 回答「是的。」這可以記成 A ≡ A. 然而,根據 [const. true] 規則,A ≡ A 可以化簡為 true. 意思是,在這個島上不管你問誰「你是騎士嗎」,對方都會回答是。

如果 A 說:「B 是騎士」呢? 這可以記成 A ≡ B. 我們仍不知道 B 到底是騎士還是惡棍,但我們可以知道 AB 是同一種人。

如果 A 說:「我和 B 是同一種人」呢?這可記成 A ≡ (A ≡ B)。我們算算看:

  A ≡ (A ≡ B)
=   { 結合律 }
  (A ≡ A) ≡ B
=   { [const. true] }
  true ≡ B
=   { [const. true] }
  B

啊,所以我們雖仍不知道 A 到底是騎士還是惡棍,卻可以知道 B 一定是騎士!

若不用演算邏輯,一般人的推理方式可能是把 A是騎士或惡棍、B是騎士或惡棍的四種可能性一一嘗試。由此我們可以體會到 Gries 所說「演算邏輯為解決問題而設計」的意思 — 利用 的性質,讓一個式子盛載多重的意義,因此我們可同時處理好幾種狀況,讓推理相當精簡迅速。當然,前提是要對邏輯規則夠熟練。

所以,要怎麼想出一個問題問 A,用來判斷島上到底有沒有金子呢?經過剛剛的討論,讀者也許已經可以猜得出來。但 Backhouse 建議我們避免瞎猜。我們應該用代數解未知數的方式把問題推演出來。把「島上有金子」這個命題記為 G. 我們希望問某個問題 Q, 如果 A 回答「是」,就表示島上有金子,反之則否:

  • 「A 對問題 Q 回答『是』」記為 A ≡ Q
  • 「A 對問題 Q 回答『是』,島上便有金子」應該是一個若且唯若的命題,寫成 G ≡ (A ≡ Q)

而根據交換律和結合律,G ≡ (A ≡ Q) 就是 Q ≡ (G ≡ A)。我們要問 A 的問題就是 G ≡ A:「『島上有金子』和『你是騎士』是不是等價的呢?」?

希望這個島上不論騎士或惡棍,邏輯都蠻不錯的,才聽得懂這種問題囉!

否定運算元

以上的討論只用了三條規則:交換律、結合律、和[const. true]. 結束本篇之前,我們再看一條關於false 與「否定」運算元 ¬ 的規則:

[negation] ¬p ≡ p ≡ false

把括號放在後面,¬p ≡ (p ≡ false)¬ 的定義;若讀解成 (¬p ≡ p) ≡ false,這條規則讓我們把算式中看到的 p¬p 兩兩消去成 false.

方才我們把「A 是騎士」記為 A,「A 是惡棍」自然是 ¬A 了。以下的練習除 3. 以外皆取自 Backhouse 的書。

  1. A 說:「我和 B 是不同種的。」由此我們可推導出什麼關於 AB 的資訊呢?
  2. 用上述的做法,推導出一個問題問A ,若 A 回答「是」,我們可得知 AB 真的不同種類。
  3. A 說:「B 說他是騎士。」由此我們可以得知什麼關於 AB 的訊息?如果 A 說:「B 說他是惡棍」呢?
  4. 試證明 ¬(p ≡ q) = (p ≡ ¬q)

參考資料

本文內容皆來自 Roland BackhouseProgram Construction: Calculating Implementations from Specifications 第五章。

Posted in 計算算計 | Tagged | 7 Responses