Mathematics in Programming

The book presents the mathematical view and tools of computer programming with broad and friendly context. It explains the basic concepts such as recursion, computation model, types, data, and etc. The book serves as an introductory and reference guide to the engineers, students, researchers, and professionals who are interested in functional programming, type system, and computer programming languages. The book covers seven topics. Firstly, it lays out the number system based on Peano Axioms and demonstrates the isomorphic computer data structures. Then, it introduces Lambda calculus as a computing model and recursion, an important programming structure, with the Y-combinator. It next presents the basic abstract algebra, including group and fields, and provides a friendly introduction to Galois theory. After that, it uses category theory as a tool to explain several concepts in computer programming, including the type system, polymorphism, null handler, and recursive data types, then followed by an application of program optimization. In the last two chapters, the author shows how to program with the concept of infinity through stream and lazy evaluation, and then explains the naïve set theory and transfinite numbers, from which the logic paradox arises. Finally, it introduces four historical views of mathematical foundation, as well as Gödel’s incompleteness theorems developed in 1930s, and how they define the boundaries of computer programming. Additionally, the book provides biographies, stories, and anecdotes of 25 mathematicians, along with over 130 exercises and their corresponding answers. Preface Exercise 1 Contents 1 Numbers 1.1 The History of Number 1.2 Peano Axioms 1.3 Natural Numbers and Programming Exercise 1.2 1.4 Structure of Natural Numbers Exercise 1.3 1.5 List Exercise 1.4 1.6 Form and Structure Exercise 1.5 2 Recursion 2.1 Everything Is Number 2.2 Euclidean Algorithm 2.2.1 Euclid's Elements 2.2.2 Euclidean Algorithm 2.2.3 Extended Euclidean Algorithm 2.2.4 Commensurable Exercise 2.1 2.3 The λ Calculus 2.3.1 Expression Reduction 2.3.2 λ Abstraction 2.3.3 λ Conversion Rules 2.4 Recursion 2.5 Compound Data Exercise 2.2 2.6 More Recursive Structures Exercise 2.3 2.7 The Recursive Pattern Exercise 2.4 Appendix: Example Program 3 Symmetry 3.1 What Is Symmetry? Exercise 3.1 3.2 Group 3.2.1 Group Exercise 3.2 3.2.2 Monoid and Semigroup Exercise 3.3 3.2.3 Properties of Group Exercise 3.4 3.2.4 Permutation Group Exercise 3.5 3.2.5 Group and Symmetry Exercise 3.6 3.2.6 Rotational Symmetry and Cyclic Group 3.2.6.1 Cyclotomic Equation Exercise 3.7 3.2.7 Subgroup Exercise 3.8 3.2.8 Lagrange's Theorem Exercise 3.9 3.3 Ring and Field 3.3.1 Ring Exercise 3.10 3.3.2 Division Ring and Field 3.4 Galois Theory 3.4.1 Field Extension Exercise 3.11 3.4.2 From Newton, Lagrange to Galois 3.4.2.1 Symmetric Polynomials and Newton's Theorem 3.4.2.2 Lagrange's Resolvent 3.4.2.3 Galois' Memoir Exercise 3.12 3.4.3 Automorphism and Galois Group Exercise 3.13 3.4.4 Fundamental Theorem of Galois Theory 3.4.5 Solvability Exercise 3.14 Appendix 4 Category 4.1 Category 4.1.1 Examples of Categories Exercise 4.1 4.1.2 Arrow ≠ Function 4.2 Functors Exercise 4.2 4.3 Products and Coproducts 4.3.1 Definition of Product and Coproduct 4.3.2 The Properties of Product and Coproduct 4.3.3 Functors from Products and Coproducts Exercise 4.3 4.4 Natural Transformation Exercise 4.4 4.5 Data Types 4.5.1 Initial and Terminal Object Exercise 4.5 4.5.2 Exponentials Exercise 4.6 4.5.3 Object Arithmetic 4.5.4 Polynomial Functors 4.5.5 F-Algebra Exercise 4.7 Exercise 4.8 Exercise 4.9 4.6 Fold Appendix: Example Programs 5 Fusion 5.1 Foldr/build Fusion 5.1.1 Foldr 5.1.2 Foldr/build Fusion Law 5.1.3 Build 5.1.4 Reduction with the Fusion Law 5.1.5 Type Constraint 5.1.6 Fusion Law in Category Theory Exercise 5.1 5.2 Make a Century 5.2.1 Exhaustive Search 5.2.2 Improvement Exercise 5.2 5.3 Further Reading Appendix: Example Source Code 6 Infinity 6.1 Zeno's Paradoxes 6.1.1 Potential Infinity and Actual Infinity 6.1.2 Method of Exhaustion 6.2 Programming with Infinity Exercise 6.1 6.2.1 Coalgebra and Infinite Stream Exercise 6.2 6.3 Infinity and Set Theory 6.3.1 Hilbert's Grand Hotel Exercise 6.3 6.3.2 One-to-one Correspondence and Infinite Set 6.3.3 Fibonacci Numbers and Hamming Numbers 6.3.4 Countable and Uncountable Infinity Exercise 6.4 6.3.5 Dedekind Cut 6.3.6 Transfinite Numbers and Continuum Hypothesis 6.4 Infinity in Art and Music Exercise 6.5 Appendix: Example Programs Appendix: Proof of Cantor's Theorem 7 Paradox 7.1 Boundary of Computation 7.2 Russell's Paradox Exercise 7.1 7.3 Philosophy of Mathematics 7.3.1 Logicism 7.3.2 Intuitionism 7.3.3 Formalism 7.3.4 Axiomatic Set Theory 7.4 Gödel's Incompleteness Theorems 7.5 Proof Sketch for the First Incompleteness Theorem 7.5.1 Formalize Arithmetic 7.5.1.1 Axioms and Reasoning Rules Exercise 7.2 7.5.2 ω Incomplete Exercise 7.3 7.5.3 Gödel Numbering 7.5.4 Construct the Self-reference 7.6 Universal Program and Diagonal Argument 7.7 Epilogue A Answers Answer of Exercise 1 Answer of Exercise 1.2 Answer of Exercise 1.3 Answer of Exercise 1.4 Answer of Exercise 1.5 Answer of Exercise 2.1 Answer of Exercise 2.2 Answer of Exercise 2.3 Answer of Exercise 2.4 Answer of Exercise 3.1 Answer of Exercise 3.2 Answer of Exercise 3.3 Answer of Exercise 3.4 Answer of Exercise 3.5 Answer of Exercise 3.6 Answer of Exercise 3.7 Answer of Exercise 3.8 Answer of Exercise 3.9 Answer of Exercise 3.10 Answer of Exercise 3.11 Answer of Exercise 3.12 Answer of Exercise 3.13 Answer of Exercise 3.14 Answer of Exercise 4.1 Answer of Exercise 4.2 Answer of Exercise 4.3 Answer of Exercise 4.4 Answer of Exercise 4.5 Answer of Exercise 4.6 Answer of Exercise 4.7 Answer of Exercise 4.8 Answer of Exercise 4.9 Answer of Exercise 5.1 Answer of Exercise 5.2 Answer of Exercise 6.1 Answer of Exercise 6.2 Answer of Exercise 6.3 Answer of Exercise 6.4 Answer of Exercise 6.5 Answer of Exercise 7.1 Answer of Exercise 7.2 Answer of Exercise 7.3 B Proof of Commutativity of Addition C Uniqueness of Product and Coproduct D Product and Coproduct of Set References Index