内容简介

本书是关于ML程序设计的经典教材，详细介绍如何使用 ML语言进行程序设计，并讲解函数式程序设计的基本原理。

书中含有大量例子，涵盖了排序、矩阵运算、多项式运算等方面。大型的例子包括一个一般性的自顶向下语法分析器、一个一演算归约程序和一个定理证明机。书中也讲述了关于数组、队列、优生队列等高效的函数式实现，并且有一章专门讨论函数式程序的形式论证。本书的代码均可以从作者网站（http://www.cl.cam.ac.uk/users/lcp/）得到。

本书详细讲解如何使用ML语言进行程序设计，并介绍函数式程序设计的基本原理。书中特别讲述了为ML的修订版所设计的新标准库的主要特性，并且给出大量例子，涵盖排序、矩阵运算、多项式运算等方面。大型的例子包括一个一般性的自顶向下语法分析器、一个l-演算归约程序和一个定理证明机。书中也讲述了关于数组、队列、优先队列等高效的函数式实现，并且有一章专门讨论函数式程序的形式论证。

本书可作为高等院校计算机专业相关课程的教材，也适合广大程序设计人员参考。

作品目录

第1章 Standard ML 1

函数式程序设计 2

1.1 表达式和命令 2

1.2 过程式程序设计语言中的表达式 3

1.3 存储管理 3

1.4 函数式语言的元素 4

1.5 函数式程序设计的效率 7

Standard ML概述 8

1.6 Standard ML的演化 8

1.7 ML的自动定理证明传统 9

1.8 新标准库 10

1.9 ML和工作中的程序员 11

第2章 名字、函数和类型 13

本章提要 13

值的声明 14

2.1 命名常量 14

2.2 声明函数 15

2.3 Standard ML中的标识符 16

数、字符串和真值 17

2.4 算术运算 17

2.5 字符串和字符 19

2.6 真值和条件表达式 20

序偶、元组和记录 21

2.7 向量：序偶的例子 21

2.8 多参数和多结果的函数 22

2.9 记录 24

2.10 中缀操作符 27

表达式的求值 29

2.11 ML中的求值：传值调用 29

2.12 传值调用下的递归函数 30

2.13 传需调用或惰性求值 33

书写递归函数 36

2.14 整数次幂 36

2.15 斐波那契数列 37

2.16 整数平方根 39

局部声明 39

2.17 例子：实数平方根 40

2.18 使用local来隐藏声明 41

2.19 联立声明 42

模块系统初步 44

2.20 复数 44

2.21 结构 45

2.22 签名 46

多态类型检测 47

2.23 类型推导 47

2.24 多态函数声明 48

要点小结 50

第3章 表 51

本章提要 51

表的简介 51

3.1 表的构造 52

3.2 表的操作 53

基本的表函数 54

3.3 表的测试和分解 55

3.4 与数量有关的表处理 56

3.5 追加和翻转 58

3.6 表的表，序偶的表 60

表的应用 61

3.7 找零钱 61

3.8 二进制算术 63

3.9 矩阵的转置 64

3.10 矩阵乘法 66

3.11 高斯消元法 67

3.12 分解一个数为两个平方数之和 70

3.13 求后继排列的问题 71

多态函数中的相等测试 72

3.14 相等类型 73

3.15 多态集合操作 73

3.16 关联表 76

3.17 图的算法 77

排序：案例研究 81

3.18 随机数 81

3.19 插入排序 82

3.20 快速排序 83

3.21 合并排序 84

多项式算术 86

3.22 表示抽象数据 87

3.23 多项式的表示 87

3.24 多项式加法和乘法 88

3.25 最大公因式 90

要点小结 91

第4章 树和具体数据 93

本章提要 93

数据类型声明 93

4.1 国王和他的臣民 94

4.2 枚举类型 95

4.3 多态数据类型 97

4.4 通过val、as、case进行模式匹配 99

异常 101

4.5 异常初步 101

4.6 声明异常 102

4.7 抛出异常 103

4.8 处理异常 105

4.9 对异常的异议 106

树 107

4.10 二叉树类型 107

4.11 枚举树的内容 109

4.12 由表建立树 111

4.13 为二叉树设计的结构 112

基于树的数据结构 112

4.14 字典 113

4.15 函数式数组和弹性数组 116

4.16 优先队列 120

重言式检测器 124

4.17 命题逻辑 124

4.18 否定范式 126

4.19 合取范式 127

要点小结 129

第5章 函数和无穷数据 131

