注冊 | 登錄讀書好,好讀書,讀好書!
讀書網-DuShu.com
當前位置: 首頁出版圖書科學技術計算機/網絡軟件與程序設計程序設計綜合ML程序設計教程(原書第2版)

ML程序設計教程(原書第2版)

ML程序設計教程(原書第2版)

定 價:¥45.00

作 者: (英)Lawrence C.Paulson著;柯韋譯;柯韋譯
出版社: 機械工業(yè)出版社
叢編項: 計算機科學叢書
標 簽: 暫缺

ISBN: 9787111161219 出版時間: 2005-05-01 包裝: 平裝
開本: 26cm 頁數: 369 字數:  

內容簡介

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

作者簡介

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

圖書目錄

第1章Standard ML
函數式程序設計 
1.1表達式和命令
1.2過程式程序設計語言中的表達式·
1.3存儲管理 
1.4函數式語言的元素 
1.5函數式程序設計的效率 Standard ML概述 
1.6 Standard ML的演化 
1.7 ML的自動定理證明傳統(tǒng)
1.8新標準庫 
1.9 ML和工作中的程序員 
第2章名字、函數和類型 
本章提要 
值的聲明 
2.1命名常量 
2.2聲明函數 
2.3 Standard ML中的標識符
數、字符串和真值 
2.4算術運算 
2.5字符串和字符 
2.6真值和條件表達式
序偶、元組和記錄 
2.7向量:序偶的例子 
2.8多參數和多結果的函數
2.9記錄 
2.10中綴操作符表達式的求值 
2.11 ML中的求值:傳值調用 
2.12傳值調用下的遞歸函數 
2.13傳需調用或惰性求值
書寫遞歸函數 
2.14整數次冪 
2.15斐波那契數列 
2.16整數平方根 
局部聲明 
2.17例子:實數平方根 
2.18使用local來隱藏聲明 
2.19聯立聲明 
模塊系統(tǒng)初步 
2.20復數 
2.21結構 
2.22簽名 
多態(tài)類型檢測 
2.23類型推導 
2.24多態(tài)函數聲明 
要點小結 
第3章表 
本章提要 
表的簡介 
3.1表的構造 
3.2表的操作 
基本的表函數 
3.3表的測試和分解 
3.4與數量有關的表處理 
3.5追加和翻轉 
3.6表的表,序偶的表 
表的應用 
3.7找零錢 
3.8 進制算術 
3.9矩陣的轉置 
3.10矩陣乘法…
3.11高斯消元法
3.12分解一個數為兩個平方數之和一
3.13求后繼排列的問題 
多態(tài)函數中的相等測試 
3.14相等類型 
3.15多態(tài)集合操作 
3.16關聯表 
3.17圖的算法 
排序:案例研究 
3.18隨機數 
3.19插入排序  
3.20快速排序 
3.21合并排序 
多項式算術 
3.22表示抽象數據 
3.23多項式的表示 
3.24多項式加法和乘法 
3.25最大公因式 
要點小結 
第4章樹和具體數據 
本章提要 
數據類型聲明 
4.1國王和他的臣民 
4.2枚舉類型 
4.3多態(tài)數據類型 
4.4通過val、as、case進行模式匹配
異?!?br />4.5異常初步 
4.6聲明異常 
4.7拋出異?!?br />4.8處理異?!?br />4.9對異常的異議 
樹 
4.10二叉樹類型 
4.11枚舉樹的內容 
4.12由表建立樹 
4.13為二叉樹設計的結構
基于樹的數據結構 
4.14字典 
4.15函數式數組和彈性數組 
4.16優(yōu)先隊列  
重言式檢測器 
4.17命題邏輯 
4.18否定范式 
4.19合取范式 
要點小結 
第5章函數和無窮數據 
本章提要 
作為值的函數 
5.1使用fn記法的匿名函數 
5.2柯里函數 
5.3數據結構中的函數 
5.4作為參數和結果的函數 
通用算子 
5.5切片 
5.6組合子
5.7表算子map(映射)和fter(過濾)
5.8表算子takewhile和dropwhile 
5.9表算子朗船(存在)和趔(全稱) 
5.10表算子foldl(左折疊)和foldr
(右折疊) 
5.11更多遞歸算子的例子 
序列,或無窮表 
5.12序列類型 
5.13基本的序列處理 
5.14基本的序列應用 
5.15數值計算 
5.16交替和序列的序列 
搜索策略和無窮表 
5.17用ML實現的搜索策略 
5.18生成回文 
5.19瓜皇后問題 
5.20迭代深化 
要點小結 
第6章函數式程序的論證 
本章提要 
一些數學證明的原理 
6.1 ML程序和數學 
6.2數學歸納法和完全歸納法 
6.3程序驗證的簡單例子 
結構歸納法 
6.4關于表的結構歸納法 
6.5關于樹的結構歸納法 
6.6函數值和算子 
一般性歸納原理 
6.7計算范式 
6.8良基歸納和遞歸 
6.9遞歸程序模式 
描述和驗證 
6.10有序謂詞 
6.11通過多重集合表示重新排列
6.12驗證的意義 
要點小結  
第7章抽象類型和函子 
本章提要 
隊列的三種表示方法 
7.1將隊列表示為表 
7.2將隊列表示為新的數據類型 
7.3將隊列表示為表的序偶 
簽名和抽象 
7.4隊列應具有的簽名 
7.5簽名約束 
7.6抽象類型(abstype)聲明 
7.7從結構導出的簽名 
函子 
7.8測試多個隊列結構 
7.9泛型矩陣運算 
7.10泛型的字典和優(yōu)先隊列 
利用模塊建立大型系統(tǒng) 
7.1l多參數函子 
7.12共享約束 
7.13全函子式程序設計 
7.14 open聲明 
7.15簽名和子結構 
模塊參考指南 
7.16簽名和結構的語法 
7.17模塊聲明的語法 
要點小結 
第8章ML中的命令式程序設計 
本章提要 
引用類型  
8.1引用及其操作 
8.2控制結構 
8.3多態(tài)引用 
數據結構中的引用 
8.4序列,或惰性表 
8.5環(huán)形緩沖區(qū) 
8.6可變更的數組和函數式的數組·
輸入和輸出 
8.7字符串處理 
8.8文本輸入輸出 
8.9文本處理的例子 
8.10美化打印程序 
要點小結 
第9章書寫λ-演算的解釋器 
本章提要 
函數式語法分析器 
9.1掃描或詞法分析 
9.2自頂向下的語法分析套件 
9.3語法分析器的ML代碼 
9.4例子:分析和顯示類型 
λ-演算簡介 
9.5 k-項和λ-歸約 
9.6在替換中防止變量的捕獲 
在ML中表示入一項 
9.7基本操作 
9.8 k-項的語法分析 
9.9顯示λ-項 
作為程序設計語言的λ-演算 
9.10 k-演算中的數據結構 
9.11 k-演算中的遞歸定義 
9.12 k-項的求值 
9.13演示求值程序 
要點小結 
第10章策略定理證明機 
本章提要 
一階邏輯的相繼式演算 
10.1命題邏輯的相繼式演算 
10.2證明相繼式演算中的定理
10.3量詞的相繼式規(guī)則 
10.4帶量詞的定理證明 
在ML中處理項和公式 
10.5表示項和公式 
10.6分析和顯示公式 
10.7合 
策略和證明狀態(tài) 
10.8證明狀態(tài) 
10.9 ML簽名 
10.10用于基本相繼式的策略 
10.11命題策略 
10.12量詞策略 
搜索證明 
10.13變換證明狀態(tài)的命令 
10.14兩個使用策略的證明實例 
10.15策略算子 
10.16一階邏輯的自動策略 
要點小結 
項目建議 
參考文獻 
Standard ML語法圖 
語法圖中英詞匯對照表 
索引  
預定義標識符

本目錄推薦

掃描二維碼
Copyright ? 讀書網 m.ranfinancial.com 2005-2020, All Rights Reserved.
鄂ICP備15019699號 鄂公網安備 42010302001612號