ML程序設(shè)計(jì)教程

出版時(shí)間：2005-5 出版社：機(jī)械工業(yè) 作者：保羅森頁數(shù)：366 譯者：柯韋
Tag標(biāo)簽：無

內(nèi)容概要

　　本書詳細(xì)講解如何使用ML語言進(jìn)行程序設(shè)計(jì)，并介紹函數(shù)式程序設(shè)計(jì)的基本原理。書中特別講述了為ML的修訂版所設(shè)計(jì)的新標(biāo)準(zhǔn)庫的主要特性，并且給出大量例子，涵蓋排序、矩陣運(yùn)算、多項(xiàng)式運(yùn)算等方面。大型的例子包括一個(gè)一般性的自頂向下語法分析器、一個(gè)l-演算歸約程序和一個(gè)定理證明機(jī)。書中也講述了關(guān)于數(shù)組、隊(duì)列、優(yōu)先隊(duì)列等高效的函數(shù)式實(shí)現(xiàn)，并且有一章專門討論函數(shù)式程序的形式論證?！　”緯勺鳛楦叩仍盒Ｓ?jì)算機(jī)專業(yè)相關(guān)課程的教材，也適合廣大程序設(shè)計(jì)人員參考。

作者簡介

作者：（英國）保羅森 譯者：柯韋Lawrence C.Paulson，于1981年在美國斯坦福大學(xué)獲得計(jì)算機(jī)科學(xué)博士學(xué)位，現(xiàn)為英國劍橋大學(xué)計(jì)算邏輯學(xué)教授。Paulson博士從事有關(guān)ML語言的教學(xué)和工作多年，擁有扎實(shí)的背景和豐富的經(jīng)驗(yàn)，并曾經(jīng)參與Standard ML的設(shè)計(jì)。Paulson博士開發(fā)和維護(hù)了lsabelle自動(dòng)定理證明系統(tǒng)，他近期正在進(jìn)行關(guān)于自動(dòng)定理證明和密碼協(xié)議驗(yàn)證方面的研究。

書籍目錄

第1章 Standard ML 函數(shù)式程序設(shè)計(jì) Standard ML概述 第2章 名字、函數(shù)和類型 本章提要 值的聲明 數(shù)、字符串和真值 序偶、元組和記錄 表達(dá)式的求值 書寫遞歸函數(shù) 局部聲明 模塊系統(tǒng)初步 多態(tài)類型檢測(cè) 要點(diǎn)小結(jié) 第3章 表 本章提要 表的簡介 基本的表函數(shù) 表的應(yīng)用 多態(tài)函數(shù)中的相等測(cè)試 排序：案例研究 多項(xiàng)式算術(shù) 要點(diǎn)小結(jié) 第4章 樹和具體數(shù)據(jù) 本章提要 數(shù)據(jù)類型聲明 異常 樹 基于樹的數(shù)據(jù)結(jié)構(gòu) 重言式檢測(cè)器 要點(diǎn)小結(jié) 第5章 函數(shù)和無數(shù)據(jù) 本章提要 作為值的函數(shù) 通用算子 序列，或無窮表 搜索策略和無窮表 要點(diǎn)小結(jié) 第6章 函數(shù)式程序的論證 本章提要 一些數(shù)學(xué)證明的原理 結(jié)構(gòu)歸納法 一般性歸納原理 描述和驗(yàn)證 要點(diǎn)小結(jié) 第7章 抽象類型和函子 本章提要 隊(duì)列的三種表示方法 簽名和抽象 函子 利用模塊建立大型系統(tǒng) 模塊參考指南 要點(diǎn)小結(jié) 第8章 ML中的命令式程序設(shè)計(jì) 本章提要 引用類型 數(shù)據(jù)結(jié)構(gòu)中的引 輸入和輸出 要點(diǎn)小結(jié) 第9章 書寫l-演算的解釋器 本章提要 函數(shù)式語法分析器 l-演算簡介 在ML中表示l-項(xiàng) 作為程序設(shè)計(jì)語言的l-演算 要點(diǎn)小結(jié) 第10章 策略定理證明機(jī) 本章提要 一階邏輯的相繼式演算 在ML中處理項(xiàng)和公式 策略和證明狀態(tài) 搜索證明 要點(diǎn)小結(jié) 項(xiàng)目建議 參考文獻(xiàn) Standard ML語法圖 語法圖中英詞匯對(duì)照表 索引 預(yù)定義標(biāo)識(shí)符

媒體關(guān)注與評(píng)論

書評(píng)本書是關(guān)于ML程序設(shè)計(jì)的經(jīng)典教材，詳細(xì)介紹如何使用 ML語言進(jìn)行程序設(shè)計(jì)，并講解函數(shù)式程序設(shè)計(jì)的基本原理。    書中含有大量例子，涵蓋了排序、矩陣運(yùn)算、多項(xiàng)式運(yùn)算等方面。大型的例子包括一個(gè)一般性的自頂向下語法分析器、一個(gè)一演算歸約程序和一個(gè)定理證明機(jī)。書中也講述了關(guān)于數(shù)組、隊(duì)列、優(yōu)生隊(duì)列等高效的函數(shù)式實(shí)現(xiàn)，并且有一章專門討論函數(shù)式程序的形式論證。本書的代碼均可以從作者網(wǎng)站（http://www.cl.cam.ac.uk/users/lcp/）得到。

