Tag: Logic
Thoughts on Mathematical Induction: Part I
Induction, even setting aside its raison d'être as an inferential tool for mathematical proofs, is a remarkably elegant concept. Most people first encounter it indirectly through recursion in programming language lessons, and in my personal experience, rarely explore any further. Pinning down the scope for this series initially perplexed me. It's best we start in known territory and gently extend outward. To that end, I will only assume that the reader is capable of basic procedural and algorithmic reasoning and that they're either curious or motivated. We'll approach induction by first understanding recursion, since that's how many encounter it. Some confusion is normal (and inevitable); repeated encounters with these ideas will clear most of it in time.
The Tao of Types
Simple Types Before ░░░░ dependent types with ░░░░ ░░░░ ░░░░ ░░░░ we’ll take ░░░░ ░░░░ ░░░░ something ░░░░ ░░░░ ░░░░ simple types░░░░ starting ░░░░ ░░░░ ░░░░ ░░░░ type of all, the functon type $\_\to\_$. ░░░░ ░░░░ ░░░░ ░░░░ types is that ░░░░ ░░░░ not ░░░░ what to ░░░░ ░░░░ We’ll ░░░░ this with ░░░░ which work ░░░░ any ░░░░ called $\textsf{Set}$ in Agda. That is, ░░░░ will ░░░░ polymorphic ░░░░ without introducing a ░░░░ ░░░░ ░░░░ ░░░░ which ░░░░ ░░░░ do later once we have dependent ░░░░ in our arsenal. ░░░░ of polymorphic constructions ░░░░ ░░░░ $\textsf{id}$ and composition $\_ \circ \_$ ░░░░ ░░░░ ░░░░ a first ░░░░ of ░░░░ ░░░░