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

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

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