ML程序设计教程（原书第2版）

　　本书是关于ML程序设计的经典教材，详细介绍如何使用ML语言进行程序设计，并讲解函数式程序设计的基本原理。书中含有大量例子，涵盖了排序、矩阵运算、多项式运算等方面。大型的例子包括一个一般性的自顶向下语法分析器、一个一演算归约程序和一个定理证明机。书中也讲述了关于数组、队列、优生队列等高效的函数式实现，并且有一章专门讨论函数式程序的形式论证。本书详细讲解如何使用ML语言进行程序设计，并介绍函数式程序设计的基本原理。书中特别讲述了为ML的修订版所设计的新标准库的主要特性，并且给出大量例子，涵盖排序、矩阵运算、多项式运算等方面。大型的例子包括一个一般性的自顶向下语法分析器、一个l-演算归约程序和一个定理证明机。书中也讲述了关于数组、队列、优先队列等高效的函数式实现，并且有一章专门讨论函数式程序的形式论证。本书可作为高等院校计算机专业相关课程的教材，也适合广大程序设计人员参考。本书前言前言：本书源于对StandardML和函数式程序设计的讲稿。它仍可以作为函数式程序设计的课本—一本面向实用，而不是标准的、理想化的书—然而，它主要是一本有效使用ML的指南。它甚至讨论了ML的命令式特性。有些内容需要离散数学的知识，例如初等逻辑和集合论。读者会发现以往的程序设计经验是有用的，但不是必需的。本书是一本程序设计手册，而不是参考手册。它覆盖了ML的主要方面，但并不尽述所有的细节。它在理论原理上花费了一些篇幅，但主要还是关心高效的算法和实际的程序设计。本书的组织反映了我的教学经验。高阶函数出现得较晚，在第5章讲述。惯常的做法是在一开始就介绍一些不甚自然的例子，这样做只能使学生们感到困惑。高阶函数的概念是不容易理解的，需要充分的预备知识。所以，本书从基本类型、表和树开始讲述。当讲到高阶函数时，很多相关的例子已经是现成的了。练习的难度相差很大。它们不是用来评测学生的，而是为了提供实践机会，拓展内容和激发讨论的。本书一览。大多数章节都专注于ML的各个方面。第1章介绍了函数式程序设计的背景思想，以及ML的历史概况。第2～5章涵盖了ML的函数式部分，包括对模块的简介。讲述了基本类型、表、树和高阶函数。对函数式程序设计的更广泛的原理也有所讨论。第6章给出了论证函数式程序的形式方法。看上去似乎偏离了程序设计的主题，然而错误的程序是没用的。易于形式论证是函数式程序设计的一大好处。第7章详细讲述了模块，包括函子（带参数的模块）。第8章讲述了ML的命令式特性：引用、数组和输入输出。本书的其余部分由较大的例子构成。第9章给出了函数式的语法分析器和一个l-演算解释器。第10章给出了一个定理证明机，这是ML的传统应用。书中的例子非常丰富。其中一些只是为了说明ML的某个方面，但大多数本身就有一定用途—排序、函数式数组、优先队列、搜索算法、美化打印。请注意：虽然我测试过这些程序，但是它们仍不免含有错误。信息和警告块。技术性的旁白、库函数的叙述以及为进一步学习而给出的笔记都会不时地出现。它们被加以如下图标以便有些读者可以跳过：亨利王的要求。他们拿不出什么理由可以反对陛下向法兰西提出王位的要求，只除了这一点，那个在法拉蒙时代制定的一条法律，InterramSalicammulieresnesuccedant，‘在撒利族的土地上妇女没有继承权’：而法国人就把这‘撒利族的土地’曲解为法兰西的土地，并且把法拉蒙认做是这条法律的创制人和妇权的剥夺者。可是他们的历史学家却忠实地宣称撒利区是在日耳曼的土地上……ML并不完美。某些缺陷会使简单的编码错误浪费掉程序员几个小时的时间。而且，新的标准库使得新旧编译器不兼容。因此，本书中有一些这样的警告图标：小心葛罗斯特公爵。呵，勃金汉！小心那个狗东西：要知道，摇尾的狗会咬人；咬了人，它的牙毒还会叫你痛极而死；莫同他来往，千万留意；罪恶、死亡和地狱都看中了他，地下的大小役吏都在供他使唤。我要赶紧补充一点，在ML里不会产生这么可怕的后果。程序里的错误是不能冲垮ML系统本身的。另一方面，程序员必须牢记，即使是正确的程序也可能给外部世界带来伤害。如何得到StandardML编译器。由于StandardML刚出现不久，很多学院没有编译器。下面列出了现有的一些StandardML编译器，并附有联系地址。书中的例子是在MoscowML、Poly/ML和StandardMLofNewJersey下开发的。我尚未尝试其他的编译器。要得到MLWorks，请联系HarlequinLimited，BarringtonHall，Barrington，Cambridge，CB25RG，England。他们的电子邮件地址是web@harlequin.com。要得到MoscowML，请联系PeterSestoft，MathematicalSection，RoyalVeterinaryandAgriculturalUniversity，Thorvaldsensvej40，DK-1871FrederiksbergC，Denmark。或从互联网上得到该系统：http：//www.dina.kvl.dk/~sestoft/mosml.html要得到Poly/ML，请联系AbstractHardwareLtd，1BrunelSciencePark，KingstonLane，Uxbridge，Middlesex，UB83PQ，England。他们的电子邮件地址是lambda@ahl.co.uk。或从互联网上得到该系统：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发现了前几次印刷中的错误。PieteBrooks、JohnCarroll和GrahamTitmus在计算机使用方面给予了帮助。我还要感谢DaveMatthews开发了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博士开发和维护了lsabelle自动定理证明系统，他近期正在进行关于自动定理证明和密码协议验证方面的研究。

