程序設(shè)計(jì)語(yǔ)言理論

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