Martin-Lof类型论程序设计导论PDF电子书下载

目录 1

1．引言 1

1.1 类型论用于程序设计 3

1.2 构造数学 6

1.3 类型论的不同表述系统 7

1.4 程序逻辑的实现 8

2．集合，命题和规格说明的等同 10

2.1 命题作为集合 10

2.2 命题作为任务和程序的规格说明 12

3．表达式与定义相等性 14

3.1 作用 14

3.2 抽象 15

3.3 组合 16

3.4 选取 17

3.5 带名分部的组合 17

3.6 相关度 17

3.7 定义 20

3.8 什么是具某个相关度的表达式的定义 20

3.9 两个表达式之间相等性的定义 21

第一部分 多型集合 25

4．判断形式的语义 25

4.1 范畴判断 27

4.2 带一个前提的假设判断 29

4.3 带多个前提的假设判断 31

5．一般规则 34

5.3 相等性规则 36

5.1 前提 36

5.2 命题作为集合 36

5.4 集合规则 37

5.5 替代规则 37

6．枚举集合 40

6.1 永假与空集合 42

6.2 单元素集合与真命题 42

6.3 集合Bool 43

7．集合族的笛氏积 45

7.1 形式规则及其论证 47

7.2 另一种原始非典则形式 48

7.3 由Ⅱ集合定义的常元 51

8.1 内涵相等性 54

8．相等性集合 54

8.2 外延相等性 57

8.3 Ⅱ-集合元素的η-相等性 59

9．自然数 61

10．列表 65

11．两个集合的笛氏积 70

11.1 形式规则 70

11.2 函数的外延相等性 72

12．两个集合的不交和 75

13．集合族的不交和 77

14．小集合之集合（第一全域） 79

14.1 形式规则 79

14.2 消去规则 87

15．良序 94

15.1 用良序表示归纳定义集合 98

16．一般树 99

16.1 形式规则 100

16.2 与良序集合构造子的关系 102

16.3 树集合构造子的异体 104

16.4 不同树集合的例子 104

第二部分 子集合 111

17．基本集合理论中的子集合 111

18．子集合理论 114

18.1 无前提判断 114

18.2 假设判断 116

18.3 子集合理论中的一般规则 119

18.4 子集合理论中的命题常元 120

18.5 由概括形成子集合 122

18.6 子集合理论中单独的成集算子 124

18.7 带全域的子集合 127

第三部分 单型集合 135

19．类型 135

19.1 类型与对象 136

19.2 集合与元素的类型 137

19.3 类型族 137

19.4 一般规则 139

19.5 前提 140

19.6 函数类型 141

20.1 Ⅱ集合 144

20．用类型定义集合 144

20.2 ∑集合 146

20.3 不交和 146

20.4 相等性集合 147

20.5 有穷集合 148

20.6 自然数 148

20.7 列表 149

第四部分 例子 153

21．杂例 153

21.1 除以2 153

21.2 偶或奇 157

21.3 Boo1仅有元素true和false 159

21.4 可判定谓词 160

21.5 强消去规则 162

22．程序推导 164

22.1 程序推导方法 164

22.2 分割问题 168

23．抽象数据类型规格说明 178

23.1 参数模 181

23.2 关于带可计算相等性集合的模 181

参考文献 183

附录A 常元及其相关度 192

A.1 集合论中的原始常元 192

A.2 集合常元 193

附录B 操作语义 194

B.1 非典则常元的求值规则 194