ML程序设计教程

封面
书名
版权
前言
目录
目录出版者的话专家指导委员会译者序第2版序前言第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（映射）和filter（过滤）
5.8  表算子takewhile和dropwhile
5.9  表算子exists（存在）和all（全称）
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.11  多参数函子
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.1  扫描或词法分析
函数式语法分析器
本章提要
第9章  书写λ-演算的解释器
9.2  自顶向下的语法分析套件
9.3  语法分析器的ML代码
9.4  例子：分析和显示类型
λ-演算简介
9.5  λ-项和λ-归约
9.6  在替换中防止变量的捕获
在ML中表示λ-项
9.7  基本操作
9.8  λ-项的语法分析
9.9  显示λ-项
作为程序设计语言的λ-演算
9.10  λ-演算中的数据结构
9.11  λ-演算中的递归定义
9.12  λ-项的求值
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语法图
语法图中英词汇对照表
索引
预定义标识符