Fulls Seldom Differ
summary
Introduces a restricted language of natural number expressions that covers doubling, iterated doubling (exponentiation), and a full operator for 2^n−1 and gives a complete, terminating algorithm to solve length equations that occur in divide‑and‑conquer and vector patterns such as merge sort. Proofs use category‑theoretic pullbacks and are formalized in Agda formalization. A practical checker and unifier live in Rocq implementation and a toy Fulbourn interpreter appears in Haskell. Complexity results are not claimed.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:03Equation solver in Brat
- 2:07Fuborn language overview
- 4:14Vector patterns motivation
- 6:23Merge sort in Brat
- 8:54Vector patterns and equations
- 12:26Fool function observation
- 14:14Equation normalization
- 16:26Category theory approach
- 19:00Unification algorithm proof
- 20:05Comparison and future work
- 21:08Q&A
related talks
30mThe conatural numbers form an exponential commutative semiring
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
27mComputation expressions in context
28mHaskell Nuggets Power Series Brought to Life
42mPractical Lambda Calculus
23mDuality and How to Delete Half (minus ε) of Your Code
30mFP²: Fully in-Place Functional Programming
01h 08mType Arithmetic and the Yoneda Lemma