編輯推薦

　　本書是關(guān)于ML程序設(shè)計(jì)的經(jīng)典教材，詳細(xì)介紹如何使用 ML語言進(jìn)行程序設(shè)計(jì)，并講解函數(shù)式程序設(shè)計(jì)的基本原理。　　書中含有大量例子，涵蓋了排序、矩陣運(yùn)算、多項(xiàng)式運(yùn)算等方面。大型的例子包括一個(gè)一般性的自頂向下語法分析器、一個(gè)一演算歸約程序和一個(gè)定理證明機(jī)。書中也講述了關(guān)于數(shù)組、隊(duì)列、優(yōu)生隊(duì)列等高效的函數(shù)式實(shí)現(xiàn)，并且有一章專門討論函數(shù)式程序的形式論證。本書的代碼均可以從作者網(wǎng)站（http://www.cl.cam.ac.uk/users/lcp/）得到?！　”緯敿?xì)講解如何使用ML語言進(jìn)行程序設(shè)計(jì)，并介紹函數(shù)式程序設(shè)計(jì)的基本原理。書中特別講述了為ML的修訂版所設(shè)計(jì)的新標(biāo)準(zhǔn)庫的主要特性，并且給出大量例子，涵蓋排序、矩陣運(yùn)算、多項(xiàng)式運(yùn)算等方面。大型的例子包括一個(gè)一般性的自頂向下語法分析器、一個(gè)l-演算歸約程序和一個(gè)定理證明機(jī)。書中也講述了關(guān)于數(shù)組、隊(duì)列、優(yōu)先隊(duì)列等高效的函數(shù)式實(shí)現(xiàn)，并且有一章專門討論函數(shù)式程序的形式論證?！　”緯勺鳛楦叩仍盒Ｓ?jì)算機(jī)專業(yè)相關(guān)課程的教材，也適合廣大程序設(shè)計(jì)人員參考。

圖書封面

圖書標(biāo)簽Tags

無

評(píng)論、評(píng)分、閱讀與下載

還沒讀過(14)
勉強(qiáng)可看(102)
一般般(175)
內(nèi)容豐富(7262)
強(qiáng)力推薦(595)

ML程序設(shè)計(jì)教程 PDF格式下載

用戶評(píng)論 (總計(jì)10條)

