第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
· · · · · · (收起)