ML程序设计教程 第2版PDF|Epub|txt|kindle电子书版本网盘下载

ML程序设计教程 第2版PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

目录出版者的话专家指导委员会译者序第2版序前言第1章 Standard ML1

函数式程序设计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

2.1 命名常量14

值的声明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

2.23 类型推导47

多态类型检测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和dropwhile141

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

一些数学证明的原理163

本章提要163

第6章 函数式程序的论证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.1 扫描或词法分析273

函数式语法分析器273

本章提要273

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

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

9.3 语法分析器的ML代码277

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

λ-演算简介284

9.5 λ-项和λ-归约284

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

在ML中表示λ-项288

9.7 基本操作288

9.8 λ-项的语法分析290

9.9 显示λ-项291

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

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

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

9.12 λ-项的求值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