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(映射)和fter(过滤)

5．8表算子takewhile和dropwhile

5．9表算子朗船(存在)和趔(全称)

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．1l多参数函子

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章书写λ-演算的解释器

本章提要

函数式语法分析器

9．1扫描或词法分析

9．2自顶向下的语法分析套件

9．3语法分析器的ML代码

9．4例子：分析和显示类型

λ-演算简介

9．5 k-项和λ-归约

9．6在替换中防止变量的捕获

在ML中表示入一项

9．7基本操作

9．8 k-项的语法分析

9．9显示λ-项

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

9．10 k-演算中的数据结构

9．11 k-演算中的递归定义

9．12 k-项的求值

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语法图

语法图中英词汇对照表

索引

预定义标识符