内容简介
本书是ML程序设计的权威教程，全面系统地介绍了标准ML（Standard ML）语言及其编程方法。作为函数式编程语言的代表，ML语言在类型安全、模式匹配、高阶函数和抽象数据类型等方面具有独特优势。本书从基础知识入手，循序渐进地讲解了ML语言的语法、语义和核心特性，包括基本类型、函数定义、列表与树等数据结构、模式匹配、异常处理、模块系统以及命令式编程等高级主题。
第二版在保留第一版精华的基础上，增加了对新标准（SML’97）的全面支持，并更新了学习资源与练习内容。书中包含大量精心设计的示例和习题，帮助读者在动手实践中掌握函数式编程的思想与技巧。无论你是计算机专业的学生、教师，还是希望提升编程能力的软件工程师，本书都能为你打开函数式编程的大门，并深入理解类型系统与语言设计之间的关系。
目录
函数式程序设计
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 字符串和字符
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语法图
语法图中英词汇对照表
预定义标识符
序偶、元组和记录
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语法图
语法图中英词汇对照表
预定义标识符
重要申明：
本书由书友@锦小书发布分享，仅供学习交流使用，版权归原作者所有。如有侵权，请联系我们删除。
本书由书友@锦小书发布分享，仅供学习交流使用，版权归原作者所有。如有侵权，请联系我们删除。
📖 支持知识自由流动
每一本书的稳定访问，都离不开服务器、存储与带宽的长期维护。