這是國內(nèi)少有的專門講FPL的書籍。盡管現(xiàn)在FP在工業(yè)、商業(yè)上用得不多，而ML用得更少，但是FPL確實(shí)給編程提供了一些非常好的理念和思路。這本書本身也寫得不錯(cuò)，翻譯也還行。
　　這本書適合沒有接觸過functional programming的同學(xué)，也適合沒有學(xué)過編程的同學(xué)。作者顯然不滿足于寫一個(gè)語言教程，而是著重于灌輸fp知識(shí)。
　　
　　所以在我看來這本書的廢話稍微多了些。好幾次我迅速的向后跳，但有意思的是每次我都被迫backtracing。因?yàn)樗?jīng)常引用之前的例子和作業(yè)。后來我終于明白，要么就拋開這本書，要么老實(shí)的把每個(gè)例子每個(gè)作業(yè)都做了。現(xiàn)在我開始從頭做作業(yè)了。做SML的作業(yè)全得靠紙筆。計(jì)算機(jī)只能幫你驗(yàn)證最后結(jié)果。很無奈但也挺有趣。
　　
　　要學(xué)SML不一定要讀這本書。Robert Harper那本不錯(cuò)，而且是免費(fèi)的。但這本書有自己獨(dú)特的味道，仔細(xì)讀一遍還是挺有意思的。
　　如果以前沒有接觸過FP，比如徹底的C/匯編程序員，看這本書能慢慢建立一些不同的編程模式；
　　如果已經(jīng)對(duì)haskell或者其他的FPL有一些了解，看這本書可能會(huì)嫌啰嗦了，可以去看看<<Programming in Standard ML>>，內(nèi)容不算很完整，不過要點(diǎn)都到了。
　　建議先看SICP，再看這本書，首先LISP語法比較簡單，其次這本書會(huì)經(jīng)常拿ML跟LISP做對(duì)比。
　　SICP在大的方向上比較清晰，章節(jié)安排上更注重思想的延伸；而這本書的確如書名一樣，ML的教程，從簡單的類型，表，樹到匿名函數(shù)無窮表，抽象類型，章節(jié)安排完全是學(xué)習(xí)語言的順序。這樣造成不同深度的主題安排的比較散亂，像剛剛開始就講解傳值調(diào)用，傳需調(diào)用，惰性求值，動(dòng)態(tài)類型檢測(cè)的相關(guān)內(nèi)容。
　　還有一些細(xì)節(jié)問題，這本書要比SICP更深入一些。比方說第7章詳細(xì)討論了隊(duì)列的實(shí)現(xiàn)，最終給出了一個(gè)進(jìn)隊(duì)出隊(duì)都是O（1）的實(shí)現(xiàn)方式，雖然很簡單，但SICP也應(yīng)該說明一下。以及第九章實(shí)現(xiàn)了一個(gè)解釋器，可以跟SICP相互對(duì)照。
　　ML意味著meta language, 本書是學(xué)習(xí)ML排名第一的課本.
　　
　　英文標(biāo)題信息是這樣的:
　　PAULSON, LAWRENCE C. (Univ. of Cambridge, Cambridge, UK)
　　ML for the working programmer (2nd ed.).
　　Cambridge University Press, New York, NY, 1996,
　　478 pp., $32.95, ISBN 0-521-56543-X.
　　
　　這里要強(qiáng)調(diào)1996的是,現(xiàn)在流行的ML的編譯器,都是按ML '97標(biāo)準(zhǔn)的.但我沒有看出這本書有什么不合適的地方. 這個(gè)問題我也想請(qǐng)專家指教. 中文版寫的原版的出版日期是2001,這是我比較有疑問的.
　　
　　還有,這本書稱為working,也是很有意思的. 因?yàn)?很多人都有疑問,函數(shù)式程序設(shè)計(jì)語言,有可以working的嗎?作者顯然是要寫一本可以working的書. 我想,這是本書最大的特點(diǎn). 這個(gè)特點(diǎn)帶來了兩個(gè)后果,一好一壞.
　　
　　我們先談壞的一方面.命令式程序設(shè)計(jì)語言及其相關(guān)書籍看過不少,LISP也簡單看過,但還是不得不說,ML是我看起來覺得最難的書.這應(yīng)該是作者要寫working的ML付出的代價(jià). ML雖然也working,但有其working的領(lǐng)域,主要還是定理證明機(jī),就像最初設(shè)計(jì)ML的動(dòng)機(jī)所指示的. 因?yàn)?這本書有很多章節(jié)與此有關(guān),而這并不是一個(gè)大多數(shù)讀者熟悉的領(lǐng)域,所以,大多數(shù)讀者應(yīng)該與我一樣,會(huì)覺得這本書可能是很難讀的.
　　
　　好的方面,如果你讀完了這本書,并且按要求完成了練習(xí),不僅學(xué)會(huì)了ML語言,而且也學(xué)會(huì)了一個(gè)ML working的領(lǐng)域,定理證明機(jī).
　　
　　我學(xué)這本書是讀到第4章最后重言式檢測(cè)器時(shí),才找到感覺的.
　　關(guān)于重言式檢測(cè)的手工做法,我有過討論:
　　http://www.douban.com/group/topic/1192440/
　　我沒有動(dòng)手去寫一個(gè)計(jì)算機(jī)程序,是因?yàn)檫@覺得這有一點(diǎn)難. 而在這本書有一個(gè)例子,50行以下的代碼. 也許一個(gè)更完善的一點(diǎn)的程序還需要能讀入一個(gè)重言式,這大概要增加一兩百行代碼. 正是這不到50行的代碼給了我定理證明的感覺,ML working的感覺.
　　
　　本書共9章,第6章是數(shù)學(xué),第8和9章是例子,而要讀完第4章才能找到點(diǎn)感覺,可以說明,這本書真的不很容易讀.
　　
　　雖然也有人用ML寫web應(yīng)用,或者別的什么應(yīng)用,但我們學(xué)ML真的是為了要寫一個(gè)ERP或CRM或一個(gè)操作系統(tǒng)嗎?如果不是想了解一些邏輯或證明的東西,我們會(huì)學(xué)ML嗎? 所以,綜合考慮, 這本書的確是學(xué)習(xí)ML的第一本教材.
　　
　　我還沒學(xué)好ML,所以這個(gè)書評(píng)也寫得特別膽小委瑣,非常慚愧.
難道你專業(yè)不是CS的？...學(xué)語言而一個(gè)程序也不寫是很離奇的（差不多和學(xué)英語只是看牛津語法然后不肯造個(gè)英文句子一樣），是因?yàn)闆]有編程經(jīng)驗(yàn)？SML的編譯器并不難找到...
在學(xué)ML，感覺這本書翻譯的比較爛。。。有機(jī)會(huì)一定借原版看看
對(duì)不起,我很邪惡,我以為是Make Love...
樓上，其實(shí)作者也說他因?yàn)闀艿讲簧倮_……
ML在程序驗(yàn)證方面的應(yīng)用還是很有用的
據(jù)說，僅僅是據(jù)說，國外的一些公司已經(jīng)開始用ML類的語言寫驗(yàn)證程序了

ML程序設(shè)計(jì)教程

用戶評(píng)論 (總計(jì)10條)

推薦圖書

相關(guān)圖書