本章提要 131

作为值的函数 131

5.1 使用fn记法的匿名函数 132

5.2 柯里函数 132

5.3 数据结构中的函数 135

5.4 作为参数和结果的函数 135

通用算子 137

5.5 切片 137

5.6 组合子 138

5.7 表算子map（映射）和 filter（过滤） 139

5.8 表算子takewhile和dropwhile 141

5.9 表算子exists（存在）和all（全称） 141

5.10 表算子 foldl（左折叠）和foldr（右折叠） 142

5.11 更多递归算子的例子 144

序列，或无穷表 147

5.12 序列类型 147

5.13 基本的序列处理 149

5.14 基本的序列应用 151

5.15 数值计算 153

5.16 交替和序列的序列 155

搜索策略和无穷表 156

5.17 用ML实现的搜索策略 158

5.18 生成回文 159

5.19 八皇后问题 160

5.20 迭代深化 161

要点小结 162

第6章 函数式程序的论证 163

本章提要 163

一些数学证明的原理 163

6.1 ML程序和数学 164

6.2 数学归纳法和完全归纳法 165

6.3 程序验证的简单例子 168

结构归纳法 171

6.4 关于表的结构归纳法 171

6.5 关于树的结构归纳法 175

6.6 函数值和算子 178

一般性归纳原理 181

6.7 计算范式 182

6.8 良基归纳和递归 185

6.9 递归程序模式 187

描述和验证 189

6.10 有序谓词 190

6.11 通过多重集合表示重新排列 191

6.12 验证的意义 194

要点小结 195

第7章 抽象类型和函子 197

本章提要 197

队列的三种表示方法 198

7.1 将队列表示为表 198

7.2 将队列表示为新的数据类型 199

7.3 将队列表示为表的序偶 200

签名和抽象 201

7.4 队列应具有的签名 202

7.5 签名约束 202

7.6 抽象类型（abstype）声明 204

7.7 从结构导出的签名 206

函子 207

7.8 测试多个队列结构 208

7.9 泛型矩阵运算 210

7.10 泛型的字典和优先队列 214

利用模块建立大型系统 217

7.11 多参数函子 217

7.12 共享约束 221

7.13 全函子式程序设计 224

7.14 open声明 228

7.15 签名和子结构 232

模块参考指南 234

7.16 签名和结构的语法 235

7.17 模块声明的语法 237

要点小结 237

第8章 ML中的命令式程序设计 239

本章提要 239

引用类型 239

8.1 引用及其操作 240

8.2 控制结构 242

8.3 多态引用 245

数据结构中的引用 249

8.4 序列，或惰性表 249

8.5 环形缓冲区 252

8.6 可变更的数组和函数式的数组 255

输入和输出 259

8.7 字符串处理 259

8.8 文本输入输出 262

8.9 文本处理的例子 264

8.10 美化打印程序 267

要点小结 271

第9章 书写l-演算的解释器 273

本章提要 273

函数式语法分析器 273

9.1 扫描或词法分析 273

9.2 自顶向下的语法分析套件 275

9.3 语法分析器的ML代码 277

9.4 例子：分析和显示类型 280

l-演算简介 284

9.5 l-项和l-归约 284

9.6 在替换中防止变量的捕获 286

在ML中表示l-项 288

9.7 基本操作 288

9.8 l-项的语法分析 290

9.9 显示l-项 291

作为程序设计语言的l-演算 293

9.10 l-演算中的数据结构 293

9.11 l-演算中的递归定义 296

9.12 l-项的求值 296

9.13 演示求值程序 299

要点小结 301

第10章 策略定理证明机 303

本章提要 303

一阶逻辑的相继式演算 303

10.1 命题逻辑的相继式演算 304

10.2 证明相继式演算中的定理 305

10.3 量词的相继式规则 307

10.4 带量词的定理证明 308

在ML中处理项和公式 310

10.5 表示项和公式 310

10.6 分析和显示公式 312

10.7 合一 316

策略和证明状态 319

10.8 证明状态 319

10.9 ML签名 320

10.10 用于基本相继式的策略 321

10.11 命题策略 323

10.12 量词策略 324

搜索证明 326

10.13 变换证明状态的命令 326

10.14 两个使用策略的证明实例 328

10.15 策略算子 330

10.16 一阶逻辑的自动策略 333

要点小结 336

项目建议 337

参考文献 339

Standard ML语法图 347

语法图中英词汇对照表 357

索引 359

预定义标识符 367