没有合适的资源?快使用搜索试试~ 我知道了~
首页通向逻辑、数学、编程的Haskell之路
资源详情
资源评论
资源推荐
The Haskell Road
to
Logic, Math and Programming
Kees Doets and Jan van Eijck
March 4, 2004
Contents
Preface v
1 Getting Started 1
1.1 Starting up the Haskell Interpreter . . . . . . . . . . . . . . . . . 2
1.2 Implementing a Prime Number Test . . . . . . . . . . . . . . . . 3
1.3 Haskell Type Declarations . . . . . . . . . . . . . . . . . . . . . 8
1.4 Identifiers in Haskell . . . . . . . . . . . . . . . . . . . . . . . . 11
1.5 Playing the Haskell Game . . . . . . . . . . . . . . . . . . . . . 12
1.6 Haskell Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.7 The Prime Factorization Algorithm . . . . . . . . . . . . . . . . . 19
1.8 The map and filter Functions . . . . . . . . . . . . . . . . . . . 20
1.9 Haskell Equations and Equational Reasoning . . . . . . . . . . . 24
1.10 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2 Talking about Mathematical Objects 27
2.1 Logical Connectives and their Meanings . . . . . . . . . . . . . . 28
2.2 Logical Validity and Related Notions . . . . . . . . . . . . . . . . 38
2.3 Making Symbolic Form Explicit . . . . . . . . . . . . . . . . . . 50
2.4 Lambda Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . 58
2.5 Definitions and Implementations . . . . . . . . . . . . . . . . . . 60
2.6 Abstract Formulas and Concrete Structures . . . . . . . . . . . . 61
2.7 Logical Handling of the Quantifiers . . . . . . . . . . . . . . . . 64
2.8 Quantifiers as Procedures . . . . . . . . . . . . . . . . . . . . . . 68
2.9 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
3 The Use of Logic: Proof 71
3.1 Proof Style . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
3.2 Proof Recipes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.3 Rules for the Connectives . . . . . . . . . . . . . . . . . . . . . . 78
3.4 Rules for the Quantifiers . . . . . . . . . . . . . . . . . . . . . . 90
i
ii
CONTENTS
3.5 Summary of the Proof Recipes . . . . . . . . . . . . . . . . . . . 96
3.6 Some Strategic Guidelines . . . . . . . . . . . . . . . . . . . . . 99
3.7 Reasoning and Computation with Primes . . . . . . . . . . . . . . 103
3.8 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
4 Sets, Types and Lists 113
4.1 Let’s Talk About Sets . . . . . . . . . . . . . . . . . . . . . . . . 114
4.2 Paradoxes, Types and Type Classes . . . . . . . . . . . . . . . . . 121
4.3 Special Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
4.4 Algebra of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
4.5 Pairs and Products . . . . . . . . . . . . . . . . . . . . . . . . . . 136
4.6 Lists and List Operations . . . . . . . . . . . . . . . . . . . . . . 139
4.7 List Comprehension and Database Query . . . . . . . . . . . . . 145
4.8 Using Lists to Represent Sets . . . . . . . . . . . . . . . . . . . . 149
4.9 A Data Type for Sets . . . . . . . . . . . . . . . . . . . . . . . . 153
4.10 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
5 Relations 161
5.1 The Notion of a Relation . . . . . . . . . . . . . . . . . . . . . . 162
5.2 Properties of Relations . . . . . . . . . . . . . . . . . . . . . . . 166
5.3 Implementing Relations as Sets of Pairs . . . . . . . . . . . . . . 175
5.4 Implementing Relations as Characteristic Functions . . . . . . . . 182
5.5 Equivalence Relations . . . . . . . . . . . . . . . . . . . . . . . . 188
5.6 Equivalence Classes and Partitions . . . . . . . . . . . . . . . . . 192
5.7 Integer Partitions . . . . . . . . . . . . . . . . . . . . . . . . . . 202
5.8 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 204
6 Functions 205
6.1 Basic Notions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206
6.2 Surjections, Injections, Bijections . . . . . . . . . . . . . . . . . 218
6.3 Function Composition . . . . . . . . . . . . . . . . . . . . . . . 222
6.4 Inverse Function . . . . . . . . . . . . . . . . . . . . . . . . . . . 226
6.5 Partial Functions . . . . . . . . . . . . . . . . . . . . . . . . . . 229
6.6 Functions as Partitions . . . . . . . . . . . . . . . . . . . . . . . 232
6.7 Products . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234
6.8 Congruences . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236
6.9 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 238
7 Induction and Recursion 239
7.1 Mathematical Induction . . . . . . . . . . . . . . . . . . . . . . . 239
7.2 Recursion over the Natural Numbers . . . . . . . . . . . . . . . . 246
7.3 The Nature of Recursive Definitions . . . . . . . . . . . . . . . . 251
CONTENTS
iii
7.4 Induction and Recursion over Trees . . . . . . . . . . . . . . . . 255
7.5 Induction and Recursion over Lists . . . . . . . . . . . . . . . . . 265
7.6 Some Variations on the Tower of Hanoi . . . . . . . . . . . . . . 273
7.7 Induction and Recursion over Other Data Structures . . . . . . . . 281
7.8 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 284
8 Working with Numbers 285
8.1 A Module for Natural Numbers . . . . . . . . . . . . . . . . . . . 286
8.2 GCD and the Fundamental Theorem of Arithmetic . . . . . . . . 289
8.3 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293
8.4 Implementing Integer Arithmetic . . . . . . . . . . . . . . . . . . 297
8.5 Rational Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . 299
8.6 Implementing Rational Arithmetic . . . . . . . . . . . . . . . . . 305
8.7 Irrational Numbers . . . . . . . . . . . . . . . . . . . . . . . . . 309
8.8 The Mechanic’s Rule . . . . . . . . . . . . . . . . . . . . . . . . 313
8.9 Reasoning about Reals . . . . . . . . . . . . . . . . . . . . . . . 315
8.10 Complex Numbers . . . . . . . . . . . . . . . . . . . . . . . . . 319
8.11 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 329
9 Polynomials 331
9.1 Difference Analysis of Polynomial Sequences . . . . . . . . . . . 332
9.2 Gaussian Elimination . . . . . . . . . . . . . . . . . . . . . . . . 337
9.3 Polynomials and the Binomial Theorem . . . . . . . . . . . . . . 344
9.4 Polynomials for Combinatorial Reasoning . . . . . . . . . . . . . 352
9.5 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 359
10 Corecursion 361
10.1 Corecursive Definitions . . . . . . . . . . . . . . . . . . . . . . . 362
10.2 Processes and Labeled Transition Systems . . . . . . . . . . . . . 365
10.3 Proof by Approximation . . . . . . . . . . . . . . . . . . . . . . 373
10.4 Proof by Coinduction . . . . . . . . . . . . . . . . . . . . . . . . 379
10.5 Power Series and Generating Functions . . . . . . . . . . . . . . 385
10.6 Exponential Generating Functions . . . . . . . . . . . . . . . . . 396
10.7 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . 398
11 Finite and Infinite Sets 399
11.1 More on Mathematical Induction . . . . . . . . . . . . . . . . . . 399
11.2 Equipollence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 406
11.3 Infinite Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410
11.4 Cantor’s World Implemented . . . . . . . . . . . . . . . . . . . . 418
11.5 Cardinal Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . 420
iv
CONTENTS
The Greek Alphabet 423
References 424
Index 428
剩余448页未读,继续阅读
drizzlynight
- 粉丝: 5
- 资源: 6
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- stc12c5a60s2 例程
- Android通过全局变量传递数据
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论0