函數程設與推論
Functional Program Construction and Reasoning
目錄
前言
0 符號、演算、與抽象化
0.1 騎士與惡棍之島
0.2 讓符號為你工作
0.3 抽象化
0.4 抽象化與表達力
0.5 正確性
0.6 可演算的程式語言
0.7 相關資料
1 值、函數、與定義
1.1 值與求值
1.2 函數定義
1.3 高階函數
1.4 函數合成
1.5 $\lambda$ 算式
1.6 簡單資料型態
1.6.1 布林值
1.6.2 字元
1.6.3 序對
1.7 弱首範式
1.8 串列
1.8.1 串列解構
1.8.2 串列生成
1.8.3 串列上的種種組件函數
1.9 全麥編程
1.10 自訂資料型別
1.11 參考資料
2 歸納定義與證明
2.1 數學歸納法
2.2 自然數上之歸納定義
2.3 自然數上之歸納證明
2.4 串列與其歸納定義
2.4.1 串列上之歸納定義
2.4.2 串列上之歸納證明
2.5 從資料、程式、到證明
2.6 更多歸納定義與證明
2.6.1
filter
,
takeWhile
, 與
dropWhile
2.6.2
elem
與不等式證明
2.6.3 串列區段
2.6.4 插入、排列、子串列、與劃分
2.7 再談「讓符號為你工作」
2.8 其他歸納資料結構
2.9 由集合論看歸納法
2.10 歸納定義的簡單變化
2.11 完全歸納
2.12 良基歸納
2.13 詞典序歸納
2.14 交互歸納
2.15 參考資料
3 搜尋樹
3.1 二元搜尋樹
3.2 紅黑樹
3.2.1 紅黑樹插入
3.2.2 紅黑樹之性質：高度
3.2.3 紅黑樹之性質：平衡
3.2.4 紅黑樹之性質：顏色
4 關於語意的基本概念
4.1 指稱語意
4.2 操作語意
5 一般程式推導
5.1 展開-收回轉換
5.2 關於執行效率
5.3 用展開-收回轉換增進效率
5.3.1 計算多項式 -- Horner 法則
5.3.2 二進位表示法
5.3.3 小結與提醒
5.4 變數換常數
5.5 組對
5.5.1 陡串列
5.5.2 以串列標記樹狀結構
5.5.3 代換為最小標籤 --- 循環程式
5.5.4 小結與提醒
5.6 累積參數
5.6.1 串列反轉與連接
5.6.2 由上到下的資訊流
5.6.3 尾遞迴
5.6.4 更多尾遞迴範例
5.6.5 尾遞迴的效率考量
5.6.6 函數作為串列
6 摺
6.1 串列的摺
6.1.1 更多串列上的摺
6.1.2 不是
foldr
的函數
6.2 摺融合定理
6.2.1 將摺融合用於定理證明
6.2.2 以摺融合生成程式
6.2.3 掃描
6.2.4 香蕉船定理
6.2.5 累積參數與摺融合
6.2.6 引入脈絡
6.3 左摺、串列同構、與 Paramorphism
6.3.1 左摺
6.3.2 串列同構
6.3.3 Paramorphism 與本原遞迴
6.4 自然數的摺
6.5 其他資料結構
6.6 參考資料
7 區段問題
7.1 最大區段和
7.2 最長高原問題
7.3 參考資料
8 單子與副作用
8.1 例外處理
8.2 單子與單子律
8.3 讀取單子
8.3.1 變數與環境
8.3.2 「讀取」副作用是單子
8.3.3 推論讀取單子程式的性質
8.4 狀態單子
8.4.1 河內塔問題
8.5 參考資料
索引
參考書目
穆信成 Shin-Cheng Mu
中央研究院 資訊科學研究所
8 單子與副作用
«
8.4 狀態單子
8.5 參考資料
Wadler [1992]
«
8.4 狀態單子