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自动定理证明系统，他近期正在进行关于自动定理证明和密码协议验证方面的研究。