ML程序設(shè)計(jì)教程（原書第2版）

　　本書是關(guān)于ML程序設(shè)計(jì)的經(jīng)典教材，詳細(xì)介紹如何使用ML語(yǔ)言進(jìn)行程序設(shè)計(jì)，并講解函數(shù)式程序設(shè)計(jì)的基本原理。書中含有大量例子，涵蓋了排序、矩陣運(yùn)算、多項(xiàng)式運(yùn)算等方面。大型的例子包括一個(gè)一般性的自頂向下語(yǔ)法分析器、一個(gè)一演算歸約程序和一個(gè)定理證明機(jī)。書中也講述了關(guān)于數(shù)組、隊(duì)列、優(yōu)生隊(duì)列等高效的函數(shù)式實(shí)現(xiàn)，并且有一章專門討論函數(shù)式程序的形式論證。本書詳細(xì)講解如何使用ML語(yǔ)言進(jìn)行程序設(shè)計(jì)，并介紹函數(shù)式程序設(shè)計(jì)的基本原理。書中特別講述了為ML的修訂版所設(shè)計(jì)的新標(biāo)準(zhǔn)庫(kù)的主要特性，并且給出大量例子，涵蓋排序、矩陣運(yùn)算、多項(xiàng)式運(yùn)算等方面。大型的例子包括一個(gè)一般性的自頂向下語(yǔ)法分析器、一個(gè)l-演算歸約程序和一個(gè)定理證明機(jī)。書中也講述了關(guān)于數(shù)組、隊(duì)列、優(yōu)先隊(duì)列等高效的函數(shù)式實(shí)現(xiàn)，并且有一章專門討論函數(shù)式程序的形式論證。本書可作為高等院校計(jì)算機(jī)專業(yè)相關(guān)課程的教材，也適合廣大程序設(shè)計(jì)人員參考。本書前言前言：本書源于對(duì)StandardML和函數(shù)式程序設(shè)計(jì)的講稿。它仍可以作為函數(shù)式程序設(shè)計(jì)的課本—一本面向?qū)嵱?，而不是?biāo)準(zhǔn)的、理想化的書—然而，它主要是一本有效使用ML的指南。它甚至討論了ML的命令式特性。有些內(nèi)容需要離散數(shù)學(xué)的知識(shí)，例如初等邏輯和集合論。讀者會(huì)發(fā)現(xiàn)以往的程序設(shè)計(jì)經(jīng)驗(yàn)是有用的，但不是必需的。本書是一本程序設(shè)計(jì)手冊(cè)，而不是參考手冊(cè)。它覆蓋了ML的主要方面，但并不盡述所有的細(xì)節(jié)。它在理論原理上花費(fèi)了一些篇幅，但主要還是關(guān)心高效的算法和實(shí)際的程序設(shè)計(jì)。本書的組織反映了我的教學(xué)經(jīng)驗(yàn)。高階函數(shù)出現(xiàn)得較晚，在第5章講述。慣常的做法是在一開始就介紹一些不甚自然的例子，這樣做只能使學(xué)生們感到困惑。高階函數(shù)的概念是不容易理解的，需要充分的預(yù)備知識(shí)。所以，本書從基本類型、表和樹開始講述。當(dāng)講到高階函數(shù)時(shí)，很多相關(guān)的例子已經(jīng)是現(xiàn)成的了。練習(xí)的難度相差很大。它們不是用來評(píng)測(cè)學(xué)生的，而是為了提供實(shí)踐機(jī)會(huì)，拓展內(nèi)容和激發(fā)討論的。本書一覽。大多數(shù)章節(jié)都專注于ML的各個(gè)方面。第1章介紹了函數(shù)式程序設(shè)計(jì)的背景思想，以及ML的歷史概況。第2～5章涵蓋了ML的函數(shù)式部分，包括對(duì)模塊的簡(jiǎn)介。講述了基本類型、表、樹和高階函數(shù)。對(duì)函數(shù)式程序設(shè)計(jì)的更廣泛的原理也有所討論。第6章給出了論證函數(shù)式程序的形式方法。看上去似乎偏離了程序設(shè)計(jì)的主題，然而錯(cuò)誤的程序是沒用的。易于形式論證是函數(shù)式程序設(shè)計(jì)的一大好處。第7章詳細(xì)講述了模塊，包括函子（帶參數(shù)的模塊）。第8章講述了ML的命令式特性：引用、數(shù)組和輸入輸出。本書的其余部分由較大的例子構(gòu)成。第9章給出了函數(shù)式的語(yǔ)法分析器和一個(gè)l-演算解釋器。第10章給出了一個(gè)定理證明機(jī)，這是ML的傳統(tǒng)應(yīng)用。書中的例子非常豐富。其中一些只是為了說明ML的某個(gè)方面，但大多數(shù)本身就有一定用途—排序、函數(shù)式數(shù)組、優(yōu)先隊(duì)列、搜索算法、美化打印。請(qǐng)注意：雖然我測(cè)試過這些程序，但是它們?nèi)圆幻夂绣e(cuò)誤。信息和警告塊。技術(shù)性的旁白、庫(kù)函數(shù)的敘述以及為進(jìn)一步學(xué)習(xí)而給出的筆記都會(huì)不時(shí)地出現(xiàn)。它們被加以如下圖標(biāo)以便有些讀者可以跳過：亨利王的要求。他們拿不出什么理由可以反對(duì)陛下向法蘭西提出王位的要求，只除了這一點(diǎn)，那個(gè)在法拉蒙時(shí)代制定的一條法律，InterramSalicammulieresnesuccedant，‘在撒利族的土地上婦女沒有繼承權(quán)’：而法國(guó)人就把這‘撒利族的土地’曲解為法蘭西的土地，并且把法拉蒙認(rèn)做是這條法律的創(chuàng)制人和婦權(quán)的剝奪者。可是他們的歷史學(xué)家卻忠實(shí)地宣稱撒利區(qū)是在日耳曼的土地上……ML并不完美。某些缺陷會(huì)使簡(jiǎn)單的編碼錯(cuò)誤浪費(fèi)掉程序員幾個(gè)小時(shí)的時(shí)間。而且，新的標(biāo)準(zhǔn)庫(kù)使得新舊編譯器不兼容。因此，本書中有一些這樣的警告圖標(biāo)：小心葛羅斯特公爵。呵，勃金漢！小心那個(gè)狗東西：要知道，搖尾的狗會(huì)咬人；咬了人，它的牙毒還會(huì)叫你痛極而死；莫同他來往，千萬(wàn)留意；罪惡、死亡和地獄都看中了他，地下的大小役吏都在供他使喚。我要趕緊補(bǔ)充一點(diǎn)，在ML里不會(huì)產(chǎn)生這么可怕的后果。程序里的錯(cuò)誤是不能沖垮ML系統(tǒng)本身的。另一方面，程序員必須牢記，即使是正確的程序也可能給外部世界帶來傷害。如何得到StandardML編譯器。由于StandardML剛出現(xiàn)不久，很多學(xué)院沒有編譯器。下面列出了現(xiàn)有的一些StandardML編譯器，并附有聯(lián)系地址。書中的例子是在MoscowML、Poly/ML和StandardMLofNewJersey下開發(fā)的。我尚未嘗試其他的編譯器。要得到MLWorks，請(qǐng)聯(lián)系HarlequinLimited，BarringtonHall，Barrington，Cambridge，CB25RG，England。他們的電子郵件地址是web@harlequin.com。要得到MoscowML，請(qǐng)聯(lián)系PeterSestoft，MathematicalSection，RoyalVeterinaryandAgriculturalUniversity，Thorvaldsensvej40，DK-1871FrederiksbergC，Denmark。或從互聯(lián)網(wǎng)上得到該系統(tǒng)：http：//www.dina.kvl.dk/~sestoft/mosml.html要得到Poly/ML，請(qǐng)聯(lián)系A(chǔ)bstractHardwareLtd，1BrunelSciencePark，KingstonLane，Uxbridge，Middlesex，UB83PQ，England。他們的電子郵件地址是lambda@ahl.co.uk?；驈幕ヂ?lián)網(wǎng)上得到該系統(tǒng)：http：//www.polyml.org/要得到PoplogStandardML，請(qǐng)聯(lián)系IntegralSolutionsLtd，BerkHouse，BasingView，Basingstoke，HampshireRG214RG，England。他們的電子郵件地址是isl@isl.co.uk。要得到StandardMLofNewJersey，請(qǐng)聯(lián)系A(chǔ)ndrewAppel，ComputerScienceDepartment，PrincetonUniversity，PrincetonNJ08544-2087，USA。更好的是可以從互聯(lián)網(wǎng)上得到文件：http：//www.cs.princeton.edu/~appel/smlnj/http：//www.smlnj.org/書中的程序和一些練習(xí)答案可以通過電子郵件得到，我的電子郵件地址是lcp@cl.cam.ac.uk。如果可能，請(qǐng)使用互聯(lián)網(wǎng)，我的主頁(yè)在http：//www.cl.cam.ac.uk/users/lcp/致謝。編輯，DavidTranah，在寫作的各個(gè)階段提供了幫助，并建議了書名。GrahamBirtwistle、GlennBruns和DavidWolfram仔細(xì)閱讀了文本。DaveBerry、SimonFinn、MikeFourman、KentKarlsson、RobinMilner、RichardO誎eefe、KeithvanRijsbergen、NickRothwell、MadsTofte、DavidN.Turner和Harlequin的工作人員也對(duì)文本提出了意見。AndrewAppel、GavinBierman、PhilBrabbin、RichardBrooksby、GuyCousineau、LalGeorge、MikeGordon、MartinHansen、DarrellKindred、SilvioMeira、AndrewMorris、KhalidMughal、TobiasNipkow、KurtOlender、AllenStoughton、ReubenThomas、RayToal和HelenWilson發(fā)現(xiàn)了前幾次印刷中的錯(cuò)誤。PieteBrooks、JohnCarroll和GrahamTitmus在計(jì)算機(jī)使用方面給予了幫助。我還要感謝DaveMatthews開發(fā)了Poly/ML，這是多年以來唯一高效的StandardML的編譯器。在眾多的參考文獻(xiàn)中，Abelson和Sussman（1985）、Bird和Wadler（1988）以及Burge（1975）的著作特別有幫助。Reade（1989）的書中包含了在ML中實(shí)現(xiàn)惰性表的有用思想。TheScienceandEngineeringResearchCouncil在過去20多年來給予了LCF和ML大量的研究資助。本書的大部分寫作工作都是我從劍橋大學(xué)休假的過程中完成的。我感謝計(jì)算機(jī)實(shí)驗(yàn)室（ComputerLaboratory）和卡萊爾學(xué)院（ClareCollege）給予休假，以及愛丁堡大學(xué)對(duì)我六個(gè)月的招待。最后，我要感謝Sue，感謝她所給我的一切幫助，以及天天耐心傾聽我關(guān)于每一章進(jìn)展的報(bào)道。

　　Lawrence C.Paulson，于1981年在美國(guó)斯坦福大學(xué)獲得計(jì)算機(jī)科學(xué)博士學(xué)位，現(xiàn)為英國(guó)劍橋大學(xué)計(jì)算邏輯學(xué)教授。Paulson博士從事有關(guān)ML語(yǔ)言的教學(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)證方面的研究。