Certainty by Construction
Certainty by Construction
Software and Mathematics in Agda
About the Book
Agda is not just a programming language; it's a completely new way of thinking about software, and mathematical objects at large. This book is on successfully wielding Agda: teaching everything you need to know to get productive in modeling problems and in verifying your solutions.
Ready for a software revolution?
The software status quo is woefully inadequate when it comes to addressing critical issues. The endless stream of hasty solutions piled on top of earlier slapdash fixes has left us mired in inefficiency. Certainty by Construction boldly proclaims that the solution lies in embracing the elegance of abstract algebra as the cornerstone of software design. Learn to model problems in Agda, and get ready to explore the captivating world of proof assistance.
Discover abstract mathematics
Ever pondered what equality truly means? Intrigued by the prospect of
automatically discovering asymptotic optimizations? Curious about the enigmatic world of monoids and how they birth fascinating programs? Certainty by Construction will unravel these mysteries and guide you on a journey of intellectual discovery.
For veterans and newcomers both
Whether you're a seasoned programmer looking for a new and exhilarating
challenge, or a mathematical amateur eager to embark on an exciting journey, this book is for you. Maguire's engaging approach will empower you to learn Agda and mathematics on your own, and equip you with an arsenal of techniques to break down complex problems into straightforward solutions.
Learn to learn
Discover the invaluable skill of learning mathematics for yourself. Maguire
doesn't just provide answers; he equips you with the tools to become your own mathematician. Don't just read about mathematics—master it for yourself.
About the Author
Table of Contents
- Contents
- Preface
- The Co-blub Paradox
- A Gentle Introduction to Agda
- The Longevity of Knowledge
- Modules and Imports
- A Note on Interaction
- Importing Code
- Semantic Highlighting
- Types and Values
- Your First Function
- Normalization
- Unit Testing
- Dealing with Unicode
- Expressions and Functions
- Operators
- Agda’s Computational Model
- Stuckness
- Records and Tuples
- Copatterns and Constructors
- Fixities
- Coproduct Types
- Function Types
- The Curry/Uncurry Isomorphism
- Implicit Arguments
- Wrapping Up
- An Exploration of Numbers
- Natural Numbers
- Brief Notes on Data and Record Types
- Playing with Naturals
- Induction
- Two Notions of Evenness
- Constructing Evidence
- Addition
- Termination Checking
- Multiplication and Exponentiation
- Semi-subtraction
- Inconvenient Integers
- Difference Integers
- Unique Integer Representations
- Pattern Synonyms
- Integer Addition
- Wrapping Up
- Proof Objects
- Constructivism
- Statements are Types; Programs are Proofs
- Hard to Prove or Simply False?
- The Equality Type
- Congruence
- Identity and Zero Elements
- Symmetry and Involutivity
- Transitivity
- Mixfix Parsing
- Equational Reasoning
- Ergonomics, Associativity and Commutativity
- Exercises in Proof
- Wrapping Up
- Relations
- Universe Levels
- Dependent Pairs
- Heterogeneous Binary Relations
- The Relationship Between Functions and Relations
- Homogeneous Relations
- Standard Properties of Relations
- Attempting to Order the Naturals
- Substitution
- Unification
- Overconstrained by Dot Patterns
- Ordering the Natural Numbers
- Preorders
- Preorder Reasoning
- Reasoning over ≤
- Graph Reachability
- Free Preorders in the Wild
- Antisymmetry
- Equivalence Relations and Posets
- Strictly Less Than
- Wrapping Up
- Modular Arithmetic
- Instance Arguments
- The Ring of Natural Numbers Modulo N
- Deriving Transitivity
- Congruence of Addition
- Congruence of Multiplication
- Automating Proofs
- Wrapping Up
- Decidability
- Negation
- Bottom
- Inequality
- Negation Considered as a Callback
- Intransitivity of Inequality
- No Monus Left-Identity Exists
- Decidability
- Transforming Decisions
- Binary Trees
- Proving Things about Binary Trees
- Decidability of Tree Membership
- The All Predicate
- Binary Search Trees
- Trichotomy
- Insertion into BSTs
- Intrinsic vs Extrinsic Proofs
- An Intrinsic BST
- Wrapping Up
- Monoids and Setoids
- Structured Sets
- Monoids
- Examples of Monoids
- Monoids as Queries
- More Monoids
- Monoidal Origami
- Composition of Monoids
- Function Extensionality
- Setoid Hell
- Function Extensionality
- The Pointwise Monoid
- Monoid Homomorphisms
- Finding Equivalent Computations
- Wrapping Up
- Isomorphisms
- Finite Numbers
- Vectors and Finite Bounds
- Characteristic Functions
- Isomorphisms
- Equivalence on Isomorphisms
- Finite Types
- Algebraic Data Types
- The Algebra of Algebraic Data Types
- Monoids on Types
- Functions as Exponents
- Wrapping Up
- Program Optimization
- Why Can This Be Done?
- Shaping the Cache
- Building the Tries
- Memoizing Functions
- Inspecting Memoized Tries
- Updating the Trie
- Wrapping It All Up
- Appendix: Ring Solving
- Rings
- Agda’s Ring Solver
- Tactical Solving
- The Pen and Paper Algorithm
- Horner Normal Form
- Multivariate Polynomials
- Building a Semiring over HNF
- Semantics
- Syntax
- Solving the Ring
- Ergonomics
- Bibliography
- Acknowledgments
- About the Author
- Other Books by Sandy Maguire
Other books by this author
The Leanpub 60 Day 100% Happiness Guarantee
Within 60 days of purchase you can get a 100% refund on any Leanpub purchase, in two clicks.
Now, this is technically risky for us, since you'll have the book or course files either way. But we're so confident in our products and services, and in our authors and readers, that we're happy to offer a full money back guarantee for everything we sell.
You can only find out how good something is by trying it, and because of our 100% money back guarantee there's literally no risk to do so!
So, there's no reason not to click the Add to Cart button, is there?
See full terms...
Earn $8 on a $10 Purchase, and $16 on a $20 Purchase
We pay 80% royalties on purchases of $7.99 or more, and 80% royalties minus a 50 cent flat fee on purchases between $0.99 and $7.98. You earn $8 on a $10 sale, and $16 on a $20 sale. So, if we sell 5000 non-refunded copies of your book for $20, you'll earn $80,000.
(Yes, some authors have already earned much more than that on Leanpub.)
In fact, authors have earnedover $14 millionwriting, publishing and selling on Leanpub.
Learn more about writing on Leanpub
Free Updates. DRM Free.
If you buy a Leanpub book, you get free updates for as long as the author updates the book! Many authors use Leanpub to publish their books in-progress, while they are writing them. All readers get free updates, regardless of when they bought the book or how much they paid (including free).
Most Leanpub books are available in PDF (for computers) and EPUB (for phones, tablets and Kindle). The formats that a book includes are shown at the top right corner of this page.
Finally, Leanpub books don't have any DRM copy-protection nonsense, so you can easily read them on any supported device.
Learn more about Leanpub's ebook formats and where to read them
