2007年3月30日 星期五

Haskell:The craft of functional

書藉基本資料: Haskell:The craft of functional

之前問大中,如果要玩functinoal language,比較推薦那一種?於是大中推薦我看這本學Haskell,浩然只有第一版,只好將就看了。

目前看完Part I Basic Functional Programming,目的是掌握functional language的思維,沒打算實際寫些什麼。2345章順著下來,一章介紹語法,下一章就介紹如何證明程式的性質(reasoning the programs, reasoning the lists),例子淺顯易懂,跟著書裡的範例思考,總算明白證明程式是怎麼一回事。

學PL的人應該會用更嚴僅無誤的方式說明,我針對我的認知說明「證明程式」是怎麼一回事。functional language沒有for, while這些”syntactic sugar”,只有if,剩下的邏輯控制都用遞迴搞定。這樣設計的結果,至少看起來和數學最為接近,程式本身就是數學式子的組合,舉例來說,對函數max(a, b)來說,數學上可以證明max(a, b)有以下的特性:

max(a, b) >= a, for any a max(a, b) >= b, for any b

只要分項討論a >= b和a < b兩個情況,就能證明上面這個性質。換成Haskell的情況,只是用Haskell的語法表示max(a, b),證明推導的過程就用Haskell的語法表示,而不是數學式子。稍微複雜一點的,可以變成對max(L),L為一list [A1,A2, A3, …, An],證明:

max([A1, A2, …, An]) >= max([A1, A2, …, An-1]) >= max([A1, A2, …, An-2]) >= … >= max([A1])

或是

n*max([A1, A2, ..., An]) >= sum_up([A1, A2, ..., An])

其中sum_up(L)表示將list L的內容加總。由於控制流程只有if和遞迴,if 的情況就是分項討論,遞迴可以用數學歸納法。能證明程式性質的話,有機會進一步驗證程式的正確性,比方證明reverse(reverse(L)) = L,或是明白各段程式一定在那些值域內,找出控制語意上的錯誤,像是函數的有效輸入範圍是正數,但輸入的參數值域卻一定是負數。

做為了解程式證明的開始,看這本書頗輕鬆愉快的。

沒有留言:

張貼留言