The Haskell Road to Logic, Maths and Programming.pdf

(1438 KB) Pobierz
68263959 UNPDF
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

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin