图书介绍
Martin-Lof类型论程序设计导论PDF|Epub|txt|kindle电子书版本网盘下载
- （瑞典）Bengt Nordstrom等著；宋方敏译 著
- 出版社： 南京：南京大学出版社
- ISBN：7305038326
- 出版时间：2002
- 标注页数：195页
- 文件大小：6MB
- 文件页数：203页
- 主题词：计算数学(学科: 高等学校) 计算数学
PDF下载
下载说明
Martin-Lof类型论程序设计导论PDF格式电子书版下载
下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！
（文件页数 要大于 标注页数，上中下等多册电子书除外）
注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具
图书目录
目录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 集合Bool43
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 除以2153
21.2 偶或奇157
21.3 Boo1仅有元素true和false159
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