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
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
