Arithmetic Made Difficult

Under construction. I don’t know exactly what this is yet. Links that don’t exist are my to-do list.

0. Arithmetic Made Difficult
1. Functions
   • Flip
   • Clone
   • Composition
2. Booleans
   • Not
   • And
   • Or
   • Implies
   • Predicates
3. Set Combinators
   • Tuples
   • Disjoint Unions
4. \(\mathbb{N}\)
   • Type
     • Natural Numbers
     • From Arrows to Programs
     • The Uniqueness of the Natural Numbers
   • Recursion Operators
     • Simple Recursion
     • Bailout Recursion
     • Mutating Recursion
     • Double Natural Recursion
   • Arithmetic
     • Addition
     • Multiplication
     • Really Simple Equations
     • Subtraction
     • Less Than or Equal To
     • Strong Induction
     • Max and Min
     • The Division Algorithm
     • Divides
     • Norm Recursion
     • Greatest Common Divisor
     • Coprime To
     • Least Common Multiple
     • Find Smallest
     • Primes
     • Exponentiation
     • Choose
     • Mutating Norm Recursion
5. \(\mathsf{Lists}(A)\)
   • Type
     • Iterative Sets Redux
     • Lists
     • Head and Tail
   • Recursion Operators
     • Left Fold
     • Double Fold
     • Consuming Fold
     • Bailout Fold
     • Double Bailout Fold
   • Arithmetic
     • Snoc
     • Reverse
     • Cat
     • Length
     • At
     • Map
     • UnfoldN
     • Range
     • Zip
     • Lookback Fold
     • ZipPad
     • Unzip
     • Prefix and Suffix
     • Longest Common Prefix
     • All and Any
     • Tails and Inits
     • Filter
     • Elt
     • Count
     • Repeat
     • Sublist
     • Infix
     • Select
     • Unique
     • Delete
     • Dedupe
     • Common
     • Disjoint
     • Concat
     • Transpose
     • Cycle
     • Replace
     • Truncation
       • Take and Drop
       • TakeBut and DropBut
       • TakeWhile and DropWhile
     • Lists of sublists
       • Sublists
       • Infixes
     • Cat Factorization
       • ChunksOf
       • ChunksBy
       • ChainsBy
     • InsertAt
     • DeleteAt
     • SwapAt
   • Topics on Lists
     • Delimiter Separated Values
     • Run Length Encoding
     • Edit Distance
     • Sums and Products
     • Fundamental Theorem of Arithmetic
     • Number Partitions
6. Binary Trees
   • Type
     • Trees
     • Leaf and Fork
   • Recursion Operators
   • Arithmetic
7. Fixed Radix Numeral Systems
   • CarryBase
   • PlusBase
   • TimesBase
8. List of Arithmetics
   • On Boring and Repetitive Proofs
   • Partial and Total Orders
     • Sorted
     • Insertion Sort
     • Merge Sort
     • Lex and Friends
     • Chains
   • Semigroups and Monoids
     • Sproduct
     • Mproduct
   • Lattices
   • Semirings
9. Streams

The old idea that there was no reasoning in Arithmetic is dead; the idea that the general axioms have no place in Arithmetic is no longer held by a progressive teacher… J.B.F. Showalter in “Arithmetic Made Easy”, 1897

Beware of bugs in the above code; I have only proved it correct, not tried it. Donald Knuth in “Notes on the van Emde Boas construction of priority deques: An instructive use of recursion”, 1977

古人の跡を求めず、古人の求めたるの所を求めよ。

Do not seek the footsteps of the wise; seek what they sought.

Matsuo Bashō (松尾芭蕉), from 「柴門の辞」 “Words by a Brushwood Gate”