第1章Standard ML
函数式程序设计 
1．1表达式和命令
1．2过程式程序设计语言中的表达式·
1．3存储管理　
1．4函数式语言的元素　
1．5函数式程序设计的效率　Standard ML概述　
1．6 Standard ML的演化　
1．7 ML的自动定理证明传统
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联立声明　
模块系统初步　
2．20复数　
2．21结构　
2．22签名　
多态类型检测　
2．23类型推导　
2．24多态函数声明　
要点小结　
第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求后继排列的问题　
多态函数中的相等测试　
3．14相等类型　
3．15多态集合操作　
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多态数据类型　
4．4通过val、as、case进行模式匹配
异常　
4．5异常初步　
4．6声明异常　
4．7抛出异常　
4．8处理异常　
4．9对异常的异议　
树　
4．10二叉树类型　
4．11枚举树的内容　
4．12由表建立树　
4．13为二叉树设计的结构
基于树的数据结构　
4．14字典　
4．15函数式数组和弹性数组　
4．16优先队列　　
重言式检测器　
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泛型的字典和优先队列 
利用模块建立大型系统 
7．1l多参数函子 
7．12共享约束 
7．13全函子式程序设计 
7．14 open声明 
7．15签名和子结构 
模块参考指南 
7．16签名和结构的语法 
7．17模块声明的语法 
要点小结 
第8章ML中的命令式程序设计 
本章提要 
引用类型  
8．1引用及其操作 
8．2控制结构 
8．3多态引用 
数据结构中的引用 
8．4序列，或惰性表 
8．5环形缓冲区 
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量词的相继式规则 
10．4带量词的定理证明 
在ML中处理项和公式 
10．5表示项和公式 
10．6分析和显示公式 
10．7合 
策略和证明状态 
10．8证明状态 
10．9 ML签名 
10．10用于基本相继式的策略 
10．11命题策略 
10．12量词策略 
搜索证明 
10．13变换证明状态的命令 
10．14两个使用策略的证明实例 
10．15策略算子 
10．16一阶逻辑的自动策略 
要点小结 
项目建议 
参考文献 
Standard ML语法图 
语法图中英词汇对照表 
索引  
预定义标识符