程序設計語言理論

第1章 引言
1.1 基本概念
1.1.1 程序設計語言的建模
1.1.2 λ表示法
1.1.3 符號和約定
1.2 等式、歸約和語義
1.2.1 公理語義
1.2.2 操作語義
1.2.3 指稱語義
1.3 類型和類型系統(tǒng)
1.3.1 類型和類型系統(tǒng)
1.3.2 類型化語言的優(yōu)點
1.4 歸納法
1.4.1 表達式上的歸納
1.4.2 證明上的歸納
1.4.3 良基歸納
習題
第2章 泛代數(shù)和代數(shù)數(shù)據(jù)類型
2.1 引言
2.2 代數(shù)、基調和項
2.2.1 代數(shù)
2.2.2 代數(shù)項的語法
2.2.3 代數(shù)以及項在代數(shù)中的解釋
2.2.4 代換引理
2.3 等式、可靠性和完備性
2.3.1 等式
2.3.2 項代數(shù)
2.3.3 語義蘊涵和等式證明系統(tǒng)
2.3.4 完備性的形式
2.3.5 同余、商和演繹完備性
2.3.6 非空類別和最小模型完備性
2.4 同態(tài)和初始性
2.4.1 同態(tài)和同構
2.4.2 初始代數(shù)
2.5 代數(shù)數(shù)據(jù)類型
2.5.1 代數(shù)數(shù)據(jù)類型
2.5.2 初始代數(shù)語義和數(shù)據(jù)類型歸納
2.5.3 解釋沒有意義的項
2.5.4 錯誤值的其他解決方法
2.6 重寫系統(tǒng)
2.6.1 基本定義
2.6.2 合流性和可證的相等性
2.6.3 終止性
2.6.4 臨界對
2.6.5 左線性無重疊重寫系統(tǒng)
2.6.6 局部合流、終止和合流之間的聯(lián)系
2.6.7 代數(shù)數(shù)據(jù)類型的應用
習題
第3章 簡單類型化λ演算
3.1 引言
3.2 類型和項
3.2.1 類型的語法
3.2.2 上下文有關語法
3.2.3 λ→項的語法
3,2.4 帶積、和及其他類型的項
3.2.5 定型算法
3.3 證明系統(tǒng)
3.3.1 等式和理論
3.3.2 歸約規(guī)則
3.3.3 有其他規(guī)則的歸約
3.4 通用模型、可靠性和完備性
3.4.1 通用模型和項的含義
3.4.2 應用結構、外延性和框架
3.4.3 環(huán)境條件
3.4.4 類型可靠性和等式可靠性
3.4.5 沒有空類型的完備性
3.4.6 有空類型的完備性
3.4.7 其他類型的通用模型
3.5 可計算函數(shù)編程語言
3.5.1 概述
3.5.2 PCF的語法
3.5.3 聲明和語法美化
3.5.4 程序和結果
3.5.5 公理語義
3.5.6 操作語義
3.5.7 由各種形式的語義定義的等價關系
3.5.8 記錄和n元組
3.6 各種歸約策略
3.6.1 歸約策略
3.6.2 最左歸約和惰性歸約
3.6.3 并行歸約
3.6.4 急切歸約
習題
第4章 類型化λ演算的模型
4.1 引言
4.2 遞歸函數(shù)和不動點算子
4.2.1 遞歸函數(shù)和不動點算子
4.2.2 有不動點算子的急切歸約
4.2.3 PCF語言的編程實例
4.3 論域理論模型和不動點
4.3.1 遞歸定義和不動點算子
4.3.2 完全偏序集合、提升和笛卡兒積
4.3.3 連續(xù)函數(shù)
4.3.4 不動點和完備連續(xù)層級
4.3.5 PCF的CPO模型
4.4 不動點歸納
習題
第5章 命令式程序的語義
5.1 引言
5.2 Kernel語言
5.2.1 存儲單元
5.2.2 表達式的解釋
5.2.3 程序狀態(tài)
5.3 操作語義
5.3.1 表達式的求值
5.3.2 命令的執(zhí)行
5.4 指稱語義
5.4.1 帶狀態(tài)的類型化λ演算
5.4.2 語義函數(shù)
5.4.3 操作語義和指稱語義的等價
5.5 Kernel語言的Hoare邏輯
5.5.1 一階斷言
5.5.2 證明規(guī)則
5.5.3 可靠性
5.5.4 小結
習題
第6章 遞歸類型
6.1 引言
6.2 歸納和余歸納
6.2.1 余歸納現(xiàn)象
6.2.2 歸納和余歸納指南
6.2.3 代數(shù)和余代數(shù)
6.3 遞歸類型
6.3.1 遞歸類型總覽
6.3.2 遞歸的數(shù)據(jù)結構
6.4 歸納類型和余歸納類型
6.4.1 歸納類型和余歸納類型總覽
6.4.2 幫助理解的實例
習題
第7章 多態(tài)性
7.1 引言
7.1.1 概述
7.1.2 類型作為函數(shù)變元
7.2 直謂式多態(tài)演算
7.2.1 類型和項的語法
7.2.2 和其他形式多態(tài)性的比較
7.2.3 等式證明和歸約
7.2.4 ML風格的多態(tài)聲明
7.3 非直謂式多態(tài)演算
7.3.1 引言
7.3.2 非直謂式多態(tài)λ演算的表達力
7.3.3 歸約的終止性
7.4 數(shù)據(jù)抽象和存在類型
7.5 類型表達式的分類
7.5.1 類型表達式的種類
7.5.2 類型表達式的定類與相等
7.5.3 項的定型
習題
第8章 依賴類型
8.1 引言
8.2 帶依賴類型的演算
8.2.1 依賴積類型
8.2.2 依賴和類型
8.3 帶依賴類型的程序設計
8.3.1 簡化DML的實例
8.3.2 簡化DML的定義
8.4 廣義積與廣義和
8.4.1 廣義積與廣義和概念
8.4.2 帶廣義積與廣義和的直謂式演算
8.4.3 ML模塊語言
8.4.4 用積與和來表示模塊
8.4.5 直謂性以及兩個全域之間的聯(lián)系
習題
第9章 命題和類型
9.1 引言
9.2 構造邏輯
9.2.1 構造語義
9.2.2 構造邏輯
9.2.3 命題當作類型
9.3 經(jīng)典邏輯
9.3.1 經(jīng)典邏輯和構造邏輯的區(qū)別與聯(lián)系
9.3.2 經(jīng)典邏輯的規(guī)則
9.3.3 推導消去形式
9.3.4 證明的動態(tài)性
習題
第10章 子定型
10.1 引言
10.2 有子定型的簡單類型化λ演算
10.3 記錄
10.3.1 記錄子定型的一般性質
10.3.2 帶記錄和子定型的類型化演算
10.4 子定型的語義模型
10.4.1 概述
10.4.2 子定型的轉換解釋
10.4.3 類型的子集解釋
10.5 對象的遞歸記錄模型
10.5.1 遞歸記錄類型
10.5.2 遞歸類型的子定型
習題
第11章 類型推斷
11.1 引言
11.2 帶類型變量的λ→類型推斷
11.2.1 語言λt→
11.2.2 代換、實例與合一
11.2.3 主定型算法
11.2.4 隱式定型
11.2.5 定型和合一的等價
11.3 帶多態(tài)聲明的類型推斷
11.3.1 ML類型推斷和多態(tài)變量
11.3.2 兩組隱式定型規(guī)則
11.3.3 類型推斷算法
習題
參考文獻